mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.AsymptoticCone
zero_mem_asymptoticCone : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] [inst_6 : TopologicalSpace k]
  [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set P},
  0 ∈ asymptoticCone k s ↔ s.Nonempty
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.coe_nsmul : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) (n : ℕ), ⇑(n • f) = n • ⇑f
-- Init.Data.List.Perm
List.Perm.contains_eq : ∀ {α : Type u_1} [inst : BEq α] {l₁ l₂ : List α}, l₁.Perm l₂ → ∀ {a : α}, l₁.contains a = l₂.contains a
-- Mathlib.CategoryTheory.Bicategory.End
CategoryTheory.tensorHom_def : ∀ {C : Type u} [inst : CategoryTheory.Bicategory C] (X : C) {X₁ Y₁ X₂ Y₂ : X ⟶ X} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f g =
    CategoryTheory.CategoryStruct.comp ((fun {x x_1} η h => CategoryTheory.Bicategory.whiskerRight η h) f X₂)
      ((fun {f x x_1} η => CategoryTheory.Bicategory.whiskerLeft f η) g)
-- Mathlib.GroupTheory.GroupAction.IterateAct
IterateAddAct.mk.sizeOf_spec : ∀ {α : Type u_1} {f : α → α} [inst : SizeOf α] (val : ℕ), sizeOf { val := val } = 1 + sizeOf val
-- Mathlib.Geometry.Manifold.Algebra.Monoid
/-- **Alias** of `contMDiffAt_finsetProd`. -/
contMDiffAt_finset_prod : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {x : M} {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiffAt I' I n (f i) x) → ContMDiffAt I' I n (fun x => ∏ i ∈ t, f i x) x
-- Lean.Level
Lean.Level.PP.Result.succ : Lean.Level.PP.Result → Lean.Level.PP.Result
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- if `f` is integrable, then `f + g` is integrable iff `g` is.
See `integrable_add_iff_integrable_right'` for the same statement with `fun x ↦ f x + g x` instead
of `f + g`.  -/
MeasureTheory.integrable_add_iff_integrable_right : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {f g : α → β}, MeasureTheory.Integrable f μ → (MeasureTheory.Integrable (f + g) μ ↔ MeasureTheory.Integrable g μ)
-- Mathlib.Condensed.TopCatAdjunction
/-- The counit of the adjunction `condensedSetToCompactlyGenerated ⊣ compactlyGeneratedToCondensedSet`
is an isomorphism.
 -/
CondensedSet.compactlyGeneratedAdjunctionCounitIso : (X : CompactlyGenerated) →
  CondensedSet.condensedSetToCompactlyGenerated.obj (CondensedSet.compactlyGeneratedToCondensedSet.obj X) ≅ X
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Head term  -/
GenContFract.h : {α : Type u_1} → GenContFract α → α
-- Mathlib.GroupTheory.Torsion
CommGroup.freeRank_congr : ∀ {G : Type u_1} {H : Type u_2} [inst : CommGroup G] [inst_1 : CommGroup H] [inst_2 : Group.FG G] [inst_3 : Group.FG H]
  (e : G ≃* H), CommGroup.freeRank G = CommGroup.freeRank H
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.vonNeumann.eq_1 : ∀ (o : Ordinal.{u}), ZFSet.vonNeumann o = ZFSet.iUnion fun a => (ZFSet.vonNeumann ↑a).powerset
-- Mathlib.Algebra.Category.Grp.Preadditive
AddCommGrpCat.instPreadditive : CategoryTheory.Preadditive AddCommGrpCat
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- Composition as a bilinear group homomorphism  -/
CategoryTheory.Preadditive.compHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] → {P Q R : C} → (P ⟶ Q) →+ (Q ⟶ R) →+ (P ⟶ R)
-- Lean.Meta.Sym.Pattern
Lean.Meta.Sym.Pattern : Type
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedTacticInfo : Inhabited Lean.Elab.TacticInfo
-- Mathlib.Topology.MetricSpace.PiNat
Metric.PiNatEmbed.forall : ∀ {ι : Type u_2} {X : Type u_3} {Y : ι → Type u_4} {f : (i : ι) → X → Y i} {P : Metric.PiNatEmbed X Y f → Prop},
  (∀ (x : Metric.PiNatEmbed X Y f), P x) ↔ ∀ (x : X), P { ofPiNat := x }
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.map_lt_map_of_le_of_sup_lt_sup : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] {p p' : Submodule R M} {f : M →ₛₗ[τ₁₂] M₂},
  p ≤ p' → p ⊔ f.ker < p' ⊔ f.ker → Submodule.map f p < Submodule.map f p'
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.linearMap_ext' : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f g : SkewPolynomial R →ₗ[R] M}, (∀ (n : ℕ), f ∘ₗ SkewPolynomial.monomial n = g ∘ₗ SkewPolynomial.monomial n) → f = g
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom.of : {B : Type u} → [inst : Quiver B] → {a b : B} → (a ⟶ b) → CategoryTheory.FreeBicategory.Hom a b
-- Init.Grind.Ring.Basic
Lean.Grind.no_int_zero_divisors : ∀ {α : Type u} [inst : Lean.Grind.IntModule α] [Lean.Grind.NoNatZeroDivisors α] {k : ℤ} {a : α},
  k ≠ 0 → k • a = 0 → a = 0
-- Mathlib.Util.Export
Lean.Export.instCoeExprEntry : Coe Lean.Expr Lean.Export.Entry
-- Std.Do.Internal.Ensures.Def
/-- {lean}`ErasesTo x y` says the property-tagged {name}`x` is bind-faithful to {name}`y`: binding
{name}`x` and forgetting the property agrees with binding {name}`y`.
 -/
Std.Do.Internal.ErasesTo : {α : Type u} → {m : Type u → Type v} → [Bind m] → {P : α → Prop} → m { b // P b } → m α → Prop
-- Mathlib.Algebra.GroupWithZero.Basic
IsNilpotent.pow_of_pos : ∀ {n : ℕ} {S : Type u_5} [inst : MonoidWithZero S] {x : S}, IsNilpotent x → n ≠ 0 → IsNilpotent (x ^ n)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- A right rigid monoidal category is one in which every object has a right dual.  -/
CategoryTheory.RightRigidCategory : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.MonoidalCategory C] → Type (max u v)
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.πFunctorObj.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)],
  CategoryTheory.SmallObject.πFunctorObj f πX =
    CategoryTheory.Limits.pushout.desc πX (CategoryTheory.SmallObject.π'FunctorObj f πX) ⋯
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.preimage_coe_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, WithTop.some ⁻¹' Set.Ico ↑a ↑b = Set.Ico a b
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
ThreeGPFree.smul_set₀ : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [IsCancelMulZero α] [NoZeroDivisors α] {s : Set α} {a : α},
  ThreeGPFree s → a ≠ 0 → ThreeGPFree (a • s)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'_Q : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₂.RightHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' φ h).Q = h.Q
