mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.ToInt
/-- The lower bound of the interval, if finite.  -/
Lean.Grind.IntInterval.lo? : Lean.Grind.IntInterval → Option ℤ
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.pullback.cone_pt : ∀ {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [inst : CompHausLike.HasExplicitPullback f g],
  (CompHausLike.pullback.cone f g).pt = CompHausLike.pullback f g
-- Lean.Data.Lsp.Workspace
Lean.Lsp.WorkspaceFolder.mk.inj : ∀ {uri : Lean.Lsp.DocumentUri} {name : String} {uri_1 : Lean.Lsp.DocumentUri} {name_1 : String},
  { uri := uri, name := name } = { uri := uri_1, name := name_1 } → uri = uri_1 ∧ name = name_1
-- Mathlib.RingTheory.KrullDimension.Module
Module.supportDim_ne_bot_iff_nontrivial : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.supportDim R M ≠ ⊥ ↔ Nontrivial M
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.map₀.eq_1 : ∀ {ι : Type u_1} [inst : Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8}
  (f : (i j : ι) → (h : i ≤ j) → T h) [inst_1 : ⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)]
  [inst_2 : DirectedSystem F fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  (ih : (i : ι) → F i), DirectLimit.map₀ f ih = ⟦⟨Classical.arbitrary ι, ih (Classical.arbitrary ι)⟩⟧
-- Mathlib.Analysis.Complex.Trigonometric
Complex.tan_sq_div_one_add_tan_sq : ∀ {x : ℂ}, Complex.cos x ≠ 0 → Complex.tan x ^ 2 / (1 + Complex.tan x ^ 2) = Complex.sin x ^ 2
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- If `M` is a quasi-coherent `𝒪_{Spec R}` module, it is isomorphic to `Γ(M)^~`.  -/
AlgebraicGeometry.Scheme.Modules.isIso_fromTildeΓ_of_isQuasicoherent : ∀ {R : CommRingCat} (M : (AlgebraicGeometry.Spec R).Modules) [SheafOfModules.IsQuasicoherent M],
  CategoryTheory.IsIso M.fromTildeΓ
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Pos.skip?_eq_skip?_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String} {pos : s.Pos},
  pos.skip? pat = Option.map String.Pos.ofToSlice (pos.toSlice.skip? pat)
-- Mathlib.LinearAlgebra.Matrix.WithConv
convOne_def : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : One α], 1 = WithConv.toConv (Matrix.of 1)
-- Mathlib.Topology.Algebra.Group.Basic
instContinuousInvMultiplicativeOfContinuousNeg : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : Neg H] [ContinuousNeg H], ContinuousInv (Multiplicative H)
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.Hom.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {A B : T.Algebra}
  [inst_1 : SizeOf C] (f : A.A ⟶ B.A)
  (h :
    autoParam (CategoryTheory.CategoryStruct.comp (T.map f) B.a = CategoryTheory.CategoryStruct.comp A.a f)
      CategoryTheory.Monad.Algebra.Hom.h._autoParam),
  sizeOf { f := f, h := h } = 1 + sizeOf f + sizeOf h
-- Mathlib.Data.Multiset.FinsetOps
Multiset.Subset.ndunion_eq_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s ⊆ t → s.ndunion t = t
-- Lean.Meta.InferType
/-- Return `LBool.true` if given level is always equivalent to universe level zero.

This is used to implement `isProp`.
 -/
_private.Lean.Meta.InferType.0.Lean.Meta.isAlwaysZero : Lean.Level → Bool
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.equivOfTensorIsoUnit_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (m n : M)
  (h₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj m n ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit M)
  (h₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj n m ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit M)
  (H :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight h₁.hom m)
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor m).hom =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator m n m).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft m h₂.hom)
          (CategoryTheory.MonoidalCategoryStruct.rightUnitor m).hom))
  [inst_3 : F.Monoidal], (CategoryTheory.equivOfTensorIsoUnit F m n h₁ h₂ H).functor = F.obj m
