mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.isClosed_image : ∀ {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 σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) {s : Set M₁}, IsClosed (⇑e '' s) ↔ IsClosed s
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.lift_eval_of : ∀ {α : Type u_1} {M : Type u_4} [inst : AddMonoid M] (f : α → M) (x : α),
  (FreeAddMonoid.lift f) (FreeAddMonoid.of x) = f x
-- Mathlib.Data.Set.Image
Set.preimage_eq_empty_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, f ⁻¹' s = ∅ ↔ Disjoint s (Set.range f)
-- Mathlib.RepresentationTheory.Maschke
LinearMap.sumOfConjugates_apply : ∀ {k : Type u_1} [inst : CommRing k] (G : Type u_2) [inst_1 : Group G] {V : Type u_3} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : Module (MonoidAlgebra k G) V] [inst_5 : IsScalarTower k (MonoidAlgebra k G) V]
  {W : Type u_4} [inst_6 : AddCommGroup W] [inst_7 : Module k W] [inst_8 : Module (MonoidAlgebra k G) W]
  [inst_9 : IsScalarTower k (MonoidAlgebra k G) W] (π : W →ₗ[k] V) [inst_10 : Fintype G] (v : W),
  (LinearMap.sumOfConjugates G π) v = ∑ g, (π.conjugate g) v
-- Mathlib.Computability.Reduce
/-- `p` is one-one reducible to `q` if there is an injective computable function translating questions
about `p` to questions about `q`.
 -/
«term_≤₁_» : Lean.TrailingParserDescr
-- Mathlib.FieldTheory.IntermediateField.Basic
Subfield.extendScalars_le_extendScalars_iff : ∀ {L : Type u_2} [inst : Field L] {F E E' : Subfield L} (h : F ≤ E) (h' : F ≤ E'),
  Subfield.extendScalars h ≤ Subfield.extendScalars h' ↔ E ≤ E'
-- Lean.Meta.Tactic.Grind.Intro
/-- Asserts a new fact `prop` with proof `proof` to the given `goal`.  -/
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.Action.assertAt : Lean.Expr → Lean.Expr → ℕ → Lean.Meta.Grind.Action
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ring.ordMonoidWithZeroHom.eq_1 : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Nontrivial R],
  Ring.ordMonoidWithZeroHom R =
    {
      toFun := fun x =>
        if x ∈ nonZeroDivisors R then ENat.recTopCoe 0 (fun x => ↑(Multiplicative.ofAdd ↑x)) (Ring.ord R x) else 0,
      map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Data.Fintype.BigOperators
/-- It is equivalent to sum a function over `fin n` or `finset.range n`.  -/
Fin.sum_univ_eq_sum_range : ∀ {α : Type u_1} [inst : AddCommMonoid α] (f : ℕ → α) (n : ℕ), ∑ i, f ↑i = ∑ i ∈ Finset.range n, f i
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.count_factors_eq_find_of_dvd_pow : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)] {a p : Associates α},
  Irreducible p → ∀ [inst_4 : (n : ℕ) → Decidable (a ∣ p ^ n)] {n : ℕ} (h : a ∣ p ^ n), Nat.find ⋯ = p.count a.factors
-- Std.Data.ExtHashMap.Basic
/-- Creates a hash map from a list of keys, associating the value `()` with each key.

This is mainly useful to implement `HashSet.ofList`, so if you are considering using this,
`HashSet` or `HashSet.Raw` might be a better fit for you.  -/
Std.ExtHashMap.unitOfList : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → List α → Std.ExtHashMap α Unit
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.coe_singleton : ∀ (x : ZFSet.{u_1}), ↑{x} = {x}
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Size of the `i`-th block in a `CompositionAsSet`, seen as a function on `Fin c.length`.  -/
CompositionAsSet.blocksFun : {n : ℕ} → (c : CompositionAsSet n) → Fin c.length → ℕ
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.moduleEndSelf_symm_apply : ∀ (R : Type u_1) {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (f : Module.End A A), (AlgEquiv.moduleEndSelf R).symm f = MulOpposite.op (f 1)
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.flip_unflip : ∀ {X : Type u_5} {α : Type u_6} {β : Type u_7} [inst : Finite α] [inst_1 : TopologicalSpace X]
  (f : α → LocallyConstant X β), (LocallyConstant.unflip f).flip = f
-- Mathlib.RingTheory.Conductor
conductor_eq_of_eq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x y : S},
  ↑R[x] = ↑R[y] → conductor R x = conductor R y
