mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Interval.Set.Monoid
Set.image_const_add_Icc : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M]
  (a b c : M), (fun x => a + x) '' Set.Icc b c = Set.Icc (a + b) (a + c)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.bfamilyOfFamily'_typein : ∀ {α : Type u_1} {ι : Type u_3} (r : ι → ι → Prop) [inst : IsWellOrder ι r] (f : ι → α) (i : ι),
  Ordinal.bfamilyOfFamily' r f ((Ordinal.typein r).toRelEmbedding i) ⋯ = f i
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContext.addJP : Lean.IR.LocalContext → Lean.IR.JoinPointId → Array Lean.IR.Param → Lean.IR.FnBody → Lean.IR.LocalContext
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get?_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t₁ \ t₂).get? k = if k ∈ t₂ then none else t₁.get? k
-- Mathlib.Algebra.GroupWithZero.Units.Basic
IsUnit.mul_right_eq_zero : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {a b : M₀}, IsUnit a → (a * b = 0 ↔ b = 0)
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_le_natTrailingDegree : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
  q ≠ 0 → p.trailingDegree ≤ q.trailingDegree → p.natTrailingDegree ≤ q.natTrailingDegree
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.instSMul : (R : Type u_1) →
  (X : Type u_2) →
    [inst : CommSemiring R] → {A : Type u_3} → [inst_1 : CommSemiring A] → [Algebra R A] → SMul R (FreeAlgebra A X)
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
TopCat.toSSetObjEquiv_δ_apply : ∀ {X : TopCat} {n : ℕ} (x : (TopCat.toSSet.obj X).obj (Opposite.op { len := n + 1 })) (i : Fin (n + 2))
  (z : ↑(stdSimplex ℝ (Fin (n + 1)))),
  ((X.toSSetObjEquiv (Opposite.op { len := n }))
        ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (TopCat.toSSet.obj X) i)) x))
      z =
    ((X.toSSetObjEquiv (Opposite.op { len := n + 1 })) x) (stdSimplex.map i.succAbove z)
-- Mathlib.Analysis.Complex.Circle
Circle.coe_mul : ∀ (z w : Circle), ↑(z * w) = ↑z * ↑w
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_neg_nhdsLE : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddCommGroup H] [inst_2 : PartialOrder H] [IsOrderedAddMonoid H]
  [ContinuousNeg H] {a : H}, Filter.Tendsto Neg.neg (nhdsWithin a (Set.Iic a)) (nhdsWithin (-a) (Set.Ici (-a)))
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
String.reduceAppend : Lean.Meta.Simp.DSimproc
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k fallback : α}, (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k (m₁.getKeyD k fallback)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Flag indicating whether `numEq0?` has been updated.  -/
Lean.Meta.Grind.Arith.CommRing.CommRing.numEq0Updated : Lean.Meta.Grind.Arith.CommRing.CommRing → Bool
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.brecOn.eq : ∀ {C : Type u} {motive : (a a_1 : CategoryTheory.FreeMonoidalCategory C) → a.Hom a_1 → Sort u_1}
  {a a_1 : CategoryTheory.FreeMonoidalCategory C} (t : a.Hom a_1)
  (F_1 :
    (a a_2 : CategoryTheory.FreeMonoidalCategory C) →
      (t : a.Hom a_2) → CategoryTheory.FreeMonoidalCategory.Hom.below t → motive a a_2 t),
  CategoryTheory.FreeMonoidalCategory.Hom.brecOn t F_1 =
    F_1 a a_1 t (CategoryTheory.FreeMonoidalCategory.Hom.brecOn.go t F_1).2
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
minpoly.instAlgebraSubtypeMemSubringSubalgebraIntegralClosure : {K : Type u_3} →
  {L : Type u_4} →
    [inst : Field K] →
      [inst_1 : Field L] → [inst_2 : Algebra K L] → (A : Subring K) → Algebra ↥A ↥(integralClosure (↥A) L)
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.eventually : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l₁ : Filter α} {l₂ : Filter β} {p : β → Prop},
  Filter.Tendsto f l₁ l₂ → (∀ᶠ (y : β) in l₂, p y) → ∀ᶠ (x : α) in l₁, p (f x)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
