mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Tree.RunMetaM
Aesop.Rapp.runMetaMInParentState' : {m : Type → Type} → [Monad m] → [MonadLiftT Lean.MetaM m] → [MonadFinally m] → {α : Type} → m α → Aesop.Rapp → m α
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.semigroup.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₂] [inst_1 : Semigroup M₁] (f : M₁ → M₂) (hf : Function.Surjective f)
  (mul : ∀ (x y : M₁), f (x * y) = f x * f y),
  Function.Surjective.semigroup f hf mul = { toMul := inst, mul_assoc := ⋯ }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α} {v : β k},
  (t.insertIfNew k v).minKey! = t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Mathlib.Util.AtLocation
/-- Use the procedure `m` to rewrite the provided goal.

Assumes `proc` is not surrounded by backticks.  -/
Mathlib.Tactic.transformAtTarget : (Lean.Expr → ReaderT Lean.Meta.Simp.Context Lean.MetaM Lean.Meta.Simp.Result) →
  String →
    Mathlib.Tactic.BehaviorIfUnchanged → Lean.MVarId → ReaderT Lean.Meta.Simp.Context Lean.MetaM (Option Lean.MVarId)
-- Mathlib.Analysis.Real.Pi.Bounds
Real.pi_lt_d6 : Real.pi < 3.141593
-- Mathlib.RingTheory.FreeRing
FreeRing.one_ne_of : ∀ {α : Type u} (x : α), 1 ≠ FreeRing.of x
-- Mathlib.Analysis.InnerProductSpace.l2Space
OrthogonalFamily.hasSum_linearIsometry : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {G : ι → Type u_4} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_5 : CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E}
  (hV : OrthogonalFamily 𝕜 G V) (f : ↥(lp G 2)), HasSum (fun i => (V i) (↑f i)) (hV.linearIsometry f)
-- Mathlib.Logic.Relation
Std.Symm.swap_eq : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Symm r], Function.swap r = r
-- Mathlib.Algebra.Algebra.Shrink
Shrink.algEquiv_symm_apply : ∀ (R : Type u_1) (α : Type u_2) [inst : Small.{v, u_2} α] [inst_1 : CommSemiring R] [inst_2 : Semiring α]
  [inst_3 : Algebra R α] (a : α), (Shrink.algEquiv R α).symm a = (equivShrink α) a
-- Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
CategoryTheory.Functor.CoconeTypes.isMulticoequalizer_iff : ∀ {J : CategoryTheory.Limits.MultispanShape} {d : CategoryTheory.Limits.MultispanIndex J (Type u)}
  (c : d.multispan.CoconeTypes),
  c.IsColimit ↔
    (∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
        c.ι (CategoryTheory.Limits.WalkingMultispan.right i₁) x₁ =
            c.ι (CategoryTheory.Limits.WalkingMultispan.right i₂) x₂ →
          d.multispan.ιColimitType (CategoryTheory.Limits.WalkingMultispan.right i₁) x₁ =
            d.multispan.ιColimitType (CategoryTheory.Limits.WalkingMultispan.right i₂) x₂) ∧
      ∀ (x : c.pt), ∃ i a, c.ι (CategoryTheory.Limits.WalkingMultispan.right i) a = x
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- Nonzero divisors have nonzero valuation.  -/
IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero' : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  (x : ↥(nonZeroDivisors R)), v.intValuation ↑x ≠ 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {fallback : β},
  Std.DHashMap.Const.getD (m₁.inter m₂) k fallback = if k ∈ m₂ then Std.DHashMap.Const.getD m₁ k fallback else fallback