-- Mathlib.AlgebraicGeometry.Restrict
/-- The open cover of `⋃ Vᵢ` by `Vᵢ`.  -/
AlgebraicGeometry.Scheme.Opens.iSupOpenCover : {J : Type u_1} → {X : AlgebraicGeometry.Scheme} → (U : J → X.Opens) → (↑(⨆ i, U i)).OpenCover
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.maxKey_modify_eq_maxKey : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β} {he : (Std.DTreeMap.Const.modify t k f).isEmpty = false},
  (Std.DTreeMap.Const.modify t k f).maxKey he = t.maxKey ⋯
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instCoeAddSubgroup : {G : Type u} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → Coe (OpenNormalAddSubgroup G) (AddSubgroup G)
-- Mathlib.Topology.Algebra.Algebra
/-- Any two continuous `R`-algebra morphisms from `R` are equal  -/
ContinuousAlgHom.ext_ring : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A] [inst_4 : TopologicalSpace R] {f g : R →A[R] A}, f = g
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
/-- If `φ : a ⟶ b` lifts `f : R ⟶ S` and both are isomorphisms, then `φ⁻¹` lifts `f⁻¹`.  -/
CategoryTheory.IsHomLift.inv : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : CategoryTheory.IsIso f]
  [inst_3 : CategoryTheory.IsIso φ] [p.IsHomLift f φ], p.IsHomLift (CategoryTheory.inv f) (CategoryTheory.inv φ)
-- Init.Data.SInt.Lemmas
Int64.ofBitVec_neg : ∀ (a : BitVec 64), Int64.ofBitVec (-a) = -Int64.ofBitVec a
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndepOn_range_iff : ∀ {ι' : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {ι : Type u_6} {f : ι → ι'},
  Function.Injective f → ∀ (g : ι' → M), LinearIndepOn R g (Set.range f) ↔ LinearIndependent R (g ∘ f)
-- Mathlib.Topology.Algebra.Valued.ValuedField
/-- A `Valued` version of `Valuation.integer`, enabling the notation `𝒪[K]` for the
valuation integers of a valued field `K`.  -/
Valued.«term𝒪[_]» : Lean.ParserDescr
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
/-- Auxiliary definition for `AlgebraicGeometry.PresheafedSpace.colimitCoconeIsColimit`.
 -/
AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc : {J : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J TopCat] →
          [inst_3 : ∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)] →
            [CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C] →
              (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) →
                (s : CategoryTheory.Limits.Cocone F) → AlgebraicGeometry.PresheafedSpace.colimit F ⟶ s.pt
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.inverseImage_inf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D) (P P' : CategoryTheory.MorphismProperty D),
  (P ⊓ P').inverseImage F = P.inverseImage F ⊓ P'.inverseImage F
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k a : α} {fallback : β a},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.getD a fallback =
    if compare k a = Ordering.eq then fallback else t.getD a fallback
-- Mathlib.Algebra.Order.SuccPred.WithBot
WithBot.succ_natCast : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] [inst_2 : AddMonoidWithOne α] [inst_3 : SuccAddOrder α]
  (n : ℕ), (↑n).succ = ↑n + 1
-- Init.System.IO
/-- Returns `true` if a handle refers to a Windows console or a Unix terminal.
 -/
