mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.den_smul : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} (x : Submonoid A)
  {α : Type u_4} [inst_2 : SMul α A] [inst_3 : SMulMemClass σ α A] (c : HomogeneousLocalization.NumDenSameDeg 𝒜 x)
  (m : α), ↑(m • c).den = ↑c.den
-- Mathlib.Order.Concept
Concept.isIntent_iff_exists_concept : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t : Set β}, Order.IsIntent r t ↔ ∃ c, c.intent = t
-- Mathlib.Data.ZMod.Basic
ZMod.isUnit_prime_iff_not_dvd : ∀ {n p : ℕ}, Nat.Prime p → (IsUnit ↑p ↔ ¬p ∣ n)
-- Std.Do.PostCond
Std.Do.PostCond.entails.mk : ∀ {α : Type u_1} {ps : Std.Do.PostShape} {P Q : Std.Do.PostCond α ps},
  (∀ (a : α), P.1 a ⊢ₛ Q.1 a) → P.2.entails Q.2 → P.entails Q
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getEntryGE_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α} {h' : ∃ a ∈ t₁, (cmp a k).isGE = true} (h : t₁.Equiv t₂), t₁.getEntryGE k h' = t₂.getEntryGE k ⋯
-- Mathlib.Topology.Algebra.Constructions
AddUnits.isOpenMap_map : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : AddMonoid M] [inst_2 : TopologicalSpace N]
  [inst_3 : AddMonoid N] {f : M →+ N}, Function.Injective ⇑f → IsOpenMap ⇑f → IsOpenMap ⇑(AddUnits.map f)
-- Init.Data.Array.BinSearch
_private.Init.Data.Array.BinSearch.0.Array.binInsertAux : {α : Type u} →
  {m : Type u → Type v} →
    [Monad m] →
      (lt : α → α → Bool) →
        (α → m α) →
          (Unit → m α) → (as : Array α) → (k : α) → (lo hi : Fin as.size) → ↑lo ≤ ↑hi → lt as[lo] k = true → m (Array α)
-- Mathlib.Algebra.Order.Group.PartialSups
partialSups_add_const : ∀ {α : Type u_1} {ι : Type u_2} [inst : SemilatticeSup α] [inst_1 : AddGroup α] [inst_2 : Preorder ι]
  [inst_3 : LocallyFiniteOrderBot ι] [AddRightMono α] (f : ι → α) (c : α) (i : ι),
  (partialSups fun x => f x + c) i = (partialSups f) i + c
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.Coindep.exists_subset_compl_isBase : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.Coindep X → ∃ B, M.IsBase B ∧ X ⊆ M.E \ B
-- Mathlib.Order.Interval.Finset.Defs
Set.finite_Ico : ∀ {α : Type u_1} [inst : Preorder α] [LocallyFiniteOrder α] (a b : α), (Set.Ico a b).Finite
-- Mathlib.Topology.Homotopy.Product
/-- Lemmas showing projection is the inverse of pi.  -/
Path.Homotopic.proj_pi : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {as bs : (i : ι) → X i} (i : ι)
  (paths : (i : ι) → Path.Homotopic.Quotient (as i) (bs i)), Path.Homotopic.proj i (Path.Homotopic.pi paths) = paths i
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
pow_left_mono : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftMono M] [MulRightMono M] (n : ℕ),
  Monotone fun a => a ^ n
