mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.minEntryD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {fallback : α × β}, t₁.Equiv t₂ → t₁.minEntryD fallback = t₂.minEntryD fallback
-- Lean.Meta.Tactic.Grind.EMatch
/-- After processing a (multi-)pattern, use the choice assignment to instantiate the proof.
Missing parameters are synthesized using type inference and type class synthesis."
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.instantiateTheorem : Lean.Meta.Grind.EMatch.Choice → Lean.Meta.Grind.EMatch.M Unit
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_X_left : ∀ {R : Type u} [inst : CommSemiring R], Polynomial.aeval Polynomial.X = AlgHom.id R (Polynomial R)
-- Lean.Widget.Commands
Lean.Widget.elabWidgetCmd : Lean.Elab.Command.CommandElab
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.left_distrib : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {a b c : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel R X (a * (b + c)) (a * b + a * c)
-- Mathlib.Computability.Partrec
Computable.pair : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable γ]
  {f : α → β} {g : α → γ}, Computable f → Computable g → Computable fun a => (f a, g a)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Lax functoriality.  -/
CategoryTheory.Lax.StrongTrans.naturality_comp_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (self : CategoryTheory.Lax.StrongTrans F G) {a b c : B} (f : a ⟶ b) (g : b ⟶ c)
  {Z : F.obj a ⟶ G.obj c}
  (h : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.comp f g)) (self.app c) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapComp f g))
      (CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.comp f g)).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (self.app a) (G.map f) (G.map g)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.naturality f).hom (G.map g))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (self.app b) (G.map g)).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (self.naturality g).hom)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (self.app c)).inv
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (self.app c))
                h)))))
-- Lean.Level
Lean.Level.isMVar : Lean.Level → Bool
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.colimitMonoid.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : CategoryTheory.IsFiltered J],
  MonCat.FilteredColimits.colimitMonoid F =
    { mul := Mul.mul, mul_assoc := ⋯, one := One.one, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α], sizeOf Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty = 1
-- Mathlib.Topology.Order.LiminfLimsup
instBoundedLENhdsClassOrderDual : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [BoundedGENhdsClass α], BoundedLENhdsClass αᵒᵈ
-- Mathlib.Topology.Algebra.StarSubalgebra
StarAlgebra.elemental.congr_simp : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : StarRing A] [inst_5 : IsSemitopologicalSemiring A] [inst_6 : ContinuousStar A]
  [inst_7 : Algebra R A] [inst_8 : StarModule R A] (x x_1 : A),
  x = x_1 → StarAlgebra.elemental R x = StarAlgebra.elemental R x_1
-- Mathlib.Tactic.Simps.Basic
/-- elaborate the syntax and run `simpsTac`.  -/
simpsTacFromSyntax : Lean.Name → Lean.Syntax → Lean.AttrM (Array Lean.Name)
-- Mathlib.Algebra.Category.HopfAlgCat.Monoidal
HopfAlgCat.tensorObj_carrier : ∀ (R : Type u) [inst : CommRing R] (X Y : HopfAlgCat R),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).carrier = TensorProduct R X.carrier Y.carrier
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.continuousWithinAt_setToFun_of_dominated : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} {X : Type u_7} [inst_4 : TopologicalSpace X] [FirstCountableTopology X]
  (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) {fs : X → α → E} {x₀ : X} {bound : α → ℝ} {s : Set X},
  (∀ᶠ (x : X) in nhdsWithin x₀ s, MeasureTheory.AEStronglyMeasurable (fs x) μ) →
    (∀ᶠ (x : X) in nhdsWithin x₀ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a) →
      MeasureTheory.Integrable bound μ →
        (∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x => fs x a) s x₀) →
          ContinuousWithinAt (fun x => MeasureTheory.setToFun μ T hT (fs x)) s x₀
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffine.of_isIso : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] [h : AlgebraicGeometry.IsAffine Y],
  AlgebraicGeometry.IsAffine X