-- Init.Data.SInt.Lemmas
Int32.ne_of_lt : ∀ {a b : Int32}, a < b → a ≠ b
-- Mathlib.Order.Filter.Pointwise
Filter.nsmul_bot : ∀ {α : Type u_2} [inst : AddMonoid α] {n : ℕ}, n ≠ 0 → n • ⊥ = ⊥
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.π_comp_H0IsoOfIsTrivial_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [A.IsTrivial]
  (x : ↑(groupCohomology.cocycles A 0)),
  (ModuleCat.Hom.hom (groupCohomology.shortComplexH0 A).f)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cocyclesIso₀ A).hom) x) =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₀ A).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.iCocycles A 0)) x)
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit.eq_1 : ∀ {α : Type u} {ρ : Type w} [inst : ForIn Id ρ α] [inst_1 : BEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) (l : ρ),
  Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l =
    (have r := ⟨m, ⋯⟩;
      do
      let __s ←
        forIn l r fun a __s =>
            let r := __s;
            have r := ⟨(↑r).insertIfNew a (), ⋯⟩;
            pure (ForInStep.yield r)
      have r :
        { m' //
          ∀ (P : (Std.DHashMap.Internal.Raw₀ α fun x => Unit) → Prop),
            (∀ {m'' : Std.DHashMap.Internal.Raw₀ α fun x => Unit} {a : α} {b : Unit}, P m'' → P (m''.insertIfNew a b)) →
              P m → P m' } :=
        __s
      pure r).run
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.derives_iff_eq_or_tail : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {u w : List (Symbol T g.NT)},
  g.Derives u w ↔ w = u ∨ ∃ v, g.Derives u v ∧ g.Produces v w
-- Mathlib.Algebra.Algebra.Equiv
LinearEquiv.restrictScalars.congr_simp : ∀ (R : Type u_1) {S : Type u_4} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module S M] [inst_7 : Module S M₂] [inst_8 : LinearMap.CompatibleSMul M M₂ R S] (f f_1 : M ≃ₗ[S] M₂),
  f = f_1 → LinearEquiv.restrictScalars R f = LinearEquiv.restrictScalars R f_1
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
_private.Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme.0.AlgebraicGeometry.Scheme.IdealSheafData.ι_gluedTo : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  CategoryTheory.CategoryStruct.comp (I.glueData.ι U) I.gluedTo =
    CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (↑U).ι