-- Mathlib.Data.Holor
/-- Take the first elements of a `HolorIndex`.  -/
HolorIndex.take : {ds₂ ds₁ : List ℕ} → HolorIndex (ds₁ ++ ds₂) → HolorIndex ds₁
-- Mathlib.Algebra.Algebra.Unitization
Unitization.fst_inl : ∀ {R : Type u_1} (A : Type u_2) [inst : Zero A] (r : R), (Unitization.inl r).toProd.1 = r
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Cotrident.π_eq_app_one : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  (t : CategoryTheory.Limits.Cotrident f), t.π = t.ι.app CategoryTheory.Limits.WalkingParallelFamily.one
-- Mathlib.Algebra.Order.Monovary
Monovary.add_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : AddCommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedAddMonoid β] {f : ι → α} {g₁ g₂ : ι → β}, Monovary f g₁ → Monovary f g₂ → Monovary f (g₁ + g₂)
-- Mathlib.Topology.UniformSpace.LocallyUniformConvergence
TendstoLocallyUniformly.tendstoLocallyUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {s : Set α} {p : Filter ι}, TendstoLocallyUniformly F f p → TendstoLocallyUniformlyOn F f p s
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
ThreeGPFree.mulRothNumber_eq : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {s : Finset α}, ThreeGPFree ↑s → mulRothNumber s = s.card
-- Mathlib.Analysis.Normed.Module.FiniteDimension
summable_of_isEquivalent : ∀ {ι : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  {f g : ι → E}, Summable g → Asymptotics.IsEquivalent Filter.cofinite f g → Summable f
-- Mathlib.Algebra.MonoidAlgebra.Cardinal
MonoidAlgebra.cardinalMk_of_infinite' : ∀ (R M : Type u) [inst : Semiring R] [Nonempty M] [Infinite R],
  Cardinal.mk (MonoidAlgebra R M) = max (Cardinal.mk R) (Cardinal.mk M)
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.iInf_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {ι : Sort u_1}
  (S : ι → CategoryTheory.Subfunctor F) (U : C), (⨅ i, S i).obj U = ⋂ i, (S i).obj U
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.toLinearEquiv_toLinearMap : ∀ {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} (φ : ρ.Equiv σ), ↑φ.toLinearEquiv = (↑φ).toLinearMap
-- Mathlib.Data.PEquiv
PEquiv.mk : {α : Type u} →
  {β : Type v} →
    (toFun : α → Option β) →
      (invFun : β → Option α) → (∀ (a : α) (b : β), invFun b = some a ↔ toFun a = some b) → α ≃. β
-- Mathlib.Algebra.BigOperators.Fin
/-- A product of a function `f : Fin (n + 1) → M` over all `Fin (n + 1)`
is the product of `f x`, for some `x : Fin (n + 1)` times the remaining product  -/
Fin.prod_univ_succAbove : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (x : Fin (n + 1)),
  ∏ i, f i = f x * ∏ i, f (x.succAbove i)
-- Lean.Language.Lean.Types
/-- Holds produced diagnostics. Separate snapshot so that it can be tagged with the header syntax,
which should not be done for this snapshot containing `firstCmdSnap`.
 -/
Lean.Language.Lean.HeaderParsedSnapshot.metaSnap : Lean.Language.Lean.HeaderParsedSnapshot → Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf
-- Init.Data.SInt.Bitwise
Int64.xor_not : ∀ {a b : Int64}, a ^^^ ~~~b = ~~~(a ^^^ b)
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.mul_add_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (R : C)
  [inst_2 : CategoryTheory.MonObj R] [inst_3 : CategoryTheory.AddMonObj R],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R CategoryTheory.AddMonObj.add)
        CategoryTheory.MonObj.mul =
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CartesianMonoidalCategory.lift
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.SemiCartesianMonoidalCategory.fst R R))
            CategoryTheory.MonObj.mul)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.SemiCartesianMonoidalCategory.snd R R))
            CategoryTheory.MonObj.mul))
        CategoryTheory.AddMonObj.add ↔
    ∀ ⦃X : C⦄ (a b c : X ⟶ R), a * (b + c) = a * b + a * c
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.small_bot : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M], Small.{u, w} ↥⊥
-- Mathlib.Order.GaloisConnection.Defs
/-- Lift the bottom along a Galois connection  -/
GaloisConnection.liftOrderBot : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [OrderBot α] → [inst_2 : PartialOrder β] → {l : α → β} → {u : β → α} → GaloisConnection l u → OrderBot β
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the largest key in the tree map, panicking if the map is empty.
 -/
