mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Equivalence.mapMon_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [inst_6 : e.IsMonoidal],
  e.mapMon.functor = e.functor.mapMon
-- Init.Data.String.Decode
Char.utf8Size_eq_three_iff : ∀ {c : Char}, c.utf8Size = 3 ↔ 2047 < c.val ∧ c.val ≤ 65535
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Finset.tsum_subtype' : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] (s : Finset β) (f : β → α),
  ∑' (x : ↑↑s), f ↑x = ∑ x ∈ s, f x
-- Aesop.Index.Basic
Aesop.IndexingMode.target.sizeOf_spec : ∀ (keys : Array Lean.Meta.DiscrTree.Key), sizeOf (Aesop.IndexingMode.target keys) = 1 + sizeOf keys
-- Mathlib.Geometry.Manifold.Instances.Real
IccLeftChart_extend_bot : ∀ {x y : ℝ} [hxy : Fact (x < y)], ↑((IccLeftChart x y).extend (modelWithCornersEuclideanHalfSpace 1)) ⊥ = 0
-- Mathlib.Algebra.Homology.QuasiIso
HomologicalComplex.quasiIso_map_of_preservesHomology : ∀ {ι : Type u_1} {c : ComplexShape ι} {C₁ : Type u_2} {C₂ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_2} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C₂] [inst_2 : CategoryTheory.Preadditive C₁]
  [inst_3 : CategoryTheory.Preadditive C₂] {K L : HomologicalComplex C₁ c} (φ : K ⟶ L)
  (F : CategoryTheory.Functor C₁ C₂) [inst_4 : F.Additive] [F.PreservesHomology] [inst_6 : ∀ (i : ι), K.HasHomology i]
  [inst_7 : ∀ (i : ι), L.HasHomology i] [inst_8 : ∀ (i : ι), ((F.mapHomologicalComplex c).obj K).HasHomology i]
  [inst_9 : ∀ (i : ι), ((F.mapHomologicalComplex c).obj L).HasHomology i] [hφ : QuasiIso φ],
  QuasiIso ((F.mapHomologicalComplex c).map φ)
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.PositivityExt.mk.sizeOf_spec : ∀
  (eval :
    {u : Lean.Level} →
      {α : Q(Type u)} →
        (zα : Q(Zero «$α»)) →
          (pα? : Option Q(PartialOrder «$α»)) →
            (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα e pα?)),
  sizeOf { eval := eval } = 1
-- Lean.Util.Diff
/-- An index of the element in the right array, if applicable  -/
Lean.Diff.Histogram.Entry.rightIndex : {α : Type u} → {lsize rsize : ℕ} → Lean.Diff.Histogram.Entry α lsize rsize → Option (Fin rsize)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_map : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → γ a} {k : α} {fallback : γ k},
  t.WF → (Std.DTreeMap.Internal.Impl.map f t).getD k fallback = (Option.map (f k) (t.get? k)).getD fallback
-- Mathlib.Analysis.RCLike.Basic
RCLike.coe_ofRealStarAlgHom : ∀ {K : Type u_1} [inst : RCLike K], ⇑(RCLike.ofRealStarAlgHom K) = RCLike.ofReal
-- Init.Data.List.Lemmas
List.concat_ne_nil : ∀ {α : Type u_1} (a : α) (l : List α), l ++ [a] ≠ []
-- Lean.ImportingFlag
_private.Lean.ImportingFlag.0.Lean.importingRef : IO.Ref Bool
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.RealizeConstKey : Type
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_ric_eq_some_iff : ∀ {k n i : ℕ}, (*...=n).toArray[i]? = some k ↔ i ≤ n ∧ i = k
-- Mathlib.Topology.NhdsSet
disjoint_nhdsSet_principal : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X},
  Disjoint (nhdsSet s) (Filter.principal t) ↔ Disjoint s (closure t)
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.inner_smul_left_real : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ A] [inst_4 : Module ℂ E] [inst_5 : PartialOrder A] [inst_6 : SMul A E] [inst_7 : Norm A]
  [inst_8 : Norm E] [inst_9 : CStarModule A E] [StarModule ℂ A] {z : ℝ} {x y : E}, inner A (z • x) y = z • inner A x y
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.instNontrivial : ∀ {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Nontrivial M],
  Nontrivial (PolynomialModule R M)
