mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.Pass.mk.sizeOf_spec : ∀ (toConfig : Mathlib.TacticAnalysis.Config) (opt : Option (Lean.Option Bool)),
  sizeOf { toConfig := toConfig, opt := opt } = 1 + sizeOf toConfig + sizeOf opt
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- **Alias** of the reverse direction of `memℓp_norm_iff`. -/
Memℓp.norm : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
  Memℓp f p → Memℓp (fun x => ‖f x‖) p
-- Mathlib.Data.Int.Order.Lemmas
Int.natAbs_le_iff_mul_self_le : ∀ {a b : ℤ}, a.natAbs ≤ b.natAbs ↔ a * a ≤ b * b
-- Mathlib.CategoryTheory.Limits.Final
/-- See also the strictly more general `final_iff_comp_final_full_faithful` below.  -/
CategoryTheory.Functor.final_iff_comp_equivalence : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [G.IsEquivalence], F.Final ↔ (F.comp G).Final
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ofHoms_v_comp_d : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (ψ : (p : ℤ) → F.X p ⟶ G.X p) (p q q' : ℤ) (hpq : p + 0 = q),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.HomComplex.Cochain.ofHoms ψ).v p q hpq) (G.d q q') =
    CategoryTheory.CategoryStruct.comp (ψ p) (G.d p q')
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiffWithinAt_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {n : WithTop ℕ∞},
  ContMDiffWithinAt I I n id s x
-- Mathlib.Data.Nat.Count
Nat.count_iff_forall_not : ∀ {p : ℕ → Prop} [inst : DecidablePred p] {n : ℕ}, Nat.count p n = 0 ↔ ∀ m < n, ¬p m
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
HasFDerivWithinAt.tendsto_nhdsWithin_nhdsNE : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E},
  HasFDerivWithinAt f f' s x →
    (∃ C, AntilipschitzWith C ⇑f') → Filter.Tendsto f (nhdsWithin x (s \ {x})) (nhdsWithin (f x) {f x}ᶜ)
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.Context.mk.inj : ∀ {mainGoalDischarger : Lean.MVarId → Lean.MetaM Bool} {sideGoalDischarger : Lean.MVarId → Lean.MetaM Unit}
  {mainGoalDischarger_1 : Lean.MVarId → Lean.MetaM Bool} {sideGoalDischarger_1 : Lean.MVarId → Lean.MetaM Unit},
  { mainGoalDischarger := mainGoalDischarger, sideGoalDischarger := sideGoalDischarger } =
      { mainGoalDischarger := mainGoalDischarger_1, sideGoalDischarger := sideGoalDischarger_1 } →
    mainGoalDischarger = mainGoalDischarger_1 ∧ sideGoalDischarger = sideGoalDischarger_1
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.IsFirstQuadrant.isZero₂ : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Abelian C}
  {Y : CategoryTheory.Abelian.SpectralObject C EInt} [self : Y.IsFirstQuadrant] (i j : EInt) (hij : i ≤ j) (n : ℤ),
  WithBotTop.coe n < i →
    CategoryTheory.Limits.IsZero ((Y.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE hij)))
-- Std.Http.Data.Headers
/-- The underlying multimap that stores headers.
 -/
Std.Http.Headers.map : Std.Http.Headers → Std.Internal.IndexMultiMap Std.Http.Header.Name Std.Http.Header.Value
-- Mathlib.CategoryTheory.Limits.Preserves.Yoneda
CategoryTheory.yonedaYonedaColimit_app_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfShape J (Type v₁)]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J (Type (max u₁ v₁))]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor Cᵒᵖ (Type v₁))) {X : C},
  ((CategoryTheory.yonedaYonedaColimit F).app (Opposite.op X)).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation (F.comp CategoryTheory.yoneda)
          (CategoryTheory.yoneda.op.obj (Opposite.op X))).hom
      (CategoryTheory.Limits.colimit.post F (CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.yoneda.obj X))))