Std.DTreeMap.maxKey! : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.DTreeMap α β cmp → α
-- Mathlib.Logic.Basic
heq_cast_iff_heq : ∀ {α β γ : Sort u_1} (e : β = γ) (a : α) (b : β), a ≍ cast e b ↔ a ≍ b
-- Mathlib.Order.LiminfLimsup
/-- A version of `limsup_le_iff` with large inequalities in densely ordered spaces  -/
Filter.limsup_le_iff' : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder β] {f : Filter α} {u : α → β}
  [DenselyOrdered β] {x : β},
  autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) Filter.limsup_le_iff'._auto_1 →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) Filter.limsup_le_iff'._auto_3 →
      (Filter.limsup u f ≤ x ↔ ∀ y > x, ∀ᶠ (a : α) in f, u a ≤ y)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [Std.LawfulEqOrd α], t.WF → ∀ {km : α}, t.maxKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (compare k km).isLE = true
-- Lean.Meta.ForEachExpr
/-- Similar to `mkForallFVars`, but tries to infer better binder names when `xs` contains metavariables.
Let `?m` be a metavariable in `xs` s.t. `?m` does not have a user facing name.
Then, we try to find an application `f ... ?m` in the other binder type and `type`, and
(temporarily) use the corresponding parameter name (with a fresh macro scope) as the user facing name for `?m`.
The "renaming" is temporary.
 -/
Lean.Meta.mkForallFVars' : Array Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Order.Module.Field
Mathlib.Meta.Positivity.smul_nonneg_of_pos_of_nonneg : ∀ {α : Type u_3} {β : Type u_4} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β] [inst_3 : Preorder α]
  [inst_4 : Preorder β] [PosSMulMono α β] {a : α} {b : β}, 0 < a → 0 ≤ b → 0 ≤ a • b
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
/-- Auxiliary function for `pureCoherence`.  -/
Mathlib.Tactic.BicategoryLike.MkEqOfNaturality.mkEqOfNaturality : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEqOfNaturality m] →
    Lean.Expr →
      Lean.Expr →
        Mathlib.Tactic.BicategoryLike.IsoLift →
          Mathlib.Tactic.BicategoryLike.IsoLift →
            Mathlib.Tactic.BicategoryLike.Mor₂Iso →
              Mathlib.Tactic.BicategoryLike.Mor₂Iso → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The centroid of a simplex does not lie in the affine span of any proper subset of its
vertices.  -/
Affine.Simplex.centroid_notMem_affineSpan_of_ne_univ : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [CharZero k] (s : Affine.Simplex k P n) {t : Set (Fin (n + 1))},
  t ≠ Set.univ → s.centroid ∉ affineSpan k (s.points '' t)
-- Lean.Data.DeclarationRange
Lean.instInhabitedDeclarationRange : Inhabited Lean.DeclarationRange
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.complexConj_ne_one : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K]
  [inst_3 : Algebra.IsIntegral ℚ K], NumberField.IsCMField.complexConj K ≠ 1
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instBoundedOrder : {M : Type u_1} → [inst : CommMonoidWithZero M] → BoundedOrder (Associates M)
-- Std.Http.Data.Headers.Name
/-- The proof that we stored the header name in stored as a lower case string.
 -/
Std.Http.Header.Name.isLowerCase : ∀ (self : Std.Http.Header.Name), Std.Http.Internal.IsLowerCase self.value
-- Init.Grind.Interactive
/-- `focus tac` focuses on the main goal, suppressing all other goals, and runs `tac` on it.
Usually `· tac`, which enforces that the goal is closed by `tac`, should be preferred.
 -/
Lean.Parser.Tactic.Grind.focus : Lean.ParserDescr
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instUniqueOfSubsingleton : {k : Type u_1} → {G : Type u_2} → [inst : AddMonoid k] → [Subsingleton k] → Unique (SkewMonoidAlgebra k G)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given a MonoidHom `f : M →* N` and Submonoid `S ⊆ M` such that `f(S) ⊆ Nˣ`, for all
`w, z : N` and `y ∈ S`, we have `w * (f y)⁻¹ = z ↔ w = f y * z`.  -/
Submonoid.LocalizationMap.mul_inv_left : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {f : M →* N}
  (h : ∀ (y : ↥S), IsUnit (f ↑y)) (y : ↥S) (w z : N),
  w * ↑((IsUnit.liftRight (f.domRestrict S) h) y)⁻¹ = z ↔ w = f ↑y * z