-- Mathlib.Algebra.Free
AddMagma.FreeAddSemigroup.hom_ext : ∀ {α : Type u} [inst : Add α] {β : Type v} [inst_1 : AddSemigroup β] {f g : AddMagma.FreeAddSemigroup α →ₙ+ β},
  f.comp AddMagma.FreeAddSemigroup.of = g.comp AddMagma.FreeAddSemigroup.of → f = g
-- Mathlib.Data.PNat.Prime
PNat.Coprime.factor_eq_gcd_right_right : ∀ {a b m n : ℕ+}, m.Coprime n → a ∣ m → b ∣ n → a = m.gcd (b * a)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- A finsupp `x : G →₀ A` satisfies the 1-boundary condition if there's a finsupp
`∑ aᵢ·(gᵢ, hᵢ) : G × G →₀ A` such that `∑ (gᵢ⁻¹ • aᵢ)·hᵢ - aᵢ·gᵢhᵢ + aᵢ·gᵢ = x`.  -/
groupHomology.IsBoundary₁ : {G : Type u_1} → {A : Type u_2} → [Mul G] → [Inv G] → [inst : AddCommGroup A] → [SMul G A] → (G →₀ A) → Prop
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.rightUnitor_inv_hom : ∀ (X : SFinKer),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv.hom =
    ProbabilityTheory.Kernel.id.map fun x => (x, PUnit.unit)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- Construct a 0-simplex from a point.  -/
Affine.Simplex.mkOfPoint : (k : Type u_1) →
  {V : Type u_2} →
    {P : Type u_5} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] → [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → P → Affine.Simplex k P 0
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Composition of two continuous homomorphisms.  -/
ContinuousAddMonoidHom.comp : {A : Type u_2} →
  {B : Type u_3} →
    {C : Type u_4} →
      [inst : AddMonoid A] →
        [inst_1 : AddMonoid B] →
          [inst_2 : AddMonoid C] →
            [inst_3 : TopologicalSpace A] →
              [inst_4 : TopologicalSpace B] → [inst_5 : TopologicalSpace C] → (B →ₜ+ C) → (A →ₜ+ B) → A →ₜ+ C
-- Mathlib.Analysis.Normed.MulAction
IsBoundedSMul.of_enorm_smul_le : ∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedRing α] [inst_1 : SeminormedAddCommGroup β] [inst_2 : Module α β],
  (∀ (r : α) (x : β), ‖r • x‖ₑ ≤ ‖r‖ₑ * ‖x‖ₑ) → IsBoundedSMul α β
-- Std.Async.Process
/-- The numeric process ID.
 -/