-- Init.Data.SInt.Lemmas
Int32.toInt32_toISize : ∀ (n : Int32), n.toISize.toInt32 = n
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.tsub_add_eq_add_tsub : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, AddLECancellable b → b ≤ a → a - b + c = a + c - b
-- Mathlib.Order.Heyting.Hom
CoheytingHom.coe_id : ∀ (α : Type u_2) [inst : CoheytingAlgebra α], ⇑(CoheytingHom.id α) = id
-- Mathlib.Algebra.Module.Rat
/-- If `E` is a vector space over two division semirings `R` and `S`, then scalar multiplications
agree on non-negative rational numbers in `R` and `S`.  -/
nnratCast_smul_eq : ∀ {E : Type u_3} (R : Type u_4) (S : Type u_5) [inst : AddCommMonoid E] [inst_1 : DivisionSemiring R]
  [inst_2 : DivisionSemiring S] [inst_3 : Module R E] [inst_4 : Module S E] (r : ℚ≥0) (x : E), ↑r • x = ↑r • x
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.mk.inj : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {inst : CommRing R} {inst_1 : LieRing L}
  {inst_2 : AddCommGroup M} {inst_3 : AddCommGroup N} {inst_4 : Module R M} {inst_5 : Module R N}
  {inst_6 : LieRingModule L M} {inst_7 : LieRingModule L N} {toLieModuleHom : M →ₗ⁅R,L⁆ N} {invFun : N → M}
  {left_inv : Function.LeftInverse invFun (↑toLieModuleHom).toFun}
  {right_inv : Function.RightInverse invFun (↑toLieModuleHom).toFun} {toLieModuleHom_1 : M →ₗ⁅R,L⁆ N} {invFun_1 : N → M}
  {left_inv_1 : Function.LeftInverse invFun_1 (↑toLieModuleHom_1).toFun}
  {right_inv_1 : Function.RightInverse invFun_1 (↑toLieModuleHom_1).toFun},
  { toLieModuleHom := toLieModuleHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
      { toLieModuleHom := toLieModuleHom_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 } →
    toLieModuleHom = toLieModuleHom_1 ∧ invFun = invFun_1
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.strictMap_le_iff_le_inverseImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D) (P : CategoryTheory.MorphismProperty C) (P' : CategoryTheory.MorphismProperty D),
  P.strictMap F ≤ P' ↔ P ≤ P'.inverseImage F
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.int_mul_sub_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : NonAssocRing α] [inst_1 : NonAssocRing β],
  Function.Antiperiodic f c → ∀ (n : ℤ), f (↑n * c - x) = ↑↑n.negOnePow * f (-x)
-- Mathlib.RingTheory.GradedAlgebra.TensorProduct
GradedAlgebra.instCommRingSubtypeTensorProductMemSubmoduleBaseChangeOfNat : {ι : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      {S : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : DecidableEq ι] →
                [inst_4 : AddCommMonoid ι] →
                  [inst_5 : CommSemiring A] →
                    [inst_6 : Algebra R A] →
                      (𝒜 : ι → Submodule R A) → [GradedAlgebra 𝒜] → CommRing ↥(Submodule.baseChange S (𝒜 0))
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_nonneg : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] (a : A), 0 ≤ CFC.abs a
-- Init.Data.Vector.Count
Vector.count_eq_size : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {n : ℕ} {a : α} {xs : Vector α n}, Vector.count a xs = n ↔ ∀ b ∈ xs, a = b
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivAt.div_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_2} [inst_1 : NormedDivisionRing 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'} {c' : 𝕜'},
  HasDerivAt c c' x → ∀ (d : 𝕜'), HasDerivAt (fun x => c x / d) (c' / d) x
-- Mathlib.Topology.Sets.VietorisTopology
Continuous.nonemptyCompacts_map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Continuous f), Continuous (TopologicalSpace.NonemptyCompacts.map f hf)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_inj : ∀ {o a b : Ordinal.{u}}, Ordinal.veblen o a = Ordinal.veblen o b ↔ a = b
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.pullback_snd_image_fst_preimage : ∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z) (U : Set ↑X),
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g)) ''
      ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g)) ⁻¹' U =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ⁻¹' ⇑(CategoryTheory.ConcreteCategory.hom f) '' U
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_insertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α Unit} [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α}, (m.insertManyIfNewUnit l).isEmpty = (m.isEmpty && l.isEmpty)
-- Aesop.Search.Expansion.Norm
Aesop.NormRuleResult.succeeded.inj : ∀ {goal : Lean.MVarId} {steps? : Option (Array Aesop.Script.LazyStep)} {goal_1 : Lean.MVarId}
  {steps?_1 : Option (Array Aesop.Script.LazyStep)},
  Aesop.NormRuleResult.succeeded goal steps? = Aesop.NormRuleResult.succeeded goal_1 steps?_1 →
    goal = goal_1 ∧ steps? = steps?_1
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.toCloseds_injective : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : T2Space α],
  Function.Injective TopologicalSpace.NonemptyCompacts.toCloseds
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Functor.op_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : Cᵒᵖ), F.op.obj X = Opposite.op (F.obj (Opposite.unop X))
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
/-- `σ k n` is the sum of the `k`th powers of the divisors of `n`  -/
ArithmeticFunction.sigma.termσ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
/-- The morphism `Xᵢ ⟶ Yₐ`.  -/
CategoryTheory.PreOneHypercover.Homotopy.a : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      {E : CategoryTheory.PreOneHypercover S} →
        {F : CategoryTheory.PreOneHypercover S} →
          {f g : E.Hom F} → (self : CategoryTheory.PreOneHypercover.Homotopy f g) → (i : E.I₀) → E.X i ⟶ F.Y (self.H i)