-- Init.Data.Array.Lemmas
Array.any_filterMap : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Option β} {p : β → Bool},
  (Array.filterMap f xs).any p =
    xs.any fun a =>
      match f a with
      | some b => p b
      | none => false
-- Init.Data.Nat.Basic
Nat.sub_one_cancel : ∀ {a b : ℕ}, 0 < a → 0 < b → a - 1 = b - 1 → a = b
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.substAlgHom_comp_substAlgHom : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} {υ : Type u_7} {T : Type u_8} [inst_3 : CommRing T]
  [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {b : τ → MvPowerSeries υ T}
  (ha : MvPowerSeries.HasSubst a) (hb : MvPowerSeries.HasSubst b),
  (AlgHom.restrictScalars R (MvPowerSeries.substAlgHom hb)).comp (MvPowerSeries.substAlgHom ha) =
    MvPowerSeries.substAlgHom ⋯
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimit.exists_desc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes},
  c.IsColimit → ∀ (c' : F.CoconeTypes), ∃ f, ∀ (j : J), f ∘ c.ι j = c'.ι j
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_inter_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₁ ∩ t₂ ↔ k ∈ t₁ ∧ k ∈ t₂
-- Mathlib.Topology.LocallyConstant.Basic
/-- Given a locally constant function to `α → β`, construct a family of locally constant
functions with values in β indexed by α.  -/
LocallyConstant.flip : {X : Type u_5} →
  {α : Type u_6} → {β : Type u_7} → [inst : TopologicalSpace X] → LocallyConstant X (α → β) → α → LocallyConstant X β
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Category.{v₁, max u₁ v₁} (CategoryTheory.Comon C)
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
hasLineDerivAt_smul_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f : E → F} {x v : E}
  {f' : F} {c : 𝕜}, c ≠ 0 → (HasLineDerivAt 𝕜 f (c • f') x (c • v) ↔ HasLineDerivAt 𝕜 f f' x v)
-- Mathlib.Order.Circular
btw_cyclic_right : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, btw a b c → btw c a b
-- Mathlib.Analysis.Normed.Lp.lpHolder
lp.dualPairing_apply : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : ι → Type u_3} {F : ι → Type u_4} [inst : RCLike 𝕜]
  [inst_1 : (i : ι) → NormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → NormedAddCommGroup (F i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)] {p q : ENNReal} {H : Type u_6}
  [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] [inst_7 : CompleteSpace H] [inst_8 : Fact (1 ≤ p)]
  [inst_9 : Fact (1 ≤ q)] [inst_10 : p.HolderConjugate q] (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] H) {K : NNReal}
  (hBK : ∀ (i : ι), ‖B i‖ ≤ ↑K) (e : ↥(lp E p)) (f : ↥(lp F q)),
  ((lp.dualPairing p q B hBK) e) f = ∑' (i : ι), ((B i) (↑e i)) (↑f i)
-- Lean.Elab.Tactic.Induction
/-- The short name of the alternative, used in `| foo =>` cases  -/
Lean.Elab.Tactic.ElimApp.Alt.name : Lean.Elab.Tactic.ElimApp.Alt → Lean.Name
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.StrictPseudofunctor.mapAdjunction_counit : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {a b : B}
  {f : a ⟶ b} {g : b ⟶ a} (F : CategoryTheory.StrictPseudofunctor B C) (adj : CategoryTheory.Bicategory.Adjunction f g),
  (F.mapAdjunction adj).counit =
    CategoryTheory.CategoryStruct.comp (F.mapComp g f).inv
      (CategoryTheory.CategoryStruct.comp (F.map₂ adj.counit) (F.mapId b).hom)