/-- The `positivity` extension which identifies expressions of the form `Gamma a`.  -/
Mathlib.Meta.Positivity.evalGamma : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₂_map_f_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {X Y : CategoryTheory.Idempotents.Karoubi (ChainComplex C ℕ)}
  (f : X ⟶ Y) (Δ : SimplexCategoryᵒᵖ),
  (AlgebraicTopology.DoldKan.Γ₂.map f).f.app Δ =
    (AlgebraicTopology.DoldKan.Γ₀.splitting X.X).desc Δ fun A =>
      CategoryTheory.CategoryStruct.comp (f.f.f (Opposite.unop A.fst).len)
        (((AlgebraicTopology.DoldKan.Γ₀.splitting Y.X).cofan Δ).inj A)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.comp_coe : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [inst_6 : RingHomInvPair σ₁₃ σ₃₁]
  [inst_7 : RingHomInvPair σ₃₁ σ₁₃] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃}
  [inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] (f : M₁ ≃ₛₗ[σ₁₂] M₂)
  (f' : M₂ ≃ₛₗ[σ₂₃] M₃), ↑f' ∘ₛₗ ↑f = ↑(f.trans f')
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_analytic : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : CharZero 𝕂] [ContinuousSMul ℚ 𝕂]
  [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸), AnalyticAt 𝕂 NormedSpace.exp x
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_left_split.eq_1 : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly) (k : ℕ),
  Int.Internal.Linear.cooper_left_split ctx p₁ p₂ k =
    (Int.Internal.Linear.Poly.denote' ctx
          (((p₁.tail.mul p₂.leadCoeff).combine (p₂.tail.mul (-p₁.leadCoeff))).addConst (p₂.leadCoeff * ↑k)) ≤
        0 ∧
      p₁.leadCoeff ∣ Int.Internal.Linear.Poly.denote' ctx (p₁.tail.addConst ↑k))
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.ofLT? : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Option (Option Lean.Expr)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_insertMany_empty_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] [inst : Std.LawfulEqOrd α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : compare k k' = Ordering.eq) {v : β k} [inst_1 : Inhabited (β k')],
  List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → (↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)).get! k' = cast ⋯ v
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).minKey? = some k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_filter_not_contains_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α},
  Std.Internal.List.DistinctKeys l₁ →
    ((List.filter (fun p => !l₂.contains p.fst) l₁).isEmpty = true ↔
      ∀ (k : α), Std.Internal.List.containsKey k l₁ = true → l₂.contains k = true)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE_trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE✝ t a b hab)
      (CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE✝ t b c hbc) =
    CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctorNatTransOfLE✝ t a c ⋯
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- For an `m × n` `α`-matrix `A`, `A.row i` is the `i`th row of `A` as a vector in `n → α`.
`A.row` is defeq to `A`, but explicitly refers to the 'row function' of `A`
while avoiding defeq abuse and noisy eta-expansions,
such as in expressions like `Set.Injective A.row` and `Set.range A.row`.
(Note 2025-04-07 : the identifier `Matrix.row` used to refer to a matrix with all rows equal;
this is now called `Matrix.replicateRow`)  -/
Matrix.row : {m : Type u_2} → {n : Type u_3} → {α : Type v} → Matrix m n α → m → n → α
-- Lean.Parser.Level
Lean.Parser.Level.ident : Lean.Parser.Parser
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.add_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] (μ' : MeasureTheory.Measure α)
  [MeasureTheory.SFinite μ'], (μ + μ').prod ν = μ.prod ν + μ'.prod ν
-- Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
instIsStablyFiniteRingOfOrzechProperty : ∀ {R : Type u_1} [inst : Semiring R] [OrzechProperty R], IsStablyFiniteRing R
-- Mathlib.CategoryTheory.Square
/-- Constructor for isomorphisms in `Square C`  -/
CategoryTheory.Square.isoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {sq₁ sq₂ : CategoryTheory.Square C} →
      (e₁ : sq₁.X₁ ≅ sq₂.X₁) →
        (e₂ : sq₁.X₂ ≅ sq₂.X₂) →
          (e₃ : sq₁.X₃ ≅ sq₂.X₃) →
            (e₄ : sq₁.X₄ ≅ sq₂.X₄) →
              CategoryTheory.CategoryStruct.comp sq₁.f₁₂ e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom sq₂.f₁₂ →
                CategoryTheory.CategoryStruct.comp sq₁.f₁₃ e₃.hom = CategoryTheory.CategoryStruct.comp e₁.hom sq₂.f₁₃ →
                  CategoryTheory.CategoryStruct.comp sq₁.f₂₄ e₄.hom =
                      CategoryTheory.CategoryStruct.comp e₂.hom sq₂.f₂₄ →
                    CategoryTheory.CategoryStruct.comp sq₁.f₃₄ e₄.hom =
                        CategoryTheory.CategoryStruct.comp e₃.hom sq₂.f₃₄ →
                      (sq₁ ≅ sq₂)
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.HomologySequence.snakeInput_v₂₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j),
  (HomologicalComplex.HomologySequence.snakeInput hS i j hij).v₂₃ =
    S.mapNatTrans (HomologicalComplex.natTransHomologyπ C c j)
