mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_single : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : α → M} (c : R) (a : α), ((Finsupp.linearCombination R v) fun₀ | a => c) = c • v a
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.monotone_comap : ∀ {α : Type u_1} {β : Type u_2} {g : β → α}, Monotone (MeasurableSpace.comap g)
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.minEntryD.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → Sort u_3)
  (fallback : α × β) (h_1 : (fallback : α × β) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : α × β) → motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                        (fallback : α × β) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            fallback),
  (match Std.DTreeMap.Internal.Impl.leaf, fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1,
      fallback => h_3 size k v l size_1 k_1 v_1 l_1 r h r_1 fallback) =
    h_1 fallback
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.constMulHom.eq_1 : ∀ (α : Type u_5) (β : Type u_6) [inst : Mul β], Pi.constMulHom α β = { toFun := Function.const α, map_mul' := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.hom_ext_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {f g : S₁ ⟶ S₂}, f = g ↔ f.τ₁ = g.τ₁ ∧ f.τ₂ = g.τ₂ ∧ f.τ₃ = g.τ₃
-- Init.Control.Id
/-- Turn a collection with a pure `ForIn` instance into an array.  -/
ForIn.toArray : {ρ : Type u_1} → {α : Type u} → [inst : ForIn Id ρ α] → ρ → Array α
-- Mathlib.Analysis.RCLike.Basic
RCLike.conj_im_ax : ∀ {K : semiOutParam (Type u_1)} [self : RCLike K] (z : K), RCLike.im ((starRingEnd K) z) = -RCLike.im z
-- Mathlib.Algebra.Category.Grp.EpiMono
CommGrpCat.mono_iff_injective : ∀ {A B : CommGrpCat} (f : A ⟶ B), CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Lean.Language.Basic
Lean.Language.SnapshotTask.mk.inj : ∀ {α : Type} {stx? : Option Lean.Syntax} {reportingRange : Lean.Language.SnapshotTask.ReportingRange}
  {cancelTk? : Option IO.CancelToken} {task : Task α} {stx?_1 : Option Lean.Syntax}
  {reportingRange_1 : Lean.Language.SnapshotTask.ReportingRange} {cancelTk?_1 : Option IO.CancelToken}
  {task_1 : Task α},
  { stx? := stx?, reportingRange := reportingRange, cancelTk? := cancelTk?, task := task } =
      { stx? := stx?_1, reportingRange := reportingRange_1, cancelTk? := cancelTk?_1, task := task_1 } →
    stx? = stx?_1 ∧ reportingRange = reportingRange_1 ∧ cancelTk? = cancelTk?_1 ∧ task = task_1
-- Init.Data.UInt.Lemmas
UInt64.div_zero : ∀ {a : UInt64}, a / 0 = 0
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefIdent.RefIdentJsonRepr.f.sizeOf_spec : ∀ (m i : String), sizeOf (Lean.Lsp.RefIdent.RefIdentJsonRepr.f m i) = 1 + sizeOf m + sizeOf i
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.ext_iff : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] {e e' : P₁ ≃ᵃ[k] P₂}, e = e' ↔ ∀ (x : P₁), e x = e' x
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.functor_map : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Group G] (n : ℕ) {X Y : Rep.{u, u, u} k G} (φ : X ⟶ Y),
  (groupCohomology.functor k G n).map φ = groupCohomology.map (MonoidHom.id G) φ n
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.coeff_rTensorAlgEquiv_tmul : ∀ {R : Type u} {N : Type v} [inst : CommSemiring R] {σ : Type u_1} {S : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : CommSemiring N] [inst_4 : Algebra R N] (s : S) (p : MvPolynomial σ N) (d : σ →₀ ℕ),
  MvPolynomial.coeff d (MvPolynomial.rTensorAlgEquiv (s ⊗ₜ[R] p)) = s ⊗ₜ[R] MvPolynomial.coeff d p
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
GenContFract.IntFractPair.stream.eq_1 : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (v : K),
  GenContFract.IntFractPair.stream v 0 = some (GenContFract.IntFractPair.of v)