-- Mathlib.Order.Filter.CountableInter
/-- `Filter.countableGenerate g` is the greatest `countableInterFilter` containing `g`.  -/
Filter.countableGenerate : {α : Type u_2} → Set (Set α) → Filter α
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.zsmul : ∀ {G : Type u_1} [inst : AddGroup G] {x : G}, IsOfFinAddOrder x → ∀ {i : ℤ}, IsOfFinAddOrder (i • x)
-- Init.MetaTypes
Lean.Meta.DSimp.Config.mk.sizeOf_spec : ∀ (zeta beta eta : Bool) (etaStruct : Lean.Meta.EtaStructMode)
  (iota proj decide autoUnfold failIfUnchanged unfoldPartialApp zetaDelta index zetaUnused zetaHave locals instances :
    Bool),
  sizeOf
      { zeta := zeta, beta := beta, eta := eta, etaStruct := etaStruct, iota := iota, proj := proj, decide := decide,
        autoUnfold := autoUnfold, failIfUnchanged := failIfUnchanged, unfoldPartialApp := unfoldPartialApp,
        zetaDelta := zetaDelta, index := index, zetaUnused := zetaUnused, zetaHave := zetaHave, locals := locals,
        instances := instances } =
    1 + sizeOf zeta + sizeOf beta + sizeOf eta + sizeOf etaStruct + sizeOf iota + sizeOf proj + sizeOf decide +
                      sizeOf autoUnfold +
                    sizeOf failIfUnchanged +
                  sizeOf unfoldPartialApp +
                sizeOf zetaDelta +
              sizeOf index +
            sizeOf zetaUnused +
          sizeOf zetaHave +
        sizeOf locals +
      sizeOf instances
-- Mathlib.LinearAlgebra.Contraction
TensorProduct.dualDistrib.eq_1 : ∀ (R : Type u_1) (M : Type u_3) (N : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N],
  TensorProduct.dualDistrib R M N =
    LinearMap.compRight R ↑(TensorProduct.lid R R) ∘ₗ TensorProduct.homTensorHomMap (RingHom.id R) M N R R
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `*` is a left cancel semigroup, if it admits an injective map that
preserves `*` to a left cancel semigroup.  See note [reducible non-instances].  -/
Function.Injective.leftCancelSemigroup : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₁] →
      [inst_1 : LeftCancelSemigroup M₂] →
        (f : M₁ → M₂) → Function.Injective f → (∀ (x y : M₁), f (x * y) = f x * f y) → LeftCancelSemigroup M₁
-- Mathlib.Topology.Metrizable.Uniformity
/-- Consider a function `d : X → X → ℝ≥0` such that `d x x = 0` and `d x y = d y x` for all `x`,
`y`. Let `dist` be the largest pseudometric distance such that `dist x y ≤ d x y`, see
`PseudoMetricSpace.ofPreNNDist`. Suppose that `d` satisfies the following triangle-like
inequality: `d x₁ x₄ ≤ 2 * max (d x₁ x₂, d x₂ x₃, d x₃ x₄)`. Then `d x y ≤ 2 * dist x y` for all
`x`, `y`.  -/
PseudoMetricSpace.le_two_mul_dist_ofPreNNDist : ∀ {X : Type u_1} (d : X → X → NNReal) (dist_self : ∀ (x : X), d x x = 0) (dist_comm : ∀ (x y : X), d x y = d y x),
  (∀ (x₁ x₂ x₃ x₄ : X), d x₁ x₄ ≤ 2 * max (d x₁ x₂) (max (d x₂ x₃) (d x₃ x₄))) → ∀ (x y : X), ↑(d x y) ≤ 2 * dist x y
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_alter_eq_add_one : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, k ∉ t → (f t[k]?).isSome = true → (t.alter k f).size = t.size + 1
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.instEquivLike : {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] → EquivLike (M ≃ₗ⁅R,L⁆ N) M N
-- Mathlib.Analysis.Normed.Group.Basic
dist_norm_norm_le' : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] (a b : E), dist ‖a‖ ‖b‖ ≤ ‖a / b‖
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- For any circle integrable function `f`, the power series `cauchyPowerSeries f c R` multiplied
by `2πI` converges to the integral `∮ z in C(c, R), (z - w)⁻¹ • f z` on the open disc
`Metric.ball c R`.  -/
hasSum_two_pi_I_cauchyPowerSeries_integral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} {R : ℝ} {w : ℂ},
  CircleIntegrable f c R →
    ‖w‖ < R →
      HasSum (fun n => ∮ (z : ℂ) in C(c, R), (w / (z - c)) ^ n • (z - c)⁻¹ • f z)
        (∮ (z : ℂ) in C(c, R), (z - (c + w))⁻¹ • f z)