-- Mathlib.Topology.Filter
Filter.isOpen_setOfPred_mem : ∀ {α : Type u_2} {s : Set α}, IsOpen {l | s ∈ l}
-- Mathlib.Order.RelSeries
RelSeries.head_eraseLast : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r), p.eraseLast.head = p.head
-- Mathlib.Order.Defs.Unbundled
/-- **Alias** of `Std.Asymm.antisymm`. -/
IsAsymm.isAntisymm : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Asymm r], Std.Antisymm r
-- Mathlib.Logic.Equiv.Basic
Equiv.piCurry_symm_apply : ∀ {α : Type u_11} {β : α → Type u_9} (γ : (a : α) → β a → Type u_10) (f : (a : α) → (b : β a) → γ a b),
  (Equiv.piCurry γ).symm f = Sigma.uncurry f
-- Mathlib.Data.List.MinMax
List.argAux.congr_simp : ∀ {α : Type u_1} (r r_1 : α → α → Prop),
  r = r_1 →
    ∀ {inst : DecidableRel r} [inst_1 : DecidableRel r_1] (a a_1 : Option α),
      a = a_1 → ∀ (b b_1 : α), b = b_1 → List.argAux r a b = List.argAux r_1 a_1 b_1
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric
CFC.continuousOn_nnrpow : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonnegSpectrumClass ℝ A] [inst_8 : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [ContinuousStar A] [CompleteSpace A] (r : NNReal), ContinuousOn (fun x => x ^ r) {a | 0 ≤ a}
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.toCone_π_app_right : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q),
  c.toCone.π.app { as := CategoryTheory.Limits.WalkingPair.right } = c.snd
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.instEmptyCollection : {α : Type u} → {le : α → α → Bool} → EmptyCollection (Batteries.BinomialHeap α le)
-- Mathlib.Order.Interval.Set.Pi
Set.image_single_Icc_left : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → Zero (α i)] (i : ι) (a : α i), Pi.single i '' Set.Icc a 0 = Set.Icc (Pi.single i a) 0
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.coe_bot : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A], ↑⊥ = Set.range ⇑(algebraMap R A)
-- Std.Sync.Channel
/-- Consumers that are blocked on a producer providing them a value. They will be resolved to `none`
if the channel closes.
 -/
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.State.consumers : {α : Type} → Std.CloseableChannel.Zero.State✝ α → Std.Queue (Std.CloseableChannel.Consumer✝ α)
-- Mathlib.Order.Basic
Pi.partialOrder : {ι : Type u_1} → {π : ι → Type u_4} → [(i : ι) → PartialOrder (π i)] → PartialOrder ((i : ι) → π i)
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.ExtensionState : Type → Type
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} {l : List α} {k : α}
  {h' : k ∈ t.insertManyIfNewUnit l}, (t.insertManyIfNewUnit l)[k] = ()
-- Mathlib.Topology.MetricSpace.PartitionOfUnity
/-- **Alias** of `Metric.exists_forall_closedEBall_subset_aux₁`.

---

Auxiliary lemma for `exists_continuous_real_forall_closedEBall_subset`
and its smooth counterpart.  -/
EMetric.exists_forall_closedBall_subset_aux₁ : ∀ {ι : Type u_1} {X : Type u_2} [inst : EMetricSpace X] {K U : ι → Set X},
  (∀ (i : ι), IsClosed (K i)) →
    (∀ (i : ι), IsOpen (U i)) →
      (∀ (i : ι), K i ⊆ U i) →
        LocallyFinite K →
          ∀ (x : X),
            ∃ r,
              ∀ᶠ (y : X) in nhds x,
                r ∈ Set.Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ i, ⋂ (_ : y ∈ K i), {r | Metric.closedEBall y r ⊆ U i}
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.mk_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (f : α →ᵈ β)
  (h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), edist (f x) (f y) = ↑r * edist x y), { toFun := ⇑f, edist_eq' := h } = f
-- Mathlib.Lean.Thunk
Thunk.instAdd_mathlib : {α : Type u} → [Add α] → Add (Thunk α)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.comap_injective_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F},
  Function.Surjective ⇑f → Function.Injective (AddSubmonoid.comap f)
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.findFinIdx?.eq_1 : ∀ {α : Type u} (p : α → Bool) (as : Array α), Array.findFinIdx? p as = Array.findFinIdx?.loop✝ p as 0
-- Mathlib.Topology.Order.NhdsSet
Iic_mem_nhdsSet_Icc : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c : α},
  b < c → Set.Iic c ∈ nhdsSet (Set.Icc a b)
