mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.IterStep.successor.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Std.IterStep α β → Sort u_3) →
      (x : Std.IterStep α β) →
        ((it : α) → (out : β) → motive (Std.IterStep.yield it out)) →
          ((it : α) → motive (Std.IterStep.skip it)) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.FieldTheory.Minpoly.Field
/-- The constant coefficient of the minimal polynomial of `x` is `0` if and only if `x = 0`.  -/
minpoly.coeff_zero_eq_zero : ∀ {A : Type u_1} {B : Type u_2} [inst : Field A] [inst_1 : Ring B] [IsDomain B] [inst_3 : Algebra A B] {x : B},
  IsIntegral A x → ((minpoly A x).coeff 0 = 0 ↔ x = 0)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.zero_def : ∀ {R : Type u_1} [inst : Semiring R], 0 = 0
-- Mathlib.Data.Complex.Basic
/-- The product of a set on the real axis and a set on the imaginary axis of the complex plane,
denoted by `s ×ℂ t`.  -/
Complex.reProdIm : Set ℝ → Set ℝ → Set ℂ
-- Init.Data.List.Lemmas
List.all_map : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {p : β → Bool}, (List.map f l).all p = l.all (p ∘ f)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
_private.Mathlib.Analysis.SpecialFunctions.Gamma.Basic.0.Complex.Gamma.eq_1 : ∀ (s : ℂ), Complex.Gamma s = Complex.GammaAux✝ ⌊1 - s.re⌋₊ s
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.comap_obj_X : ∀ {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.MonoidalLeftAction C D]
  {A B : C} [inst_4 : CategoryTheory.MonObj A] [inst_5 : CategoryTheory.MonObj B] (f : A ⟶ B)
  [inst_6 : CategoryTheory.IsMonHom f] (M : CategoryTheory.Mod D B), ((CategoryTheory.Mod.comap f).obj M).X = M.X
-- Mathlib.RingTheory.Nilpotent.Defs
nilpotencyClass_zero : ∀ {R : Type u_1} [inst : MonoidWithZero R] [Nontrivial R], nilpotencyClass 0 = 1
-- Mathlib.Data.Multiset.UnionInter
Multiset.count_union : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (s t : Multiset α),
  Multiset.count a (s ∪ t) = max (Multiset.count a s) (Multiset.count a t)
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.divRight.eq_1 : ∀ {G : Type u_5} [inst : Group G] (a : G),
  Equiv.divRight a = { toFun := fun b => b / a, invFun := fun b => b * a, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
/-- For `z : ℂ` the function `c : ℤ ↦ ((c z + d) ^ k)⁻¹` is Summable for `2 ≤ k`.  -/
EisensteinSeries.linear_left_summable : ∀ {z : ℂ}, z ≠ 0 → ∀ (d : ℤ) {k : ℤ}, 2 ≤ k → Summable fun c => ((↑c * z + ↑d) ^ k)⁻¹
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.mk.injEq : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (A : Matrix ι ι ℤ) (h e f : ι → L)
  (cartan_eq_lieSpan : H = LieSubalgebra.lieSpan R L (Set.range h))
  (span_ef : LieSubalgebra.lieSpan R L (Set.range e ∪ Set.range f) = ⊤) (linInd : LinearIndependent R h)
  (nondegen : A.Nondegenerate) (sl2 : ∀ (i : ι), IsSl2Triple (h i) (e i) (f i)) (lie_h_h : ∀ (i j : ι), ⁅h i, h j⁆ = 0)
  (lie_h_e : ∀ (i j : ι), ⁅h j, e i⁆ = A i j • e i) (lie_h_f : ∀ (i j : ι), ⁅h j, f i⁆ = -A i j • f i)
  (lie_e_f_ne : ∀ (i j : ι), i ≠ j → ⁅e i, f j⁆ = 0) (A_1 : Matrix ι ι ℤ) (h_1 e_1 f_1 : ι → L)
  (cartan_eq_lieSpan_1 : H = LieSubalgebra.lieSpan R L (Set.range h_1))
  (span_ef_1 : LieSubalgebra.lieSpan R L (Set.range e_1 ∪ Set.range f_1) = ⊤) (linInd_1 : LinearIndependent R h_1)
  (nondegen_1 : A_1.Nondegenerate) (sl2_1 : ∀ (i : ι), IsSl2Triple (h_1 i) (e_1 i) (f_1 i))
  (lie_h_h_1 : ∀ (i j : ι), ⁅h_1 i, h_1 j⁆ = 0) (lie_h_e_1 : ∀ (i j : ι), ⁅h_1 j, e_1 i⁆ = A_1 i j • e_1 i)
  (lie_h_f_1 : ∀ (i j : ι), ⁅h_1 j, f_1 i⁆ = -A_1 i j • f_1 i) (lie_e_f_ne_1 : ∀ (i j : ι), i ≠ j → ⁅e_1 i, f_1 j⁆ = 0),
  ({ A := A, h := h, e := e, f := f, cartan_eq_lieSpan := cartan_eq_lieSpan, span_ef := span_ef, linInd := linInd,
        nondegen := nondegen, sl2 := sl2, lie_h_h := lie_h_h, lie_h_e := lie_h_e, lie_h_f := lie_h_f,
        lie_e_f_ne := lie_e_f_ne } =
      { A := A_1, h := h_1, e := e_1, f := f_1, cartan_eq_lieSpan := cartan_eq_lieSpan_1, span_ef := span_ef_1,
        linInd := linInd_1, nondegen := nondegen_1, sl2 := sl2_1, lie_h_h := lie_h_h_1, lie_h_e := lie_h_e_1,
        lie_h_f := lie_h_f_1, lie_e_f_ne := lie_e_f_ne_1 }) =
    (A = A_1 ∧ h = h_1 ∧ e = e_1 ∧ f = f_1)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_updateRow_add_smul_self : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : Matrix n n R)
  {i j : n}, i ≠ j → ∀ (c : R), (A.updateRow i (A i + c • A j)).det = A.det