IO.FS.Handle.isTty : IO.FS.Handle → BaseIO Bool
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_ofList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List ((a : α) × β a)},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l → (Std.ExtDTreeMap.ofList l cmp).size = l.length
-- Mathlib.GroupTheory.Perm.Option
Equiv.optionCongr_swap : ∀ {α : Type u_1} [inst : DecidableEq α] (x y : α), Equiv.optionCongr (Equiv.swap x y) = Equiv.swap (some x) (some y)
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.instInhabitedTerminationHints.default : Lean.Elab.TerminationHints
-- Mathlib.CategoryTheory.Limits.Sifted
/-- A category `C` `IsSifted` if
1. the diagonal functor `C ⥤ C × C` is final.
2. there exists some object.  -/
CategoryTheory.IsSifted : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.leibniz : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  (X : LeftInvariantDerivation I G) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤)
  {f' : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤}, X (f * f') = f • X f' + f' • X f
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.of_le_one : ∀ {b o : Ordinal.{u_1}}, b ≤ 1 → o ≠ 0 → Ordinal.CNF b o = [(0, o)]
-- Mathlib.Dynamics.TopologicalEntropy.Semiconj
Dynamics.le_coverEntropyEntourage_image : ∀ {X : Type u_1} {Y : Type u_2} {V : SetRel Y Y} {S : X → X} {T : Y → Y} {φ : X → Y},
  Function.Semiconj φ S T →
    ∀ (F : Set X) [V.IsSymm],
      Dynamics.coverEntropyEntourage S F (Prod.map φ φ ⁻¹' V.comp V) ≤ Dynamics.coverEntropyEntourage T (φ '' F) V
-- Mathlib.Geometry.Convex.Set
Convexity.IsConvexSet.iInter : ∀ {R : Type u_3} {X : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {ι : Sort u_7} {s : ι → Set X},
  (∀ (i : ι), Convexity.IsConvexSet R (s i)) → Convexity.IsConvexSet R (⋂ i, s i)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelIsoOfEq_inv_comp_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f g : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] [inst_3 : CategoryTheory.Limits.HasKernel g] (h : f = g)
  {Z : C} (h_1 : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelIsoOfEq h).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι f) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) h_1
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.isoZero'.eq_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) (A : Type u_4) [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] (a : A) (ha : a = 0),
  CategoryTheory.Functor.CommShift.isoZero' F A a ha =
    CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.shiftFunctorZero' C a ha) F ≪≫
      F.leftUnitor ≪≫ F.rightUnitor.symm ≪≫ F.isoWhiskerLeft (CategoryTheory.shiftFunctorZero' D a ha).symm
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Algebra.IsIntegral.quotient : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {I : Ideal A}
  [Algebra.IsIntegral R A], Algebra.IsIntegral (R ⧸ Ideal.comap (algebraMap R A) I) (A ⧸ I)
-- Mathlib.CategoryTheory.WithTerminal.FinCategory
CategoryTheory.WithInitial.instFintype : (C : Type u) → [Fintype C] → Fintype (CategoryTheory.WithInitial C)
-- Mathlib.CategoryTheory.Localization.LocallySmall
CategoryTheory.MorphismProperty.hasLocalizationOfLocallySmall'_def : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] (W : CategoryTheory.MorphismProperty C) {D : Type u_3}
  [inst_1 : CategoryTheory.Category.{u_4, u_3} D] [inst_2 : CategoryTheory.LocallySmall.{u_5, u_4, u_3} D]
  (L : CategoryTheory.Functor C D) [inst_3 : L.IsLocalization W],
  W.hasLocalizationOfLocallySmall' L =
    have this := ⋯;
    let L' :=
      { obj := fun X => X, map := fun {X Y} f => CategoryTheory.InducedCategory.homMk (L.map f), map_id := ⋯,
        map_comp := ⋯ };
    have this_1 := ⋯;
    have this_2 := ⋯;
    have this_3 := ⋯;
    have e := (CategoryTheory.inducedFunctor L.obj).asEquivalence;
    have e' := L'.associator e.functor e.inverse ≪≫ L'.isoWhiskerLeft e.unitIso.symm ≪≫ L'.rightUnitor;
    have this_4 := ⋯;
    W.hasLocalizationOfLocallySmall L'
-- Init.Data.String.Lemmas.FindPos
String.Slice.posLE_eq_iff : ∀ {s : String.Slice} {p : String.Pos.Raw} {q : s.Pos},
  s.posLE p = q ↔ q.offset ≤ p ∧ ∀ (q' : s.Pos), q'.offset ≤ p → q' ≤ q
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
_private.Mathlib.CategoryTheory.Limits.Types.Coproducts.0.CategoryTheory.Limits.WalkingPair.swap.match_1.eq_2 : ∀ (motive : CategoryTheory.Limits.WalkingPair → Sort u_1) (h_1 : Unit → motive CategoryTheory.Limits.WalkingPair.left)
  (h_2 : Unit → motive CategoryTheory.Limits.WalkingPair.right),
  (match CategoryTheory.Limits.WalkingPair.right with
    | CategoryTheory.Limits.WalkingPair.left => h_1 ()
    | CategoryTheory.Limits.WalkingPair.right => h_2 ()) =
    h_2 ()
-- Mathlib.RingTheory.TensorProduct.Maps
/-- Heterobasic version of `Algebra.TensorProduct.map` as a ring homomorphism.

Note that this would generalise `map` if we were to have `SemiAlgHom`.  -/
Algebra.TensorProduct.mapRingHom : {R : Type u_3} →
  {S : Type u_4} →
    {T : Type u_5} →
      {R' : Type u_6} →
        {S' : Type u_7} →
          {T' : Type u_8} →
            [inst : CommSemiring R] →
              [inst_1 : CommSemiring S] →
                [inst_2 : CommSemiring T] →
                  [inst_3 : Algebra R S] →
                    [inst_4 : Algebra R T] →
                      [inst_5 : CommSemiring R'] →
                        [inst_6 : CommSemiring S'] →
                          [inst_7 : CommSemiring T'] →
                            [inst_8 : Algebra R' S'] →
                              [inst_9 : Algebra R' T'] →
                                (fR : R →+* R') →
                                  (fS : S →+* S') →
                                    (fT : T →+* T') →
                                      fS.comp (algebraMap R S) = (algebraMap R' S').comp fR →
                                        fT.comp (algebraMap R T) = (algebraMap R' T').comp fR →
                                          TensorProduct R S T →+* TensorProduct R' S' T'
-- ProofWidgets.Component.RefreshComponent
_private.ProofWidgets.Component.RefreshComponent.0.ProofWidgets.RefreshToken.mk.sizeOf_spec : ∀ (state : IO.Ref ProofWidgets.RefreshComponent.RefreshState) (cancelTk : IO.CancelToken)
  (promise : IO.Ref (IO.Promise Unit)),
  sizeOf { state := state, cancelTk := cancelTk, promise := promise } =
    1 + sizeOf state + sizeOf cancelTk + sizeOf promise
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
/-- Elements of the character space are non-unital algebra homomorphisms.  -/
WeakDual.CharacterSpace.instNonUnitalAlgHomClass : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : NonUnitalNonAssocSemiring A] [inst_5 : TopologicalSpace A]
  [inst_6 : Module 𝕜 A], NonUnitalAlgHomClass (↑(WeakDual.characterSpace 𝕜 A)) 𝕜 A 𝕜
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.toEquiv : {α : Type u_4} → {β : Type u_5} → [inst : UniformSpace α] → [inst_1 : UniformSpace β] → α ≃ᵤ β → α ≃ β
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.sigmaIsoSigma_hom_ι_apply : ∀ {ι : Type v} (α : ι → TopCat) (i : ι) (x : ↑(α i)),
  (CategoryTheory.ConcreteCategory.hom (TopCat.sigmaIsoSigma α).hom)
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Sigma.ι α i)) x) =
    ⟨i, x⟩
-- Mathlib.Probability.UniformOn
ProbabilityTheory.instIsProbabilityMeasure_uniformOn_univ : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [Finite Ω] [Nonempty Ω],
  MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.uniformOn Set.univ)
-- Mathlib.Algebra.Group.Ext
AddRightCancelMonoid.ext : ∀ {M : Type u} ⦃m₁ m₂ : AddRightCancelMonoid M⦄, HAdd.hAdd = HAdd.hAdd → m₁ = m₂
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsTrivialOn.mk : ∀ {Γ₀ : Type u_4} [inst : LinearOrderedCommMonoidWithZero Γ₀] {B : Type u_7} {A : Type u_8} [inst_1 : CommSemiring A]
  [inst_2 : Ring B] [inst_3 : Algebra A B] {v : Valuation B Γ₀},
  (∀ (a : A), a ≠ 0 → v ((algebraMap A B) a) = 1) → Valuation.IsTrivialOn A v
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} [inst_2 : SizeOf C] (h₀ : S₁.X₁ ⟶ S₂.X₁)
  (h₀_f :
    autoParam (CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) CategoryTheory.ShortComplex.Homotopy.h₀_f._autoParam)
  (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃)
  (g_h₃ :
    autoParam (CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0) CategoryTheory.ShortComplex.Homotopy.g_h₃._autoParam)
  (comm₁ :
    autoParam (φ₁.τ₁ = CategoryTheory.CategoryStruct.comp S₁.f h₁ + h₀ + φ₂.τ₁)
      CategoryTheory.ShortComplex.Homotopy.comm₁._autoParam)
  (comm₂ :
    autoParam (φ₁.τ₂ = CategoryTheory.CategoryStruct.comp S₁.g h₂ + CategoryTheory.CategoryStruct.comp h₁ S₂.f + φ₂.τ₂)
      CategoryTheory.ShortComplex.Homotopy.comm₂._autoParam)
  (comm₃ :
    autoParam (φ₁.τ₃ = h₃ + CategoryTheory.CategoryStruct.comp h₂ S₂.g + φ₂.τ₃)
      CategoryTheory.ShortComplex.Homotopy.comm₃._autoParam),
  sizeOf
      { h₀ := h₀, h₀_f := h₀_f, h₁ := h₁, h₂ := h₂, h₃ := h₃, g_h₃ := g_h₃, comm₁ := comm₁, comm₂ := comm₂,
        comm₃ := comm₃ } =
    1 + sizeOf h₀ + sizeOf h₀_f + sizeOf h₁ + sizeOf h₂ + sizeOf h₃ + sizeOf g_h₃ + sizeOf comm₁ + sizeOf comm₂ +
      sizeOf comm₃
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.tensoringRight_additive : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] (X : C),
  ((CategoryTheory.MonoidalCategory.tensoringRight C).obj X).Additive
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.radius_le_radius_continuousLinearMap_comp : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (p : FormalMultilinearSeries 𝕜 E F) (f : F →L[𝕜] G),
  p.radius ≤ (f.compFormalMultilinearSeries p).radius
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.setBlack_toList : ∀ {α : Type u_1} {t : RBTree.RBNode α}, t.setBlack.toList = t.toList
-- Mathlib.RingTheory.QuasiFinite.Basic
PrimeSpectrum.preimageOrderIsoFiber.eq_1 : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : PrimeSpectrum R),
  PrimeSpectrum.preimageOrderIsoFiber R S p = { toEquiv := PrimeSpectrum.preimageEquivFiber R S p, map_rel_iff' := ⋯ }
-- Lean.Parser.Extension
Lean.Parser.AliasValue.binary : {α : Type} → (α → α → α) → Lean.Parser.AliasValue α
-- Mathlib.Algebra.Notation.Prod
Prod.pow_fst : ∀ {E : Type u_8} {α : Type u_9} {β : Type u_10} [inst : Pow α E] [inst_1 : Pow β E] (p : α × β) (c : E),
  (p ^ c).1 = p.1 ^ c
-- Mathlib.Topology.Constructions.SumProd
isOpenMap_inl : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], IsOpenMap Sum.inl
-- Mathlib.Combinatorics.SimpleGraph.Prod
/-- The box product distributes over the disjoint sum of graphs.  -/
SimpleGraph.Iso.sumBoxProdDistrib : {V₁ : Type u_5} →
  {V₂ : Type u_6} →
    {W : Type u_7} →
      (G₁ : SimpleGraph V₁) → (G₂ : SimpleGraph V₂) → (H : SimpleGraph W) → (G₁ ⊕g G₂) □ H ≃g G₁ □ H ⊕g G₂ □ H
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.instSMul : {G : Type u_3} → [DivInvMonoid G] → SMul (ConjAct G) G
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.Initial.strInv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {A : CategoryTheory.Endofunctor.Algebra F} (h : CategoryTheory.Limits.IsInitial A),
  CategoryTheory.Endofunctor.Algebra.Initial.strInv h = (h.to { a := F.obj A.a, str := F.map A.str }).f
-- Mathlib.Data.List.Sigma
_private.Mathlib.Data.List.Sigma.0.List.kextract.match_3.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : List (Sigma β) → Sort u_3) (s : Sigma β) (l : List (Sigma β))
  (h_1 : Unit → motive []) (h_2 : (s : Sigma β) → (l : List (Sigma β)) → motive (s :: l)),
  (match s :: l with
    | [] => h_1 ()
    | s :: l => h_2 s l) =
    h_2 s l
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.var : {L : FirstOrder.Language} → {α : Type u'} → α → L.Term α
-- Mathlib.Tactic.Algebra.Lemmas
Mathlib.Tactic.Algebra.rat_ofNat_smul_2 : ∀ {n d : ℕ} {R : Type u_3} {A : Type u_4} [inst : Field R] [inst_1 : Field A] [inst_2 : Algebra R A] {a : A}
  [inst_3 : n.AtLeastTwo] [inst_4 : d.AtLeastTwo],
  (-OfNat.ofNat n / OfNat.ofNat d) • a = -OfNat.ofNat n / OfNat.ofNat d * a
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- An expression for the inverse of a lower block-triangular matrix, when either both elements of
diagonal are invertible, or both are not.  -/
Matrix.inv_fromBlocks_zero₁₂_of_isUnit_iff : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] (A : Matrix m m α) (C : Matrix n m α) (D : Matrix n n α),
  (IsUnit A ↔ IsUnit D) → (Matrix.fromBlocks A 0 C D)⁻¹ = Matrix.fromBlocks A⁻¹ 0 (-(D⁻¹ * C * A⁻¹)) D⁻¹
-- Mathlib.Analysis.Convex.Segment
openSegment_eq_Ioo' : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y : 𝕜},
  x ≠ y → openSegment 𝕜 x y = Set.Ioo (min x y) (max x y)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ ∩ t₂).getKey! k = t₁.getKey! k
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.length_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w),
  (p.append q).length = p.length + q.length
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_rco_eq_add : ∀ {m n i : ℕ}, i < n - m → (m...n).toArray[i]! = m + i
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indepSet_congr : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ η : ProbabilityTheory.Kernel α Ω}
  {μ : MeasureTheory.Measure α} {s t : Set Ω},
  ⇑κ =ᵐ[μ] ⇑η → (ProbabilityTheory.Kernel.IndepSet s t κ μ ↔ ProbabilityTheory.Kernel.IndepSet s t η μ)
-- Std.Do.SPred.SVal
_private.Std.Do.SPred.SVal.0.Std.Do.SVal.uncurry.match_1.eq_1 : ∀ (head : Type u_1) (tail : List (Type u_1)) (motive : Std.Do.SVal.StateTuple (head :: tail) → Sort u_2) (s : head)
  (t : Std.Do.SVal.StateTuple tail) (h_1 : (s : head) → (t : Std.Do.SVal.StateTuple tail) → motive (s, t)),
  (match (s, t) with
    | (s, t) => h_1 s t) =
    h_1 s t