-- Init.Data.UInt.Lemmas
UInt64.toNat_mod_size : ∀ (n : UInt64), n.toNat % UInt64.size = n.toNat
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.GrothendieckTopology.instIsIsoFunctorOppositeSheafSheafComposeNatTransPlusPlusAdjunction : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_3}
  {E : Type u_4} [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  [inst_8 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  {FD : D → D → Type u_5} {CD : D → Type u_6} {FE : E → E → Type u_7} {CE : E → Type u_8}
  [inst_9 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_10 : (X Y : E) → FunLike (FE X Y) (CE X) (CE Y)]
  [instCCD : CategoryTheory.ConcreteCategory D FD] [instCCE : CategoryTheory.ConcreteCategory E FE]
  [inst_11 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [inst_12 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget E)]
  [inst_13 :
    CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_3, u_6, u_3, u_6 + 1} (CategoryTheory.forget D)]
  [inst_14 :
    CategoryTheory.Limits.PreservesLimitsOfSize.{max v u, max v u, v_4, u_8, u_4, u_8 + 1} (CategoryTheory.forget E)]
  [inst_15 : (CategoryTheory.forget D).ReflectsIsomorphisms] [inst_16 : (CategoryTheory.forget E).ReflectsIsomorphisms],
  CategoryTheory.IsIso
    (CategoryTheory.sheafComposeNatTrans J F (CategoryTheory.plusPlusAdjunction J D)
      (CategoryTheory.plusPlusAdjunction J E))
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.isSome_getKey?_iff_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, (m.getKey? a).isSome = true ↔ a ∈ m
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y : C}
  (f : W ⟶ X) (g : X ⟶ Y) (Z : C) {Z_1 : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.CategoryStruct.comp f g) Z) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z) h)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- Corollary of the Chinese remainder theorem: given elements `x i : R`,
we can choose a representative `y : R` such that `y - x i ∈ P i ^ e i`.  -/
IsDedekindDomain.exists_forall_sub_mem_ideal : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R] {ι : Type u_4} {s : Finset ι} (P : ι → Ideal R) (e : ι → ℕ),
  (∀ i ∈ s, Prime (P i)) →
    (∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j) → ∀ (x : ↥s → R), ∃ y, ∀ (i : ι) (hi : i ∈ s), y - x ⟨i, hi⟩ ∈ P i ^ e i
-- Mathlib.Topology.Continuous
Continuous.congr : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f g : X → Y},
  Continuous f → (∀ (x : X), f x = g x) → Continuous g
-- Mathlib.Data.Int.Cast.Basic
Int.cast_add : ∀ {R : Type u} [inst : AddGroupWithOne R] (m n : ℤ), ↑(m + n) = ↑m + ↑n
-- Mathlib.Data.Finset.Union
Finset.erase_biUnion : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (f : α → Finset β) (s : Finset α) (b : β),
  (s.biUnion f).erase b = s.biUnion fun x => (f x).erase b