-- Lean.Elab.InfoTree.Main
Lean.Elab.addConstInfo : {m : Type → Type} →
  [Monad m] →
    [Lean.Elab.MonadInfoTree m] →
      [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Syntax → Lean.Name → optParam (Option Lean.Expr) none → m Unit
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
CategoryTheory.Grpd.piIsoPi.eq_1 : ∀ (J : Type u) (f : J → CategoryTheory.Grpd),
  CategoryTheory.Grpd.piIsoPi J f =
    (CategoryTheory.Grpd.piLimitFanIsLimit f).conePointUniqueUpToIso
      (CategoryTheory.Limits.limit.isLimit (CategoryTheory.Discrete.functor f))
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.all.sizeOf_spec : ∀ {L : FirstOrder.Language} {α : Type u'} [inst : SizeOf α] {n : ℕ} (f : L.BoundedFormula α (n + 1)),
  sizeOf f.all = 1 + sizeOf n + sizeOf f
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.rnDeriv_toReal_pos : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ} {κ η : ProbabilityTheory.Kernel α γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] [ProbabilityTheory.IsFiniteKernel κ]
  [ProbabilityTheory.IsFiniteKernel η] {a : α},
  (κ a).AbsolutelyContinuous (η a) → ∀ᵐ (x : γ) ∂κ a, 0 < (κ.rnDeriv η a x).toReal
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering}, ∅.min? = none
-- Mathlib.InformationTheory.Hamming
hammingNorm_lt_one : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
  [inst_2 : (i : ι) → Zero (β i)] {x : (i : ι) → β i}, hammingNorm x < 1 ↔ x = 0
-- Mathlib.Topology.Instances.ENNReal.Lemmas
isClosed_setOfPred_lipschitzWith : ∀ {α : Type u_4} {β : Type u_5} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (K : NNReal),
  IsClosed {f | LipschitzWith K f}