-- Mathlib.RingTheory.Binomial
Ring.choose_zero_succ : ∀ (R : Type u_2) [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [NatPowAssoc R] [inst_3 : BinomialRing R] (n : ℕ),
  Ring.choose 0 (n + 1) = 0
-- Mathlib.RingTheory.Algebraic.Integral
instFiniteDimensionalFractionRingOfFinite : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : IsDomain R]
  [inst_4 : IsDomain S] [inst_5 : Module.IsTorsionFree R S] [Module.Finite R S],
  FiniteDimensional (FractionRing R) (FractionRing S)
-- Mathlib.Topology.Algebra.LinearMapCompletion
ContinuousLinearMap.toAddMonoidHom_completion : ∀ {α : Type u_1} {β : Type u_2} {R₁ : Type u_3} {R₂ : Type u_4} [inst : UniformSpace α] [inst_1 : AddCommGroup α]
  [inst_2 : IsUniformAddGroup α] [inst_3 : Semiring R₁] [inst_4 : Module R₁ α]
  [inst_5 : UniformContinuousConstSMul R₁ α] [inst_6 : Semiring R₂] [inst_7 : UniformSpace β] [inst_8 : AddCommGroup β]
  [inst_9 : IsUniformAddGroup β] [inst_10 : Module R₂ β] [inst_11 : UniformContinuousConstSMul R₂ β] {σ : R₁ →+* R₂}
  (f : α →SL[σ] β), (↑f.completion).toAddMonoidHom = (↑f).toAddMonoidHom.completion ⋯
-- Lean.Meta.Sym.InstantiateS
_private.Lean.Meta.Sym.InstantiateS.0.Lean.Meta.Sym.instantiateRevBetaS'.visitChild : Array Lean.Expr → Lean.Expr → ℕ → Lean.Meta.Sym.M✝ Lean.Expr
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- The type of functions `f : ∀ a, β a` such that for all `a` we have `p a (f a)` is measurably
equivalent to the type of functions `∀ a, {b : β a // p a b}`.  -/
MeasurableEquiv.subtypePiEquivPi : {δ' : Type u_5} →
  {π : δ' → Type u_6} →
    [inst : (x : δ') → MeasurableSpace (π x)] →
      {p : (a : δ') → π a → Prop} → { f // ∀ (a : δ'), p a (f a) } ≃ᵐ ((a : δ') → { b // p a b })
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v)),
  (CategoryTheory.CategoryOfElements.costructuredArrowYonedaEquivalence F).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        (CategoryTheory.CategoryOfElements.isoMk
            ((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).obj
              (Opposite.op ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).obj X)))
            (Opposite.unop X)
            (CategoryTheory.Iso.refl
              ((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).obj
                  (Opposite.op ((CategoryTheory.CategoryOfElements.toCostructuredArrow F).obj X))).fst)
            ⋯).op)
      ⋯
-- Init.Data.Nat.Div.Lemmas
Nat.mod_mod_eq_mod_mod_of_dvd : ∀ {a b c : ℕ}, b ∣ c → a % b % c = a % c % b
-- Std.Data.HashSet.RawDecidableEquiv
Std.HashSet.Raw.instDecidableEquiv : {α : Type u} →
  [inst : BEq α] →
    [LawfulBEq α] → [inst_2 : Hashable α] → {m₁ m₂ : Std.HashSet.Raw α} → m₁.WF → m₂.WF → Decidable (m₁.Equiv m₂)
-- Mathlib.Combinatorics.Matroid.Loop
/-- **Alias** of `Matroid.closure_inter_setOfPred_isNonloop_eq`. -/
Matroid.closure_inter_setOf_isNonloop_eq : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M.closure (X ∩ {e | M.IsNonloop e}) = M.closure X
-- Mathlib.Topology.UniformSpace.Closeds
isRefl_hausdorffEntourage : ∀ {α : Type u_1} (U : SetRel α α) [U.IsRefl], (hausdorffEntourage U).IsRefl
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyFunctor_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  {X Y : CategoryTheory.ShortComplex C} (φ : X ⟶ Y),
  (CategoryTheory.ShortComplex.rightHomologyFunctor C).map φ = CategoryTheory.ShortComplex.rightHomologyMap φ
-- Mathlib.RepresentationTheory.Subrepresentation
/-- A subrepresentation of `ofModule M` can be thought of as an `A[G]` submodule of `M`.
 -/
Subrepresentation.asSubmodule' : {A : Type u_1} →
  {G : Type u_2} →
    {M : Type u_4} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Module (MonoidAlgebra A G) M] →
              Subrepresentation (Representation.ofModule M) → Submodule (MonoidAlgebra A G) M
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
MulOpposite.nndist_op : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] (x y : α), nndist (MulOpposite.op x) (MulOpposite.op y) = nndist x y
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.Equivalence.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} [inst_1 : SizeOf B] (hom : a ⟶ b) (inv : b ⟶ a)
  (unit : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp hom inv)
  (counit : CategoryTheory.CategoryStruct.comp inv hom ≅ CategoryTheory.CategoryStruct.id b)
  (left_triangle :
    autoParam
      (CategoryTheory.Bicategory.leftZigzagIso unit counit =
        CategoryTheory.Bicategory.leftUnitor hom ≪≫ (CategoryTheory.Bicategory.rightUnitor hom).symm)
      CategoryTheory.Bicategory.Equivalence.left_triangle._autoParam),
  sizeOf { hom := hom, inv := inv, unit := unit, counit := counit, left_triangle := left_triangle } =
    1 + sizeOf hom + sizeOf inv + sizeOf unit + sizeOf counit + sizeOf left_triangle
