mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- The Lie bracket of vector fields in manifolds satisfies the Leibniz identity
`[U, [V, W]] = [[U, V], W] + [V, [U, W]]` (also called Jacobi identity).  -/
VectorField.leibniz_identity_mlieBracketWithin_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I (minSmoothness 𝕜 3) M]
  [CompleteSpace E] {U V W : (x : M) → TangentSpace I x} {s : Set M} {x : M},
  UniqueMDiff[s] →
    x ∈ closure (interior s) →
      x ∈ s →
        ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x => ⟨x, U x⟩) s x →
          ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x => ⟨x, V x⟩) s x →
            ContMDiffWithinAt I I.tangent (minSmoothness 𝕜 2) (fun x => ⟨x, W x⟩) s x →
              VectorField.mlieBracketWithin I U (VectorField.mlieBracketWithin I V W s) s x =
                VectorField.mlieBracketWithin I (VectorField.mlieBracketWithin I U V s) W s x +
                  VectorField.mlieBracketWithin I V (VectorField.mlieBracketWithin I U W s) s x
-- Mathlib.Algebra.Category.Grp.FiniteGrp
FiniteGrp.isFinite : ∀ (self : FiniteGrp.{u}), Finite ↑self.toGrp
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.adjoint.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F],
  LinearMap.adjoint =
    (LinearMap.toContinuousLinearMap.trans ContinuousLinearMap.adjoint.toLinearEquiv).trans
      LinearMap.toContinuousLinearMap.symm
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.toSingleMk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f f_1 : K.X p ⟶ X)
  (e_f : f = f_1) {n : ℤ} (h : p + n = q) (p' p'_1 : ℤ) (e_p' : p' = p'_1) (hp' : p' + 1 = p)
  (hf : CategoryTheory.CategoryStruct.comp (K.d p' p) f = 0),
  CochainComplex.HomComplex.Cocycle.toSingleMk f h p' hp' hf =
    CochainComplex.HomComplex.Cocycle.toSingleMk f_1 h p'_1 ⋯ ⋯
-- Std.Http.Server.Connection
/-- Applies a successful handler response to the machine.
Optionally injects a `Date` header, records the known body size, and sends the
response head. Returns the updated machine and the body stream to drain, or `none`
when the body should be omitted (e.g., for HEAD requests).
 -/
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.applyResponse : {β : Type} →
  [Std.Http.Body β] →
    Std.Http.Config →
      Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving →
        Std.Http.Response β →
          Std.Async.Async (Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving × Option β)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiff_of_locally_contMDiffOn : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {n : WithTop ℕ∞},
  (∀ (x : M), ∃ u, IsOpen u ∧ x ∈ u ∧ ContMDiffOn I I' n f u) → ContMDiff I I' n f
-- Mathlib.Data.Set.Lattice
Set.Nonempty.of_sUnion_eq_univ : ∀ {α : Type u_1} [Nonempty α] {s : Set (Set α)}, ⋃₀ s = Set.univ → s.Nonempty
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.isUnit_iff : ∀ {n : ℕ} (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)), c.isUnit = some l ↔ c.toList = [l]
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.corootSubmodule.congr_simp : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  (α α_1 : LieModule.Weight K (↥H) L),
  α = α_1 → LieAlgebra.IsKilling.corootSubmodule α = LieAlgebra.IsKilling.corootSubmodule α_1
-- Mathlib.Order.Category.Lat
Lat.ofHom_apply : ∀ {X Y : Type u} [inst : Lattice X] [inst_1 : Lattice Y] (f : LatticeHom X Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (Lat.ofHom f)) x = f x
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.smul_restrictAppIso_hom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules)
  (U : X.Opens) (r : ↑(X.presheaf.obj (Opposite.op U))),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.smul r)
      (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).hom =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).hom
      (AlgebraicGeometry.Scheme.Modules.smul
        ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso f U).inv) r))
-- Mathlib.CategoryTheory.Category.Preorder
CategoryTheory.homOfLE_comp_eqToHom : ∀ {X : Type u} [inst : Preorder X] {a b c : X} (hab : a ≤ b) (hbc : b = c),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE hab) (CategoryTheory.eqToHom hbc) =
    CategoryTheory.homOfLE ⋯