-- Mathlib.Algebra.ContinuedFractions.TerminatedStable
GenContFract.contsAux_stable_step_of_terminated : ∀ {K : Type u_1} {g : GenContFract K} {n : ℕ} [inst : DivisionRing K],
  g.TerminatedAt n → g.contsAux (n + 2) = g.contsAux (n + 1)
-- Mathlib.Data.List.Sublists
List.Pairwise.sublists' : ∀ {α : Type u} {R : α → α → Prop} {l : List α},
  List.Pairwise R l → List.Pairwise (List.Lex (Function.swap R)) l.sublists'
-- Mathlib.RingTheory.ClassGroup.Basic
FractionalIdeal.coe_mk0 : ∀ {R : Type u_1} (K : Type u_2) [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDomain R] [inst_5 : IsDedekindDomain R] (I : ↥(nonZeroDivisors (Ideal R))),
  ↑((FractionalIdeal.mk0 K) I) = ↑↑I
-- Mathlib.Logic.Encodable.Basic
Encodable.decode_sum_val : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst_1 : Encodable β] (n : ℕ),
  Encodable.decode n = Encodable.decodeSum n
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_assoc_left_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom
      (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).hom (F.map h)) =
    CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h).hom)
      (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h).hom)
          (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).inv))
-- Mathlib.SetTheory.ZFC.Basic
/-- The Cartesian product, `{(a, b) | a ∈ x, b ∈ y}`  -/
ZFSet.prod : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}
-- Init.Control.Lawful.MonadAttach.Instances
_private.Init.Control.Lawful.MonadAttach.Instances.0.ExceptT.bindCont.match_1.splitter : {ε α : Type u_1} →
  (motive : Except ε α → Sort u_2) →
    (x : Except ε α) → ((a : α) → motive (Except.ok a)) → ((e : ε) → motive (Except.error e)) → motive x
-- Mathlib.Data.Sum.Lattice
Sum.Lex.inr_inf : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] (b₁ b₂ : β),
  Sum.inrₗ (b₁ ⊓ b₂) = Sum.inrₗ b₁ ⊓ Sum.inrₗ b₂
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.Hom.ext_iff : ∀ {A B : ProfiniteAddGrp.{u}} {x y : A.Hom B}, x = y ↔ x.hom' = y.hom'
-- Mathlib.AlgebraicTopology.SimplexCategory.Rev
SimplexCategory.rev_map_δ : ∀ {n : ℕ} (i : Fin (n + 2)), SimplexCategory.rev.map (SimplexCategory.δ i) = SimplexCategory.δ i.rev
-- Lean.ParserCompiler.Attribute
Lean.ParserCompiler.CombinatorAttribute.setDeclFor : Lean.ParserCompiler.CombinatorAttribute → Lean.Environment → Lean.Name → Lean.Name → Lean.Environment
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the forward direction of `Units.one_le_inv_mul`. -/
Units.le_of_one_le_inv_mul : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ) {a : M}, 1 ≤ ↑u⁻¹ * a → ↑u ≤ a
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Supermartingale.stronglyMeasurable : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [inst_3 : LE E],
  MeasureTheory.Supermartingale f ℱ μ → ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.setLIntegral_lt_top : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} {s : Set α},
  MeasureTheory.IntegrableOn f s μ → ∫⁻ (x : α) in s, ENNReal.ofReal (f x) ∂μ < ⊤
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.PreservesColimitOfIsSplitPair.mk : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C},
  (∀ {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g],
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G) →
    CategoryTheory.Monad.PreservesColimitOfIsSplitPair G
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPLetVarTypes : Lean.Options → Bool
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.δToCycles_πE : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.δToCycles_πE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.δToCycles_πE._auto_3),
  CategoryTheory.CategoryStruct.comp (X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁) (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₈_of_isCharThreeJNeZeroNF_of_char_three : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] [CharP R 3], W.b₈ = W.a₂ * W.a₆