-- Mathlib.Topology.Closure
Dense.nonempty : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} [h : Nonempty X], Dense s → s.Nonempty
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : ↑Y.affineOpens),
  (AlgebraicGeometry.Scheme.Hom.ker f).ideal U ≤
    RingHom.ker
      (CommRingCat.Hom.hom
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso (Y.presheaf.obj (Opposite.op ↑U))).inv
          (AlgebraicGeometry.Scheme.Hom.appTop
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (↑U).ι) (↑U).toSpecΓ))))
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- Any linearly ordered archimedean additive group is either isomorphic (and order-isomorphic)
to the integers, or is densely ordered, exclusively.

(See also `LinearOrderedAddCommGroup.isAddCyclic_iff_not_denselyOrdered`.)  -/
LinearOrderedAddCommGroup.discrete_iff_not_denselyOrdered : ∀ (G : Type u_2) [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G],
  Nonempty (G ≃+o ℤ) ↔ ¬DenselyOrdered G
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.any_eq_false_iff_forall_mem_getKey_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [LawfulHashable α]
  [EquivBEq α] {p : α → β → Bool},
  m.any p = false ↔ ∀ (a : α) (h : a ∈ m), p (m.getKey a h) (Std.DHashMap.Const.get m a h) = false
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
/-- All `P_δ` are split monos as composition of such.  -/
SimplexCategoryGenRel.isSplitMono_P_δ : ∀ {x y : SimplexCategoryGenRel} {m : x ⟶ y}, SimplexCategoryGenRel.P_δ m → CategoryTheory.IsSplitMono m
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxKey!_eq_get!_maxKey? : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited α] {l : Std.DTreeMap.Internal.Impl α β}, l.maxKey! = l.maxKey?.get!
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.isEmpty_iff : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLeast? α], r.isEmpty = true ↔ ¬Nonempty α
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLink.symm : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β}, G.IsLink e x y → G.IsLink e y x
-- Init.Data.BitVec.Lemmas
BitVec.zero_concat_false : ∀ {w : ℕ}, (0#w).concat false = 0#(w + 1)
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.out_eq' : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} (a : α ⧸ s), ↑(Quotient.out a) = a
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.eval₂Hom_C_eq_bind₁ : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] (f : σ → MvPolynomial τ R),
  MvPolynomial.eval₂Hom MvPolynomial.C f = ↑(MvPolynomial.bind₁ f)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.equifibered_op_iff : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] {F G : CategoryTheory.Functor J C} {α : F ⟶ G},
  CategoryTheory.NatTrans.Equifibered (CategoryTheory.NatTrans.op α) ↔ CategoryTheory.NatTrans.Coequifibered α
-- Init.Data.Array.Basic
/-- Returns the index of the first element for which `p` returns `true`, or `none` if there is no such
element. The index is returned as a `Fin`, which guarantees that it is in bounds.

Examples:
* `#[7, 6, 5, 8, 1, 2, 6].findFinIdx? (· < 5) = some (4 : Fin 7)`
* `#[7, 6, 5, 8, 1, 2, 6].findFinIdx? (· < 1) = none`
 -/
Array.findFinIdx? : {α : Type u} → (α → Bool) → (as : Array α) → Option (Fin as.size)
-- Lean.Meta.IndPredBelow
Lean.Meta.IndPredBelow.RecursionContext.mk : Lean.FVarIdMap (Lean.Name × Lean.Expr) → Lean.FVarIdMap (ℕ × Lean.Expr) → Lean.Meta.IndPredBelow.RecursionContext
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.ramificationIdx'_algebra_tower' : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra S T] [inst_5 : Algebra R T] [IsScalarTower R S T] [IsDedekindDomain S]
  [IsDedekindDomain T] [IsDomain R] [Module.IsTorsionFree R S] [Module.IsTorsionFree S T] (p : Ideal R) (P : Ideal S)
  (Q : Ideal T) [Q.IsPrime] [Q.LiesOver P] [P.LiesOver p],
  p.ramificationIdx' Q = p.ramificationIdx' P * P.ramificationIdx' Q