-- Mathlib.Topology.Bases
TopologicalSpace.FirstCountableTopology.tendsto_subseq : ∀ {α : Type u} [t : TopologicalSpace α] [FirstCountableTopology α] {u : ℕ → α} {x : α},
  MapClusterPt x Filter.atTop u → ∃ ψ, StrictMono ψ ∧ Filter.Tendsto (u ∘ ψ) Filter.atTop (nhds x)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The group structure.  -/
ProfiniteGrp.group : (self : ProfiniteGrp.{u}) → Group ↑self.toProfinite.toTop
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.ofFactorizationData_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {A : C}
  (h :
    (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C)
      (CategoryTheory.Limits.codiag A)),
  (HomotopicalAlgebra.Cylinder.ofFactorizationData h).π = h.p
-- Mathlib.Algebra.Homology.HomologicalBicomplex
/-- Flipping a complex of complexes over the diagonal, as a functor.  -/
HomologicalComplex₂.flipFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          (c₁ : ComplexShape I₁) →
            (c₂ : ComplexShape I₂) → CategoryTheory.Functor (HomologicalComplex₂ C c₁ c₂) (HomologicalComplex₂ C c₂ c₁)
-- Mathlib.Algebra.GroupWithZero.Subgroup
Subgroup.pointwise_smul_le_pointwise_smul_iff₀ : ∀ {G₀ : Type u_1} {G : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Group G] [inst_2 : MulDistribMulAction G₀ G]
  {S T : Subgroup G} {a : G₀}, a ≠ 0 → (a • S ≤ a • T ↔ S ≤ T)
-- Init.Data.String.Lemmas.Splits
String.Slice.copy_sliceFrom_eq_iff_splits : ∀ {s : String.Slice} {p : s.Pos} {t₂ : String}, (s.sliceFrom p).copy = t₂ ↔ p.Splits (s.sliceTo p).copy t₂
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.eval_eq_eval_mv_eval' : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} (s : Fin n → R) (y : R) (f : MvPolynomial (Fin (n + 1)) R),
  (MvPolynomial.eval (Fin.cons y s)) f =
    Polynomial.eval y (Polynomial.map (MvPolynomial.eval s) ((MvPolynomial.finSuccEquiv R n) f))
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.«grind_filterGen=_» : Lean.ParserDescr
-- Init.Data.List.MinMaxIdx
List.minIdxOn?_cons_eq_some_minIdxOn : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {x : α} {xs : List α},
  List.minIdxOn? f (x :: xs) = some (List.minIdxOn f (x :: xs) ⋯)
-- Init.Data.Array.Monadic
/-- We can express a for loop over an array which always yields as a fold.  -/
Array.forIn_yield_eq_foldlM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β γ : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Array α}
  (f : α → β → m γ) (g : α → β → γ → β) (init : β),
  (forIn xs init fun a b => (fun c => ForInStep.yield (g a b c)) <$> f a b) =
    Array.foldlM (fun b a => g a b <$> f a b) init xs
-- Mathlib.Topology.Convenient.GeneratedBy
/-- The homeomorphism `WithGeneratedByTopology X Y ≃ₜ Y` when `Y` is `X`-generated.  -/
Topology.IsGeneratedBy.homeomorph : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {Y : Type v} →
        [tY : TopologicalSpace Y] → [Topology.IsGeneratedBy X Y] → Topology.WithGeneratedByTopology X Y ≃ₜ Y
-- Std.Time.Zoned.ZoneRules
/-- Represents a time zone transition, mapping a time to a local time type.
 -/
Std.Time.TimeZone.Transition : Type
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Pullbacks
CategoryTheory.Limits.HasPullback.of_createsLimit : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S)
  [CategoryTheory.CreatesLimit (CategoryTheory.Limits.cospan f g) F]
  [CategoryTheory.Limits.HasPullback (F.map f) (F.map g)], CategoryTheory.Limits.HasPullback f g
-- Mathlib.Data.Vector3
Fin2.left.eq_1 : ∀ (k n : ℕ), Fin2.left k Fin2.fz = Fin2.fz
-- Init.Data.List.Lemmas
List.filterMap_some_fun : ∀ {α : Type u_1}, List.filterMap some = id
-- Lean.Declaration
Lean.QuotKind.lift.sizeOf_spec : sizeOf Lean.QuotKind.lift = 1
-- Mathlib.Topology.Order.ExtendFrom
continuousOn_Ico_extendFrom_Ioo : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [DenselyOrdered α]
  [OrderTopology α] [inst_4 : TopologicalSpace β] {f : α → β} {a b : α} {la : β} [RegularSpace β],
  ContinuousOn f (Set.Ioo a b) →
    Filter.Tendsto f (nhdsWithin a (Set.Ioi a)) (nhds la) → ContinuousOn (extendFrom (Set.Ioo a b) f) (Set.Ico a b)
