mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.InfoTree.Main
Lean.Elab.CommandContextInfo.save : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadEnv m] →
      [Lean.MonadMCtx m] →
        [Lean.MonadOptions m] →
          [Lean.MonadResolveName m] →
            [Lean.MonadNameGenerator m] → [Lean.MonadFileMap m] → m Lean.Elab.CommandContextInfo
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.ext_getKey_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α],
  (∀ (k : α) (hk : k ∈ m₁) (hk' : k ∈ m₂), m₁.getKey k hk = m₂.getKey k hk') →
    (∀ (k : α), Std.ExtDHashMap.Const.get? m₁ k = Std.ExtDHashMap.Const.get? m₂ k) → m₁ = m₂
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then
`seminormFromBounded' f` is nonnegative.  -/
seminormFromBounded_nonneg : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
  0 ≤ f → (∀ (x y : R), f (x * y) ≤ c * f x * f y) → 0 ≤ seminormFromBounded' f
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.instFintypePairwise : {ι : Type u_1} → [Fintype ι] → Fintype (CategoryTheory.Pairwise ι)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.intercalateTR.match_1.eq_2 : ∀ {α : Type u_1} (motive : List (List α) → Sort u_2) (x : List α) (h_1 : Unit → motive [])
  (h_2 : (x : List α) → motive [x]) (h_3 : (x : List α) → (xs : List (List α)) → motive (x :: xs)),
  (match [x] with
    | [] => h_1 ()
    | [x] => h_2 x
    | x :: xs => h_3 x xs) =
    h_2 x
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.natCast_lt_top : ∀ {α : Type u} [inst : AddMonoidWithOne α] [inst_1 : LT α] (n : ℕ), ↑n < ⊤
-- Std.Data.DHashMap.Raw
/-- Transforms the hash map into a list of mappings in some order.  -/
Std.DHashMap.Raw.toList : {α : Type u} → {β : α → Type v} → Std.DHashMap.Raw α β → List ((a : α) × β a)
-- Mathlib.SetTheory.ZFC.PSet
PSet.le_def : ∀ (x y : PSet.{u_1}), x ⊆ y ↔ x ⊆ y
-- Mathlib.Data.ZMod.Basic
ZMod.lift_comp_coe : ∀ (n : ℕ) {A : Type u_2} [inst : AddGroup A] (f : { f // f ↑n = 0 }), ⇑((ZMod.lift n) f) ∘ Int.cast = ⇑↑f
-- Aesop.Forward.RuleInfo
Aesop.instInhabitedForwardRuleInfo.default : Aesop.ForwardRuleInfo
-- Mathlib.Order.Filter.Basic
Filter.GenerateSets.below.superset : ∀ {α : Type u} {g : Set (Set α)} {motive : (a : Set α) → Filter.GenerateSets g a → Prop} {s t : Set α}
  (a : Filter.GenerateSets g s) (a_1 : s ⊆ t), Filter.GenerateSets.below a → motive s a → Filter.GenerateSets.below ⋯
-- Mathlib.Data.Finset.Slice
/-- The `r`-th slice of a set family is the subset of its elements which have cardinality `r`.  -/
Finset.«term_#_» : Lean.TrailingParserDescr
-- Mathlib.Tactic.TacticAnalysis.Declarations
_private.Mathlib.Tactic.TacticAnalysis.Declarations.0.Mathlib.TacticAnalysis.TerminalReplacementOutcome.error.injEq : ∀ (stx : Lean.TSyntax `tactic) (msg : Lean.MessageData) (stx_1 : Lean.TSyntax `tactic) (msg_1 : Lean.MessageData),
  (Mathlib.TacticAnalysis.TerminalReplacementOutcome.error✝ stx msg =
      Mathlib.TacticAnalysis.TerminalReplacementOutcome.error✝ stx_1 msg_1) =
    (stx = stx_1 ∧ msg = msg_1)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.FiniteCyclic
Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (A : Rep.{u, u, u} k G) (g : G)
  (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ)
  (a :
    TensorProduct k (↑A) (MonoidAlgebra k G) ⧸
      (Representation.Coinvariants.ker (A.ρ.tprod (Representation.leftRegular k G))).toAddSubgroup),
  (ModuleCat.Hom.hom ((Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso A g hg).hom.f i)) a =
    (QuotientAddGroup.lift (Representation.Coinvariants.ker (A.ρ.tprod (Representation.leftRegular k G))).toAddSubgroup
        (TensorProduct.lift ((Finsupp.linearCombination k fun g => A.ρ g⁻¹) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
            ↑(TensorProduct.comm k (↑A) (MonoidAlgebra k G))).toAddMonoidHom
        ⋯)
      a
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- A partially applied version of `Matrix.col_apply`  -/
Matrix.col_apply' : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) (i : n), A.col i = fun j => A j i
-- Mathlib.RingTheory.Coalgebra.MonoidAlgebra
LaurentPolynomial.instIsCocomm : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] [Coalgebra.IsCocomm R A], Coalgebra.IsCocomm R (LaurentPolynomial A)
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf_map_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  {X Y : CategoryTheory.Endofunctor.Coalgebra G} (f : X ⟶ Y),
  ((CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf adj).map f).f = f.f
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
Std.Tactic.BVDecide.LRAT.Internal.Formula.readyForRupAdd_ofArray : ∀ {α : outParam (Type u)} {β : outParam (Type v)} {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} {σ : Type w}
  {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
  (arr : Array (Option β)),
  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd (Std.Tactic.BVDecide.LRAT.Internal.Formula.ofArray arr)
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.balRight.match_1.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (l : 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),
  (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α), l = RBTree.RBNode.node RBTree.RBColor.black a x b → False) →
    (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α) (y : α) (c : RBTree.RBNode α),
        l = RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c) → False) →
      (match l 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_3 l
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {k a : α} {v : β},
  (m.insert k v).getKey! a = if (k == a) = true then k else m.getKey! a
-- Batteries.Data.MLList.Basic
/-- Apply a function returning a monadic lazy list to each element of a monadic lazy list,
joining the results.  -/
MLList.bind : {m : Type u_1 → Type u_1} → {α β : Type u_1} → [Monad m] → MLList m α → (α → MLList m β) → MLList m β
-- Mathlib.GroupTheory.Index
Subgroup.disjoint_of_coprime_natCard : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, (Nat.card ↥H).Coprime (Nat.card ↥K) → Disjoint H K
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_eq_false_iff_exists_contains_eq_true : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → (t.isEmpty = false ↔ ∃ a, t.contains a = true)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.mk''_mapId : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  [inst_2 : CategoryTheory.Bicategory.Strict B] [inst_3 : CategoryTheory.Bicategory.Strict C]
  (S : CategoryTheory.StrictPseudofunctorPreCore B C) (x : B),
  (CategoryTheory.StrictPseudofunctor.mk'' S).mapId x = CategoryTheory.eqToIso ⋯
-- Aesop.Tree.UnsafeQueue
Aesop.UnsafeQueueEntry.name : Aesop.UnsafeQueueEntry → Aesop.RuleName
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.leftHomologyData_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Limits.HasZeroObject C] (s : S.Splitting),
  s.leftHomologyData.i = S.f
-- Init.Tactics
/-- The command `by?` will print a suggestion for replacing the proof block with a proof term
using `show_term`.
 -/
Lean.Parser.Tactic.by? : Lean.ParserDescr
-- Mathlib.Topology.Instances.PNat
PNat.dist_eq : ∀ (x y : ℕ+), dist x y = |↑↑x - ↑↑y|
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.coe_pow : ∀ {α : Type u_2} {x : NonAssocSemiring α} (f : α →+* α) (n : ℕ), ⇑(f ^ n) = (⇑f)^[n]
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.ker_coeff_eq_max_ideal : ∀ {k : Type u_2} [inst : Field k], RingHom.ker PowerSeries.constantCoeff = IsLocalRing.maximalIdeal (PowerSeries k)
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.curryLeft_apply : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G) (x : Ei 0)
  (m : (i : Fin n) → Ei i.succ), (f.curryLeft x) m = f (Fin.cons x m)
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The proposed colimit cocone is a colimit in `AddMonCat`.  -/
AddMonCat.FilteredColimits.colimitCoconeIsColimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J AddMonCat) →
      [inst_1 : CategoryTheory.IsFiltered J] →
        CategoryTheory.Limits.IsColimit (AddMonCat.FilteredColimits.colimitCocone F)
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.filtrationOfSet_eq_natural : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {β : ι → Type u_3} [inst : (i : ι) → TopologicalSpace (β i)]
  [inst_1 : ∀ (i : ι), TopologicalSpace.MetrizableSpace (β i)] [mβ : (i : ι) → MeasurableSpace (β i)]
  [inst_2 : ∀ (i : ι), BorelSpace (β i)] [inst_3 : Preorder ι] [inst_4 : (i : ι) → MulZeroOneClass (β i)]
  [∀ (i : ι), Nontrivial (β i)] {s : ι → Set Ω} (hsm : ∀ (i : ι), MeasurableSet (s i)),
  MeasureTheory.filtrationOfSet hsm = MeasureTheory.Filtration.natural (fun i => (s i).indicator fun x => 1) ⋯
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.IsComplex.zero' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C n},
  S.IsComplex →
    ∀ (i j k : ℕ) (hij : autoParam (i + 1 = j) CategoryTheory.ComposableArrows.IsComplex.zero'._auto_1)
      (hjk : autoParam (j + 1 = k) CategoryTheory.ComposableArrows.IsComplex.zero'._auto_3)
      (hk : autoParam (k ≤ n) CategoryTheory.ComposableArrows.IsComplex.zero'._auto_5),
      CategoryTheory.CategoryStruct.comp (S.map' i j ⋯ ⋯) (S.map' j k ⋯ hk) = 0
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.isRegular_or_isSingular : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → c.IsRegular ∨ c.IsSingular
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoUniformly.tendstoLocallyUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {p : Filter ι}, TendstoUniformly F f p → TendstoLocallyUniformly F f p
-- Mathlib.Algebra.Group.Finsupp
/-- Note the general `SMul` instance for `Finsupp` doesn't apply as `ℤ` is not distributive
unless `F i`'s addition is commutative.  -/
Finsupp.instIntSMul : {ι : Type u_1} → {G : Type u_6} → [inst : AddGroup G] → SMul ℤ (ι →₀ G)
-- Mathlib.MeasureTheory.Integral.MeanValue
/-- **First mean value theorem for set integrals (a.e. nonnegativity).**
Let `s` be a connected measurable set. If `f` is continuous on `s`, `g` is integrable on `s`,
`f * g` is integrable on `s`, and `g` is nonnegative a.e. on `s` w.r.t. `μ.restrict s`, then
`∃ c ∈ s, (∫ x in s, f x * g x ∂μ) = f c * (∫ x in s, g x ∂μ)`.  -/
exists_eq_const_mul_setIntegral_of_ae_nonneg : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {s : Set α} {f g : α → ℝ}
  {μ : MeasureTheory.Measure α},
  IsConnected s →
    MeasurableSet s →
      ContinuousOn f s →
        MeasureTheory.IntegrableOn g s μ →
          MeasureTheory.IntegrableOn (fun x => f x * g x) s μ →
            (∀ᵐ (x : α) ∂μ.restrict s, 0 ≤ g x) → ∃ c ∈ s, ∫ (x : α) in s, f x * g x ∂μ = f c * ∫ (x : α) in s, g x ∂μ
-- Init.Data.String.Lemmas.Basic
String.Slice.slice.eq_1 : ∀ (s : String.Slice) (newStart newEnd : s.Pos) (h : newStart ≤ newEnd),
  s.slice newStart newEnd h =
    { str := s.str, startInclusive := newStart.str, endExclusive := newEnd.str, startInclusive_le_endExclusive := ⋯ }
-- Mathlib.Order.BooleanAlgebra.Basic
compl_lt_self : ∀ {α : Type u} {x : α} [inst : BooleanAlgebra α] [Nontrivial α], xᶜ < x ↔ x = ⊤
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
/-- The homology functor on the derived category is induced by the homology
functor on the homotopy category of cochain complexes.  -/
DerivedCategory.homologyFunctorFactorsh : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        (n : ℤ) →
          DerivedCategory.Qh.comp (DerivedCategory.homologyFunctor C n) ≅
            HomotopyCategory.homologyFunctor C (ComplexShape.up ℤ) n
-- Init.Data.Repr
Nat.toSuperDigitsAux : ℕ → List Char → List Char
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.mapDomainBialgHom_single : ∀ {R : Type u_1} {M : Type u_8} {N : Type u_9} [inst : CommSemiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N]
  (f : M →+ N) (m : M) (r : R),
  (AddMonoidAlgebra.mapDomainBialgHom R f) (AddMonoidAlgebra.single m r) = AddMonoidAlgebra.single (f m) r
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NFBelow.lt : ∀ {e : ONote} {n : ℕ+} {a : ONote} {b : Ordinal.{0}}, (e.oadd n a).NFBelow b → e.repr < b
-- Mathlib.Topology.Algebra.GroupWithZero
/-- Eta-expanded form of `Continuous.inv₀` -/
Continuous.fun_inv₀ : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : Zero G₀] [inst_1 : Inv G₀] [inst_2 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  {f : α → G₀} [inst_4 : TopologicalSpace α], Continuous f → (∀ (x : α), f x ≠ 0) → Continuous fun i => (f i)⁻¹
-- Mathlib.GroupTheory.Abelianization.Defs
abelianizationCongr_refl : ∀ {G : Type u} [inst : Group G], (MulEquiv.refl G).abelianizationCongr = MulEquiv.refl (Abelianization G)
-- Mathlib.Topology.Inseparable
SeparationQuotient.lift_mk : ∀ {X : Type u_1} {α : Type u_4} [inst : TopologicalSpace X] {f : X → α} (hf : ∀ (x y : X), Inseparable x y → f x = f y)
  (x : X), SeparationQuotient.lift f hf (SeparationQuotient.mk x) = f x
-- Mathlib.Data.Finset.NAry
Finset.biUnion_image_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β},
  (s.biUnion fun a => Finset.image (f a) t) = Finset.image₂ f s t
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_lt_mul_iff_left₀ : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [MulPosStrictMono α]
  [MulPosReflectLT α], 0 < a → (b * a < c * a ↔ b < c)
-- Mathlib.Data.Real.ConjExponents
/-- For `r`, instead of `p`  -/
Real.HolderTriple.inv_ne_zero' : ∀ {p q r : ℝ}, p.HolderTriple q r → r⁻¹ ≠ 0
-- Mathlib.LinearAlgebra.Prod
/-- Taking the product of two maps with the same domain is equivalent to taking the product of
their codomains.

See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.  -/
LinearMap.prodEquiv : {R : Type u} →
  {M : Type v} →
    {M₂ : Type w} →
      {M₃ : Type y} →
        (S : Type u_3) →
          [inst : Semiring R] →
            [inst_1 : Semiring S] →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : AddCommMonoid M₃] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module R M₂] →
                        [inst_7 : Module R M₃] →
                          [inst_8 : Module S M₂] →
                            [inst_9 : Module S M₃] →
                              [inst_10 : SMulCommClass R S M₂] →
                                [inst_11 : SMulCommClass R S M₃] → ((M →ₗ[R] M₂) × (M →ₗ[R] M₃)) ≃ₗ[S] M →ₗ[R] M₂ × M₃
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.mk : {ι : Type u_5} →
  {B : Type u_6} →
    [inst : TopologicalSpace B] →
      {F : Type u_7} →
        [inst_1 : TopologicalSpace F] →
          (baseSet : ι → Set B) →
            (∀ (i : ι), IsOpen (baseSet i)) →
              (indexAt : B → ι) →
                (∀ (x : B), x ∈ baseSet (indexAt x)) →
                  (coordChange : ι → ι → B → F → F) →
                    (∀ (i : ι), ∀ x ∈ baseSet i, ∀ (v : F), coordChange i i x v = v) →
                      (∀ (i j : ι),
                          ContinuousOn (fun p => coordChange i j p.1 p.2) ((baseSet i ∩ baseSet j) ×ˢ Set.univ)) →
                        (∀ (i j k : ι),
                            ∀ x ∈ baseSet i ∩ baseSet j ∩ baseSet k,
                              ∀ (v : F), coordChange j k x (coordChange i j x v) = coordChange i k x v) →
                          FiberBundleCore ι B F
