mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
CuspForm.divByDiscriminant_slash_eq : ∀ {k : ℤ} (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) (γ : Matrix.SpecialLinearGroup (Fin 2) ℤ),
  (SlashAction.map (k - 12) γ fun z => f z / ModularForm.discriminant z) = fun z => f z / ModularForm.discriminant z
-- Mathlib.CategoryTheory.Quotient
/-- The condition that a `HomRel` is stable under precomposition.  -/
CategoryTheory.HomRel.IsStableUnderPrecomp : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → HomRel C → Prop
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- **Alias** of `CategoryTheory.Presieve.isSheafFor_top`.

---

Every presheaf is a sheaf for the maximal sieve.

[Elephant] C2.1.5(ii)
 -/
CategoryTheory.Presieve.isSheafFor_top_sieve : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type w)),
  CategoryTheory.Presieve.IsSheafFor P ⊤
-- Mathlib.Data.ENNReal.Inv
_private.Mathlib.Data.ENNReal.Inv.0.ENNReal.exists_lt_mul_right : ∀ {a b c : ENNReal}, c < a * b → ∃ b' < b, c < a * b'
-- Aesop.RuleTac.Basic
/-- A subgoal produced by a rule.  -/
Aesop.Subgoal : Type
-- Mathlib.Geometry.Convex.Cone.TensorProduct
/-- Characterization of the maximal tensor product: `z` lies in `maxTensorProduct C₁ C₂` iff
all pairings with elementary dual tensors are nonnegative.  -/
PointedCone.mem_maxTensorProduct : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {G : Type u_2}
  [inst_3 : AddCommGroup G] [inst_4 : Module R G] {H : Type u_3} [inst_5 : AddCommGroup H] [inst_6 : Module R H]
  {C₁ : PointedCone R G} {C₂ : PointedCone R H} {z : TensorProduct R G H},
  z ∈ C₁.maxTensorProduct C₂ ↔
    ∀ φ ∈ PointedCone.dual (Module.Dual.eval R G) ↑C₁,
      ∀ ψ ∈ PointedCone.dual (Module.Dual.eval R H) ↑C₂, 0 ≤ ((TensorProduct.dualDistrib R G H) (φ ⊗ₜ[R] ψ)) z
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.ι₁_snd : ∀ (X : TopCat),
  CategoryTheory.CategoryStruct.comp TopCat.ι₁ (CategoryTheory.SemiCartesianMonoidalCategory.snd X TopCat.I) =
    TopCat.const 1
