mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
IntermediateField.fg_of_noetherian : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : IntermediateField F E)
  [IsNoetherian F E], S.FG
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_mul_cancel_left : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] (x : R) (y : ↥M),
  IsLocalization.mk' S (↑y * x) y = (algebraMap R S) x
-- Lean.Parser.Extension
Lean.Parser.AliasValue.binary.injEq : ∀ {α : Type} (p p_1 : α → α → α), (Lean.Parser.AliasValue.binary p = Lean.Parser.AliasValue.binary p_1) = (p = p_1)
-- Init.Data.String.Lemmas.Basic
String.append_eq_left_iff : ∀ {s t : String}, s ++ t = s ↔ t = ""
-- Init.Data.SInt.Bitwise
Int32.not_ne_self : ∀ {a : Int32}, ~~~a ≠ a
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.inter_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → m₃.WF → m₁.Equiv m₂ → (m₁ ∩ m₃).Equiv (m₂ ∩ m₃)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.unitOfList_eq_insertManyIfNewUnit_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α},
  Std.ExtHashMap.unitOfList l = ∅.insertManyIfNewUnit l
-- Init.Data.List.MinMaxIdx
List.maxIdxOn?_eq_minIdxOn? : ∀ {β : Type u_1} {α : Type u_2} {le : LE β} {x : DecidableLE β} {f : α → β} {xs : List α},
  List.maxIdxOn? f xs = List.minIdxOn? f xs
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
DirectSum.toAddMonoidAlgebra.eq_1 : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring M] [inst_2 : (m : M) → Decidable (m ≠ 0)]
  (f : DirectSum ι fun x => M), f.toAddMonoidAlgebra = AddMonoidAlgebra.ofCoeff (DFinsupp.toFinsupp f)
-- Mathlib.RingTheory.Valuation.Integers
/-- The ring of integers under a given valuation is the subring of elements with valuation ≤ 1.  -/
Valuation.integer : {R : Type u} →
  {Γ₀ : Type v} → [inst : Ring R] → [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → Valuation R Γ₀ → Subring R
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.isHashSelf_alterₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (m : Std.DHashMap.Internal.Raw₀ α β),
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ (a : α) (f : Option (β a) → Option (β a)), Std.DHashMap.Internal.IsHashSelf (↑(m.alterₘ a f)).buckets
-- Mathlib.Order.Hom.Lattice
SupHom.id.eq_1 : ∀ (α : Type u_2) [inst : Max α], SupHom.id α = { toFun := id, map_sup' := ⋯ }
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {G H : CategoryTheory.Pseudofunctor B C} (θ : G ⟶ H) {a b : B} {a' : C} (f : a' ⟶ G.obj a) {g h : a ⟶ b} (β : g ⟶ h),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.map₂ β) (θ.app b)))
      (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality h).hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality g).hom)
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.map₂ β)))
-- Mathlib.Data.NNReal.Basic
NNReal.coe_expect : ∀ {ι : Type u_2} (s : Finset ι) (f : ι → NNReal), ↑(s.expect fun i => f i) = s.expect fun i => ↑(f i)
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.IsWeaklyEisensteinAt.pow_natDegree_le_of_aeval_zero_of_monic_mem_map : ∀ {R : Type u} [inst : CommRing R] {𝓟 : Ideal R} {f : Polynomial R} {S : Type v} [inst_1 : CommRing S]
  [inst_2 : Algebra R S],
  f.IsWeaklyEisensteinAt 𝓟 →
    ∀ {x : S},
      (Polynomial.aeval x) f = 0 →
        f.Monic → ∀ (i : ℕ), (Polynomial.map (algebraMap R S) f).natDegree ≤ i → x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
-- Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique
/-- Local integral curves are unique.