-- Mathlib.Analysis.Calculus.FDeriv.Mul
HasFDerivWithinAt.multiset_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {ι : Type u_5} {𝔸' : Type u_7} [inst_3 : NormedCommRing 𝔸']
  [inst_4 : NormedAlgebra 𝕜 𝔸'] {g : ι → E → 𝔸'} {g' : ι → E →L[𝕜] 𝔸'} [inst_5 : DecidableEq ι] {u : Multiset ι}
  {x : E},
  (∀ i ∈ u, HasFDerivWithinAt (fun x => g i x) (g' i) s x) →
    HasFDerivWithinAt (fun x => (Multiset.map (fun x_1 => g x_1 x) u).prod)
      (Multiset.map (fun i => (Multiset.map (fun x_1 => g x_1 x) (u.erase i)).prod • g' i) u).sum s x
-- Mathlib.CategoryTheory.Monoidal.Ring
/-- A morphism of commutative ring objects.  -/
CategoryTheory.CommRingObjCat.Hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.CommRingObjCat C → CategoryTheory.CommRingObjCat C → Type v
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
/-- Forgetting the positivity condition, we may regard a `RootPositiveForm` as an `InvariantForm`.
 -/
RootPairing.RootPositiveForm.toInvariantForm : {ι : Type u_1} →
  {R : Type u_2} →
    {S : Type u_3} →
      {M : Type u_4} →
        {N : Type u_5} →
          [inst : CommRing S] →
            [inst_1 : LinearOrder S] →
              [inst_2 : CommRing R] →
                [inst_3 : Algebra S R] →
                  [inst_4 : AddCommGroup M] →
                    [inst_5 : Module R M] →
                      [inst_6 : AddCommGroup N] →
                        [inst_7 : Module R N] →
                          {P : RootPairing ι R M N} →
                            [inst_8 : P.IsValuedIn S] →
                              RootPairing.RootPositiveForm S P → [FaithfulSMul S R] → P.InvariantForm
-- Std.Data.DHashMap.Internal.AssocList.Basic
_private.Std.Data.DHashMap.Internal.AssocList.Basic.0.Std.DHashMap.Internal.AssocList.filter.go : {α : Type u} →
  {β : α → Type v} →
    ((a : α) → β a → Bool) →
      Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α β
-- Init.Data.Array.Lemmas
Array.getElem?_set_ne : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h : i < xs.size) {v : α} {j : ℕ}, i ≠ j → (xs.set i v h)[j]? = xs[j]?
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- **Alias** of `FunLike.coeMonoidHom`. -/
SlashInvariantForm.coeHom : (F : Type u_1) →
  (α : Type u_2) →
    (β : Type u_3) →
      [inst : FunLike F α β] →
        [inst_1 : MulOne F] → [inst_2 : MulOneClass β] → [IsOneApply F α β] → [IsMulApply F α β] → F →* α → β
-- Init.Data.Iterators.Basic
Std.Iter.IsPlausibleIndirectOutput.trans : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {it' it : Std.Iter β} {out : β},
  it'.IsPlausibleIndirectSuccessorOf it → it'.IsPlausibleIndirectOutput out → it.IsPlausibleIndirectOutput out
-- Mathlib.Topology.Algebra.ConstMulAction
Continuous.const_vadd : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : VAdd M α] [ContinuousConstVAdd M α]
  [inst_3 : TopologicalSpace β] {g : β → α}, Continuous g → ∀ (c : M), Continuous (c +ᵥ g)
-- Std.Do.SPred.SVal
Std.Do.SVal.uncurry.eq_2 : ∀ {α : Type u} (head : Type u) (tail : List (Type u)) (f_2 : Std.Do.SVal (head :: tail) α),
  f_2.uncurry = fun x =>
    match x with
    | (s, t) => (f_2 s).uncurry t
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IsPurelyInseparable.natSepDegree_eq_one : ∀ (F : Type u) {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsPurelyInseparable F E]
  (x : E), (minpoly F x).natSepDegree = 1
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.coe_quotLeftToQuotSupₐ : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I J : Ideal A),
  ⇑(DoubleQuot.quotLeftToQuotSupₐ R I J) = ⇑(DoubleQuot.quotLeftToQuotSup I J)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.comp_map₂ : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictPseudofunctor B C)
  (G : CategoryTheory.StrictPseudofunctor C D) {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  (F.comp G).map₂ η = G.map₂ (F.map₂ η)
-- Mathlib.LinearAlgebra.Matrix.IsDiag
/-- This is the `iff` version of `Matrix.IsDiag.fromBlocks`.  -/
Matrix.isDiag_fromBlocks_iff : ∀ {α : Type u_1} {n : Type u_4} {m : Type u_5} [inst : Zero α] {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α}
  {D : Matrix n n α}, (Matrix.fromBlocks A B C D).IsDiag ↔ A.IsDiag ∧ B = 0 ∧ C = 0 ∧ D.IsDiag
-- Std.Data.HashSet.Lemmas
Std.HashSet.singleton_eq_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {a : α}, {a} = ∅.insert a
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.IntroResult.newHyp.inj : ∀ {fvarId : Lean.FVarId} {goal : Lean.Meta.Grind.Goal} {fvarId_1 : Lean.FVarId} {goal_1 : Lean.Meta.Grind.Goal},
  Lean.Meta.Grind.IntroResult.newHyp✝ fvarId goal = Lean.Meta.Grind.IntroResult.newHyp✝ fvarId_1 goal_1 →
    fvarId = fvarId_1 ∧ goal = goal_1
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.primeFactors_zero : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M],
  UniqueFactorizationMonoid.primeFactors 0 = ∅
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.eraseMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (l : List α), (t₁.eraseMany l).Equiv (t₂.eraseMany l)
-- Init.Data.Array.Lemmas
Array.filter_push_of_neg : ∀ {α : Type u_1} {stop : ℕ} {p : α → Bool} {a : α} {xs : Array α},
  ¬p a = true → stop = xs.size + 1 → Array.filter p (xs.push a) 0 stop = Array.filter p xs
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_bound : ∀ {x : ℝ}, |x| ≤ 1 → |Real.cos x - (1 - x ^ 2 / 2)| ≤ |x| ^ 4 * (5 / 96)
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.instConcreteCategoryMonoidHomCarrier.eq_1 : CommMonCat.instConcreteCategoryMonoidHomCarrier =
  { hom := fun {X Y} => CommMonCat.Hom.hom', ofHom := fun {X Y} => CommMonCat.Hom.mk✝,
    hom_ofHom := @CommMonCat.instConcreteCategoryMonoidHomCarrier._proof_1,
    ofHom_hom := @CommMonCat.instConcreteCategoryMonoidHomCarrier._proof_2,
    id_apply := @CommMonCat.instConcreteCategoryMonoidHomCarrier._proof_3,
    comp_apply := @CommMonCat.instConcreteCategoryMonoidHomCarrier._proof_4 }
-- Mathlib.Topology.Algebra.Valued.NormedValued
Valued.toNormedField.norm_lt_iff : ∀ {L : Type u_1} [inst : Field L] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [val : Valued L Γ₀]
  [hv : Valued.v.RankOne] {x x' : L}, ‖x‖ < ‖x'‖ ↔ Valued.v x < Valued.v x'
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- The unique morphism between classifiers mapping each others characteristic maps  -/
CategoryTheory.Subobject.Classifier.hom : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (𝒞₁ 𝒞₂ : CategoryTheory.Subobject.Classifier C) → 𝒞₁.Ω ⟶ 𝒞₂.Ω
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get?_eq_some_getD : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {a fallback : α}, a ∈ m → m.get? a = some (m.getD a fallback)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.instInhabitedRefinedDiscrTree.default : {α : Type} → Lean.Meta.RefinedDiscrTree α
-- Mathlib.Logic.Equiv.Defs
Equiv.forall_congr_right : ∀ {α : Sort u} {β : Sort v} {q : β → Prop} (e : α ≃ β), (∀ (a : α), q (e a)) ↔ ∀ (b : β), q b
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- **Alias** of `ProperVAdd.isCompact_setOfPred_inter_nonempty`.

---

If `G` acts properly on `X`, then for each pair of compacts `U, V ⊆ X`,
the set of `g` such that `g +ᵥ U` intersects `V` is compact.

See `AddAction.properVAdd_iff_isCompact_setOfPred_inter_nonempty` for the two-way implication
under additional conditions on `G` and `X`.  -/
ProperVAdd.isCompact_setOf_inter_nonempty : ∀ {X : Type u_2} [inst : TopologicalSpace X] {G : Type u_3} [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [inst_3 : TopologicalSpace G] [ProperVAdd G X] {U V : Set X},
  IsCompact U → IsCompact V → IsCompact {g | ((g +ᵥ U) ∩ V).Nonempty}
-- Mathlib.Data.Real.Basic
Real.instNeg : Neg ℝ
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.univ_add_of_zero_mem : ∀ {α : Type u_2} [inst : AddMonoid α] {t : Set α}, 0 ∈ t → Set.univ + t = Set.univ
-- Std.Data.DHashMap.Raw
_private.Std.Data.DHashMap.Raw.0.Std.DHashMap.Raw.insertMany.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ ((a : α) × β a)]
  (m : Std.DHashMap.Raw α β) (l : ρ),
  m.insertMany l = if h : 0 < m.buckets.size then ↑↑(Std.DHashMap.Internal.Raw₀.insertMany ⟨m, h⟩ l) else m
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.instBEqPolyCnstr.beq_spec_1 : ∀ (a : Bool) (a_1 a_2 : Nat.Internal.Linear.Poly) (b : Bool) (b_1 b_2 : Nat.Internal.Linear.Poly),
  ({ eq := a, lhs := a_1, rhs := a_2 } == { eq := b, lhs := b_1, rhs := b_2 }) = (a == b && (a_1 == b_1 && a_2 == b_2))
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.hasSum_int_cosKernel : ∀ (a : ℝ) {t : ℝ},
  0 < t →
    HasSum (fun n => Complex.exp (2 * ↑Real.pi * Complex.I * ↑a * ↑n) * ↑(Real.exp (-Real.pi * ↑n ^ 2 * t)))
      ↑(HurwitzZeta.cosKernel (↑a) t)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
_private.Init.Data.String.Lemmas.Pattern.TakeDrop.Basic.0.String.Slice.Pos.skipWhile.match_1.eq_2 : ∀ {s : String.Slice} (motive : Option s.Pos → Sort u_1) (h_1 : (nextCurr : s.Pos) → motive (some nextCurr))
  (h_2 : Unit → motive none),
  (match none with
    | some nextCurr => h_1 nextCurr
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.nsmul_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddMonoid β]
  [inst_3 : ContinuousAdd β] (f : C(α, β)) (n : ℕ) (x : α), (n • f) x = n • f x
-- Mathlib.Computability.NFA
NFA.mem_evalFrom_iff_exists : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} {s : σ} {S : Set σ} {x : List α},
  s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x
-- Init.Data.Nat.Basic
Nat.mul_add : ∀ (n m k : ℕ), n * (m + k) = n * m + n * k
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Mathlib.Tactic.Monoidal.Context.mk : (level₂ level₁ : Lean.Level) →
  (C : Q(Type level₁)) →
    (instCat : Q(CategoryTheory.Category.{level₂, level₁} «$C»)) →
      Option Q(CategoryTheory.MonoidalCategory «$C») → Mathlib.Tactic.Monoidal.Context
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.mk.inj : ∀ {R : Type u_1} {S : Type u_2} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S} {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  {f : P.toExtension.Cotangent → ↥P.toExtension.ker}
  {hf : ∀ (b : P.toExtension.Cotangent), Algebra.Extension.Cotangent.mk (f b) = b} {g : P.Ring} {hgmem : g - 1 ∈ P.ker}
  {hg : g • P.ker ≤ Ideal.span (Set.range (Subtype.val ∘ f ∘ ⇑b))} {f_1 : P.toExtension.Cotangent → ↥P.toExtension.ker}
  {hf_1 : ∀ (b : P.toExtension.Cotangent), Algebra.Extension.Cotangent.mk (f_1 b) = b} {g_1 : P.Ring}
  {hgmem_1 : g_1 - 1 ∈ P.ker} {hg_1 : g_1 • P.ker ≤ Ideal.span (Set.range (Subtype.val ∘ f_1 ∘ ⇑b))},
  { f := f, hf := hf, g := g, hgmem := hgmem, hg := hg } =
      { f := f_1, hf := hf_1, g := g_1, hgmem := hgmem_1, hg := hg_1 } →
    f = f_1 ∧ g = g_1
-- Mathlib.Analysis.Convex.Side
Affine.Simplex.sOppSide_affineSpan_faceOpposite_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {n : ℕ}
  [inst_6 : NeZero n] (s : Affine.Simplex R P n) {w₁ w₂ : Fin (n + 1) → R},
  ∑ j, w₁ j = 1 →
    ∑ j, w₂ j = 1 →
      ∀ {i : Fin (n + 1)},
        (affineSpan R (Set.range (s.faceOpposite i).points)).SOppSide
            ((Finset.affineCombination R Finset.univ s.points) w₁)
            ((Finset.affineCombination R Finset.univ s.points) w₂) ↔
          SignType.sign (w₁ i) = -SignType.sign (w₂ i) ∧ w₁ i ≠ 0
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.transpose_replicateRow : ∀ {m : Type u_2} {α : Type v} {ι : Type u_6} (v : m → α), (Matrix.replicateRow ι v).transpose = Matrix.replicateCol ι v