-- Mathlib.Order.CompleteLattice.SetLike
CompleteSublattice.mem_iInf : ∀ {X : Type u_1} {L : CompleteSublattice (Set X)} {I : Sort u_2} {f : I → ↥L} {x : X}, x ∈ ⨅ i, f i ↔ ∀ (i : I), x ∈ f i
-- Mathlib.Algebra.Star.Unitary
Unitary.instStarSubtypeMemSubmonoidUnitary : {R : Type u_1} → [inst : Monoid R] → [inst_1 : StarMul R] → Star ↥(unitary R)
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.re_eq_re_of_cexp_eq_cexp : ∀ {x y : ℂ}, Complex.exp x = Complex.exp y → x.re = y.re
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbit_subgroup_subset : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (H : Subgroup G) (a : α),
  MulAction.orbit (↥H) a ⊆ MulAction.orbit G a
-- Mathlib.Algebra.Ring.Subsemiring.Order
Subsemiring.nonneg_toAddSubmonoid : ∀ (R : Type u_1) [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R],
  (Subsemiring.nonneg R).toAddSubmonoid = AddSubmonoid.nonneg R
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.algebraEquivOfIsoMonads_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ : CategoryTheory.Monad C} (h : T₁ ≅ T₂),
  (CategoryTheory.Monad.algebraEquivOfIsoMonads h).inverse = CategoryTheory.Monad.algebraFunctorOfMonadHom h.hom
-- Mathlib.Data.Set.Countable
Set.Countable.union : ∀ {α : Type u} {s t : Set α}, s.Countable → t.Countable → (s ∪ t).Countable
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.proj_eq_of_subset : ∀ {I : Type u} (C : Set (I → Bool)) (J K : I → Prop) [inst : (i : I) → Decidable (J i)]
  [inst_1 : (i : I) → Decidable (K i)],
  (∀ (i : I), J i → K i) → Profinite.NobelingProof.π (Profinite.NobelingProof.π C K) J = Profinite.NobelingProof.π C J
-- Mathlib.Data.Ordmap.Invariants
Ordnode.splitMax_eq : ∀ {α : Type u_1} (s : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α),
  l.splitMax' x r = ((Ordnode.node s l x r).eraseMax, Ordnode.findMax' x r)
-- Init.Data.Nat.Lemmas
Nat.div_pow : ∀ {a b c : ℕ}, a ∣ b → (b / a) ^ c = b ^ c / a ^ c
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedCommGroup.ofMulDist.eq_1 : ∀ {E : Type u_5} [inst : Norm E] [inst_1 : CommGroup E] [inst_2 : PseudoMetricSpace E] (h₁ : ∀ (x : E), ‖x‖ = dist 1 x)
  (h₂ : ∀ (x y z : E), dist x y ≤ dist (z * x) (z * y)),
  SeminormedCommGroup.ofMulDist h₁ h₂ =
    { toNorm := (SeminormedGroup.ofMulDist h₁ h₂).toNorm, toGroup := (SeminormedGroup.ofMulDist h₁ h₂).toGroup,
      mul_comm := ⋯, toPseudoMetricSpace := (SeminormedGroup.ofMulDist h₁ h₂).toPseudoMetricSpace, dist_eq := ⋯ }
-- Mathlib.Algebra.Azumaya.Basic
/-- An Azumaya algebra is a central algebra.  -/
Algebra.IsCentral.instIsAzumaya : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [Module.Free R A]
  [IsAzumaya R A], Algebra.IsCentral R A
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.mem_stabilizer_set_iff_smul_set_subset : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {a : G} {s : Set α},
  s.Finite → (a ∈ MulAction.stabilizer G s ↔ a • s ⊆ s)