-- Init.Data.Int.Gcd
Int.gcd_sub_left_right_of_dvd : ∀ {n k : ℤ} (m : ℤ), n ∣ k → n.gcd (k - m) = n.gcd m
-- Mathlib.Data.Rat.Cast.Defs
Rat.cast_one : ∀ {α : Type u_3} [inst : DivisionRing α], ↑1 = 1
-- Mathlib.RingTheory.Kaehler.Basic
Derivation.tensorProductTo_tmul : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (D : Derivation R S M) (s t : S), D.tensorProductTo (s ⊗ₜ[R] t) = s • D t
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.hasPullback_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁)
  (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄]
  [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃)
      f₄],
  CategoryTheory.Limits.HasPullback f₁
    (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.eval.eq_3 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor F R) (ι : C → Type (max u v))
  (t : (X : C) → ι X → F.obj (Opposite.op X)) (x : C) (R : CategoryTheory.Presieve x) (hR : R ∈ K.coverings x)
  (h : ⦃W : C⦄ → (r : W ⟶ x) → R r → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι W),
  CategoryTheory.Precoverage.SmallConstruction.Witness.eval✝ hF ι t
      (CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate✝ hR h) =
    if hall :
        ∀ (W : C) (r : W ⟶ x) (hr : R r),
          ((fun W r hr => CategoryTheory.Precoverage.SmallConstruction.Witness.eval✝ hF ι t (h r hr)) W r hr).isSome =
            true then
      have y := fun x_1 x_2 hr =>
        ((fun W r hr => CategoryTheory.Precoverage.SmallConstruction.Witness.eval✝ hF ι t (h r hr)) x_1 x_2 hr).get ⋯;
      if hy : y.Compatible then some (Exists.choose ⋯) else none
    else none