-- Mathlib.Probability.Distributions.Cauchy
ProbabilityTheory.instIsProbabilityMeasure_cauchyMeasure : ∀ (x₀ : ℝ) (γ : NNReal), MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.cauchyMeasure x₀ γ)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.skipRestOfLine : Lean.Parser.ParserFn
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.map_op_inv : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Inv α] (s : Finset α),
  Finset.map MulOpposite.opEquiv.toEmbedding s⁻¹ = (Finset.map MulOpposite.opEquiv.toEmbedding s)⁻¹
-- Aesop.Stats.Basic
Aesop.instToJsonGoalKind : Lean.ToJson Aesop.GoalKind
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Proof that `blocks` sums to `n`  -/
Composition.blocks_sum : ∀ {n : ℕ} (self : Composition n), self.blocks.sum = n
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_zero_pos : ∀ (x : ENNReal), 0 < x ^ 0
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.instInhabitedSemiring.default : Lean.Meta.Grind.Arith.CommRing.Semiring
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.fintypeSetPathLengthLT : {V : Type u} →
  (G : SimpleGraph V) →
    [DecidableEq V] → [G.LocallyFinite] → (u v : V) → (n : ℕ) → Fintype ↑{p | p.IsPath ∧ p.length < n}
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.NormalExpr.brecOn.eq : ∀ {motive : Mathlib.Tactic.Abel.NormalExpr → Sort u} (t : Mathlib.Tactic.Abel.NormalExpr)
  (F_1 : (t : Mathlib.Tactic.Abel.NormalExpr) → Mathlib.Tactic.Abel.NormalExpr.below t → motive t),
  Mathlib.Tactic.Abel.NormalExpr.brecOn t F_1 = F_1 t (Mathlib.Tactic.Abel.NormalExpr.brecOn.go t F_1).2
-- Mathlib.Topology.Homeomorph.Lemmas
Topology.IsEmbedding.toHomeomorph.congr_simp : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  (hf : Topology.IsEmbedding f), hf.toHomeomorph = hf.toHomeomorph
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.Const.beq_of_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] [inst_1 : BEq β] [ReflBEq β]
  (m₁ m₂ : Std.ExtDTreeMap α (fun x => β) cmp), m₁ = m₂ → Std.ExtDTreeMap.Const.beq m₁ m₂ = true
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.prod_sigma_eq_prod : ∀ {n : ℕ} (c : OrderedFinpartition n) {α : Type u_5} [inst : CommMonoid α] (v : Fin n → α),
  ∏ m, ∏ r, v (c.emb m r) = ∏ i, v i
-- Mathlib.Computability.Primrec.List
Primrec.list_getElem? : ∀ {α : Type u_1} [inst : Primcodable α], Primrec₂ fun x1 x2 => x1[x2]?
-- Mathlib.RingTheory.Extension.ExtendScalars
Algebra.Extension.cotangentComplex_comp_h1CotangentEquivCotangent : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S), P.cotangentComplex ∘ₗ ↑P.h1CotangentEquivCotangent = Algebra.H1Cotangent.δ R P.Ring S
-- Mathlib.ModelTheory.Complexity
/-- A theory is universal when it is comprised only of universal sentences - these theories apply
also to substructures.  -/
FirstOrder.Language.Theory.IsUniversal : {L : FirstOrder.Language} → L.Theory → Prop
-- Mathlib.Combinatorics.Quiver.Basic
/-- A quiver is thin if it has no parallel arrows.  -/
Quiver.IsThin : (V : Type u) → [Quiver V] → Prop
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PrepathObject.symm_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C} (P : HomotopicalAlgebra.PrepathObject A),
  P.symm.p₁ = P.p₀
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
/-- Nonzero integral ideals in a Dedekind domain are invertible.

We will use this to show that nonzero fractional ideals are invertible,
and finally conclude that fractional ideals in a Dedekind domain form a group with zero.
 -/