-- Init.Data.String.Decode
UInt8.isUTF8FirstByte_getElem_zero_utf8EncodeChar : ∀ {c : Char}, (String.utf8EncodeChar c)[0].IsUTF8FirstByte
-- Mathlib.Topology.Convenient.Category
/-- The full subcategory of `TopCat` consisting of `X`-generated spaces.  -/
GeneratedByTopCat : {ι : Type t} → (X : ι → Type u) → [(i : ι) → TopologicalSpace (X i)] → Type (v + 1)
-- Lean.MetavarContext
/-- The nesting depth of this metavariable. We do not want
unification subproblems to influence the results of parent
problems. The depth keeps track of this information and ensures
that unification subproblems cannot leak information out, by unifying
based on depth.  -/
Lean.LevelMetavarDecl.depth : Lean.LevelMetavarDecl → ℕ
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.coe_mul_eq_bind : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {a : α},
  a ≠ 0 → ∀ (b : WithTop α), ↑a * b = Option.bind b fun b => some (a * b)
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.qExpansion_add : ∀ {h : ℝ} {f g : UpperHalfPlane → ℂ},
  AnalyticAt ℂ (UpperHalfPlane.cuspFunction h f) 0 →
    AnalyticAt ℂ (UpperHalfPlane.cuspFunction h g) 0 →
      UpperHalfPlane.qExpansion h (f + g) = UpperHalfPlane.qExpansion h f + UpperHalfPlane.qExpansion h g
-- Lean.Meta.Tactic.Grind.Main
_private.Lean.Meta.Tactic.Grind.Main.0.Lean.Meta.Grind.processHypotheses.go : Lean.Meta.Grind.Goal → Option ℕ → ExceptT Unit Lean.Meta.Grind.GoalM Unit
-- Mathlib.Data.Nat.Factorial.Basic
Nat.factorial_eq_factorialBinarySplitting : Nat.factorial = Nat.factorialBinarySplitting
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearEquiv.congrRight₂_refl : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N₁ : Type u_9}
  [inst_3 : AddCommMonoid N₁] [inst_4 : Module R N₁],
  (LinearEquiv.refl R N₁).congrRight₂ = LinearEquiv.refl R (LinearMap.BilinMap R M N₁)
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
GenContFract.IntFractPair.b : {K : Type u_1} → GenContFract.IntFractPair K → ℤ
-- Mathlib.Topology.Order.Lattice
/-- Let `L` be a topological space and let `L×L` be equipped with the product topology and let
`⊓:L×L → L` be an infimum. Then `L` is said to have *(jointly) continuous infimum* if the map
`⊓:L×L → L` is continuous.
 -/
ContinuousInf : (L : Type u_1) → [TopologicalSpace L] → [Min L] → Prop
-- Init.SizeOf
Prod.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : SizeOf α] [inst_1 : SizeOf β] (fst : α) (snd : β),
  sizeOf (fst, snd) = 1 + sizeOf fst + sizeOf snd
-- Mathlib.Data.Nat.Init
Nat.leRec.eq_1 : ∀ {n : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯)
  (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) (H : n ≤ 0),
  Nat.leRec refl le_succ_of_le H =
    (fun h =>
        Eq.ndrec (motive := fun {n} =>
          {motive : (m : ℕ) → n ≤ m → Sort u_1} →
            motive n ⋯ → (⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) → (H : n ≤ 0) → motive 0 H)
          (fun {motive} refl le_succ_of_le H => refl) ⋯ refl le_succ_of_le H)
      ⋯
-- Mathlib.CategoryTheory.Sites.CompatibleSheafification
CategoryTheory.GrothendieckTopology.whiskerRight_toSheafify_sheafifyCompIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} 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]
  [inst_7 : ∀ (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]
  (P : CategoryTheory.Functor Cᵒᵖ D),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (J.toSheafify P) F)
      (J.sheafifyCompIso F P).hom =
    J.toSheafify (P.comp F)
-- Lean.DocString.Markdown
/-- Runs a renderer with a fallback.

If the renderer fails or exceeds its heartbeat budget, then the fallback content is rendered
instead.
 -/
Lean.Doc.withRendererFallback : Lean.Doc.MarkdownM (Array String) → Lean.Doc.MarkdownM (Array String) → Lean.Doc.MarkdownM (Array String)
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.IfInput : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type
-- Mathlib.Topology.UniformSpace.Basic
/-- The uniform neighborhoods of all points of a dense indexed collection cover the whole space.  -/
DenseRange.iUnion_uniformity_ball : ∀ {α : Type ua} [inst : UniformSpace α] {ι : Type u_2} {xs : ι → α},
  DenseRange xs → ∀ {U : SetRel α α}, U ∈ uniformity α → ⋃ i, UniformSpace.ball (xs i) U = Set.univ
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.y_spec : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ),
  FermatLastTheoremForThreeGen.Solution'.a✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) +
      ↑⋯.unit * FermatLastTheoremForThreeGen.Solution'.b✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) =
    (hζ.toInteger - 1) * FermatLastTheoremForThreeGen.Solution.y✝ S