Std.IO.Process.PId.toUInt64 : Std.IO.Process.PId → UInt64
-- Lean.Data.Json.Basic
Lean.Json.brecOn.eq : ∀ {motive_1 : Lean.Json → Sort u} {motive_2 : Array Lean.Json → Sort u}
  {motive_3 : Std.TreeMap.Raw String Lean.Json compare → Sort u} {motive_4 : List Lean.Json → Sort u}
  {motive_5 : Std.DTreeMap.Raw String (fun x => Lean.Json) compare → Sort u}
  {motive_6 : (Std.DTreeMap.Internal.Impl String fun x => Lean.Json) → Sort u} (t : Lean.Json)
  (F_1 : (t : Lean.Json) → t.below → motive_1 t) (F_2 : (t : Array Lean.Json) → Lean.Json.below_1 t → motive_2 t)
  (F_3 : (t : Std.TreeMap.Raw String Lean.Json compare) → Lean.Json.below_2 t → motive_3 t)
  (F_4 : (t : List Lean.Json) → Lean.Json.below_3 t → motive_4 t)
  (F_5 : (t : Std.DTreeMap.Raw String (fun x => Lean.Json) compare) → Lean.Json.below_4 t → motive_5 t)
  (F_6 : (t : Std.DTreeMap.Internal.Impl String fun x => Lean.Json) → Lean.Json.below_5 t → motive_6 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 = F_1 t (Lean.Json.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6).2
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.Functor.essImage.eq_1 : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (Y : D), F.essImage Y = ∃ X, Nonempty (F.obj X ≅ Y)
-- Aesop.Options.Public
/-- (aesop) Write statistics about Aesop invocations to the given file in JSONL format.
 -/
Aesop.aesop.stats.file : Lean.Option String
-- Mathlib.Order.CompleteLattice.Finset
Finset.set_biInter_finset_image : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq α] {f : γ → α} {g : α → Set β} {s : Finset γ},
  ⋂ x ∈ Finset.image f s, g x = ⋂ y ∈ s, g (f y)
-- Mathlib.Topology.Algebra.ConstMulAction
MulAction.IsPretransitive.discreteTopology_iff : ∀ {α : Type u_2} (G : Type u_4) [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] (x : α) [MulAction.IsPretransitive G α], DiscreteTopology α ↔ IsOpen {x}
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [toIsMultiplicative : W.IsMultiplicative],
  (∀ ⦃X Y : C⦄ (φ : W.RightFraction X Y),
      ∃ ψ, CategoryTheory.CategoryStruct.comp φ.f ψ.s = CategoryTheory.CategoryStruct.comp φ.s ψ.f) →
    (∀ ⦃X' X Y : C⦄ (f₁ f₂ : X ⟶ Y) (s : X' ⟶ X),
        W s →
          CategoryTheory.CategoryStruct.comp s f₁ = CategoryTheory.CategoryStruct.comp s f₂ →
            ∃ Y' t, ∃ (_ : W t), CategoryTheory.CategoryStruct.comp f₁ t = CategoryTheory.CategoryStruct.comp f₂ t) →
      W.HasLeftCalculusOfFractions
-- Mathlib.LinearAlgebra.CliffordAlgebra.Inversion
/-- $aba^{-1}$ is a vector.  -/
CliffordAlgebra.ι_mul_ι_mul_invOf_ι : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (a b : M) [inst_3 : Invertible ((CliffordAlgebra.ι Q) a)] [inst_4 : Invertible (Q a)],
  (CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b * ⅟((CliffordAlgebra.ι Q) a) =
    (CliffordAlgebra.ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
HomogeneousIdeal.comap_mono : ∀ {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} {ι : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] [inst_4 : AddSubmonoidClass σ A] [inst_5 : AddSubmonoidClass τ B]
  [inst_6 : DecidableEq ι] [inst_7 : AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} [inst_8 : GradedRing 𝒜]
  [inst_9 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ), Monotone (HomogeneousIdeal.comap f)
-- Lean.Elab.Deriving.Basic
Lean.Elab.DerivingClassView.hasExpose : Lean.Elab.DerivingClassView → Bool
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.closure_empty : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R], NonUnitalSubring.closure ∅ = ⊥
-- Mathlib.CategoryTheory.Abelian.Projective.Extend
/-- If `R : ProjectiveResolution X`, then `R.cochainComplex.X n` (with `n : ℕ`)
is isomorphic to `R.complex.X k` (with `k : ℕ`) when `k = n`.  -/
CategoryTheory.ProjectiveResolution.cochainComplexXIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        {X : C} →
          (R : CategoryTheory.ProjectiveResolution X) →
            (n : ℤ) →
              (k : ℕ) →
                autoParam (-↑k = n) CategoryTheory.ProjectiveResolution.cochainComplexXIso._auto_1 →
                  (R.cochainComplex.X n ≅ R.complex.X k)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Not an instance, to avoid loops with `IsRightCancelMul.mulRightStrictMono_of_mulRightMono`.  -/
MulRightStrictMono.toIsRightCancelMul : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LinearOrder α] [MulRightStrictMono α], IsRightCancelMul α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp] {k : α}, k ∉ t₁ → (t₁ ∪ t₂).getKey! k = t₂.getKey! k
-- Lean.Elab.PreDefinition.Basic
/-- A (potentially recursive) definition.
The elaborator converts it into Kernel definitions using many different strategies.
 -/