-- Aesop.Tree.Data
Aesop.GoalUnsafe.brecOn_4.eq : ∀ {motive_1 : Aesop.GoalUnsafe → Sort u} {motive_2 : Aesop.MVarClusterUnsafe → Sort u}
  {motive_3 : Aesop.RappUnsafe → Sort u} {motive_4 : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_5 : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe → Sort u}
  {motive_6 : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe → Sort u}
  {motive_7 : Array (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_8 : Option (IO.Ref Aesop.RappUnsafe) → Sort u}
  {motive_9 : Array (IO.Ref Aesop.GoalUnsafe) → Sort u} {motive_10 : Array (IO.Ref Aesop.MVarClusterUnsafe) → Sort u}
  {motive_11 : List (IO.Ref Aesop.RappUnsafe) → Sort u} {motive_12 : List (IO.Ref Aesop.GoalUnsafe) → Sort u}
  {motive_13 : List (IO.Ref Aesop.MVarClusterUnsafe) → Sort u} (t : Array (IO.Ref Aesop.RappUnsafe))
  (F_1 : (t : Aesop.GoalUnsafe) → t.below → motive_1 t) (F_2 : (t : Aesop.MVarClusterUnsafe) → t.below → motive_2 t)
  (F_3 : (t : Aesop.RappUnsafe) → t.below → motive_3 t)
  (F_4 : (t : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_1 t → motive_4 t)
  (F_5 : (t : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe) → Aesop.GoalUnsafe.below_2 t → motive_5 t)
  (F_6 : (t : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_3 t → motive_6 t)
  (F_7 : (t : Array (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_4 t → motive_7 t)
  (F_8 : (t : Option (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_5 t → motive_8 t)
  (F_9 : (t : Array (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_6 t → motive_9 t)
  (F_10 : (t : Array (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_7 t → motive_10 t)
  (F_11 : (t : List (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_8 t → motive_11 t)
  (F_12 : (t : List (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_9 t → motive_12 t)
  (F_13 : (t : List (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_10 t → motive_13 t),
  Aesop.GoalUnsafe.brecOn_4 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13 =
    F_7 t (Aesop.GoalUnsafe.brecOn_4.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13).2
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.enumMember : Lean.Lsp.SymbolKind
-- Lean.Environment
/-- Extra entries for the `const2ModIdx` map in the `Environment` object.
The code generator creates auxiliary declarations that are not in the
mapping `constants`, but we want to know in which module they were generated.
 -/
Lean.ModuleData.extraConstNames : Lean.ModuleData → Array Lean.Name
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_zero_le : ∀ {R : Type u} [inst : Semiring R], Polynomial.degree 0 ≤ 0
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Under.w : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q : CategoryTheory.MorphismProperty T} {X : T}
  [inst_1 : Q.IsMultiplicative] {A B : P.Under Q X} (f : A ⟶ B),
  CategoryTheory.CategoryStruct.comp A.hom f.right = B.hom
-- Mathlib.CategoryTheory.Products.Basic
/-- Construct an isomorphism in `C × D` out of two isomorphisms in `C` and `D`.  -/
CategoryTheory.Iso.prod : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → {P Q : C} → {S T : D} → (P ≅ Q) → (S ≅ T) → ((P, S) ≅ (Q, T))
-- Mathlib.RepresentationTheory.Rep.Res
/-- An object of `Rep k G` is zero iff its restriction to `H` is zero.  -/
Rep.isZero_res_iff : ∀ {G : Type v1} {H : Type v2} [inst : Monoid G] [inst_1 : Monoid H] (f : H →* G) {k : Type u} [inst_2 : Ring k]
  (M : Rep.{u_1, u, v1} k G), CategoryTheory.Limits.IsZero (Rep.res f M) ↔ CategoryTheory.Limits.IsZero M
-- Mathlib.Order.Interval.Multiset
Multiset.card_Ioc_eq_card_Icc_sub_one : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] (a b : α),
  (Multiset.Ioc a b).card = (Multiset.Icc a b).card - 1
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_alter_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k : α} {f : Option β → Option β}, m.WF → (m.alter k f).contains k = (f m[k]?).isSome
-- Mathlib.CategoryTheory.Sites.LocallyBijective
CategoryTheory.Presheaf.isLocallyInjective_presheafToSheaf_map_iff : ∀ {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]
  [inst_4 : CategoryTheory.HasWeakSheafify J A] [J.WEqualsLocallyBijective A] {P Q : CategoryTheory.Functor Cᵒᵖ A}
  (φ : P ⟶ Q),
  CategoryTheory.Sheaf.IsLocallyInjective ((CategoryTheory.presheafToSheaf J A).map φ) ↔
    CategoryTheory.Presheaf.IsLocallyInjective J φ
-- Mathlib.Tactic.GRewrite.Core
Mathlib.Tactic.GRewrite.Config.mk.inj : ∀ {toConfig : Lean.Meta.Rewrite.Config} {useRewrite implicationHyp useKAbstract : Bool}
  {toConfig_1 : Lean.Meta.Rewrite.Config} {useRewrite_1 implicationHyp_1 useKAbstract_1 : Bool},
  { toConfig := toConfig, useRewrite := useRewrite, implicationHyp := implicationHyp, useKAbstract := useKAbstract } =
      { toConfig := toConfig_1, useRewrite := useRewrite_1, implicationHyp := implicationHyp_1,
        useKAbstract := useKAbstract_1 } →
    toConfig = toConfig_1 ∧
      useRewrite = useRewrite_1 ∧ implicationHyp = implicationHyp_1 ∧ useKAbstract = useKAbstract_1
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.apply_dfoldCast : ∀ {n : ℕ} {α : (i : ℕ) → autoParam (i ≤ n) Nat.apply_dfoldCast._auto_3✝ → Type u}
  (f : (i : ℕ) → (h : i < n) → α i ⋯ → α (i + 1) ⋯) {i j : ℕ} (h : i < n) {w : i = j} {x : α i ⋯},
  f j ⋯ (Nat.dfoldCast✝ α w x) = Nat.dfoldCast✝ (fun i h => α i h) ⋯ (f i h x)
-- Mathlib.Topology.TietzeExtension
/-- **Tietze extension theorem** for `TietzeExtension` spaces. Let `e` be a closed embedding of a
nonempty topological space `X₁` into a normal topological space `X`. Let `f` be a continuous
function on `X₁` with values in a `TietzeExtension` space `Y`. Then there exists a
continuous function `g : C(X, Y)` such that `g ∘ e = f`.

This version is provided for convenience and backwards compatibility. Here the composition is
phrased in terms of bare functions.  -/
ContinuousMap.exists_extension' : ∀ {X₁ : Type u₁} [inst : TopologicalSpace X₁] {X : Type u} [inst_1 : TopologicalSpace X] [NormalSpace X] {e : X₁ → X}
  {Y : Type v} [inst_3 : TopologicalSpace Y] [TietzeExtension Y],
  Topology.IsClosedEmbedding e → ∀ (f : C(X₁, Y)), ∃ g, ⇑g ∘ e = ⇑f
-- Mathlib.CategoryTheory.Sites.CartesianMonoidal
/-- **Alias** of `CategoryTheory.Sheaf.cartesianMonoidalCategoryFst_hom`. -/
CategoryTheory.Sheaf.cartesianMonoidalCategoryFst_val : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) [inst_2 : CategoryTheory.CartesianMonoidalCategory A]
  (X Y : CategoryTheory.Sheaf J A),
  (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y).hom =
    CategoryTheory.SemiCartesianMonoidalCategory.fst X.obj Y.obj
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.irreducible_minpoly : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsAlgebraic K L]
  (c : ConjRootClass K L), Irreducible c.minpoly
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.hasPullback_of_comp_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ W) (g : Y ⟶ W) (i : W ⟶ Z)
  [CategoryTheory.Mono i] [CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)
-- Mathlib.LinearAlgebra.Dimension.Finite
Module.finrank_eq_zero_of_rank_eq_zero : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.rank R M = 0 → Module.finrank R M = 0
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_bot : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α], Set.Ici ⊥ = Set.univ
-- Init.Data.Vector.Erase
Vector.mem_eraseIdx_iff_getElem : ∀ {α : Type u_1} {n : ℕ} {x : α} {xs : Vector α n} {k : ℕ} {h : k < n},
  x ∈ xs.eraseIdx k h ↔ ∃ i, ∃ (w : i < n), i ≠ k ∧ xs[i] = x
-- Std.Http.Data.Body.Basic
Std.Http.Body.instToByteArrayByteArray : Std.Http.Body.ToByteArray ByteArray
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwiseDisjoint_insert_of_notMem : ∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] {s : Set ι} {f : ι → α} {i : ι},
  i ∉ s → ((insert i s).PairwiseDisjoint f ↔ s.PairwiseDisjoint f ∧ ∀ j ∈ s, Disjoint (f i) (f j))
-- Mathlib.RingTheory.DiscreteValuationRing.TFAE
IsLocalRing.finrank_CotangentSpace_eq_one_iff : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] [inst_2 : IsLocalRing R] [inst_3 : IsDomain R],
  Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
CategoryTheory.SubmonoidFunctor.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : CategoryTheory.Functor C MonCat} [inst_1 : SizeOf C]
  (obj : (U : C) → Submonoid ↑(M.obj U))
  (map :
    autoParam (∀ {U V : C} (i : U ⟶ V), obj U ≤ Submonoid.comap (MonCat.Hom.hom (M.map i)) (obj V))
      CategoryTheory.SubmonoidFunctor.map._autoParam),
  sizeOf { obj := obj, map := map } = 1
-- Std.Data.DHashMap.Raw
/-- Modifies in place the value associated with a given key,
allowing creating new values and deleting values via an `Option` valued replacement function.

This function ensures that the value is used linearly.
 -/
Std.DHashMap.Raw.Const.alter : {α : Type u} →
  [inst : BEq α] →
    [EquivBEq α] →
      [Hashable α] →
        {β : Type v} → (Std.DHashMap.Raw α fun x => β) → α → (Option β → Option β) → Std.DHashMap.Raw α fun x => β
-- Aesop.Tree.Data
Aesop.RappData.originalSubgoals : {Goal MVarCluster : Type} → Aesop.RappData Goal MVarCluster → Array Lean.MVarId
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.linearEquivAt.congr_simp : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F] [inst_4 : Module R F]
  [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
  (e e_1 : Bundle.Pretrivialization F Bundle.TotalSpace.proj) (e_e : e = e_1)
  [inst_7 : Bundle.Pretrivialization.IsLinear R e] (b : B) (hb : b ∈ e.baseSet),
  Bundle.Pretrivialization.linearEquivAt R e b hb = Bundle.Pretrivialization.linearEquivAt R e_1 b ⋯
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsFoelner.mean.eq_1 : ∀ {X : Type u_2} [inst : MeasurableSpace X] (μ : MeasureTheory.Measure X) {ι : Type u_3} (u : Ultrafilter ι)
  (F : ι → Set X) (s : Set X), IsFoelner.mean μ u F s = (↑u).limUnder fun i => μ (s ∩ F i) / μ (F i)
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- The Sylvester matrix for `f` and `f.derivative`, modified by dividing the bottom row by
the leading coefficient of `f`. Important because its determinant is (up to a sign) the
discriminant of `f`.
 -/
Polynomial.sylvesterDeriv : {R : Type u_1} →
  [inst : Semiring R] →
    (f : Polynomial R) → Matrix (Fin (f.natDegree - 1 + f.natDegree)) (Fin (f.natDegree - 1 + f.natDegree)) R
-- Init.Data.Array.Sort.Lemmas
Array.size_mergeSort : ∀ {α : Type u_1} {le : α → α → Bool} {xs : Array α}, (xs.mergeSort le).size = xs.size
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.instHasEqualizers : CategoryTheory.Limits.HasEqualizers SemiNormedGrp
-- Mathlib.Data.Set.Function
/-- **Alias** of the forward direction of `Set.surjOn_iff_exists_bijOn_subset`. -/
Set.SurjOn.exists_bijOn_subset : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.SurjOn f s t → ∃ s' ⊆ s, Set.BijOn f s' t
-- Init.Data.Iterators.Basic
Std.IterM.IsPlausibleIndirectOutput.brecOn : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β]
  {motive : (a : Std.IterM m β) → (a_1 : β) → a.IsPlausibleIndirectOutput a_1 → Prop} {a : Std.IterM m β} {a_1 : β}
  (t : a.IsPlausibleIndirectOutput a_1),
  (∀ (a : Std.IterM m β) (a_2 : β) (t : a.IsPlausibleIndirectOutput a_2),
      Std.IterM.IsPlausibleIndirectOutput.below t → motive a a_2 t) →
    motive a a_1 t
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
/-- To prove something for an arbitrary integrable function in a normed group,
it suffices to show that
* the property holds for (multiples of) characteristic functions;
* is closed under addition;
* the set of functions in the `L¹` space for which the property holds is closed.
* the property is closed under the almost-everywhere equal relation.

It is possible to make the hypotheses in the induction steps a bit stronger, and such conditions
can be added once we need them (for example in `h_add` it is only necessary to consider the sum of
a simple function with a multiple of a characteristic function and that the intersection
of their images is a subset of `{0}`).
 -/
MeasureTheory.Integrable.induction : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α}
  (P : (α → E) → Prop),
  (∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)) →
    (∀ ⦃f g : α → E⦄,
        Disjoint (Function.support f) (Function.support g) →
          MeasureTheory.Integrable f μ → MeasureTheory.Integrable g μ → P f → P g → P (f + g)) →
      IsClosed {f | P ↑↑f} →
        (∀ ⦃f g : α → E⦄, f =ᵐ[μ] g → MeasureTheory.Integrable f μ → P f → P g) →
          ∀ ⦃f : α → E⦄, MeasureTheory.Integrable f μ → P f
-- Mathlib.Data.Finset.Lattice.Fold
Finset.lt_sup_iff : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α} {a : α},
  a < s.sup f ↔ ∃ b ∈ s, a < f b
-- Mathlib.RingTheory.RingHom.QuasiFinite
RingHom.QuasiFinite.isStableUnderBaseChange : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => RingHom.QuasiFinite
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.isAddUnit_coe : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SubtractionMonoid α] {s : Finset α}, IsAddUnit ↑s ↔ IsAddUnit s
-- Mathlib.Tactic.NormNum.Ineq
Mathlib.Meta.NormNum.isRat_le_false : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α} {na nb : ℤ} {da db : ℕ},
  Mathlib.Meta.NormNum.IsRat a na da → Mathlib.Meta.NormNum.IsRat b nb db → decide (nb * ↑da < na * ↑db) = true → ¬a ≤ b
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instInhabitedInjectiveTheorem.default : Lean.Meta.Grind.InjectiveTheorem
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.mk.congr_simp : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (toFun toFun_1 : ((i : ι) → M₁ i) → M₂) (e_toFun : toFun = toFun_1)
  (map_update_add' :
    ∀ [inst : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (x y : M₁ i),
      toFun (Function.update m i (x + y)) = toFun (Function.update m i x) + toFun (Function.update m i y))
  (map_update_smul' :
    ∀ [inst_5 : DecidableEq ι] (m : (i : ι) → M₁ i) (i : ι) (c : R) (x : M₁ i),
      toFun (Function.update m i (c • x)) = c • toFun (Function.update m i x)),
  { toFun := toFun, map_update_add' := map_update_add', map_update_smul' := map_update_smul' } =
    { toFun := toFun_1, map_update_add' := ⋯, map_update_smul' := ⋯ }
-- Mathlib.RingTheory.FractionalIdeal.Extended
/-- **Alias** of `FractionalIdeal.extendedHom_le_one_iff`. -/
FractionalIdeal.extendedHomₐ_le_one_iff : ∀ {A : Type u_1} {K : Type u_2} (L : Type u_3) (B : Type u_4) [inst : CommRing A] [inst_1 : IsDomain A]
  [inst_2 : CommRing B] [inst_3 : IsDomain B] [inst_4 : Algebra A B] [inst_5 : Module.IsTorsionFree A B]
  [inst_6 : Field K] [inst_7 : Field L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : IsFractionRing A K]
  [inst_11 : IsFractionRing B L] {I : FractionalIdeal (nonZeroDivisors A) K} [inst_12 : Algebra K L]
  [inst_13 : Algebra A L] [IsScalarTower A B L] [IsScalarTower A K L] [Algebra.IsIntegral A B] [IsIntegrallyClosed A]
  [IsIntegrallyClosed B], (FractionalIdeal.extendedHom L B) I ≤ 1 ↔ I ≤ 1