mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.toNormalization_inr_normalizationCoprodIso_hom_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U V : AlgebraicGeometry.Scheme} {iU : U ⟶ X} {iV : V ⟶ X}
  (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV))
  [inst_2 : AlgebraicGeometry.QuasiCompact iU] [inst_3 : AlgebraicGeometry.QuasiSeparated iU]
  [inst_4 : AlgebraicGeometry.QuasiCompact iV] [inst_5 : AlgebraicGeometry.QuasiSeparated iV]
  {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Scheme.Hom.normalization f ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.toNormalization (CategoryTheory.CategoryStruct.comp iV f))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso f e).hom h)) =
    CategoryTheory.CategoryStruct.comp iV
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.toNormalization f) h)
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiff.prodMk : ∀ {𝕜 : 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' : Type u_11}
  [inst_11 : NormedAddCommGroup F'] [inst_12 : NormedSpace 𝕜 F'] {G' : Type u_12} [inst_13 : TopologicalSpace G']
  {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [inst_14 : TopologicalSpace N'] [inst_15 : ChartedSpace G' N']
  {n : WithTop ℕ∞} {f : M → M'} {g : M → N'},
  ContMDiff I I' n f → ContMDiff I J' n g → ContMDiff I (I'.prod J') n fun x => (f x, g x)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.top_injective_iff : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (f : ⊤.LocalizationMap N),
  Function.Injective ⇑f ↔ IsCancelAdd M
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion_surjective : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  Function.Surjective IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.descentDataEquivalence_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j))
  (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)),
  (CategoryTheory.Pseudofunctor.DescentData'.descentDataEquivalence F sq sq₃).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun D =>
        CategoryTheory.Pseudofunctor.DescentData.isoMk
          (fun x =>
            CategoryTheory.Iso.refl
              ((((CategoryTheory.Pseudofunctor.DescentData'.fromDescentDataFunctor F sq sq₃).comp
                        (CategoryTheory.Pseudofunctor.DescentData'.toDescentDataFunctor F sq sq₃)).obj
                    D).obj
                x))
          ⋯)
      ⋯
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
/-- The functor `Γ₀' : ChainComplex C ℕ ⥤ SimplicialObject.Split C`
that induces `Γ₀ : ChainComplex C ℕ ⥤ SimplicialObject C`, which
shall be the inverse functor of the Dold-Kan equivalence for
abelian or pseudo-abelian categories.  -/
AlgebraicTopology.DoldKan.Γ₀' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasFiniteCoproducts C] →
        CategoryTheory.Functor (ChainComplex C ℕ) (CategoryTheory.SimplicialObject.Split C)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context.subExpr : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.Context → Lean.SubExpr
-- Mathlib.Topology.ContinuousMap.ContinuousSqrt
instContinuousSqrtNNReal : ContinuousSqrt NNReal
-- Mathlib.Data.List.Lattice
_private.Mathlib.Data.List.Lattice.0.List.bagInter.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (a : α) (l₁ l₂ : List α) (h_1 : (x : List α) → motive [] x)
  (h_2 : (x : List α) → motive x []) (h_3 : (a : α) → (l₁ l₂ : List α) → motive (a :: l₁) l₂),
  (l₂ = [] → False) →
    (match a :: l₁, l₂ with
      | [], x => h_1 x
      | x, [] => h_2 x
      | a :: l₁, l₂ => h_3 a l₁ l₂) =
      h_3 a l₁ l₂
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.mul_eq : ∀ {G : Type u_1} [inst : Group G] {S T : Set G}, Subgroup.IsComplement S T → S * T = Set.univ
-- Mathlib.Tactic.NormNum.LegendreSymbol
/-- Use quadratic reciprocity to reduce to smaller `b`.  -/
Mathlib.Meta.NormNum.jacobiSymNat.qr₁ : ∀ (a b : ℕ) (r : ℤ),
  a % 4 = 1 → b % 2 = 1 → Mathlib.Meta.NormNum.jacobiSymNat b a = r → Mathlib.Meta.NormNum.jacobiSymNat a b = r
-- Mathlib.AlgebraicGeometry.SpreadingOut
AlgebraicGeometry.Scheme.IsGermInjective.of_openCover : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) [∀ (i : 𝒰.I₀), (𝒰.X i).IsGermInjective], X.IsGermInjective
-- Mathlib.Computability.ContextFreeGrammar
instDecidableEqContextFreeRule.decEq : {T : Type u_1} →
  {N : Type u_2} → [DecidableEq T] → [DecidableEq N] → (x x_1 : ContextFreeRule T N) → Decidable (x = x_1)
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_fun_sum_right : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ}
  [MeasureTheory.IsFiniteMeasure μ] [inst : Fintype ι],
  (∀ (i : ι), MeasureTheory.MemLp (X i) 2 μ) →
    MeasureTheory.MemLp Y 2 μ →
      ProbabilityTheory.covariance Y (fun ω => ∑ i, X i ω) μ = ∑ i, ProbabilityTheory.covariance Y (X i) μ
-- Std.Time.Zoned.RecurringRule
/-- Rule for the end of DST, if any.
 -/
Std.Time.TimeZone.DaylightSavingRule.end_ : Std.Time.TimeZone.DaylightSavingRule → Option Std.Time.TimeZone.TransitionRule
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Opens.compl_bijective : ∀ {α : Type u_2} [inst : TopologicalSpace α], Function.Bijective TopologicalSpace.Opens.compl
-- Std.Data.TreeMap.Basic
/-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails.  -/
Std.TreeMap.all : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → (α → β → Bool) → Bool
-- Mathlib.CategoryTheory.Filtered.Small
/-- The second, fully faithful part of a factoring of a functor from a small category to a filtered
category through a small filtered category.  -/
CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.inclusion : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          (F : CategoryTheory.Functor D C) →
            CategoryTheory.Functor (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate F) C
-- Std.Data.String.ToInt
Int.isInt_repr : ∀ (a : ℤ), a.repr.isInt = true
-- Lean.Elab.DeclModifiers
Lean.Elab.ComputeKind.regular.sizeOf_spec : sizeOf Lean.Elab.ComputeKind.regular = 1
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.adjp_mul_apply_ne : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (A : Matrix n n R)
  (i j : n), i ≠ j → (Matrix.adjp 1 A * A) i j = (Matrix.adjp (-1) A * A) i j
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instIsScalarTower_2 : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {S : Type u_3} {P : Type u_4}
  [inst_1 : Ring S] [inst_2 : SMul P R] [inst_3 : SMul S R] [inst_4 : SMul P S] [IsScalarTower P S R]
  (v : Valuation S Γ₀), IsScalarTower P (WithVal v) R
-- Mathlib.LinearAlgebra.Coevaluation
coevaluation.eq_1 : ∀ (K : Type u) [inst : Field K] (V : Type v) [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : FiniteDimensional K V],
  coevaluation K V =
    ((Module.Basis.singleton Unit K).constr K) fun x =>
      ∑ i, (Module.Basis.ofVectorSpace K V) i ⊗ₜ[K] (Module.Basis.ofVectorSpace K V).coord i
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- The functor `Opens X ⥤ Opens Y` associated with an open immersion `f : X ⟶ Y`.  -/
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.opensFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : AlgebraicGeometry.SheafedSpace C} →
      (f : X ⟶ Y) →
        [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] →
          CategoryTheory.Functor (TopologicalSpace.Opens ↑↑X.toPresheafedSpace)
            (TopologicalSpace.Opens ↑↑Y.toPresheafedSpace)