If a $C^1$ vector field `v` admits two local integral curves `γ γ' : ℝ → M` at `t₀` with
`γ t₀ = γ' t₀`, then `γ` and `γ'` agree on some open interval containing `t₀`.  -/
isMIntegralCurveAt_eventuallyEq_of_contMDiffAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : IsManifold I 1 M] {γ γ' : ℝ → M} {v : (x : M) → TangentSpace I x} {t₀ : ℝ},
  I.IsInteriorPoint (γ t₀) →
    ContMDiffAt I I.tangent 1 (fun x => ⟨x, v x⟩) (γ t₀) →
      IsMIntegralCurveAt γ v t₀ → IsMIntegralCurveAt γ' v t₀ → γ t₀ = γ' t₀ → γ =ᶠ[nhds t₀] γ'
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
CategoryTheory.MonoidalCoherence.right_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  [inst_2 : CategoryTheory.MonoidalCoherence X Y],
  CategoryTheory.MonoidalCoherence.iso =
    CategoryTheory.MonoidalCategoryStruct.rightUnitor X ≪≫ CategoryTheory.MonoidalCoherence.iso
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
SSet.Subcomplex.fromPreimage_ι : ∀ {X Y : SSet} (A : X.Subcomplex) (p : Y ⟶ X),
  CategoryTheory.CategoryStruct.comp (A.fromPreimage p) A.ι = CategoryTheory.CategoryStruct.comp (A.preimage p).ι p
-- Mathlib.LinearAlgebra.Dimension.Finite
natCast_le_rank_iff_finset : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R] {n : ℕ},
  ↑n ≤ Module.rank R M ↔ ∃ s, s.card = n ∧ LinearIndependent R Subtype.val
-- Std.Do.SPred.SVal
_private.Std.Do.SPred.SVal.0.Std.Do.SVal.uncurry.match_3.eq_1 : ∀ {α : Type u_1} (motive : (σs : List (Type u_1)) → Std.Do.SVal σs α → Sort u_2) (f : Std.Do.SVal [] α)
  (h_1 : (f : Std.Do.SVal [] α) → motive [] f)
  (h_2 : (head : Type u_1) → (tail : List (Type u_1)) → (f : Std.Do.SVal (head :: tail) α) → motive (head :: tail) f),
  (match [], f with
    | [], f => h_1 f
    | head :: tail, f => h_2 head tail f) =
    h_1 f
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.IsEquiv.refl : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  (v : AbsoluteValue R S), v.IsEquiv v
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  {l : List α} {k : α} {h' : k ∈ Std.ExtDTreeMap.Const.insertManyIfNewUnit t l},
  Std.ExtDTreeMap.Const.get (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l) k h' = ()
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.maxDegree_mono : ∀ {V : Type u_1} {G H : SimpleGraph V} [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableRel H.Adj],
  G ≤ H → G.maxDegree ≤ H.maxDegree
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_of_contains_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, (t.erase k).contains a = true → t.contains a = true
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDerivWithin_succ_apply_right : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : ℕ},
  UniqueDiffOn 𝕜 s →
    x ∈ s →
      ∀ (m : Fin (n + 1) → E),
        (iteratedFDerivWithin 𝕜 (n + 1) f s x) m =
          ((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 f s y) s x) (Fin.init m)) (m (Fin.last n))
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.sameCycle_symm_apply_left : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle ((Equiv.symm f) x) y ↔ f.SameCycle x y
-- Init.Data.SInt.Basic
ISize.ofUSize.inj : ∀ {toUSize toUSize_1 : USize}, { toUSize := toUSize } = { toUSize := toUSize_1 } → toUSize = toUSize_1
-- Mathlib.Algebra.Group.Hom.Defs
/-- Group homomorphisms preserve division.  -/
MonoidHom.map_div : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : DivisionMonoid β] (f : α →* β) (g h : α),
  f (g / h) = f g / f h
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_list_prod : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : CommSemiring S] (f : R →+* S) (l : List (Polynomial R))
  (x : S), Polynomial.eval₂ f x l.prod = (List.map (Polynomial.eval₂ f x) l).prod