-- Mathlib.Order.Max
IsTop.lt_of_ne' : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, IsTop a → a ≠ b → b < a
-- Mathlib.Control.Monad.Writer
WriterT.run_listen : ∀ {M : Type u → Type v} {α ω : Type u} [inst : Monad M] (cmd : WriterT ω M α),
  (listen cmd).run =
    (fun x =>
        match x with
        | (a, w) => ((a, w), w)) <$>
      cmd.run
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.CommMon.equivLaxBraidedFunctorPUnit.counitIso =
    CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso C
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- If a functor preserves a certain right homology data of a short complex `S`, then it
preserves the right homology of `S`.  -/
CategoryTheory.Functor.PreservesRightHomologyOf.mk' : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData) [h.IsPreservedBy F],
  F.PreservesRightHomologyOf S
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_union : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Raw.Const.get! (m₁ ∪ m₂) k = Std.DTreeMap.Raw.Const.getD m₂ k (Std.DTreeMap.Raw.Const.get! m₁ k)
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.isUniformEmbedding : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} [inst_2 : Fact (1 ≤ p)], IsUniformEmbedding Subtype.val
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, k ∉ t₁ → (t₁ ∪ t₂).getKeyD k fallback = t₂.getKeyD k fallback
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.d_f_comp_d_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (i₁ i₁' i₁'' : I₁) (i₂ : I₂) {Z : C} (h : (K.X i₁'').X i₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (CategoryTheory.CategoryStruct.comp ((K.d i₁' i₁'').f i₂) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.RingTheory.Derivation.Basic
/-- `D : Derivation R A M` is an `R`-linear map from `A` to `M` that satisfies the `leibniz`
equality. We also require that `D 1 = 0`. See `Derivation.mk'` for a constructor that deduces this
assumption from the Leibniz rule when `M` is cancellative.

TODO: update this when bimodules are defined.  -/
Derivation : (R : Type u_1) →
  (A : Type u_2) →
    (M : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M] → [Algebra R A] → [Module A M] → [Module R M] → Type (max u_2 u_3)
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.log_ten_eq : Real.log 10 = Real.log 2 + Real.log 5
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.coe_sInf : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] (S : Set (NonUnitalStarSubalgebra R A)), ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Generators.naive.congr_simp : ∀ {R : Type u} [inst : CommRing R] {σ : Type u_2} {I : Ideal (MvPolynomial σ R)}
  (s s_1 : MvPolynomial σ R ⧸ I → MvPolynomial σ R) (e_s : s = s_1)
  (hs : ∀ (x : MvPolynomial σ R ⧸ I), (Ideal.Quotient.mk I) (s x) = x),
  Algebra.Generators.naive s hs = Algebra.Generators.naive s_1 ⋯