Lean.Elab.PreDefinition : Type
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.flip.congr_simp : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] [inst_10 : RingHomIsometric σ₁₃] (f f_1 : E →SL[σ₁₃] F →SL[σ₂₃] G),
  f = f_1 → f.flip = f_1.flip
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
AddGroup.toOrderedSub : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α], OrderedSub α
-- Mathlib.Topology.Bornology.Basic
Bornology.isBounded_def : ∀ {α : Type u_2} {x : Bornology α} {s : Set α}, Bornology.IsBounded s ↔ sᶜ ∈ Bornology.cobounded α
-- Mathlib.Algebra.Category.Grp.Limits
/-- The chosen cone is a limit cone.
(Generally, you'll just want to use `limit.cone F`.)  -/
AddGrpCat.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddGrpCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddGrpCat)).sections] →
        CategoryTheory.Limits.IsLimit (AddGrpCat.limitCone F)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If the coproduct of `X` and `Y` exists, then every pair of morphisms `f : X ⟶ W` and
`g : Y ⟶ W` induces a morphism `coprod.desc f g : X ⨿ Y ⟶ W`.  -/
CategoryTheory.Limits.coprod.desc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y : C} → [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y] → (X ⟶ W) → (Y ⟶ W) → (X ⨿ Y ⟶ W)
-- Mathlib.Order.PrimeIdeal
Order.Ideal.PrimePair.F : {P : Type u_2} → [inst : Preorder P] → Order.Ideal.PrimePair P → Order.PFilter P
-- Batteries.Data.Fin.Lemmas
/-- **Alias** of `Fin.isNone_findSome?_iff`. -/
Fin.findSome?_isNone_iff : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Option α}, (Fin.findSome? f).isNone = true ↔ ∀ (i : Fin n), (f i).isNone = true
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- the compatibility isomorphism relating the two dual notions of
`LeftHomologyData` and `RightHomologyData`  -/
CategoryTheory.ShortComplex.HomologyData.iso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} → (self : S.HomologyData) → self.left.H ≅ self.right.H
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.functorOfNatTrans_obj_str : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (α : G ⟶ F)
  (A : CategoryTheory.Endofunctor.Algebra F),
  ((CategoryTheory.Endofunctor.Algebra.functorOfNatTrans α).obj A).str =
    CategoryTheory.CategoryStruct.comp (α.app A.a) A.str
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.compLeft_hom : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D E : HomologicalComplex V c} {f g : D ⟶ E} (h : Homotopy f g) (e : C ⟶ D) (i j : ι),
  (h.compLeft e).hom i j = CategoryTheory.CategoryStruct.comp (e.f i) (h.hom i j)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
summable_pnat_iff_summable_nat : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {f : ℕ → G},
  (Summable fun n => f ↑n) ↔ Summable f
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.centerCongr_symm_apply_coe : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (e : R ≃+* S)
  (s : ↥(Subsemigroup.center S)), ↑((Subring.centerCongr e).symm s) = e.symm ↑s
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.ofHom_apply : ∀ {X Y : Type u} [inst : AddGroup X] [inst_1 : AddGroup Y] (f : X →+ Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (AddGrpCat.ofHom f)) x = f x
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.coeff_comapDomain : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (hf : Function.Injective f)
  (x : MonoidAlgebra R N), (MonoidAlgebra.comapDomain f hf x).coeff = Finsupp.comapDomain f x.coeff ⋯