-- Mathlib.GroupTheory.Congruence.Defs
/-- The addition induced on the quotient by an additive congruence relation on a type
with an addition.  -/
AddCon.hasAdd : {M : Type u_1} → [inst : Add M] → (c : AddCon M) → Add c.Quotient
-- Mathlib.CategoryTheory.Monad.Kleisli
/-- The composition of the adjunction gives the original functor.  -/
CategoryTheory.Kleisli.Adjunction.toKleisliCompFromKleisliIsoSelf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (T : CategoryTheory.Monad C) →
      (CategoryTheory.Kleisli.Adjunction.toKleisli T).comp (CategoryTheory.Kleisli.Adjunction.fromKleisli T) ≅
        T.toFunctor
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.tensorObj.add_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : C} [inst_3 : CategoryTheory.AddMonObj M]
  [inst_4 : CategoryTheory.AddMonObj N],
  CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.add CategoryTheory.AddMonObj.add)
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
_private.Lean.Elab.PreDefinition.PartialFixpoint.Eqns.0.Lean.Elab.PartialFixpoint.mkUnfoldEq.doRealize : Lean.Name → Lean.Elab.PartialFixpoint.EqnInfo → Lean.Name → Lean.MetaM Unit
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rco_eq_if_push : ∀ {m n : ℤ}, (m...n).toArray = if m < n then (m...n - 1).toArray.push (n - 1) else #[]
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.Hom.instVAddHom.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M] {X : C} [inst_3 : CategoryTheory.AddModObj M X] (Y : C),
  CategoryTheory.Hom.instVAddHom Y =
    {
      vadd := fun m x =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift m x)
          CategoryTheory.AddModObj.vadd }
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
/-- If `f : Box ι → M` is box additive on partitions of the form `split I i x`, then it is box
additive.  -/
BoxIntegral.BoxAdditiveMap.ofMapSplitAdd : {ι : Type u_1} →
  {M : Type u_2} →
    [inst : AddCommMonoid M] →
      [Finite ι] →
        (f : BoxIntegral.Box ι → M) →
          (I₀ : WithTop (BoxIntegral.Box ι)) →
            (∀ (I : BoxIntegral.Box ι),
                ↑I ≤ I₀ →
                  ∀ {i : ι} {x : ℝ},
                    x ∈ Set.Ioo (I.lower i) (I.upper i) →
                      Option.elim' 0 f (I.splitLower i x) + Option.elim' 0 f (I.splitUpper i x) = f I) →
              BoxIntegral.BoxAdditiveMap ι M I₀
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.monotoneOn_sin : MonotoneOn Real.sin (Set.Icc (-(Real.pi / 2)) (Real.pi / 2))
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullback.eq_lift_of_comp_eq : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  (arrows : (j : J) → objs j ⟶ B) [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f : X ⟶ B)
  (fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f)
  (g : X ⟶ CategoryTheory.Limits.widePullback B objs arrows),
  (∀ (j : J), CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.WidePullback.π arrows j) = fs j) →
    CategoryTheory.CategoryStruct.comp g (CategoryTheory.Limits.WidePullback.base arrows) = f →
      g = CategoryTheory.Limits.WidePullback.lift f fs w
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_ofNatTruncate_of_lt : ∀ {n : ℕ} (hn : n < UInt64.size), (UInt64.ofNatClamp n).toBitVec = n#'hn
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.fdiv.match_1.splitter : (motive : ℤ → ℤ → Sort u_1) →
  (x x_1 : ℤ) →
    ((x : ℤ) → motive 0 x) →
      ((m n : ℕ) → (m = 0 → False) → motive (Int.ofNat m) (Int.ofNat n)) →
        ((m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n)) →
          ((a : ℕ) → motive (Int.negSucc a) 0) →
            ((m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ)) →
              ((m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)) → motive x x_1