-- Mathlib.RingTheory.Ideal.Operations
/-- See also `Ideal.IsPrime.mem_pow_mul` for prime ideal in Dedekind domain.  -/
Ideal.IsMaximal.mem_pow_mul : ∀ {R : Type u_2} [inst : CommSemiring R] (I : Ideal R) [I.IsMaximal] {a b : R} {n : ℕ},
  a * b ∈ I ^ n → a ∈ I ^ n ∨ b ∈ I
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.UsedSimps.map : Lean.Meta.Simp.UsedSimps → Lean.PHashMap Lean.Meta.Origin ℕ
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.Hom.hom_f_zero_comp_π_f_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} {P : CategoryTheory.ProjectiveResolution Z} {Z' : C}
  {P' : CategoryTheory.ProjectiveResolution Z'} {f : Z ⟶ Z'} (self : P.Hom P' f),
  CategoryTheory.CategoryStruct.comp (self.hom.f 0) (P'.π.f 0) =
    CategoryTheory.CategoryStruct.comp (P.π.f 0) (((ChainComplex.single₀ C).map f).f 0)
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.TheoremLike.getOrigin : {α : Type} → [self : Lean.Meta.Grind.TheoremLike α] → α → Lean.Meta.Grind.Origin
-- Mathlib.Data.Num.Basic
/-- The number of bits required to represent a `Num`, as a `Num`. `size 0` is defined to be `0`.  -/
Num.size : Num → Num
-- Init.GetElem
List.getElem_cons_drop_succ_eq_drop : ∀ {α : Type u_1} {as : List α} {i : ℕ} (h : i < as.length), as[i] :: List.drop (i + 1) as = List.drop i as
-- Mathlib.Topology.Algebra.Group.Pointwise
IsClosed.add_right_of_isCompact : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {s t : Set G},
  IsClosed t → IsCompact s → IsClosed (t + s)
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonInsideType : Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.MaxProducts.eq_1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
  Profinite.NobelingProof.GoodProducts.MaxProducts C ho =
    {l | Profinite.NobelingProof.Products.isGood C l ∧ Profinite.NobelingProof.term I ho ∈ ↑l}
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.panicWithPosWithDecl_eq : ∀ {α : Type u} [inst : Inhabited α] {modName declName : String} {line col : ℕ} {msg : String},
  panicWithPosWithDecl modName declName line col msg = default
-- Mathlib.Order.Nucleus
Nucleus.coe_le_coe : ∀ {X : Type u_1} [inst : SemilatticeInf X] {n m : Nucleus X}, ⇑m ≤ ⇑n ↔ m ≤ n
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.Measure.trim.eq_1 : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (hm : m ≤ m0), μ.trim hm = μ.toMeasure ⋯
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.IsReduced.eq : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B},
  cs.IsReduced ω → cs.length (cs.wordProd ω) = ω.length
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.ιCompMap_inv_app_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C CategoryTheory.Cat}
  (α : F ⟶ F') (c : C) (X : ↑(F.obj c)),
  ((CategoryTheory.Grothendieck.ιCompMap α c).inv.app X).base = CategoryTheory.CategoryStruct.id c
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.isometry_id : ∀ {V : Type u_1} [inst : SeminormedAddCommGroup V], Isometry ⇑(NormedAddGroupHom.id V)
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderiv_comp_add_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} (a : E), fderiv 𝕜 (fun x => f (x + a)) x = fderiv 𝕜 f (x + a)
-- Lean.Widget.InteractiveCode
Lean.Widget.DiffTag.willDelete : Lean.Widget.DiffTag
-- Mathlib.Order.NonemptyFiniteChains
PartialOrder.NonemptyFiniteChains.mk.inj : ∀ {X : Type u} {inst : PartialOrder X} {finset : Finset X}
  {nonempty : autoParam finset.Nonempty PartialOrder.NonemptyFiniteChains.nonempty._autoParam}
  {comparable : ∀ (a b : ↥finset), a ≤ b ∨ b ≤ a} {finset_1 : Finset X}
  {nonempty_1 : autoParam finset_1.Nonempty PartialOrder.NonemptyFiniteChains.nonempty._autoParam}
  {comparable_1 : ∀ (a b : ↥finset_1), a ≤ b ∨ b ≤ a},
  { finset := finset, nonempty := nonempty, comparable := comparable } =
      { finset := finset_1, nonempty := nonempty_1, comparable := comparable_1 } →
    finset = finset_1
-- Std.Data.TreeSet.Basic
/-- Checks if given key is contained and returns the key if it is, otherwise `none`.
The result in the `some` case is guaranteed to be pointer equal to the key in the map.
 -/
Std.TreeSet.get? : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → α → Option α
-- Std.Data.DTreeMap.Raw.Basic
/-- Removes the mapping for the given key if it exists.  -/
Std.DTreeMap.Raw.erase : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → Std.DTreeMap.Raw α β cmp
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toLinearEquiv : {R : Type u_1} →
  {R₂ : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring R₂] →
        {σ₁₂ : R →+* R₂} →
          {σ₂₁ : R₂ →+* R} →
            [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
              [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                {E : Type u_11} →
                  {E₂ : Type u_12} →
                    [inst_4 : SeminormedAddCommGroup E] →
                      [inst_5 : SeminormedAddCommGroup E₂] →
                        [inst_6 : Module R E] → [inst_7 : Module R₂ E₂] → (E ≃ₛₗᵢ[σ₁₂] E₂) → E ≃ₛₗ[σ₁₂] E₂
-- Lean.ResolveName
_private.Lean.ResolveName.0.Lean.ResolveName.resolvePrivateName : Lean.Environment → Lean.Options → Lean.Name → Option Lean.Name
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.instMulAction : {G : Type u_1} →
  {X : Type u_2} →
    {ιₚ : Type u_3} →
      [inst : Group G] →
        [inst_1 : MulAction G X] → {ps : DiscreteTiling.Protoset G X ιₚ} → MulAction G (DiscreteTiling.PlacedTile ps)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDocumentSymbolAux.toJson : {Self : Type} → [Lean.ToJson Self] → Lean.Lsp.DocumentSymbolAux Self → Lean.Json
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.unit_actionHomRight_assoc : ∀ {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.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {x y : D} (f : x ⟶ y) {Z : D}
  (h :
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) y ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f)
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso x).hom
      (CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso y).inv h))
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.mul_le_edist : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → ∀ (x y : α), (↑K)⁻¹ * edist x y ≤ edist (f x) (f y)
-- Lean.Server.CodeActions.Provider
Lean.CodeAction.FindTacticResult.tacticSeq.injEq : ∀ (preferred : Bool) (insertIdx : ℕ) (a : Lean.Syntax.Stack) (preferred_1 : Bool) (insertIdx_1 : ℕ)
  (a_1 : Lean.Syntax.Stack),
  (Lean.CodeAction.FindTacticResult.tacticSeq preferred insertIdx a =
      Lean.CodeAction.FindTacticResult.tacticSeq preferred_1 insertIdx_1 a_1) =
    (preferred = preferred_1 ∧ insertIdx = insertIdx_1 ∧ a = a_1)