-- Lean.Data.Lsp.CodeActions
/-- The kind of the code action.  -/
Lean.Lsp.CodeAction.kind? : Lean.Lsp.CodeAction → Option Lean.Lsp.CodeActionKind
-- Mathlib.Algebra.Exact.Basic
Function.MulExact.of_ladder_mulEquiv_of_mulExact : ∀ {X₁ : Type u_8} {X₂ : Type u_9} {X₃ : Type u_10} {Y₁ : Type u_11} {Y₂ : Type u_12} {Y₃ : Type u_13}
  [inst : CommMonoid X₁] [inst_1 : CommMonoid X₂] [inst_2 : CommMonoid X₃] [inst_3 : CommMonoid Y₁]
  [inst_4 : CommMonoid Y₂] [inst_5 : CommMonoid Y₃] (e₁ : X₁ ≃* Y₁) (e₂ : X₂ ≃* Y₂) (e₃ : X₃ ≃* Y₃) {f₁₂ : X₁ →* X₂}
  {f₂₃ : X₂ →* X₃} {g₁₂ : Y₁ →* Y₂} {g₂₃ : Y₂ →* Y₃},
  g₁₂.comp ↑e₁ = (↑e₂).comp f₁₂ →
    g₂₃.comp ↑e₂ = (↑e₃).comp f₂₃ → Function.MulExact ⇑f₁₂ ⇑f₂₃ → Function.MulExact ⇑g₁₂ ⇑g₂₃
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instAddCommGroup : {k : Type u_1} → {G : Type u_2} → [inst : AddCommGroup k] → AddCommGroup (SkewMonoidAlgebra k G)
-- Mathlib.CategoryTheory.Linear.Yoneda
CategoryTheory.linearYoneda_obj_obj_carrier : ∀ (R : Type w) [inst : Ring R] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] (X : C) (Y : Cᵒᵖ),
  ↑(((CategoryTheory.linearYoneda R C).obj X).obj Y) = (Opposite.unop Y ⟶ X)
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.haveLebesgueDecompositionRnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α),
  (ν.withDensity (μ.rnDeriv ν)).HaveLebesgueDecomposition ν
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_toArray : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → m.toArray.size = m.size
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Set.Finite.toFinset_zero : ∀ {α : Type u_2} [inst : Zero α] (h : optParam (Set.Finite 0) ⋯), h.toFinset = 0
-- Mathlib.RingTheory.WittVector.Compare
WittVector.toPadicInt_comp_fromPadicInt : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], (WittVector.toPadicInt p).comp (WittVector.fromPadicInt p) = RingHom.id ℤ_[p]
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The `vectorSpan` of a family indexed by a `Fintype` is
finite-dimensional.  -/
finiteDimensional_vectorSpan_range : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [Finite ι] (p : ι → P),
  FiniteDimensional k ↥(vectorSpan k (Set.range p))
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Inhabited α]
  {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey! k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
      ((Std.Internal.List.getKey? k l).pfilter fun x h => (f x (Std.Internal.List.getValueCast x l ⋯)).isSome).get!
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.iSup_toSubsemiring : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {ι : Sort u_1}
  [Nonempty ι] (S : ι → Subalgebra R A), (iSup S).toSubsemiring = ⨆ i, (S i).toSubsemiring
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.instNonUnitalSemiring : {ι : Type u_1} →
  {R : Type u_3} →
    {A : ι → Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → NonUnitalSemiring (A i)] →
          [inst_2 : (i : ι) → Module R (A i)] →
            [∀ (i : ι), SMulCommClass R (A i) (A i)] →
              [∀ (i : ι), IsScalarTower R (A i) (A i)] → NonUnitalSemiring (PiTensorProduct R fun i => A i)
-- Lean.Elab.Calc
/-- Adds a type annotation to a hole that occurs immediately at the beginning of the term.
This is so that coercions can trigger when elaborating the term.
See https://github.com/leanprover/lean4/issues/2040 for further rationale.

- `_ < 3` is annotated
- `(_) < 3` is not, because it occurs after an atom
- in `_ < _` only the first one is annotated
- `_ + 2 < 3` is annotated (not the best heuristic, ideally we'd like to annotate `_ + 2`)
- `lt _ 3` is not, because it occurs after an identifier
 -/
Lean.Elab.Term.annotateFirstHoleWithType : Lean.Term → Lean.Expr → Lean.Elab.TermElabM Lean.Term
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasProd.compl_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a b : α}
  [ContinuousMul α] {s : Set β}, HasProd (f ∘ Subtype.val) a → HasProd (f ∘ Subtype.val) b → HasProd f (a * b)
-- Init.Data.UInt.Lemmas
UInt8.mod_lt : ∀ (a : UInt8) {b : UInt8}, 0 < b → a % b < b
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.wideCoequalizer.condition : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : J → (X ⟶ Y))
  [inst_1 : CategoryTheory.Limits.HasWideCoequalizer f] (j₁ j₂ : J),
  CategoryTheory.CategoryStruct.comp (f j₁) (CategoryTheory.Limits.wideCoequalizer.π f) =
    CategoryTheory.CategoryStruct.comp (f j₂) (CategoryTheory.Limits.wideCoequalizer.π f)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.zero_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : AddZeroClass α] [inst_4 : AddZeroClass β] [inst_5 : AddZeroClass γ] (f : α →+o β),
  OrderAddMonoidHom.comp 0 f = 0
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Expr.toPoly.match_1.eq_5 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast n))
  (h_3 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (x : Lean.Grind.CommRing.Expr) → motive x),
  (∀ (n : ℤ), x = Lean.Grind.CommRing.Expr.num n → False) →
    (∀ (n : ℤ), x = Lean.Grind.CommRing.Expr.intCast n → False) →
      (∀ (n : ℕ), x = Lean.Grind.CommRing.Expr.natCast n → False) →
        (∀ (x_4 : Lean.Grind.CommRing.Var), x = Lean.Grind.CommRing.Expr.var x_4 → False) →
          (match x with
            | Lean.Grind.CommRing.Expr.num n => h_1 n
            | Lean.Grind.CommRing.Expr.intCast n => h_2 n
            | Lean.Grind.CommRing.Expr.natCast n => h_3 n
            | Lean.Grind.CommRing.Expr.var x => h_4 x
            | x => h_5 x) =
            h_5 x