-- Mathlib.Topology.Compactness.SigmaCompact
/-- A topological space is σ-compact iff `univ` is σ-compact.  -/
isSigmaCompact_univ_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsSigmaCompact Set.univ ↔ SigmaCompactSpace X
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.orbitEquivQuotientStabilizer_symm_apply : ∀ (G : Type u) {X : Type v} [inst : Group G] [inst_1 : MulAction G X] (b : X) (g : G),
  ↑((MulAction.orbitEquivQuotientStabilizer G b).symm ↑g) = g • b
-- Mathlib.FieldTheory.RatFunc.Degree
RatFunc.intDegree_neg : ∀ {K : Type u} [inst : Field K] (x : RatFunc K), (-x).intDegree = x.intDegree
-- Mathlib.Analysis.Calculus.Deriv.Inverse
HasDerivWithinAt.tendsto_nhdsWithin_nhdsNE : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {s : Set 𝕜} {x : 𝕜},
  HasDerivWithinAt f f' s x → f' ≠ 0 → Filter.Tendsto f (nhdsWithin x (s \ {x})) (nhdsWithin (f x) {f x}ᶜ)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Γ_map : ∀ {X Y : AlgebraicGeometry.Schemeᵒᵖ} (f : X ⟶ Y),
  AlgebraicGeometry.Scheme.Γ.map f = AlgebraicGeometry.Scheme.Hom.appTop f.unop
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_filter_of_getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {f : α → β → Bool} {k k' : α},
  m.getKey? k = some k' →
    Std.DHashMap.Const.get! (Std.DHashMap.filter f m) k =
      (Option.filter (fun x => f k' x) (Std.DHashMap.Const.get? m k)).get!
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim_ι_ι_hom_assoc : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape K C] (j : J) (k : K) {Z : C}
  (h : CategoryTheory.Limits.colimit (F.comp CategoryTheory.Limits.colim) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.flip.obj k) j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.flip.comp CategoryTheory.Limits.colim) k)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitFlipCompColimIsoColimitCompColim F).hom h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.obj j) k)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.Limits.colim) j) h)