-- Mathlib.Algebra.Group.Pi.Basic
Pi.involutiveInv.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → InvolutiveInv (f i)],
  Pi.involutiveInv = { toInv := Pi.instInv, inv_inv := ⋯ }
-- Lean.Message
Lean.MessageData.group.sizeOf_spec : ∀ (a : Lean.MessageData), sizeOf a.group = 1 + sizeOf a
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Ring homomorphisms preserve multiplication.  -/
RingHom.map_mul : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (a b : α),
  f (a * b) = f a * f b
-- Mathlib.Data.Multiset.Basic
Multiset.strongDownwardInduction_eq : ∀ {α : Type u_1} {p : Multiset α → Sort u_3} {n : ℕ}
  (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁) (s : Multiset α),
  Multiset.strongDownwardInduction H s = H s fun {t₂} ht _hst => Multiset.strongDownwardInduction H t₂ ht
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
NonUnitalStarSubsemiring.coe_ofClass : ∀ {S : Type u_1} {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst_1 : StarRing R] [inst_2 : SetLike S R]
  [inst_3 : NonUnitalSubsemiringClass S R] [inst_4 : StarMemClass S R] (s : S),
  ↑(NonUnitalStarSubsemiring.ofClass s) = ↑s
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.edgeFinset_inf : ∀ {V : Type u_1} {G₁ G₂ : SimpleGraph V} [inst : Fintype ↑G₁.edgeSet] [inst_1 : Fintype ↑G₂.edgeSet]
  [inst_2 : Fintype ↑(G₁ ⊓ G₂).edgeSet] [inst_3 : DecidableEq V], (G₁ ⊓ G₂).edgeFinset = G₁.edgeFinset ∩ G₂.edgeFinset
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NF.out : ∀ {o : ONote} [self : o.NF], Exists o.NFBelow
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Cache.mk.injEq : ∀ (ngen : Lean.NameGenerator) (core : Lean.Core.Cache) («meta» : Lean.Meta.Cache) (ngen_1 : Lean.NameGenerator)
  (core_1 : Lean.Core.Cache) (meta_1 : Lean.Meta.Cache),
  ({ ngen := ngen, core := core, «meta» := «meta» } = { ngen := ngen_1, core := core_1, «meta» := meta_1 }) =
    (ngen = ngen_1 ∧ core = core_1 ∧ «meta» = meta_1)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_inv_hom_id'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ⟶ W) [inst_2 : CategoryTheory.IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) {Z_1 : C}
  (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj Z W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.inv f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom h f) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.CategoryStruct.id W))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom h (CategoryTheory.CategoryStruct.id W)) h_1)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey!_eq_maxKeyD_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t.maxKey! = t.maxKeyD default
-- Mathlib.SetTheory.Cardinal.ENat
/-- The coercion `Cardinal.ofENat` and the projection `Cardinal.toENat`
form a Galois coinsertion.  -/
Cardinal.gciENat : GaloisCoinsertion Cardinal.ofENat ⇑Cardinal.toENat
-- Aesop.Util.Basic
/-- If the input expression `e` reduces to `f x₁ ... xₙ` via repeated `whnf`, this
function returns `f` and `[x₁, ⋯, xₙ]`. Otherwise it returns `e` (unchanged, not
in WHNF!) and `[]`.
 -/