-- Mathlib.Analysis.Calculus.FDeriv.Mul
differentiableWithinAt_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {R : Type u_5} [inst_1 : NormedDivisionRing R]
  [inst_2 : NormedAlgebra 𝕜 R] {x : R}, x ≠ 0 → ∀ (s : Set R), DifferentiableWithinAt 𝕜 (fun x => x⁻¹) s x
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.kronecker_mulVec_vec : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_4} {p : Type u_5} {R : Type u_3} [inst : NonUnitalCommSemiring R]
  [inst_1 : Fintype m] [inst_2 : Fintype n] (A : Matrix l m R) (X : Matrix m n R) (B : Matrix p n R),
  (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) B A).mulVec X.vec = (A * X * B.transpose).vec
-- Init.Data.Array.Lemmas
Array.getElem?_pop : ∀ {α : Type u_1} {xs : Array α} {i : ℕ}, xs.pop[i]? = if i < xs.size - 1 then xs[i]? else none
-- Mathlib.GroupTheory.Coprod.Basic
MulEquiv.coprodAssoc_symm_apply_inr_inl : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Monoid P] (x : N),
  (MulEquiv.coprodAssoc M N P).symm (Monoid.Coprod.inr (Monoid.Coprod.inl x)) = Monoid.Coprod.inl (Monoid.Coprod.inr x)
-- Aesop.Tree.UnsafeQueue
Aesop.UnsafeQueueEntry.instOrd : Ord Aesop.UnsafeQueueEntry
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.opNNNorm_pi : ∀ {𝕜 : Type u} {ι : Type v} {ι' : Type v'} {E : ι → Type wE} {E' : ι' → Type wE'} [inst : Fintype ι']
  [inst_1 : NontriviallyNormedField 𝕜] [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_4 : Fintype ι] [inst_5 : (i' : ι') → SeminormedAddCommGroup (E' i')]
  [inst_6 : (i' : ι') → NormedSpace 𝕜 (E' i')] (f : (i' : ι') → ContinuousMultilinearMap 𝕜 E (E' i')),
  ‖ContinuousMultilinearMap.pi f‖₊ = ‖f‖₊
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Reorder a product.

The difference with `Finset.prod_nbij'` is that the bijection is specified as a surjective
injection, rather than by an inverse function.