-- Batteries.Recycling.MonadSatisfying.Basic
MonadSatisfying.instStateRefT' : {m : Type → Type} →
  {ω σ : Type} → [inst : Monad m] → [inst_1 : LawfulMonad m] → [MonadSatisfying m] → MonadSatisfying (StateRefT' ω σ m)
-- Mathlib.GroupTheory.Torsion
CommGroup.map_torsion_le : ∀ {G : Type u_1} {H : Type u_2} [inst : CommGroup G] [inst_1 : CommGroup H] (f : G →* H),
  Subgroup.map f (CommGroup.torsion G) ≤ CommGroup.torsion H
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.mk : {X Y S : AlgebraicGeometry.Scheme} →
  {f : X ⟶ S} →
    {g : Y ⟶ S} → (x : ↥X) → (y : ↥Y) → (s : ↥S) → f x = s → g y = s → AlgebraicGeometry.Scheme.Pullback.Triplet f g
-- Lean.Elab.SyntheticMVars
/-- Pending synthetic metavariables cannot be postponed.
 -/
Lean.Elab.Term.PostponeBehavior.no : Lean.Elab.Term.PostponeBehavior
-- Mathlib.RingTheory.Congruence.Defs
/-- The quotient by a decidable congruence relation has decidable equality.  -/
RingCon.instDecidableEqQuotientOfDecidableCoeForallProp : {R : Type u_1} →
  [inst : Add R] → [inst_1 : Mul R] → (c : RingCon R) → [_d : (a b : R) → Decidable (c a b)] → DecidableEq c.Quotient
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforwardNatIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F G : CategoryTheory.Functor C D} {T : CategoryTheory.Sheaf J RingCat} {S : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] [inst_3 : G.IsContinuous J K] (φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S)
  (α : F ≅ G),
  (SheafOfModules.pushforwardNatIso φ α).inv =
    CategoryTheory.CategoryStruct.comp
      (SheafOfModules.pushforwardNatTrans
        (CategoryTheory.CategoryStruct.comp φ
          ((CategoryTheory.Functor.sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S))
        α.inv)
      (SheafOfModules.pushforwardCongr ⋯).hom
-- Mathlib.Computability.StateTransition
StateTransition.reaches_eval : ∀ {σ : Type u_1} {f : σ → Option σ} {a b : σ},
  StateTransition.Reaches f a b → StateTransition.eval f a = StateTransition.eval f b
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.instMin.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M],
  AddSubmonoid.instMin = { min := fun S₁ S₂ => { carrier := ↑S₁ ∩ ↑S₂, add_mem' := ⋯, zero_mem' := ⋯ } }
-- Lean.Data.JsonRpc
Lean.JsonRpc.ErrorCode.workerCrashed.sizeOf_spec : sizeOf Lean.JsonRpc.ErrorCode.workerCrashed = 1
-- Lean.Level
Lean.Level.mkData : UInt64 → optParam ℕ 0 → optParam Bool false → optParam Bool false → Lean.Level.Data
-- Mathlib.Analysis.Normed.Lp.lpSpace
memℓp_gen_iff' : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
  0 < p.toReal → (Memℓp f p ↔ ∀ (s : Finset α), ∑ i ∈ s, ‖f i‖ ^ p.toReal ≤ ∑' (i : α), ‖f i‖ ^ p.toReal)
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_top : ∀ {α : Type u_2} {a : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : OrderTop α],
  Finset.Ioc a ⊤ = Finset.Ioi a
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
String.reduceLE : Lean.Meta.Simp.Simproc