-- Std.Data.HashSet.Basic
Std.HashSet.instRepr : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → [Repr α] → Repr (Std.HashSet α)
-- Lean.Declaration
Lean.ConstantVal.mk.inj : ∀ {name : Lean.Name} {levelParams : List Lean.Name} {type : Lean.Expr} {name_1 : Lean.Name}
  {levelParams_1 : List Lean.Name} {type_1 : Lean.Expr},
  { name := name, levelParams := levelParams, type := type } =
      { name := name_1, levelParams := levelParams_1, type := type_1 } →
    name = name_1 ∧ levelParams = levelParams_1 ∧ type = type_1
-- Mathlib.Order.Filter.Pointwise
Filter.map₂_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f : Filter α} {g : Filter β},
  Filter.map₂ (fun x1 x2 => x1 • x2) f g = f • g
-- Mathlib.Data.List.SplitBy
List.splitBy.loop.eq_2 : ∀ {α : Type u} (R : α → α → Bool) (a : α) (a_1 : List α) (a_2 : List (List α)),
  List.splitBy.loop R [] a a_1 a_2 = ((a :: a_1).reverse :: a_2).reverse
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.stmts₁.eq_4 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (a : Γ → σ → Bool) (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1.stmts₁ (Turing.TM1.Stmt.branch a q₁ q₂) =
    insert (Turing.TM1.Stmt.branch a q₁ q₂) (Turing.TM1.stmts₁ q₁ ∪ Turing.TM1.stmts₁ q₂)
-- Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
LaurentPolynomial.antipode_T : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] (n : ℤ),
  (HopfAlgebraStruct.antipode R) (LaurentPolynomial.T n) = LaurentPolynomial.T (-n)
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : CategoryTheory.MorphismProperty C} {κ : Cardinal.{w}}
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType],
  autoParam (CategoryTheory.MorphismProperty.IsSmall.{w, v, u} I)
      CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.isSmall._autoParam →
    autoParam (CategoryTheory.LocallySmall.{w, v, u} C)
        CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.locallySmall._autoParam →
      autoParam (CategoryTheory.Limits.HasPushouts C)
          CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.hasPushouts._autoParam →
        autoParam (CategoryTheory.Limits.HasCoproducts C)
            CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.hasCoproducts._autoParam →
          autoParam (CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C)
              CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.hasIterationOfShape._autoParam →
            (∀ {A B X Y : C} (i : A ⟶ B),
                I i →
                  ∀ (f : X ⟶ Y) (hf : HomotopicalAlgebra.RelativeCellComplex (fun x => I.homFamily) f),
                    CategoryTheory.Limits.PreservesColimit hf.F (CategoryTheory.coyoneda.obj (Opposite.op A))) →
              I.IsCardinalForSmallObjectArgument κ
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsColoop.notMem_closure_of_notMem : ∀ {α : Type u_1} {M : Matroid α} {e : α} {X : Set α}, M.IsColoop e → e ∉ X → e ∉ M.closure X
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.primeSpectrumProd_symm_inr_asIdeal : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (x : PrimeSpectrum S),
  ((PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inr x)).asIdeal = ⊤.prod x.asIdeal
-- Mathlib.Analysis.Convolution
MeasureTheory.ConvolutionExistsAt.integrable_swap : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'} {x : G}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  {L : E →L[𝕜] E' →L[𝕜] F} [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : AddCommGroup G]
  [MeasurableNeg G] [μ.IsAddLeftInvariant] [MeasurableAdd G] [μ.IsNegInvariant],
  MeasureTheory.ConvolutionExistsAt f g x L μ → MeasureTheory.Integrable (fun t => (L (f (x - t))) (g t)) μ
-- Mathlib.AlgebraicGeometry.Sites.Representability
AlgebraicGeometry.Scheme.LocalRepresentability.instIsOpenImmersionToGlued : ∀ {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} {ι : Type u}
  {X : ι → AlgebraicGeometry.Scheme} {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj}
  (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) (i : ι),
  AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Scheme.LocalRepresentability.toGlued hf i)