-- Mathlib.Algebra.Group.Submonoid.Membership
/-- A dependent version of `Submonoid.iSup_induction`.  -/
Submonoid.iSup_induction' : ∀ {M : Type u_1} [inst : MulOneClass M] {ι : Sort u_4} (S : ι → Submonoid M) {motive : (x : M) → x ∈ ⨆ i, S i → Prop},
  (∀ (i : ι) (x : M) (hxS : x ∈ S i), motive x ⋯) →
    motive 1 ⋯ →
      (∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), motive x hx → motive y hy → motive (x * y) ⋯) →
        ∀ {x : M} (hx : x ∈ ⨆ i, S i), motive x hx
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_radical : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M}, UniqueFactorizationMonoid.radical (UniqueFactorizationMonoid.radical a) = UniqueFactorizationMonoid.radical a
-- Lean.Meta.Sym.Pattern
Lean.Meta.Sym.instInhabitedPattern : Inhabited Lean.Meta.Sym.Pattern
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_eq_some_getKey! : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {a : α}, a ∈ m → m.getKey? a = some (m.getKey! a)
-- Mathlib.Order.RelClasses
/-- All values are accessible under the well-founded `<`.  -/
WellFoundedLT.apply : ∀ {α : Type u} [inst : LT α] [WellFoundedLT α] (a : α), Acc (fun x1 x2 => x1 < x2) a
-- Mathlib.Order.SetAccumulate
Set.accumulate_subset_accumulate : ∀ {α : Type u_1} {β : Type u_2} {s : α → Set β} [inst : Preorder α] {x y : α},
  x ≤ y → Set.accumulate s x ⊆ Set.accumulate s y
-- Mathlib.Data.List.Basic
List.getLast_concat' : ∀ {α : Type u} {a : α} (l : List α), (l.concat a).getLast ⋯ = a
-- Init.Data.Int.DivMod.Lemmas
Int.mul_add_bmod_self_right : ∀ (a : ℤ) (b : ℕ) (c : ℤ), (a * ↑b + c).bmod b = c.bmod b
-- Mathlib.Topology.Order.LeftRightNhds
nhds_basis_abs_sub_lt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : AddCommGroup α] [inst_2 : LinearOrder α] [IsOrderedAddMonoid α]
  [OrderTopology α] [NoMaxOrder α] (a : α), (nhds a).HasBasis (fun ε => 0 < ε) fun ε => {b | |b - a| < ε}
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow.congr_simp : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] (a a_1 : A), a = a_1 → ∀ (y y_1 : ℝ), y = y_1 → CFC.rpow a y = CFC.rpow a_1 y_1
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsTangent.eq_orthRadius_or_eq_orthRadius_pointReflection_of_parallel_orthRadius : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {as : AffineSubspace ℝ P} {p : P},
  s.IsTangent as →
    as.Parallel (s.orthRadius p) → p ∈ s → as = s.orthRadius p ∨ as = s.orthRadius ((Equiv.pointReflection s.center) p)