-- Mathlib.Computability.Reduce
ManyOneDegree.instSemilatticeSup : SemilatticeSup ManyOneDegree
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isEmpty_insertMany_list : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List ((a : α) × β a)}, (t.insertMany l).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.Combinatorics.Graph.Basic
Graph.isNonloopAt_iff_inc_not_isLoopAt : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β}, G.IsNonloopAt e x ↔ G.Inc e x ∧ ¬G.IsLoopAt e x
-- Lean.Data.Lsp.Workspace
Lean.Lsp.instFromJsonFileEvent : Lean.FromJson Lean.Lsp.FileEvent
-- Mathlib.Algebra.Module.LocalizedModule.Basic
_private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.smul_add_aux : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {T : Type u_1} [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [inst_5 : IsLocalization S T] (x : T)
  (p q : LocalizedModule S M), x • (p + q) = x • p + x • q
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.preimage_map : ∀ {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 Y : C} [inst_2 : F.Full] [F.Faithful] (f : X ⟶ Y), F.preimage (F.map f) = f
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `lt_inv_mul_iff_mul_lt`. -/
lt_inv_mul_of_mul_lt : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a b c : α}, a * b < c → b < a⁻¹ * c
-- Mathlib.Data.Nat.Totient
Nat.totient_mul_of_prime_of_not_dvd : ∀ {p n : ℕ}, Nat.Prime p → ¬p ∣ n → (p * n).totient = (p - 1) * n.totient
-- Mathlib.Algebra.Order.Group.Abs
le_of_mabs_le : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b : G}, |a|ₘ ≤ b → a ≤ b
-- Mathlib.RingTheory.Ideal.Height
Ideal.height_bot : ∀ {R : Type u_1} [inst : CommRing R] [Nontrivial R], ⊥.height = 0
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.separatingRight_iff_forall_mulVec_eq_zero : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Finite m]
  [inst_2 : Fintype n], M.SeparatingRight ↔ ∀ (v : n → R), M.mulVec v = 0 → v = 0
-- Mathlib.Analysis.Seminorm
Seminorm.zero_or_exists_apply_eq_finset_sup : ∀ {𝕜 : Type u_3} {E : Type u_7} {ι : Type u_11} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] (p : ι → Seminorm 𝕜 E) (s : Finset ι) (x : E), (s.sup p) x = 0 ∨ ∃ i ∈ s, (s.sup p) x = (p i) x
-- Lean.Elab.DefView
Lean.Elab.Command.mkDefViewOfAbbrev : Lean.Elab.Modifiers → Lean.Syntax → Lean.Elab.DefView
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
/-- The real embedding associated to a real infinite place.  -/
NumberField.InfinitePlace.embedding_of_isReal : {K : Type u_1} → [inst : Field K] → {w : NumberField.InfinitePlace K} → w.IsReal → K →+* ℝ
-- Mathlib.Analysis.Fourier.AddCircle
/-- **Parseval's identity**: for an `L²` function `f` on `AddCircle T`, the sum of the squared
norms of the Fourier coefficients equals the `L²` norm of `f`.  -/
hasSum_sq_fourierCoeff : ∀ {T : ℝ} [hT : Fact (0 < T)] (f : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)),
  HasSum (fun i => ‖fourierCoeff (↑↑f) i‖ ^ 2) (∫ (t : AddCircle T), ‖↑↑f t‖ ^ 2 ∂AddCircle.haarAddCircle)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.entryAtIdx!_eq_get!_map_getElem? : ∀ {α : Type u} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.Balanced →
    ∀ {i : ℕ} [inst : Inhabited (α × β)],
      Std.DTreeMap.Internal.Impl.Const.entryAtIdx! t i = (Option.map (fun x => (x.fst, x.snd)) t.toListModel[i]?).get!
-- Mathlib.Analysis.Analytic.CPolynomial
HasFiniteFPowerSeriesOnBall.add : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {pf pg : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} {n m : ℕ},
  HasFiniteFPowerSeriesOnBall f pf x n r →
    HasFiniteFPowerSeriesOnBall g pg x m r → HasFiniteFPowerSeriesOnBall (f + g) (pf + pg) x (max n m) r