-- Mathlib.RingTheory.LaurentSeries
/-- To any Cauchy filter ℱ of `K⸨X⸩`, we can attach a laurent series that is the limit
of the filter. Its `d`-th coefficient is defined as the limit of `Cauchy.coeff hℱ d`, which is
again Cauchy but valued in the discrete space `K`. That sufficiently negative coefficients vanish
follows from `Cauchy.coeff_support_bddBelow`  -/
LaurentSeries.Cauchy.limit : {K : Type u_2} → [inst : Field K] → {ℱ : Filter (LaurentSeries K)} → Cauchy ℱ → LaurentSeries K
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.skipSuffix?_eq_backwardPatternSkipSuffix? : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String.Slice},
  s.skipSuffix? pat = String.Slice.Pattern.BackwardPattern.skipSuffix? pat s
-- Mathlib.Data.Set.Operations
Set.rangeFactorization_eq_iff : ∀ {ι : Sort u_2} {α : Type u_3} {f : ι → α} (a : ι) (b : ↑(Set.range f)), Set.rangeFactorization f a = b ↔ f a = ↑b
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.JordanSub
MeasureTheory.Measure.toSignedMeasure_restrict_sub : ∀ {X : Type u_1} {mX : MeasurableSpace X} {s : Set X} {μ ν : MeasureTheory.Measure X}
  [inst : MeasureTheory.IsFiniteMeasure μ] [inst_1 : MeasureTheory.IsFiniteMeasure ν],
  MeasureTheory.IsHahnDecomposition μ ν s →
    ((ν - μ).restrict s).toSignedMeasure =
      MeasureTheory.VectorMeasure.restrict ν.toSignedMeasure s -
        MeasureTheory.VectorMeasure.restrict μ.toSignedMeasure s
-- Mathlib.RingTheory.PrincipalIdealDomain
Ideal.exists_maximal_not_isPrincipal : ∀ {R : Type u} [inst : Semiring R], ¬IsPrincipalIdealRing R → ∃ I, Maximal (fun x => ¬Submodule.IsPrincipal x) I
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1
-- Mathlib.Algebra.Group.Commute.Units
Units.commute_iff_mul_inv_cancel_assoc : ∀ {M : Type u_1} [inst : Monoid M] {u : Mˣ} {a : M}, Commute (↑u) a ↔ ↑u * (a * ↑u⁻¹) = a
-- Mathlib.Tactic.Widget.GCongr
/-- The gcongr widget.  -/
GCongrSelectionPanel : ProofWidgets.Component SelectInsertParams
-- Mathlib.Algebra.Group.Hom.Defs
/-- Group homomorphisms preserve integer power.  -/
MonoidHom.map_zpow : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : DivisionMonoid β] (f : α →* β) (g : α) (n : ℤ),
  f (g ^ n) = f g ^ n
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx'_lt`. -/
Ideal.ramificationIdx_lt : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R} {P : Ideal S}
  {n : ℕ}, ¬Ideal.map (algebraMap R S) p ≤ P ^ n → p.ramificationIdx' P < n
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.head?_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Min α]
  [inst_1 : LE α] [Std.LawfulOrderCmp cmp] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α]
  [Std.LawfulEqCmp cmp], t.keys.head? = t.minKey?
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- The forward functor of the identity equivalence is compatible with shifts.
 -/
CategoryTheory.Equivalence.CommShift.instCommShiftFunctorRefl : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (A : Type u_3) →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] → CategoryTheory.Equivalence.refl.functor.CommShift A
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] [CompactSpace ↥Y], CompactSpace ↥X
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_cWeight_eq_expect : ∀ {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [inst : Fintype ι] [inst_1 : RCLike 𝕜]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → InnerProductSpace 𝕜 (E i)]
  (f g : (i : ι) → E i), ⟪f, g⟫ₙ_[𝕜] = Finset.univ.expect fun i => inner 𝕜 (f i) (g i)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.snd.instIsFiniteMeasure : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {ρ : MeasureTheory.Measure (α × β)} [MeasureTheory.IsFiniteMeasure ρ], MeasureTheory.IsFiniteMeasure ρ.snd
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
/-- If `f : X ⟶ Y` is a quasi-compact immersion, then `X` is the pullback of the
closed immersion `im f ⟶ Y` and an open immersion `U ⟶ Y`.
 -/