-- Init.Data.UInt.Lemmas
UInt32.ofNat_size : UInt32.ofNat UInt32.size = 0
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
neg_le_neg_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] {a b : α} [AddRightMono α], -a ≤ -b ↔ b ≤ a
-- Mathlib.Algebra.Torsor.Defs
Equiv.constVAdd.eq_1 : ∀ {G : Type u_1} (P : Type u_2) [inst : AddGroup G] [inst_1 : AddTorsor G P] (v : G),
  Equiv.constVAdd P v = { toFun := fun x => v +ᵥ x, invFun := fun x => -v +ᵥ x, left_inv := ⋯, right_inv := ⋯ }
-- Lean.Data.Lsp.Internal
Lean.Lsp.instHashableRefIdent.hash : Lean.Lsp.RefIdent → UInt64
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {k a : α}, (t.erase k).get! a = if cmp k a = Ordering.eq then default else t.get! a
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.CommMonoid.prod_insertIdx : ∀ {M : Type u_4} [inst : CommMonoid M] {a : M} {l : List M} {i : ℕ}, i ≤ l.length → (l.insertIdx i a).prod = a * l.prod
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₁ → (m₁ \ m₂).getKey? k = none
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.Spec.thunk : {m : Type u → Type u} →
  (self : MLList.Spec✝ m) → {α : Type u} → (Unit → MLList.Spec.listM✝ self α) → MLList.Spec.listM✝ self α
-- Init.Data.BitVec.Basic
/-- Prepends a single bit to the front of a bitvector, using big-endian order (see `append`).

The new bit is the most significant bit.
 -/
BitVec.cons : {n : ℕ} → Bool → BitVec n → BitVec (n + 1)
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- **Riesz's theorem**: if a T2 topological vector space over a complete non-trivial
normed field admits a totally bounded neighborhood of some point, then it is
finite-dimensional.  -/
FiniteDimensional.of_totallyBounded_nhds : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {Eᵤ : Type u_6} [inst_2 : AddCommGroup Eᵤ]
  [inst_3 : Module 𝕜 Eᵤ] [inst_4 : UniformSpace Eᵤ] [T2Space Eᵤ] [IsUniformAddGroup Eᵤ] [ContinuousSMul 𝕜 Eᵤ] {x : Eᵤ}
  {U : Set Eᵤ}, U ∈ nhds x → TotallyBounded U → FiniteDimensional 𝕜 Eᵤ
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_of_functorial_resolutions : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂)
  {ρ : CategoryTheory.Functor C₂ C₁} (i : CategoryTheory.Functor.id C₂ ⟶ ρ.comp Φ.functor),
  (∀ (X₂ : C₂), W₂ (i.app X₂)) →
    W₁ = W₂.inverseImage Φ.functor →
      ∀ [Φ.functor.Full] [Φ.functor.Faithful] [W₂.HasTwoOutOfThreeProperty] [W₂.IsMultiplicative],
        Φ.IsRightDerivabilityStructure