-- Mathlib.Algebra.Lie.Ideal
LieHom.range_toSubmodule : ∀ {R : Type u} {L : Type v} {L' : Type w₂} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieRing L']
  [inst_3 : LieAlgebra R L'] [inst_4 : LieAlgebra R L] (f : L →ₗ⁅R⁆ L'), f.range.toSubmodule = (↑f).range
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Reinterpret an ordered additive monoid isomorphism as an order isomorphism.  -/
OrderAddMonoidIso.toOrderIso : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] → [inst_1 : Preorder β] → [inst_2 : Add α] → [inst_3 : Add β] → (α ≃+o β) → α ≃o β
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instModuleHom : {S : Type u_1} → [inst : CommRing S] → [inst_1 : TopologicalSpace S] → {X Y : TopModuleCat S} → Module S (X ⟶ Y)
-- Mathlib.RepresentationTheory.Tannaka
TannakaDuality.FiniteGroup.forget_map : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (X Y : FDRep k G) (f : X ⟶ Y),
  (TannakaDuality.FiniteGroup.forget k G).map f = f.hom
-- Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving
MeasureTheory.AEDisjoint.preimage : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {f : α → β} {s t : Set β},
  MeasureTheory.AEDisjoint ν s t →
    MeasureTheory.Measure.QuasiMeasurePreserving f μ ν → MeasureTheory.AEDisjoint μ (f ⁻¹' s) (f ⁻¹' t)
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.natCast_mul_left_comm : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a : α) (b : ℕ) (c : α), a * (↑b * c) = ↑b * (a * c)
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.overMapPullbackCongr_hom_app_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {X Y : C} {f g : X ⟶ Y} (h : f = g)
  (M : CategoryTheory.Sheaf (J.over Y) A) (X_1 : (CategoryTheory.Over X)ᵒᵖ),
  ((J.overMapPullbackCongr A h).hom.app M).hom.app X_1 =
    M.obj.map ((CategoryTheory.Over.mapCongr f g h).inv.app (Opposite.unop X_1)).op