-- Init.Data.SInt.Lemmas
Int64.toInt32_ofIntClamp : ∀ {n : ℤ}, -2 ^ 63 ≤ n → n < 2 ^ 63 → (Int64.ofIntClamp n).toInt32 = Int32.ofInt n
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- (Pseudo) metric space has discrete `UniformSpace` structure
iff the distances between distinct points are uniformly bounded away from zero.  -/
Metric.uniformSpace_eq_bot : ∀ {α : Type u} [inst : PseudoMetricSpace α],
  PseudoMetricSpace.toUniformSpace = ⊥ ↔ ∃ r, 0 < r ∧ Pairwise fun x1 x2 => r ≤ dist x1 x2
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.checkHeaders.eq_def : ∀ (rs : Array Lean.Elab.Command.PreElabHeaderResult) (numParams i : ℕ) (firstType? : Option Lean.Expr),
  Lean.Elab.Command.checkHeaders✝ rs numParams i firstType? =
    if h : i < rs.size then do
      let type ← Lean.Elab.Command.checkHeaders.checkHeader✝ rs[i] numParams firstType?
      Lean.Elab.Command.checkHeaders✝ rs numParams (i + 1) (some type)
    else pure ()
-- Mathlib.Logic.Equiv.Defs
Equiv.injective : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), Function.Injective ⇑e
-- Lean.Syntax
_private.Lean.Syntax.0.Lean.Syntax.updateInfo : Lean.SourceInfo → String.Pos.Raw → String.Pos.Raw → Lean.SourceInfo
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_comm : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, (fun x => f₁ x - f₂ x) =O[l] g ↔ (fun x => f₂ x - f₁ x) =O[l] g
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.span_orbit_eq_top : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [NeZero 2]
  [P.IsIrreducible] (i : ι), Submodule.span R (MulAction.orbit (↥P.weylGroup) (P.root i)) = ⊤
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_lt : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], y ≤ x → y ≠ ⊥ → x \ y < x
-- Lean.Elab.Command
/-- Like `Core.tryCatchRuntimeEx`; runtime errors are generally used to abort term elaboration, so we do
want to catch and process them at the command level.
 -/
Lean.Elab.Command.tryCatch : {α : Type} →
  Lean.Elab.Command.CommandElabM α →
    (Lean.Exception → Lean.Elab.Command.CommandElabM α) → Lean.Elab.Command.CommandElabM α
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.coe_lt_coe : ∀ {E : Type u_3} [inst : AddGroup E] {p q : AddGroupNorm E}, ⇑p < ⇑q ↔ p < q
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.addValuation.apply : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℚ_[p]}, x ≠ 0 → Padic.addValuation x = ↑x.valuation
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.drewritePost : Lean.Meta.Simp.DSimproc
-- Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
CategoryTheory.ShortComplex.zero_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.HasForget₂ C Ab] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C]
  [(CategoryTheory.forget₂ C Ab).PreservesZeroMorphisms] (S : CategoryTheory.ShortComplex C)
  (x : ↑((CategoryTheory.forget₂ C Ab).obj S.X₁)),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map S.g))
      ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map S.f)) x) =
    0
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- The additive submonoid consisting of the additive units of an additive monoid  -/
IsAddUnit.addSubmonoid : (M : Type u_4) → [inst : AddMonoid M] → AddSubmonoid M
-- Mathlib.Analysis.Complex.TaylorSeries
/-- A function that is complex differentiable on the complex plane is given by evaluating
its Taylor series at any point `c`.  -/
Complex.hasSum_taylorSeries_of_entire : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] ⦃f : ℂ → E⦄,
  Differentiable ℂ f → ∀ (c z : ℂ), HasSum (fun n => (↑n.factorial)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)
-- Batteries.Lean.PersistentHashMap
/-- Merge two `PersistentHashMap`s. The values of keys which appear in both maps are
combined using `f`.
 -/
Lean.PersistentHashMap.mergeWith : {α : Type u_1} →
  [inst : BEq α] →
    [inst_1 : Hashable α] →
      {β : Type u_2} →
        Lean.PersistentHashMap α β → Lean.PersistentHashMap α β → (α → β → β → β) → Lean.PersistentHashMap α β