FractionalIdeal.coe_ideal_mul_inv : ∀ {A : Type u_2} {K : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] [inst_4 : IsDedekindDomain A] (I : Ideal A), I ≠ ⊥ → ↑I * (↑I)⁻¹ = 1
-- Init.Data.SInt.Lemmas
Int8.toBitVec_add : ∀ {a b : Int8}, (a + b).toBitVec = a.toBitVec + b.toBitVec
-- Std.Sat.AIG.Lemmas
_private.Std.Sat.AIG.Lemmas.0.Std.Sat.AIG.toGraphviz.go.match_1.eq_2 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1) (idx : α)
  (h_1 : Std.Sat.AIG.Decl.atom idx = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false)
  (h_2 : (idx_1 : α) → Std.Sat.AIG.Decl.atom idx = Std.Sat.AIG.Decl.atom idx_1 → motive (Std.Sat.AIG.Decl.atom idx_1))
  (h_3 :
    (lhs rhs : Std.Sat.AIG.Fanin) →
      Std.Sat.AIG.Decl.atom idx = Std.Sat.AIG.Decl.gate lhs rhs → motive (Std.Sat.AIG.Decl.gate lhs rhs)),
  (match elem : Std.Sat.AIG.Decl.atom idx with
    | Std.Sat.AIG.Decl.false => h_1 elem
    | Std.Sat.AIG.Decl.atom idx_1 => h_2 idx_1 elem
    | Std.Sat.AIG.Decl.gate lhs rhs => h_3 lhs rhs elem) =
    h_2 idx ⋯
-- Mathlib.Analysis.Convex.Strict
StrictConvex.is_linear_image : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : TopologicalSpace E] [inst_3 : TopologicalSpace F] [inst_4 : AddCommMonoid E] [inst_5 : AddCommMonoid F]
  [inst_6 : Module 𝕜 E] [inst_7 : Module 𝕜 F] {s : Set E},
  StrictConvex 𝕜 s → ∀ {f : E → F}, IsLinearMap 𝕜 f → IsOpenMap f → StrictConvex 𝕜 (f '' s)
-- Mathlib.Order.LiminfLimsup
Filter.limsup_le_iSup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {u : β → α}, Filter.limsup u f ≤ ⨆ n, u n
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_zero_left : ∀ {α : 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 α}
  {C : ℝ} {f : α → E} {hT : MeasureTheory.DominatedFinMeasAdditive μ 0 C}, MeasureTheory.setToFun μ 0 hT f = 0
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.cancelBaseChange_symm_tmul : ∀ (R : Type uR) (S : Type uS) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (T : Type u_3)
  (A : Type u_4) (B : Type u_5) [inst_3 : CommSemiring T] [inst_4 : CommSemiring A] [inst_5 : CommSemiring B]
  [inst_6 : Algebra R T] [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : Algebra T A]
  [inst_10 : IsScalarTower R T A] [inst_11 : Algebra S A] [inst_12 : IsScalarTower R S A] [inst_13 : Algebra S T]
  [inst_14 : IsScalarTower S T A] (a : A) (b : B),
  (Algebra.TensorProduct.cancelBaseChange R S T A B).symm (a ⊗ₜ[R] b) = a ⊗ₜ[S] (1 ⊗ₜ[R] b)
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.rep_gHSpace_nonempty : ∀ {p : GromovHausdorff.GHSpace}, Nonempty p.Rep
-- Mathlib.Data.Set.Basic
/-- **Alias** of `Set.coe_ofPred`. -/
Set.coe_setOf : ∀ {α : Type u} (p : α → Prop), ↑{x | p x} = { x // p x }
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- A graph embedding induces an embedding of edge sets.  -/
SimpleGraph.Embedding.mapEdgeSet : {V : Type u_1} → {W : Type u_2} → {G : SimpleGraph V} → {G' : SimpleGraph W} → G ↪g G' → ↑G.edgeSet ↪ ↑G'.edgeSet
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.mono_map_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive]
  {X Y : C} (f : X ⟶ Y), CategoryTheory.Mono (L.map f) ↔ P.monoModSerre f
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.setTR.go.eq_def : ∀ {α : Type u_1} (l : List α) (a : α) (a_1 : List α) (a_2 : ℕ) (a_3 : Array α),
  List.setTR.go✝ l a a_1 a_2 a_3 =
    match a_1, a_2, a_3 with
    | [], x, x_1 => l
    | head :: xs, 0, acc => acc.toListAppend (a :: xs)
    | x :: xs, n.succ, acc => List.setTR.go✝ l a xs n (acc.push x)
-- Mathlib.Topology.Semicontinuity.Defs
UpperSemicontinuousOn.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace γ]
  [inst_2 : Preorder β] {f : α → β} {s : Set α} {g : γ → α} {t : Set γ},
  UpperSemicontinuousOn f s → ContinuousOn g t → Set.MapsTo g t s → UpperSemicontinuousOn (f ∘ g) t
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_update_eq_ite : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] [inst_1 : DecidableEq ι] [inst_2 : DecidableEq M] (f : ι → M) (x : ι)
  (y : M),
  Function.mulSupport (Function.update f x y) =
    if y = 1 then Function.mulSupport f \ {x} else insert x (Function.mulSupport f)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.inter_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {t₃ : Std.TreeSet.Raw α cmp},
  t₁.WF → t₂.WF → t₃.WF → t₁.Equiv t₂ → (t₁ ∩ t₃).Equiv (t₂ ∩ t₃)
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.coe_zeta_smul_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : MulAction R M]
  {f : ArithmeticFunction M} {x : ℕ}, (↑ArithmeticFunction.zeta • f) x = ∑ i ∈ x.divisors, f i