-- Mathlib.Algebra.Homology.DerivedCategory.KInjective
CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {K L : CochainComplex C ℤ}
  {n : ℤ}
  [inst_2 :
    CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L]
  [inst_3 : L.IsKInjective]
  (b : CategoryTheory.Localization.SmallShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) K L n),
  CochainComplex.HomComplex.CohomologyClass.equivOfIsKInjective.symm b = Function.surjInv ⋯ b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isSome_apply_of_mem_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α} (h : k ∈ Std.DTreeMap.filterMap f t),
  (f (t.getKey k ⋯) (Std.DTreeMap.Const.get t k ⋯)).isSome = true
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.op_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData), h.op.π = h.ι.op
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMulticospan.left.inj : ∀ {J : CategoryTheory.Limits.MulticospanShape} {a a_1 : J.L},
  CategoryTheory.Limits.WalkingMulticospan.left a = CategoryTheory.Limits.WalkingMulticospan.left a_1 → a = a_1
-- Mathlib.Order.ModularLattice
Codisjoint.isCompl_inf_right_of_isCompl_inf_left : ∀ {α : Type u_1} {a b c : α} [inst : Lattice α] [inst_1 : BoundedOrder α] [IsModularLattice α],
  Codisjoint a b → IsCompl (a ⊓ b) c → IsCompl a (b ⊓ c)
-- Mathlib.RingTheory.SimpleModule.Basic
LinearMap.surjective_or_eq_zero : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsSimpleModule R N] (f : M →ₗ[R] N), Function.Surjective ⇑f ∨ f = 0
-- Init.Data.Array.Lemmas
Array.getD_getElem? : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {d : α}, xs[i]?.getD d = if p : i < xs.size then xs[i] else d
-- Mathlib.CategoryTheory.Subfunctor.Equalizer
CategoryTheory.Subfunctor.equalizer.lift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F₁ F₂ : CategoryTheory.Functor C (Type w)}
  {A : CategoryTheory.Subfunctor F₁} (f g : A.toFunctor ⟶ F₂) {G : CategoryTheory.Functor C (Type w)}
  (φ φ_1 : G ⟶ A.toFunctor) (e_φ : φ = φ_1)
  (w : CategoryTheory.CategoryStruct.comp φ f = CategoryTheory.CategoryStruct.comp φ g),
  CategoryTheory.Subfunctor.equalizer.lift f g φ w = CategoryTheory.Subfunctor.equalizer.lift f g φ_1 ⋯
-- Init.Data.Option.Attach
_private.Init.Data.Option.Attach.0.OptionT.bind.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) →
    (__do_lift : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive __do_lift
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.postcompCLM_apply : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : RCLike 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : NormedAddCommGroup G] [inst_7 : NormedSpace ℝ G] [inst_8 : NormedSpace 𝕜 G] (L : F →L[𝕜] G)
  (f : SchwartzMap E F) (x : E), ((SchwartzMap.postcompCLM L) f) x = L (f x)