AlgebraicGeometry.IsImmersion.isPullback_toImage_liftCoborder : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsImmersion f]
  [AlgebraicGeometry.QuasiCompact f],
  CategoryTheory.IsPullback (AlgebraicGeometry.Scheme.Hom.toImage f) (AlgebraicGeometry.Scheme.Hom.liftCoborder f)
    (AlgebraicGeometry.Scheme.Hom.imageι f) (AlgebraicGeometry.Scheme.Hom.coborderRange f).ι
-- Lean.Meta.InferType
/-- Auxiliary function for `isArrowProposition`.

Remark: we have added the `.bvar _` case to be able to return a definite value for
polymorphic functions. For example, suppose we are trying to check whether the
term `1 + 1` is a proof. The function `isArrowProposition type 6` is invoked where
`type` is of the form:
```
{α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HAdd α β γ] → α → β → γ
```
It is the type of `HAdd.hAdd`.
Note that the resulting type is a de Bruijn variable.
 -/
_private.Lean.Meta.InferType.0.Lean.Meta.isArrowProposition' : Lean.Expr → ℕ → Lean.MetaM Lean.Meta.ArrowPropResult✝
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprodX_ext_from : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c}
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] {A : C} {i : ι}
  {f g : (K ⊞ L).X i ⟶ A},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) g →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) g →
      f = g
-- Mathlib.Analysis.Asymptotics.LinearGrowth
/-- See `le_linearGrowthSup_add'` for a version with swapped argument `u` and `v`.  -/
LinearGrowth.le_linearGrowthSup_add : ∀ {u v : ℕ → EReal},
  LinearGrowth.linearGrowthSup u + LinearGrowth.linearGrowthInf v ≤ LinearGrowth.linearGrowthSup (u + v)
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
Nat.sum_divisors : ∀ {n : ℕ}, n ≠ 0 → ∑ d ∈ n.divisors, d = ∏ p ∈ n.primeFactors, ∑ k ∈ Finset.range (n.factorization p + 1), p ^ k
-- Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
MeasureTheory.measurableEmbedding_embeddingReal : ∀ (Ω : Type u_2) [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω],
  MeasurableEmbedding (MeasureTheory.embeddingReal Ω)
-- Mathlib.Computability.Primrec.Basic
Primrec.ulower_up : ∀ {α : Type u_1} [inst : Primcodable α], Primrec ULower.up
-- Mathlib.Order.BoundedOrder.Basic
BoundedOrder.mk : {α : Type u} → [inst : LE α] → [toOrderTop : OrderTop α] → [toOrderBot : OrderBot α] → BoundedOrder α
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulPosReflectLE.toContravariantClass : ∀ {α : Type u_1} {inst : Mul α} {inst_1 : Zero α} {inst_2 : Preorder α} [self : MulPosReflectLE α],
  ContravariantClass { x // 0 < x } α (fun x y => y * ↑x) fun x1 x2 => x1 ≤ x2
-- Mathlib.Data.Num.ZNum
PosNum.to_nat_eq_succ_pred : ∀ (n : PosNum), ↑n = ↑n.pred' + 1
-- Mathlib.NumberTheory.RamificationInertia.Galois
/-- The cardinality of the inertia group is equal to the ramification index.  -/
Ideal.card_inertia_eq_ramificationIdxIn : ∀ {R : Type u_1} {S : Type u_2} {G : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G S] [IsGaloisGroup G R S] [Finite G] [IsDomain R] [IsDomain S]
  [Module.Finite R S] [Module.Flat R S] (p : Ideal R) (P : Ideal S) [P.LiesOver p] [inst_12 : p.IsPrime] [P.IsPrime]
  [PerfectField p.ResidueField], Nat.card ↥(Ideal.inertia G P) = p.ramificationIdxIn S
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasStrictFDerivAt.comp_hasStrictDerivAt_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : 𝕜 → F}
  {f' : F} (x : 𝕜) {l : F → E} {l' : F →L[𝕜] E} {y : F},
  HasStrictFDerivAt l l' y → HasStrictDerivAt f f' x → y = f x → HasStrictDerivAt (l ∘ f) (l' f') x
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
ContDiff.differentiable_iteratedDeriv' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} (m : ℕ), ContDiff 𝕜 (↑m + 1) f → Differentiable 𝕜 (iteratedDeriv m f)
-- Mathlib.Topology.MetricSpace.Antilipschitz
/-- **Alias** of the reverse direction of `antilipschitzWith_iff_le_mul_nndist`. -/
AntilipschitzWith.of_le_mul_nndist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
  (∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)) → AntilipschitzWith K f
-- Lean.Data.Lsp.Window
Lean.Lsp.MessageType.noConfusionType : Sort v✝ → Lean.Lsp.MessageType → Lean.Lsp.MessageType → Sort v✝