-- Mathlib.MeasureTheory.Measure.WithDensity
/-- If `μ` is a σ-finite measure, then so is `μ.withDensity fun x ↦ f x`
for any `ℝ≥0`-valued function `f`.  -/
MeasureTheory.SigmaFinite.withDensity : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ] (f : α → NNReal),
  MeasureTheory.SigmaFinite (μ.withDensity fun x => ↑(f x))
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_add_restrict_compl : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → μ.restrict s + μ.restrict sᶜ = μ
-- Mathlib.Data.ZMod.Defs
/-- Multiplicative commutative semigroup structure on `Fin n`.  -/
Fin.instCommSemigroup : (n : ℕ) → CommSemigroup (Fin n)
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_sigma' : ∀ {α : Type u_1} {β : α → Type u_4} (f : (a : α) × β a → ENNReal),
  ∑' (p : (a : α) × β a), f p = ∑' (a : α) (b : β a), f ⟨a, b⟩
-- Aesop.Search.Expansion.Norm
Aesop.eraseForwardRuleMatch : Aesop.ForwardRuleMatch → Aesop.NormM Unit
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.instOne : {K : Type u} → [inst : CommRing K] → One (RatFunc K)
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.isPresentable_of_isCardinalPresentable : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalPresentable X κ], CategoryTheory.IsPresentable.{w, v₁, u₁} X
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.AnchorRef.mk.sizeOf_spec : ∀ (numDigits : ℕ) (anchorPrefix : UInt64),
  sizeOf { numDigits := numDigits, anchorPrefix := anchorPrefix } = 1 + sizeOf numDigits + sizeOf anchorPrefix
-- Lean.MetavarContext
Lean.MetavarDecl.mk.sizeOf_spec : ∀ (userName : Lean.Name) (lctx : Lean.LocalContext) (type : Lean.Expr) (depth : ℕ)
  (localInstances : Lean.LocalInstances) (kind : Lean.MetavarKind) (numScopeArgs index : ℕ),
  sizeOf
      { userName := userName, lctx := lctx, type := type, depth := depth, localInstances := localInstances,
        kind := kind, numScopeArgs := numScopeArgs, index := index } =
    1 + sizeOf userName + sizeOf lctx + sizeOf type + sizeOf depth + sizeOf localInstances + sizeOf kind +
        sizeOf numScopeArgs +
      sizeOf index
-- Mathlib.Data.Set.Prod
Set.prod_subset_preimage_snd : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β), s ×ˢ t ⊆ Prod.snd ⁻¹' t
-- Mathlib.Data.Nat.Squarefree
Nat.minSqFac_prime : ∀ {n d : ℕ}, n.minSqFac = some d → Nat.Prime d
-- Mathlib.Data.Finset.Update
Function.updateFinset_updateFinset : ∀ {ι : Type u_1} {π : ι → Type u_2} {x : (i : ι) → π i} [inst : DecidableEq ι] {s t : Finset ι} {y : (i : ↥s) → π ↑i}
  {z : (i : ↥t) → π ↑i} (hst : Disjoint s t),
  Function.updateFinset (Function.updateFinset x s y) t z =
    Function.updateFinset x (s ∪ t) ((Equiv.piFinsetUnion π hst) (y, z))
-- Mathlib.Algebra.GCDMonoid.Basic
Associates.instGCDMonoid : {α : Type u_1} → [inst : CommMonoidWithZero α] → [GCDMonoid α] → GCDMonoid (Associates α)
-- Mathlib.Order.BoundedOrder.Monotone
StrictAnti.apply_eq_bot_iff : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : Preorder β] {f : α → β} {a : α},
  StrictAnti f → (f a = f ⊥ ↔ a = ⊥)
-- Mathlib.RingTheory.Unramified.LocalStructure
Polynomial.fiberEquivQuotient.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (f : Polynomial R →ₐ[R] S) (hf : Function.Surjective ⇑f) (p : Ideal R) [inst_3 : p.IsPrime],
  Polynomial.fiberEquivQuotient f hf p = Polynomial.fiberEquivQuotient f hf p