-- Mathlib.Algebra.Order.UpperLower
UpperSet.commSemigroup : {α : Type u_1} → [inst : CommGroup α] → [inst_1 : Preorder α] → [IsOrderedMonoid α] → CommSemigroup (UpperSet α)
-- Mathlib.Data.Set.Image
Set.Nonempty.image_const : ∀ {α : Type u_1} {β : Type u_2} {s : Set α}, s.Nonempty → ∀ (a : β), (fun x => a) '' s = {a}
-- Mathlib.Topology.Category.Stonean.Basic
CompHaus.lift.congr_simp : ∀ {X Y : CompHaus} {Z : Stonean} (e e_1 : Z.compHaus ⟶ Y),
  e = e_1 → ∀ (f f_1 : X ⟶ Y) (e_f : f = f_1) [inst : CategoryTheory.Epi f], CompHaus.lift e f = CompHaus.lift e_1 f_1
-- Batteries.Data.List.Lemmas
List.isPrefixOf?.eq_1 : ∀ {α : Type u} [inst : BEq α] (x : List α), [].isPrefixOf? x = some x
-- Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory
CategoryTheory.MorphismProperty.instComonObjWideSubcategoryOfIsStableUnderComonoidObj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (P : CategoryTheory.MorphismProperty C) →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : P.IsMonoidalStable] →
          (c : CategoryTheory.WideSubcategory P) →
            [inst_3 : CategoryTheory.ComonObj c.obj] → [P.IsStableUnderComonoid c.obj] → CategoryTheory.ComonObj c
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.instReprMatchEqns : Repr Lean.Meta.Match.MatchEqns
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda_mapId_inv_as_app_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a : B) (a_1 : Bᵒᵖ) (X : Opposite.unop a_1 ⟶ a),
  ((CategoryTheory.Bicategory.yoneda.mapId a).inv.as.app a_1).toNatTrans.app X =
    (CategoryTheory.Bicategory.rightUnitor X).inv
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_diff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α},
  (m₁ \ m₂).getKeyD k fallback = if k ∈ m₂ then fallback else m₁.getKeyD k fallback