The difference with `Finset.prod_bij` is that the bijection is a non-dependent function, rather than
being allowed to use membership of the domain of the product.  -/
Finset.prod_nbij : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : CommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M}
  {g : κ → M} (i : ι → κ),
  (∀ a ∈ s, i a ∈ t) → Set.InjOn i ↑s → Set.SurjOn i ↑s ↑t → (∀ a ∈ s, f a = g (i a)) → ∏ x ∈ s, f x = ∏ x ∈ t, g x
-- Mathlib.Analysis.Fourier.AddCircle
AddCircle.instIsAddHaarMeasureRealHaarAddCircle : ∀ {T : ℝ} [hT : Fact (0 < T)], AddCircle.haarAddCircle.IsAddHaarMeasure
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.piEquivL_symm_apply : ∀ (𝕜 : Type u_1) [inst : NormedField 𝕜] (E : Type u_2) {ι : Type u_3} (F : ι → Type u_4) [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : (i : ι) → AddCommGroup (F i)]
  [inst_5 : (i : ι) → Module 𝕜 (F i)] [inst_6 : (i : ι) → TopologicalSpace (F i)]
  [inst_7 : ∀ (i : ι), IsTopologicalAddGroup (F i)] [inst_8 : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)]
  (f : E →L[𝕜] (i : ι) → F i) (i : ι), (ContinuousLinearMap.piEquivL 𝕜 E F).symm f i = ContinuousLinearMap.proj i ∘SL f
-- Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
/-- `MulAction.stabilizer (alternatingGroup α) s` is a maximal subgroup of `alternatingGroup α`,
provided `s ≠ ∅`, `sᶜ ≠ ∅` and `Nat.card α ≠ 2 * s.ncard`.

This is the intransitive case of the O'Nan–Scott classification.  -/
alternatingGroup.isCoatom_stabilizer : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Set α},
  s.Nonempty → sᶜ.Nonempty → Nat.card α ≠ 2 * s.ncard → IsCoatom (MulAction.stabilizer (↥(alternatingGroup α)) s)
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.eval₂.eq_1 : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] (φ : R →+* S) (a : σ → S) (f : MvPowerSeries σ R),
  MvPowerSeries.eval₂ φ a f =
    if H : ∃ p, ↑p = f then MvPolynomial.eval₂ φ a H.choose else ⋯.extend (MvPolynomial.eval₂ φ a) f
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.extendToSucc_obj_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (hj : ¬IsMax j) (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {X : C}
  (τ : F.obj ⟨j, ⋯⟩ ⟶ X) (i : J) (hi : i ≤ j),
  (CategoryTheory.SmallObject.SuccStruct.extendToSucc hj F τ).obj ⟨i, ⋯⟩ = F.obj ⟨i, hi⟩
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of `Left.one_lt_inv_iff`.

---

Uses `left` co(ntra)variant.  -/
one_lt_inv' : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a : α}, 1 < a⁻¹ ↔ a < 1
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.toList_symm : ∀ {α : Type u_1}, FreeMonoid.toList.symm = FreeMonoid.ofList
-- Mathlib.Data.Set.Insert
/-- **Alias** of `Set.insert_sdiff_eq_singleton`. -/
Set.insert_diff_eq_singleton : ∀ {α : Type u_1} {a : α} {s : Set α}, a ∉ s → insert a s \ s = {a}
-- Init.Data.SInt.Bitwise
UInt8.toInt8_or : ∀ (a b : UInt8), (a ||| b).toInt8 = a.toInt8 ||| b.toInt8
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A binary bicone for a pair of objects `P Q : C` consists of the cone point `X`,
maps from `X` to both `P` and `Q`, and maps from both `P` and `Q` to `X`,
so that `inl ≫ fst = 𝟙 P`, `inl ≫ snd = 0`, `inr ≫ fst = 0`, and `inr ≫ snd = 𝟙 Q`  -/
CategoryTheory.Limits.BinaryBicone : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] → [CategoryTheory.Limits.HasZeroMorphisms C] → C → C → Type (max uC uC')
-- Mathlib.Logic.Function.Defs
Function.comp_assoc : ∀ {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} (f : φ → δ) (g : β → φ) (h : α → β), (f ∘ g) ∘ h = f ∘ g ∘ h
-- Mathlib.Topology.Separation.Hausdorff
t2_separation_compact_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyCompactSpace X] [T2Space X] {x y : X},
  x ≠ y → ∃ u v, u ∈ nhds x ∧ v ∈ nhds y ∧ IsCompact u ∧ IsCompact v ∧ Disjoint u v