-- Batteries.Data.DList.Basic
Batteries.DList.instInhabited : {α : Type u} → Inhabited (Batteries.DList α)
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- Positive part of an `AEEqFun`.  -/
MeasureTheory.AEEqFun.posPart : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] →
          [inst_2 : LinearOrder γ] → [OrderClosedTopology γ] → [Zero γ] → (α →ₘ[μ] γ) → α →ₘ[μ] γ
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckGroup.inv_mk : ∀ {M : Type u_1} [inst : CommMonoid M] (m : M) (s : ↥⊤), (Localization.mk m s)⁻¹ = Localization.mk ↑s ⟨m, ⋯⟩
-- Batteries.Data.Array.Scan
Array.scanrM.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → β → m β) (init : β) (as : Array α)
  (start stop : ℕ), Array.scanrM f init as start stop = Array.scanrM.loop f init as (min start as.size) stop ⋯ #[]
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.IterM.fold_mapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {ps : Std.Do.PostShape} [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Monad n] [inst_5 : MonadAttach n]
  [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_8 : Std.Do.WPMonad n ps] [inst_9 : Std.IteratorLoop α m n]
  [Std.LawfulIteratorLoop α m n] [inst_11 : MonadLiftT m n] [LawfulMonadLiftT m n] {f : β → n γ} {g : δ → γ → δ}
  {init : δ} {it : Std.IterM m β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.IterM.foldM
        (fun d b => do
          let c ← f b
          pure (g d c))
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.fold g init (Std.IterM.mapM f it) ⦃Q⦄
-- Mathlib.RingTheory.Finiteness.Basic
/-- [Stacks Tag 0519](https://stacks.math.columbia.edu/tag/0519) ((3)) -/
Module.Finite.of_surjective : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_7}
  {P : Type u_6} [inst_3 : Semiring S] [inst_4 : AddCommMonoid P] [inst_5 : Module S P] {σ : R →+* S}
  [hM : Module.Finite R M] (f : M →ₛₗ[σ] P), Function.Surjective ⇑f → Module.Finite S P
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.basisDivisor.eq_1 : ∀ {F : Type u_1} [inst : Field F] (x y : F),
  Lagrange.basisDivisor x y = Polynomial.C (x - y)⁻¹ * (Polynomial.X - Polynomial.C y)
-- Mathlib.Combinatorics.Matroid.Minor.Order
Matroid.IsStrictMinor.not_isMinor : ∀ {α : Type u_1} {M N : Matroid α}, N <m M → ¬M ≤m N
-- Mathlib.Topology.Algebra.InfiniteSum.Real
Real.tsum_le_of_sum_range_le : ∀ {f : ℕ → ℝ} {c : ℝ}, (∀ (n : ℕ), 0 ≤ f n) → (∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c) → ∑' (n : ℕ), f n ≤ c
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_cos : ∀ {x : ℝ}, 0 ≤ x → x ≤ Real.pi → Real.arccos (Real.cos x) = x
-- Mathlib.Data.Seq.Parallel
Computation.Corec.f.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : α ⊕ β → Sort u_3) (x : α ⊕ β) (h_1 : (a : α) → motive (Sum.inl a))
  (h_2 : (val : β) → motive (Sum.inr val)) (a : α),
  x = Sum.inl a →
    (match x with
      | Sum.inl a => h_1 a
      | Sum.inr val => h_2 val) ≍
      h_1 a
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
instConcreteCategoryProfiniteAddGrpContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite : CategoryTheory.ConcreteCategory ProfiniteAddGrp.{u_1} fun X Y => ↑X.toProfinite.toTop →ₜ+ ↑Y.toProfinite.toTop
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.coe_prodEquivOfIsTopCompl : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} [inst_4 : IsTopologicalAddGroup M] (h : Submodule.IsTopCompl p q),
  ⇑(p.prodEquivOfIsTopCompl q h) = ⇑(p.prodEquivOfIsCompl q ⋯)
-- Mathlib.Algebra.Lie.Semisimple.Defs
/-- In a semisimple Lie algebra, the supremum of the atoms is the whole Lie algebra.  -/
LieAlgebra.IsSemisimple.sSup_atoms_eq_top : ∀ {R : Type u_1} {L : Type u_2} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
  [self : LieAlgebra.IsSemisimple R L], sSup {I | IsAtom I} = ⊤
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.diff_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp}, t₁.diff t₂ = t₁ \ t₂
-- Mathlib.Analysis.Calculus.Deriv.Abs
DifferentiableAt.abs_of_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  DifferentiableAt ℝ f x → 0 < f x → DifferentiableAt ℝ (fun x => |f x|) x
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPushforward_union : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X : C} (S R : CategoryTheory.Sieve X),
  CategoryTheory.Sieve.functorPushforward F (S ⊔ R) =
    CategoryTheory.Sieve.functorPushforward F S ⊔ CategoryTheory.Sieve.functorPushforward F R
-- Mathlib.Data.Set.Prod
Set.univ_pi_eq_singleton_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)} {a : (i : ι) → α i},
  Set.univ.pi t = {a} ↔ ∀ (i : ι), t i = {a i}