-- Mathlib.RingTheory.Polynomial.Pochhammer
/-- `descPochhammer S n` is positive on `(n-1, ∞)`.  -/
descPochhammer_pos : ∀ {S : Type u_1} [inst : Ring S] [inst_1 : PartialOrder S] [IsStrictOrderedRing S] {n : ℕ} {s : S},
  ↑n - 1 < s → 0 < Polynomial.eval s (descPochhammer S n)
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeIsoApp'_tensor : ∀ (C : Type u) (X Y : CategoryTheory.FreeMonoidalCategory C)
  (n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C),
  CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) n =
    (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.FreeMonoidalCategory.inclusionObj n) X Y).symm ≪≫
      CategoryTheory.MonoidalCategory.whiskerRightIso (CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C X n) Y ≪≫
        CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C Y (X.normalizeObj n)
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.limitsClosure.brecOn : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {α : Type t}
  {J : α → Type u'} [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)]
  {motive : (a : C) → P.limitsClosure J a → Prop} {a : C} (t : P.limitsClosure J a),
  (∀ (a : C) (t : P.limitsClosure J a), CategoryTheory.ObjectProperty.limitsClosure.below t → motive a t) → motive a t
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
/-- An integrability criterion for the continuous functional calculus.
For a version with stronger assumptions which in practice are often easier to verify, see
`integrable_cfcₙ`.  -/
integrable_cfcₙ' : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NonUnitalNormedRing A] [inst_3 : StarRing A] [inst_4 : NormedSpace 𝕜 A]
  [inst_5 : IsScalarTower 𝕜 A A] [inst_6 : SMulCommClass 𝕜 A A] [inst_7 : NonUnitalContinuousFunctionalCalculus 𝕜 A p]
  [inst_8 : CompleteSpace A] (f : X → 𝕜 → 𝕜) (a : A),
  MeasureTheory.Integrable (fun x => ContinuousMapZero.mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ →
    autoParam (p a) integrable_cfcₙ'._auto_1 → MeasureTheory.Integrable (fun x => cfcₙ (f x) a) μ
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.toExtension_Ring : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι), P.toExtension.Ring = P.Ring
-- Mathlib.Data.Finset.Powerset
/-- Given an integer `n` and a finset `s`, then `powersetCard n s` is the finset of subsets of `s`
of cardinality `n`.  -/
Finset.powersetCard : {α : Type u_1} → ℕ → Finset α → Finset (Finset α)
-- Mathlib.MeasureTheory.Measure.PreVariation
MeasureTheory.preVariationFun_of_not_measurableSet : ∀ {X : Type u_1} [inst : MeasurableSpace X] (f : Set X → ENNReal) {s : Set X},
  ¬MeasurableSet s → MeasureTheory.preVariationFun f s = 0
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ} {k k' : α} {fallback : γ},
  m.getKey? k = some k' →
    Std.DHashMap.Const.getD (Std.DHashMap.filterMap f m) k fallback =
      ((Std.DHashMap.Const.get? m k).bind (f k')).getD fallback
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.bitblast_aig_IsPrefix : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
  (input : Std.Tactic.BVDecide.BVExpr.WithCache (Std.Tactic.BVDecide.BVExpr w) aig),
  Std.Sat.AIG.IsPrefix aig.decls (↑(Std.Tactic.BVDecide.BVExpr.bitblast aig input).result).aig.decls
-- Mathlib.Algebra.Homology.Precylinder
HomologicalComplex.prepathObject_P : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} [inst_2 : DecidableRel c.Rel] (K : HomologicalComplex C c)
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject],
  K.prepathObject.P = K.pathObject
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.termIh : Lean.ParserDescr
-- Mathlib.Logic.Basic
/-- **Alias** of `propext`. -/
Iff.eq : ∀ {a b : Prop}, (a ↔ b) → a = b
-- Init.Data.Iterators.Combinators.Monadic.ULift
Std.Iterators.Types.ULiftIterator.instIterator : {α : Type u} →
  {m : Type u → Type u'} →
    {n : Type (max u v) → Type v'} →
      {β : Type u} →
        {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} →
          [Std.Iterator α m β] →
            [Monad n] → Std.Iterator (Std.Iterators.Types.ULiftIterator α m n β lift) n (ULift.{v, u} β)
-- Mathlib.Topology.Order.WithTop
/-- If `ι` has a top element, then `WithTop ι` is homeomorphic to `ι ⊕ Unit`.  -/
WithTop.sumHomeomorph : (ι : Type u_1) →
  [inst : LinearOrder ι] →
    [inst_1 : TopologicalSpace ι] → [inst_2 : OrderTopology ι] → [OrderTop ι] → WithTop ι ≃ₜ ι ⊕ Unit
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPolyC.go.match_4.congr_eq_1 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) (k : ℤ),
  x = Lean.Grind.CommRing.Expr.num k →
    (match x with
      | Lean.Grind.CommRing.Expr.num k => h_1 k
      | Lean.Grind.CommRing.Expr.natCast k => h_2 k
      | Lean.Grind.CommRing.Expr.intCast k => h_3 k
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | a.add b => h_5 a b
      | a.mul b => h_6 a b
      | a.neg => h_7 a
      | a.sub b => h_8 a b
      | a.pow k => h_9 a k) ≍
      h_1 k
-- Lean.PrettyPrinter.Parenthesizer
/-- Adds necessary parentheses to the syntax in the given category (for example, `term`, `tactic`, or `command`).
 -/
Lean.PrettyPrinter.parenthesizeCategory : Lean.Name → Lean.Syntax → Lean.CoreM Lean.Syntax
-- Mathlib.Data.Real.Pointwise
Real.smul_iInf_of_nonpos : ∀ {ι : Sort u_1} {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Module α ℝ]
  [IsOrderedModule α ℝ] {a : α}, a ≤ 0 → ∀ (f : ι → ℝ), a • ⨅ i, f i = ⨆ i, a • f i
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instNegZeroClass.eq_1 : ∀ {α : Type u} [inst : Neg α],
  WithZero.instNegZeroClass = { toZero := WithZero.instZero, toNeg := WithZero.instNeg, neg_zero := ⋯ }
-- Lean.Server.References
/-- Result of `filterMapMod`.  -/
Lean.Server.References.MatchedDefinition.mod : {α : Type} → Lean.Server.References.MatchedDefinition α → Lean.Name
-- Init.Grind.AC
Lean.Grind.AC.simp_suffix_cert : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Bool
-- Mathlib.Topology.Order.ScottTopology
/-- If `α` is equipped with the Scott topology, then it is homeomorphic to `WithScott α`.
 -/
Topology.IsScott.withScottHomeomorph : {α : Type u_1} →
  [inst : Preorder α] → [inst_1 : TopologicalSpace α] → [Topology.IsScott α Set.univ] → Topology.WithScott α ≃ₜ α
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- A group is finitely presented if it has a finite generating set such that the kernel
of the induced map from the free group on that set is the normal closure of finitely many
relations.  -/
Group.IsFinitelyPresented : (G : Type u_5) → [Group G] → Prop
-- Mathlib.SetTheory.Ordinal.Notation
ONote.repr_opow_aux₂ : ∀ {a0 a' : ONote} [N0 : a0.NF] [Na' : a'.NF] (m : ℕ),
  Ordinal.omega0 ∣ a'.repr →
    a0.repr ≠ 0 →
      a'.repr + ↑m < Ordinal.omega0 ^ a0.repr →
        ∀ (n : ℕ+) (k : ℕ),
          have R := (ONote.opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr;
          (k ≠ 0 → R < (Ordinal.omega0 ^ a0.repr) ^ Order.succ ↑k) ∧
            (Ordinal.omega0 ^ a0.repr) ^ ↑k * (Ordinal.omega0 ^ a0.repr * ↑↑n + a'.repr) + R =
              (Ordinal.omega0 ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ Order.succ ↑k
-- Init.SimpLemmas
ite_cond_eq_false : ∀ {α : Sort u} {c : Prop} {x : Decidable c} (a b : α), c = False → (if c then a else b) = b
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedNewRawFact : Inhabited Lean.Meta.Grind.NewRawFact
-- Mathlib.RingTheory.Jacobson.Ring
/-- A variant of `isJacobsonRing_of_isIntegral` that takes `RingHom.IsIntegral` instead.  -/
isJacobsonRing_of_isIntegral' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  f.IsIntegral → ∀ [IsJacobsonRing R], IsJacobsonRing S
-- Mathlib.Analysis.Analytic.Constructions
analyticAt_neg : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E},
  AnalyticAt 𝕜 (-f) x ↔ AnalyticAt 𝕜 f x
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- Galois insertion between `adjoin` and `SetLike.coe`.  -/
NonUnitalStarAlgebra.gi : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : StarRing R] →
        [inst_2 : NonUnitalSemiring A] →
          [inst_3 : StarRing A] →
            [inst_4 : Module R A] →
              [inst_5 : IsScalarTower R A A] →
                [inst_6 : SMulCommClass R A A] →
                  [inst_7 : StarModule R A] → GaloisInsertion (NonUnitalStarAlgebra.adjoin R) SetLike.coe
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_filterMap : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} {m : Std.DHashMap.Internal.Raw₀ α β}
  {f : (a : α) → β a → Option (δ a)},
  (Std.DHashMap.Internal.toListModel (↑(Std.DHashMap.Internal.Raw₀.filterMap f m)).buckets).Perm
    (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd))
      (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- When `n` is either a natural number or `ω`, one can characterize the property of being `C^n`
as the existence of a neighborhood on which there is a Taylor series up to order `n`,
requiring in addition that its terms are analytic in the `ω` case.  -/
contDiffWithinAt_iff_of_ne_infty : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞},
  n ≠ ↑⊤ →
    (ContDiffWithinAt 𝕜 n f s x ↔
      ∃ u ∈ nhdsWithin x (insert x s),
        ∃ p, HasFTaylorSeriesUpToOn n f p u ∧ (n = ⊤ → ∀ (i : ℕ), AnalyticOn 𝕜 (fun x => p x i) u))
-- Mathlib.Data.Ordmap.Invariants
Ordnode.size_balanceR : ∀ {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α},
  l.Balanced →
    r.Balanced →
      l.Sized →
        r.Sized →
          ((∃ l', Ordnode.Raised l.size l' ∧ Ordnode.BalancedSz l' r.size) ∨
              ∃ r', Ordnode.Raised r' r.size ∧ Ordnode.BalancedSz l.size r') →
            (l.balanceR x r).size = l.size + r.size + 1
-- Std.Time.Date.Unit.Weekday
/-- Defines the enumeration for days of the week. Each variant corresponds to a day of the week.
 -/
Std.Time.Weekday : Type