-- Mathlib.Logic.Basic
/-- **Alias** of `ne_of_mem_of_not_mem'`. -/
Membership.mem.ne_of_notMem' : ∀ {α : Type u_1} {β : Type u_2} [inst : Membership α β] {s t : β} {a : α}, a ∈ s → a ∉ t → s ≠ t
-- Init.Data.Nat.Bitwise.Lemmas
Nat.and_two_pow_sub_one_of_lt_two_pow : ∀ {n x : ℕ}, x < 2 ^ n → x &&& 2 ^ n - 1 = x
-- Lean.Meta.Tactic.Simp.Rewrite
_private.Lean.Meta.Tactic.Simp.Rewrite.0.Lean.Meta.Simp.tryTheoremCore.go : Lean.Expr →
  Array Lean.Expr →
    Array Lean.BinderInfo →
      Lean.Expr → Lean.Expr → Lean.Meta.SimpTheorem → Lean.Expr → Lean.Meta.SimpM (Option Lean.Meta.Simp.Result)
-- Mathlib.CategoryTheory.Presentable.Dense
CategoryTheory.IsFinitelyAccessibleCategory.instEssentiallySmallIsFinitelyPresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFinitelyAccessibleCategory C],
  CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} (CategoryTheory.ObjectProperty.isFinitelyPresentable C)
-- Mathlib.Topology.Algebra.Group.Basic
nhds_one_symm : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G],
  Filter.comap Inv.inv (nhds 1) = nhds 1
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_exp_mul_I_eq_sin : ∀ (r : ℝ), ∫ (t : ℝ) in -r..r, Complex.exp (↑t * Complex.I) = 2 * ↑(Real.sin r)
-- Mathlib.CategoryTheory.Bicategory.Basic
/-- Left whiskering for morphisms  -/
CategoryTheory.Bicategory.«term_◁_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Convex.Visible
IsVisible.rfl : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsOrderedRing 𝕜]
  [inst_3 : AddCommGroup V] [inst_4 : Module 𝕜 V] [inst_5 : AddTorsor V P] {s : Set P} {x : P}, IsVisible 𝕜 s x x
-- Mathlib.Order.Heyting.Basic
/-- `(p → q) ∧ p ↔ q ∧ p`  -/
himp_inf_self : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] (a b : α), (a ⇨ b) ⊓ a = b ⊓ a
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.ofProfinite.eq_1 : ∀ (G : Profinite) [inst : Group ↑G.toTop] [inst_1 : IsTopologicalGroup ↑G.toTop],
  ProfiniteGrp.ofProfinite G = ProfiniteGrp.of ↑G.toTop
-- Mathlib.Data.Finset.Basic
/-- After filtering out everything that does not equal a given value, at most that value remains.

This is equivalent to `filter_eq'` with the equality the other way.
 -/
Finset.filter_eq : ∀ {β : Type u_2} [inst : DecidableEq β] (s : Finset β) (b : β), Finset.filter (Eq b) s = if b ∈ s then {b} else ∅
-- Mathlib.Order.SymmDiff
symmDiff_sdiff_left : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b : α), symmDiff a b \ a = b \ a
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        [inst_2 : Mul α] →
          [inst_3 : Mul β] →
            (toMulEquiv : α ≃* β) → (∀ {a b : α}, toMulEquiv.toFun a ≤ toMulEquiv.toFun b ↔ a ≤ b) → α ≃*o β
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.sameCycle_symm_apply_right : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α}, f.SameCycle x ((Equiv.symm f) y) ↔ f.SameCycle x y
-- Mathlib.Algebra.Squarefree.Basic
Squarefree.of_mul_right : ∀ {R : Type u_1} [inst : CommMonoid R] {m n : R}, Squarefree (m * n) → Squarefree n
-- Mathlib.RingTheory.RootsOfUnity.Basic
instFiniteSubtypeUnitsMemSubgroupRootsOfUnity : ∀ (R : Type u_4) (k : ℕ) [NeZero k] [inst : CommRing R] [IsDomain R], Finite ↥(rootsOfUnity k R)
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
/-- The underlying relation of the tripartite-from-triangles graph.