-- Mathlib.Topology.NhdsWithin
continuousAt_iff_punctured_nhds : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {a : α},
  ContinuousAt f a ↔ Filter.Tendsto f (nhdsWithin a {a}ᶜ) (nhds (f a))
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_roc_eq_zero_iff : ∀ {m n i : ℕ}, (m<...=n).toList[i]! = 0 ↔ n ≤ i + m
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.sdiff_indep_iff_indep_of_subset_coloops : ∀ {α : Type u_1} {M : Matroid α} {I K : Set α}, K ⊆ M.coloops → (M.Indep (I \ K) ↔ M.Indep I)
-- Mathlib.Combinatorics.Colex
Finset.Colex.instBoundedOrder : {α : Type u_1} → [inst : LinearOrder α] → [Fintype α] → BoundedOrder (Colex (Finset α))
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.ofHom_hom : ∀ {M N : SemiNormedGrp} (f : M ⟶ N), SemiNormedGrp.ofHom (SemiNormedGrp.Hom.hom f) = f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instInhabitedCompletionItem.default : Lean.Lsp.CompletionItem
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.π_comp_H2Iso_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupHomology.π A 2) (groupHomology.H2Iso A).hom =
    CategoryTheory.CategoryStruct.comp (groupHomology.isoCycles₂ A).hom
      (groupHomology.shortComplexH2 A).moduleCatLeftHomologyData.π
-- Std.Time.Format.DateFormat
/-- Narrow quarter names (4 elements, index 0 = 1).
 -/
Std.Time.DateFormatSymbols.quarterNarrow : Std.Time.DateFormatSymbols → Vector String 4
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.rpowIntegrand₀₁_le_rpow_sub_one : ∀ {p t x : ℝ}, p ∈ Set.Ioo 0 1 → 0 ≤ t → 0 ≤ x → p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_union_of_not_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (∀ a ∈ t₁, a ∉ t₂) → (t₁ ∪ t₂).size = t₁.size + t₂.size
-- Mathlib.LinearAlgebra.Dimension.Finite
Module.finite_of_rank_eq_nat : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  {n : ℕ}, Module.rank R M = ↑n → Module.Finite R M
-- Lean.Setup
Lean.instBEqImport.beq : Lean.Import → Lean.Import → Bool
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
Finset.smul_inv_mul_opSMul_eq_mul_of_doubling_lt_three_halves : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G} {a : G},
  ↑(A * A).card < 3 / 2 * ↑A.card → a ∈ A → a • MulOpposite.op a • (A⁻¹ * A) = A * A
-- Mathlib.Analysis.Calculus.LocalExtr.Rolle
/-- **Rolle's Theorem**, a version for a function on an open interval: if `f` has the same limit
`l` at `𝓝[>] a` and `𝓝[<] b`, then `deriv f c = 0` for some `c ∈ (a, b)`. This version
does not require differentiability of `f` because we define `deriv f c = 0` whenever `f` is not
differentiable at `c`.  -/
exists_deriv_eq_zero' : ∀ {f : ℝ → ℝ} {a b l : ℝ},
  a < b →
    Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds l) →
      Filter.Tendsto f (nhdsWithin b (Set.Iio b)) (nhds l) → ∃ c ∈ Set.Ioo a b, deriv f c = 0
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- Given `E : Functor.RightExtension L F`, this is the property of objects where
`E` is a pointwise right Kan extension.  -/
CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionAt : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} → L.RightExtension F → CategoryTheory.ObjectProperty D
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isNone_minKey?_eq_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.minKey?.isNone = t.isEmpty
-- Mathlib.Analysis.Normed.Module.FiniteDimension
Module.Basis.opNNNorm_le : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : CompleteSpace 𝕜] {ι : Type u_1} [inst_6 : Fintype ι] (v : Module.Basis ι 𝕜 E) {u : E →L[𝕜] F} (M : NNReal),
  (∀ (i : ι), ‖u (v i)‖₊ ≤ M) → ‖u‖₊ ≤ Fintype.card ι • ‖↑v.equivFunL‖₊ * M
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.instMkEvalBicategoryM : Mathlib.Tactic.BicategoryLike.MkEval Mathlib.Tactic.Bicategory.BicategoryM
-- Std.Async.Timer
_private.Std.Async.Timer.0.Std.Async.Interval.ofNative : Std.Internal.UV.Timer → Std.Async.Interval
-- Batteries.Recycling.RBTree.Basic
/-- Returns true if `t₁` and `t₂` are equal as sets (assuming `cmp` and `==` are compatible),
ignoring the internal tree structure.
 -/