-- Mathlib.Algebra.Category.Grp.Yoneda
AddCommGrpCat.coyonedaForget_hom_app_app_hom_apply_hom : ∀ (X : AddCommGrpCatᵒᵖ) (X_1 : AddCommGrpCat) (f : ↑(Opposite.unop X) →+ ↑X_1),
  AddCommGrpCat.Hom.hom ((CategoryTheory.ConcreteCategory.hom ((AddCommGrpCat.coyonedaForget.hom.app X).app X_1)) f) = f
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.instBraidedCategoryDiscrete : (M : Type u) → [inst : CommMonoid M] → CategoryTheory.BraidedCategory (CategoryTheory.Discrete M)
-- Init.Data.Iterators.Basic
/-- `IterStep.skip it` describes the situation that an iterator does not emit anything in this
iteration and provides `it'` as the succeeding iterator.

Allowing `skip` steps is necessary to generate efficient code from a loop over an iterator.
 -/
Std.IterStep.skip : {α : Sort u_1} → {β : Sort u_2} → α → Std.IterStep α β
-- Mathlib.Algebra.Algebra.Opposite
/-- An algebra hom `A →ₐ[R] B` can equivalently be viewed as an algebra hom `Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ`.
This is the action of the (fully faithful) `ᵐᵒᵖ`-functor on morphisms.  -/
AlgHom.op : {R : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A →ₐ[R] B) ≃ (Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ)
-- Mathlib.Topology.Order.SuccPred
AccPt.not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [SuccOrder α] [NoMaxOrder α]
  {a : α} {s : Set α}, AccPt a (Filter.principal s) → ¬IsMin a
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.opNorm_smul_le : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι] {𝕜' : Type u_1}
  [inst_6 : SeminormedRing 𝕜'] [inst_7 : Module 𝕜' G] [inst_8 : IsBoundedSMul 𝕜' G] [inst_9 : SMulCommClass 𝕜 𝕜' G]
  (c : 𝕜') (f : ContinuousMultilinearMap 𝕜 E G), ‖c • f‖ ≤ ‖c‖ * ‖f‖
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.evariance_lt_top_iff_memLp : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.AEStronglyMeasurable X μ → (ProbabilityTheory.evariance X μ < ⊤ ↔ MeasureTheory.MemLp X 2 μ)
-- Mathlib.CategoryTheory.Join.Sum
/-- The canonical functor from the sum to the join.
It sends `inl c` to `left c` and `inr d` to `right d`.  -/
CategoryTheory.Join.fromSum : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] → CategoryTheory.Functor (C ⊕ D) (CategoryTheory.Join C D)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.const.sizeOf_spec : ∀ (a : Lean.Name) (a_1 : ℕ), sizeOf (Lean.Meta.LazyDiscrTree.Key.const a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrixAlgEquiv'_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (f g : (n → R) →ₗ[R] n → R),
  LinearMap.toMatrixAlgEquiv' (f * g) = LinearMap.toMatrixAlgEquiv' f * LinearMap.toMatrixAlgEquiv' g
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Protoset.instInhabited : {G : Type u_1} →
  {X : Type u_2} →
    {ιₚ : Type u_3} → [inst : Group G] → [inst_1 : MulAction G X] → Inhabited (DiscreteTiling.Protoset G X ιₚ)
-- Mathlib.Topology.UniformSpace.Cauchy
SequentiallyComplete.seq_mem : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α}
  (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) (n : ℕ),
  SequentiallyComplete.seq hf U_mem n ∈ SequentiallyComplete.setSeq hf U_mem n