-- Mathlib.Geometry.Manifold.ContMDiffMap
/-- The second projection of a product, as a `C^n` map.  -/
ContMDiffMap.snd : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {H' : Type u_5} →
                      [inst_6 : TopologicalSpace H'] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {M : Type u_6} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {M' : Type u_7} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        {n : WithTop ℕ∞} → ContMDiffMap (I.prod I') I' (M × M') M' n
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.Ordered.eq_3 : ∀ {α : Type u_1} (cmp : α → α → Ordering) (c : RBTree.RBColor) (l : RBTree.RBNode α) (x_1 : α)
  (parent : RBTree.RBNode.Path α),
  RBTree.RBNode.Path.Ordered cmp (RBTree.RBNode.Path.right c l x_1 parent) =
    (RBTree.RBNode.Path.Ordered cmp parent ∧
      RBTree.RBNode.All (fun x => RBTree.RBNode.cmpLT cmp x x_1) l ∧
        RBTree.RBNode.Path.RootOrdered cmp parent x_1 ∧
          RBTree.RBNode.All (RBTree.RBNode.Path.RootOrdered cmp parent) l ∧ RBTree.RBNode.Ordered cmp l)
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile.0.Std.IterM.step_intermediateDropWhileWithPostcondition.match_1.eq_2 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)} (out : β)
  (motive : Subtype (P out).Property → Sort u_3) (h'' : (P out).Property { down := false })
  (h_1 : (h'' : (P out).Property { down := true }) → motive ⟨{ down := true }, h''⟩)
  (h_2 : (h'' : (P out).Property { down := false }) → motive ⟨{ down := false }, h''⟩),
  (match ⟨{ down := false }, h''⟩ with
    | ⟨{ down := true }, h''⟩ => h_1 h''
    | ⟨{ down := false }, h''⟩ => h_2 h'') =
    h_2 h''
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counitIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal],
  CategoryTheory.CategoryStruct.comp (e.functor.map (CategoryTheory.Functor.LaxMonoidal.ε e.inverse))
      (e.counitIso.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) =
    CategoryTheory.Functor.OplaxMonoidal.η e.functor
-- Init.Data.List.MinMaxIdx
List.left_le_minIdxOn_append : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α}
  {f : α → β} (h : xs ≠ []), List.minIdxOn f xs h ≤ List.minIdxOn f (xs ++ ys) ⋯
-- Mathlib.Algebra.Ring.Int.Parity
Int.isSquare_ofNat_iff : ∀ {n : ℕ}, IsSquare (OfNat.ofNat n) ↔ IsSquare (OfNat.ofNat n)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.assemble₃_eq_some_of_toBitVec : ∀ {w x y : UInt8},
  ByteArray.utf8DecodeChar?.isInvalidContinuationByte x = false →
    ByteArray.utf8DecodeChar?.isInvalidContinuationByte y = false →
      ∀ {c : Char},
        2048 ≤ c.val →
          c.val.toBitVec =
              BitVec.setWidth 32
                (BitVec.setWidth 4 w.toBitVec ++ BitVec.setWidth 6 x.toBitVec ++ BitVec.setWidth 6 y.toBitVec) →
            ByteArray.utf8DecodeChar?.assemble₃ w x y = some c
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Solvers.propagateDiseqs.go.match_1.eq_1 : ∀ (motive : Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.SolverTerms → Sort u_1) (x : Lean.Meta.Grind.SolverTerms)
  (h_1 : (x : Lean.Meta.Grind.SolverTerms) → motive Lean.Meta.Grind.SolverTerms.nil x)
  (h_2 : (x : Lean.Meta.Grind.SolverTerms) → motive x Lean.Meta.Grind.SolverTerms.nil)
  (h_3 :
    (id₁ : ℕ) →
      (lhs : Lean.Expr) →
        (lhsTerms : Lean.Meta.Grind.SolverTerms) →
          (id₂ : ℕ) →
            (rhs : Lean.Expr) →
              (rhsTerms : Lean.Meta.Grind.SolverTerms) →
                motive (Lean.Meta.Grind.SolverTerms.next id₁ lhs lhsTerms)
                  (Lean.Meta.Grind.SolverTerms.next id₂ rhs rhsTerms)),
  (match Lean.Meta.Grind.SolverTerms.nil, x with
    | Lean.Meta.Grind.SolverTerms.nil, x => h_1 x
    | x, Lean.Meta.Grind.SolverTerms.nil => h_2 x
    | Lean.Meta.Grind.SolverTerms.next id₁ lhs lhsTerms, Lean.Meta.Grind.SolverTerms.next id₂ rhs rhsTerms =>
      h_3 id₁ lhs lhsTerms id₂ rhs rhsTerms) =
    h_1 x
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
_private.Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic.0.MeasureTheory.simpleFuncAux.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : MeasurableSingletonClass α] (f : α → β) (g : ℕ → α),
  MeasureTheory.simpleFuncAux✝ f g 0 = MeasureTheory.SimpleFunc.const α (f (g 0))