Aesop.getAppUpToDefeq : Lean.Expr → Lean.MetaM (Lean.Expr × Array Lean.Expr)
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.measure_union₀_aux : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s μ →
    MeasureTheory.NullMeasurableSet t μ → MeasureTheory.AEDisjoint μ s t → μ (s ∪ t) = μ s + μ t
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.instIsRegularPairing : ∀ {m : ℕ} (k : Fin (m + 2)) (n : ℕ), (SSet.prodStdSimplex.pairing k n).IsRegular
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.normalizationPullback_snd_assoc : ∀ {X S Y : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationPullback f g)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Scheme.Hom.fromNormalization f) g) h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.fromNormalization (CategoryTheory.Limits.pullback.snd f g)) h
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.isEmpty_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.intCast_def : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] [inst_1 : AddZeroClass M] (z : ℤ), ↑z = AddMonoidAlgebra.single 0 ↑z
-- Mathlib.Logic.Equiv.Set
Equiv.Set.rangeInr_symm_apply_coe : ∀ (α : Type u_3) (β : Type u_4) (x : β), ↑((Equiv.Set.rangeInr α β).symm x) = Sum.inr x
-- Lean.Elab.Term.TermElabM
/-- If `checkDeprecated := true`, then `Linter.checkDeprecated` when creating constants.
 -/
Lean.Elab.Term.Context.checkDeprecated : Lean.Elab.Term.Context → Bool
-- Mathlib.Topology.Order.MonotoneConvergence
tendsto_atBot_isLUB : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α] [inst_2 : Preorder α]
  [SupConvergenceClass α] {f : ι → α} {a : α},
  Antitone f → IsLUB (Set.range f) a → Filter.Tendsto f Filter.atBot (nhds a)
-- Mathlib.Combinatorics.Digraph.Orientation
Digraph.toSimpleGraphInclusive_bot : ∀ {V : Type u_1}, ⊥.toSimpleGraphInclusive = ⊥
-- Aesop.EMap
Aesop.EMap.alterM : {m : Type → Type u_1} →
  [Monad m] →
    [MonadLiftT Lean.MetaM m] →
      {α β : Type} → Lean.Expr → (α → m (Option α × β)) → Aesop.EMap α → m (Aesop.EMap α × Option β)
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.nil_comp : ∀ {V : Type u} [inst : Quiver V] {a b : V} (p : Quiver.Path a b), Quiver.Path.nil.comp p = p
-- Mathlib.Topology.Algebra.InfiniteSum.Module
QuotientGroup.automorphize.eq_1 : ∀ {M : Type u_11} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M] {G : Type u_13} [inst_2 : Group G]
  {Γ : Subgroup G} (f : G → M), QuotientGroup.automorphize f = MulAction.automorphize f
-- Mathlib.Algebra.Category.Grp.Zero
CommGrpCat.isZero_iff_subsingleton : ∀ {G : CommGrpCat}, CategoryTheory.Limits.IsZero G ↔ Subsingleton ↑G
-- Mathlib.Data.PNat.Prime
PNat.Coprime.mul : ∀ {k m n : ℕ+}, m.Coprime k → n.Coprime k → (m * n).Coprime k
-- Std.Do.SPred.Laws
Std.Do.SPred.entails.refl : ∀ {σs : List (Type u)} (P : Std.Do.SPred σs), P ⊢ₛ P
-- Mathlib.Data.Num.ZNum
ZNum.dvd_to_int : ∀ (m n : ZNum), ↑m ∣ ↑n ↔ m ∣ n
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.balRight.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α) (y : α)
  (c : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a x b))
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c)))
  (h_3 : (l : RBTree.RBNode α) → motive l),
  (match RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c) with
    | RBTree.RBNode.node RBTree.RBColor.black a x b => h_1 a x b
    | RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c) => h_2 a x b y c
    | l => h_3 l) =
    h_2 a x b y c
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.mk.injEq : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] {x y : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (fst : x.fst ⟶ y.fst) (snd : x.snd ⟶ y.snd)
  (w :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight fst F) y.iso.hom =
        CategoryTheory.CategoryStruct.comp x.iso.hom (CategoryTheory.Functor.whiskerRight snd G))
      CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.w._autoParam)
  (fst_1 : x.fst ⟶ y.fst) (snd_1 : x.snd ⟶ y.snd)
  (w_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight fst_1 F) y.iso.hom =
        CategoryTheory.CategoryStruct.comp x.iso.hom (CategoryTheory.Functor.whiskerRight snd_1 G))
      CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.Hom.w._autoParam),
  ({ fst := fst, snd := snd, w := w } = { fst := fst_1, snd := snd_1, w := w_1 }) = (fst = fst_1 ∧ snd = snd_1)
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.totalShift₁Iso_hom_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)} (f : K ⟶ L) (x : ℤ)
  [inst_2 : K.HasTotal (ComplexShape.up ℤ)] [inst_3 : L.HasTotal (ComplexShape.up ℤ)],
  CategoryTheory.CategoryStruct.comp
      (HomologicalComplex₂.total.map ((HomologicalComplex₂.shiftFunctor₁ C x).map f) (ComplexShape.up ℤ))
      (L.totalShift₁Iso x).hom =
    CategoryTheory.CategoryStruct.comp (K.totalShift₁Iso x).hom
      ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) x).map
        (HomologicalComplex₂.total.map f (ComplexShape.up ℤ)))