Two vertices are related iff there exists a triangle index containing them both.  -/
SimpleGraph.TripartiteFromTriangles.Rel : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → Finset (α × β × γ) → α ⊕ β ⊕ γ → α ⊕ β ⊕ γ → Prop
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.isAffine_affineScheme : ∀ (X : AlgebraicGeometry.AffineScheme), AlgebraicGeometry.IsAffine X.obj
-- Mathlib.RepresentationTheory.Invariants
Representation.mem_linHom_invariants_iff_isIntertwining : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommRing k] [inst_1 : Group G]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  {ρ : Representation k G V} {σ : Representation k G W} (f : V →ₗ[k] W),
  (∀ (g : G), σ g ∘ₗ f ∘ₗ ρ g⁻¹ = f) ↔ ρ.IsIntertwiningMap σ f
-- Mathlib.Tactic.Widget.LibraryRewrite
_private.Mathlib.Tactic.Widget.LibraryRewrite.0.Mathlib.Tactic.LibraryRewrite.ExtState : Type
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.toTrivSqZeroExt_comp_map : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u4}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : Module Rᵐᵒᵖ M] [inst_6 : IsCentralScalar R M]
  [inst_7 : Module Rᵐᵒᵖ N] [inst_8 : IsCentralScalar R N] (f : M →ₗ[R] N),
  ExteriorAlgebra.toTrivSqZeroExt.comp (ExteriorAlgebra.map f) =
    (TrivSqZeroExt.map f).comp ExteriorAlgebra.toTrivSqZeroExt
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {a fallback : α} {c : ℕ},
  (Std.DHashMap.emptyWithCapacity c).getKeyD a fallback = fallback
-- Mathlib.Data.Finset.Max
Finset.isGLB_mem : ∀ {α : Type u_2} [inst : LinearOrder α] {i : α} (s : Finset α), IsGLB (↑s) i → s.Nonempty → i ∈ s
-- Mathlib.Data.Sigma.Basic
Function.Injective.sigma_map_iff : ∀ {α₁ : Type u_2} {α₂ : Type u_3} {β₁ : α₁ → Type u_5} {β₂ : α₂ → Type u_6} {f₁ : α₁ → α₂}
  {f₂ : (a : α₁) → β₁ a → β₂ (f₁ a)},
  Function.Injective f₁ → (Function.Injective (Sigma.map f₁ f₂) ↔ ∀ (a : α₁), Function.Injective (f₂ a))
-- Mathlib.LinearAlgebra.Eigenspace.ContinuousLinearMap
ContinuousLinearMap.isClosed_eigenspace : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] [T0Space M] [ContinuousConstSMul R M] [IsTopologicalAddGroup M] (f : M →L[R] M) (μ : R),
  IsClosed ↑(Module.End.eigenspace (↑f) μ)
-- Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
UpperHalfPlane.tendsto_comap_im_ofComplex : Filter.Tendsto (↑UpperHalfPlane.ofComplex) (Filter.comap Complex.im Filter.atTop) UpperHalfPlane.atImInfty
-- Std.Time.Internal.Bounded
/-- Returns the absolute value of the bounded number `bo` with bounds `-(i - 1)` to `i - 1`. The result
will be a new bounded number with bounds `0` to `i - 1`.
 -/
Std.Time.Internal.Bounded.LE.abs : {i : ℤ} → Std.Time.Internal.Bounded.LE (-i) i → Std.Time.Internal.Bounded.LE 0 i
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.abs_eval_T_real_le_one : ∀ (n : ℤ) {x : ℝ}, |x| ≤ 1 → |Polynomial.eval x (Polynomial.Chebyshev.T ℝ n)| ≤ 1
-- Init.Data.Array.Monadic
/-- Variant of `filterMapM_toArray` with a side condition for the stop position.  -/
List.filterMapM_toArray' : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {stop : ℕ} [inst : Monad m] [LawfulMonad m] {l : List α}
  {f : α → m (Option β)}, stop = l.length → Array.filterMapM f l.toArray 0 stop = List.toArray <$> List.filterMapM f l
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidtOrthonormalBasis_inv_triangular' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι]
  [inst_6 : Fintype ι] [inst_7 : FiniteDimensional 𝕜 E] (h : Module.finrank 𝕜 E = Fintype.card ι) (f : ι → E) {i j : ι},
  i < j → ((InnerProductSpace.gramSchmidtOrthonormalBasis h f).repr (f i)).ofLp j = 0