-- Mathlib.MeasureTheory.Measure.FiniteMeasureExt
MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_polish : ∀ {E : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace E] [inst_2 : TopologicalSpace E]
  [PolishSpace E] [BorelSpace E] {P P' : MeasureTheory.Measure E} [MeasureTheory.IsFiniteMeasure P]
  [MeasureTheory.IsFiniteMeasure P'] {A : StarSubalgebra 𝕜 (BoundedContinuousFunction E 𝕜)},
  (StarSubalgebra.map (BoundedContinuousFunction.toContinuousMapStarₐ 𝕜) A).SeparatesPoints →
    (∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P') → P = P'
-- Init.Data.Int.Linear
/-- Returns `true` if `k` divides all coefficients and the constant of the given
linear polynomial.
 -/
Int.Internal.Linear.Poly.divAll : ℤ → Int.Internal.Linear.Poly → Bool
-- Mathlib.Tactic.Rify
/-- Translate a proof and the proposition into rified form.  -/
Mathlib.Tactic.Rify.rifyProof : Lean.Expr → Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.StainData.mk.injEq : ∀ (stained : Mathlib.Linter.Flexible.Stained✝) (stx : Lean.Syntax) (ci : Lean.Elab.ContextInfo)
  (mctx : Lean.MetavarContext) (goals : List Lean.MVarId) (stained_1 : Mathlib.Linter.Flexible.Stained✝)
  (stx_1 : Lean.Syntax) (ci_1 : Lean.Elab.ContextInfo) (mctx_1 : Lean.MetavarContext) (goals_1 : List Lean.MVarId),
  ({ stained := stained, stx := stx, ci := ci, mctx := mctx, goals := goals } =
      { stained := stained_1, stx := stx_1, ci := ci_1, mctx := mctx_1, goals := goals_1 }) =
    (stained = stained_1 ∧ stx = stx_1 ∧ ci = ci_1 ∧ mctx = mctx_1 ∧ goals = goals_1)
-- Mathlib.NumberTheory.SmoothNumbers
Nat.mem_smoothNumbers : ∀ {n m : ℕ}, m ∈ n.smoothNumbers ↔ m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p < n
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.PairingCore.RankFunction.mk.sizeOf_spec : ∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} {α : Type v} [inst : PartialOrder α] [inst_1 : SizeOf α]
  (rank : h.ι → α) (lt : ∀ {x y : h.ι}, h.AncestralRel x y → rank x < rank y), sizeOf { rank := rank, lt := lt } = 1
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.map_inv_atTop : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : PartialOrder G] [IsOrderedMonoid G],
  Filter.map Inv.inv Filter.atTop = Filter.atBot
-- Mathlib.Computability.StateTransition
StateTransition.Reaches₀.trans : ∀ {σ : Type u_1} {f : σ → Option σ} {a b c : σ},
  StateTransition.Reaches₀ f a b → StateTransition.Reaches₀ f b c → StateTransition.Reaches₀ f a c
-- Mathlib.RingTheory.Smooth.Kaehler
Algebra.Extension.Cotangent.map_toInfinitesimal_bijective : ∀ {R : Type u_1} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S), Function.Bijective ⇑(Algebra.Extension.Cotangent.map P.toInfinitesimal)
-- Mathlib.Data.Rel
SetRel.comp_subset_comp_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R₁ R₂ : SetRel α β} {S : SetRel β γ}, R₁ ⊆ R₂ → R₁.comp S ⊆ R₂.comp S
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
/-- An isomorphism of rings induces an isomorphism of residue fields.  -/
Ideal.residueFieldAlgEquiv' : {R : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : CommRing B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                (I : Ideal R) →
                  [inst_5 : I.IsPrime] →
                    (J : Ideal A) →
                      (K : Ideal B) →
                        [inst_6 : J.IsPrime] →
                          [inst_7 : K.IsPrime] →
                            [inst_8 : J.LiesOver I] →
                              [inst_9 : Algebra (Localization.AtPrime I) (Localization.AtPrime J)] →
                                [inst_10 : Localization.AtPrime.IsLiesOverAlgebra I J] →
                                  [inst_11 : K.LiesOver I] →
                                    [inst_12 : Algebra (Localization.AtPrime I) (Localization.AtPrime K)] →
                                      [inst_13 : Localization.AtPrime.IsLiesOverAlgebra I K] →
                                        (f : A ≃ₐ[R] B) →
                                          J = Ideal.comap f K → J.ResidueField ≃ₐ[I.ResidueField] K.ResidueField
-- Mathlib.RingTheory.Finiteness.Cardinality
AddSubmonoid.fg_iff_exists_fin_addMonoidHom : ∀ {M : Type u_3} [inst : AddCommMonoid M] {S : AddSubmonoid M}, S.FG ↔ ∃ n f, AddMonoidHom.mrange f = S
-- Mathlib.Analysis.Normed.Group.Quotient
_private.Mathlib.Analysis.Normed.Group.Quotient.0.QuotientGroup.norm_aux : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] {S : Subgroup M} (x : M ⧸ S), {m | ↑m = x}.Nonempty
-- Mathlib.NumberTheory.SmoothNumbers
/-- `m` is `n`-smooth if and only if `m` is nonzero and all prime divisors `≤ m` of `m`
are less than `n`.  -/
Nat.mem_smoothNumbers_iff_forall_le : ∀ {n m : ℕ}, m ∈ n.smoothNumbers ↔ m ≠ 0 ∧ ∀ p ≤ m, Nat.Prime p → p ∣ m → p < n