-- Mathlib.Analysis.CStarAlgebra.Matrix
/-- The normed ring structure on `Matrix n n 𝕜` arising from the operator norm given by the
identification with (continuous) linear endomorphisms of `EuclideanSpace 𝕜 n`.  -/
Matrix.instL2OpNormedRing : {𝕜 : Type u_1} → {n : Type u_3} → [RCLike 𝕜] → [Fintype n] → [DecidableEq n] → NormedRing (Matrix n n 𝕜)
-- Mathlib.Analysis.Calculus.Deriv.Inv
HasDerivWithinAt.fun_div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1}
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'} {c' d' : 𝕜'},
  HasDerivWithinAt c c' s x →
    HasDerivWithinAt d d' s x → d x ≠ 0 → HasDerivWithinAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) s x
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.liftCycles_i_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) {i : ι} [inst_2 : K.HasHomology i] {A : C}
  (k : A ⟶ K.X i) (j : ι) (hj : c.next i = j) (hk : CategoryTheory.CategoryStruct.comp k (K.d i j) = 0) {Z : C}
  (h : K.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.liftCycles k j hj hk) (CategoryTheory.CategoryStruct.comp (K.iCycles i) h) =
    CategoryTheory.CategoryStruct.comp k h
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
range_cfcₙ_subset : ∀ (𝕜 : Type u_1) {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A]
  [inst_3 : Module 𝕜 A] [inst_4 : IsScalarTower 𝕜 A A] [inst_5 : SMulCommClass 𝕜 A A] [inst_6 : TopologicalSpace A]
  [inst_7 : ContinuousConstSMul 𝕜 A] [inst_8 : StarModule 𝕜 A] [inst_9 : IsTopologicalRing A]
  [inst_10 : ContinuousStar A] [inst_11 : NonUnitalContinuousFunctionalCalculus 𝕜 A p] {a : A},
  p a → (Set.range fun x => cfcₙ x a) ⊆ ↑(NonUnitalStarAlgebra.elemental 𝕜 a)
-- Mathlib.LinearAlgebra.Determinant
LinearMap.equivOfIsUnitDet.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] {f f_1 : M →ₗ[R] M} (e_f : f = f_1)
  (h : IsUnit (LinearMap.det f)), LinearMap.equivOfIsUnitDet h = LinearMap.equivOfIsUnitDet ⋯
-- Lean.Meta.Basic
Lean.Meta.instInhabitedConfig.default : Lean.Meta.Config
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.module' : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    {R : Type u_2} →
      [inst_1 : Semiring R] →
        [inst_2 : TopologicalSpace R] →
          {M : Type u_3} →
            [inst_3 : TopologicalSpace M] →
              [inst_4 : AddCommMonoid M] →
                [inst_5 : Module R M] →
                  [ContinuousSMul R M] →
                    [inst_7 : IsTopologicalSemiring R] → [inst_8 : ContinuousAdd M] → Module C(α, R) C(α, M)
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A normed commutative ring is a non-unital normed commutative ring.  -/
NormedCommRing.toNonUnitalNormedCommRing : {α : Type u_2} → [β : NormedCommRing α] → NonUnitalNormedCommRing α
-- Mathlib.Data.Sym.Sym2
Sym2.range_diag : ∀ {α : Type u_1}, Set.range Sym2.diag = Sym2.diagSet
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- The angle between a nonzero vector and its negation is `π`.  -/
Orientation.oangle_neg_self_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x : V}, x ≠ 0 → o.oangle x (-x) = ↑Real.pi
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.pairing_reflectionPerm_self_right : ∀ {ι : 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) (i j : ι),
  P.pairing i ((P.reflectionPerm j) j) = -P.pairing i j