RBTree.RBSet.instBEq : {α : Type u_1} → {cmp : α → α → Ordering} → [BEq α] → BEq (RBTree.RBSet α cmp)
-- Mathlib.Algebra.Module.Submodule.LinearMap
SMulMemClass.coe_subtype : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_1}
  [inst_3 : SetLike A M] [inst_4 : AddSubmonoidClass A M] [inst_5 : SMulMemClass A R M] (S' : A),
  ⇑(SMulMemClass.subtype S') = Subtype.val
-- Std.Data.DTreeMap.Internal.Operations
/-- The tree has size at most `ub`.  -/
Std.DTreeMap.Internal.Impl.SizedBalancedTree.size_impl_le_ub : ∀ {α : Type u} {β : α → Type v} {lb ub : ℕ} (self : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β lb ub),
  self.impl.size ≤ ub
-- Mathlib.Analysis.Calculus.Deriv.Basic
fderivWithin_derivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}, (fderivWithin 𝕜 f s x) 1 = derivWithin f s x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.contains a = false → t.getKey? a = none
-- Batteries.Data.List.Lemmas
List.disjoint_of_disjoint_append_right_right : ∀ {α : Type u_1} {l l₁ l₂ : List α}, l.Disjoint (l₁ ++ l₂) → l.Disjoint l₂
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RccSliceData.treeMap : {α : Type u} →
  {β : Type v} → [inst : Ord α] → Std.DTreeMap.Internal.Const.RccSliceData α β → Std.DTreeMap.Internal.Impl α fun x => β
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k a : α} [inst_1 : Inhabited (β a)],
  (t.erase k).get! a = if cmp k a = Ordering.eq then default else t.get! a
-- Mathlib.Algebra.Opposites
AddOpposite.instDecidableEq.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α], AddOpposite.instDecidableEq = ⋯.decidableEq
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_1 : HSub Std.Time.Nanosecond.Offset Std.Time.Second.Offset Std.Time.Nanosecond.Offset
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.mono₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, T.mor₁ = 0 → CategoryTheory.Mono T.mor₂
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.congr_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.DTreeMap.Raw α β cmp},
  t₁.Equiv t₂ → (t₁.Equiv t₃ ↔ t₂.Equiv t₃)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.eq_succMany?_of_toArray_eq_append_append : ∀ {α : Type u} {r : Std.Roi α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxi.IsAlwaysFinite α] {pref suff : Array α} {cur : α} (h : r.toArray = pref ++ #[cur] ++ suff),
  cur = (Std.PRange.succMany? (pref.size + 1) r.lower).get ⋯
-- Mathlib.Data.ZMod.Basic
/-- For non-zero `n : ℕ`, the ring `Fin n` is equivalent to `ZMod n`.  -/
ZMod.finEquiv : (n : ℕ) → [NeZero n] → Fin n ≃+* ZMod n
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexInduction
/-- Given `p₀ : ℤ`, this is the condition on two cochains `α` and `β` in `Cochain K L N`
saying that `α.v p q _ = β.v p q _` when `p ≤ p₀`.  -/
CochainComplex.HomComplex.Cochain.EqUpTo : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        {n : ℤ} → CochainComplex.HomComplex.Cochain K L n → CochainComplex.HomComplex.Cochain K L n → ℤ → Prop
-- Lean.Expr
Lean.Nat.mkInstHDiv : Lean.Expr
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.mul.sizeOf_spec : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} [inst_1 : SizeOf J]
  (a a_1 : CommRingCat.Colimits.Prequotient F), sizeOf (a.mul a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_eq_opow_iff : ∀ {o a x : Ordinal.{u}},
  a < Ordinal.veblen o a → (Ordinal.veblen o a = Ordinal.omega0 ^ x ↔ x.invVeblen₁ = o ∧ x.invVeblen₂ = a)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.enumMember.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.enumMember = 1
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.Limit.lift_π_apply' : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F' : CategoryTheory.Functor J (Type v))
  (s : CategoryTheory.Limits.Cone F') (j : J) (x : s.pt),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F' j))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.lift F' s)) x) =
    (CategoryTheory.ConcreteCategory.hom (s.π.app j)) x