-- Aesop.Frontend.Tactic
Aesop.Frontend.TacticConfig.mk.injEq : ∀ (additionalRules erasedRules : Array Aesop.Frontend.RuleExpr) (enabledRuleSets : Std.HashSet Aesop.RuleSetName)
  (options : Aesop.Options) (simpConfig : Lean.Meta.Simp.Config) (simpConfigSyntax? : Option Lean.Term)
  (additionalRules_1 erasedRules_1 : Array Aesop.Frontend.RuleExpr) (enabledRuleSets_1 : Std.HashSet Aesop.RuleSetName)
  (options_1 : Aesop.Options) (simpConfig_1 : Lean.Meta.Simp.Config) (simpConfigSyntax?_1 : Option Lean.Term),
  ({ additionalRules := additionalRules, erasedRules := erasedRules, enabledRuleSets := enabledRuleSets,
        options := options, simpConfig := simpConfig, simpConfigSyntax? := simpConfigSyntax? } =
      { additionalRules := additionalRules_1, erasedRules := erasedRules_1, enabledRuleSets := enabledRuleSets_1,
        options := options_1, simpConfig := simpConfig_1, simpConfigSyntax? := simpConfigSyntax?_1 }) =
    (additionalRules = additionalRules_1 ∧
      erasedRules = erasedRules_1 ∧
        enabledRuleSets = enabledRuleSets_1 ∧
          options = options_1 ∧ simpConfig = simpConfig_1 ∧ simpConfigSyntax? = simpConfigSyntax?_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.ι_isoColimit_hom : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct fun j => X.obj { as := j }] [inst_2 : CategoryTheory.Limits.HasColimit X]
  (j : α),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun j => X.obj { as := j }) j)
      (CategoryTheory.Limits.Sigma.isoColimit X).hom =
    CategoryTheory.Limits.colimit.ι X { as := j }
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.ConnectionState.respStream : {β : Type} → Std.Http.Server.Connection.ConnectionState✝ β → Option β
-- Mathlib.Order.Hom.Lattice
LatticeHom.symm_dual_id : ∀ {α : Type u_2} [inst : Lattice α], LatticeHom.dual.symm (LatticeHom.id αᵒᵈ) = LatticeHom.id α
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.of_zero : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (c : ↥(LieModule.Cohomology.twoCocycle R L M)), (LieAlgebra.ofProd c) 0 = 0
-- Mathlib.Topology.Path
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections.  -/
Path.simps.apply : {X : Type u_1} → [inst : TopologicalSpace X] → {x y : X} → Path x y → ↑unitInterval → X
-- Mathlib.Data.Multiset.Powerset
/-- The power set of a multiset.  -/
Multiset.powerset : {α : Type u_1} → Multiset α → Multiset (Multiset α)
-- Mathlib.Data.Stream.Init
Stream'.zip_inits_tails : ∀ {α : Type u} (s : Stream' α), Stream'.zip Stream'.appendStream' s.inits s.tails = Stream'.const s
-- Mathlib.Topology.Order.LeftRightNhds
/-- **Alias** of `countable_setOfPred_isolated_left_within`.

---

The set of points in a set which are isolated on the left in this set is countable when the
space is second-countable.  -/
countable_setOf_isolated_left_within : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {s : Set α}, {x | x ∈ s ∧ nhdsWithin x (s ∩ Set.Iio x) = ⊥}.Countable
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- `1` in the localization, defined as `1 /ₒ 1`.  -/
OreLocalization.one : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] → {X : Type u_2} → [inst_2 : MulAction R X] → [One X] → OreLocalization S X
-- Mathlib.Algebra.Order.Ring.Canonical
mul_tsub : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R] [inst_3 : Sub R]
  [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [AddLeftReflectLE R] (a b c : R), a * (b - c) = a * b - a * c
-- Init.Data.Bool
Bool.cond_eq_false_distrib : ∀ (c t f : Bool), ((bif c then t else f) = false) = if c = true then t = false else f = false
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonLeanModuleQuery : Lean.FromJson Lean.Lsp.LeanModuleQuery
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.Simps.symm_apply.eq_1 : ∀ (G : Type u) [inst : TopologicalSpace G] (H : Type v) [inst_1 : TopologicalSpace H] [inst_2 : Add G] [inst_3 : Add H]
  (e : G ≃ₜ+ H), ContinuousAddEquiv.Simps.symm_apply G H e = ⇑e.symm
-- Mathlib.Algebra.Order.Kleene
/-- The Kleene star operator on a Kleene algebra  -/
KStar.kstar : {α : Type u_5} → [self : KStar α] → α → α
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k fallback : α},
  (List.map Sigma.fst l).contains k = false → (t.insertMany l).getKeyD k fallback = t.getKeyD k fallback
-- Std.Time.Format.Modifier
Std.Time.instReprOffsetO : Repr Std.Time.OffsetO
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.Hom.nsmul : {M N : SemiNormedGrp} → SMul ℕ (M ⟶ N)
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.IsWeaklyRegular.of_perm_of_subset_jacobson_annihilator : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherian R M]
  {rs rs' : List R},
  RingTheory.Sequence.IsWeaklyRegular M rs →
    rs.Perm rs' → (∀ r ∈ rs, r ∈ (Module.annihilator R M).jacobson) → RingTheory.Sequence.IsWeaklyRegular M rs'
-- Mathlib.NumberTheory.NumberField.Discriminant.Defs
/-- The absolute discriminant of the number field `ℚ` is 1.  -/
Rat.numberField_discr : NumberField.discr ℚ = 1
-- Std.Internal.UV.System
/-- Gets the current high-resolution time in nanoseconds.
 -/
Std.Internal.UV.System.hrtime : IO UInt64
-- Lean.Data.FuzzyMatching
_private.Lean.Data.FuzzyMatching.0.Lean.FuzzyMatching.fuzzyMatchCore.getIdx : String → ℕ → ℕ → ℕ