mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.BoxIntegral.UnitPartition
/-- For `x : ι → ℝ`, its index is the index of the unique `unitPartition.box` to which
it belongs.  -/
BoxIntegral.unitPartition.index : {ι : Type u_1} → ℕ → (ι → ℝ) → ι → ℤ
-- Mathlib.Combinatorics.SimpleGraph.Prod
_private.Mathlib.Combinatorics.SimpleGraph.Prod.0.SimpleGraph.sum.match_1.eq_2 : ∀ {V : Type u_1} {W : Type u_2} (motive : V ⊕ W → V ⊕ W → Sort u_3) (u v : W)
  (h_1 : (u v : V) → motive (Sum.inl u) (Sum.inl v)) (h_2 : (u v : W) → motive (Sum.inr u) (Sum.inr v))
  (h_3 : (x x_1 : V ⊕ W) → motive x x_1),
  (match Sum.inr u, Sum.inr v with
    | Sum.inl u, Sum.inl v => h_1 u v
    | Sum.inr u, Sum.inr v => h_2 u v
    | x, x_1 => h_3 x x_1) =
    h_2 u v
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.Integrable.integrableAtFilter : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  MeasureTheory.Integrable f μ → ∀ (l : Filter α), MeasureTheory.IntegrableAtFilter f l μ
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inter_mul_union_subset : ∀ {α : Type u_2} [inst : CommSemigroup α] {s t : Set α}, s ∩ t * (s ∪ t) ⊆ s * t
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roo_eq_push : ∀ {m n : ℕ}, m + 1 < n → (m<...n).toArray = (m<...n - 1).toArray.push (n - 1)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.var.inj : ∀ {i i_1 : Nat.Internal.Linear.Var}, Nat.Internal.Linear.Expr.var i = Nat.Internal.Linear.Expr.var i_1 → i = i_1
-- Mathlib.Data.Multiset.Bind
Multiset.bind_congr : ∀ {α : Type u_1} {β : Type v} {f g : α → Multiset β} {m : Multiset α}, (∀ a ∈ m, f a = g a) → m.bind f = m.bind g
-- Init.Data.Vector.Lemmas
Vector.reverse_eq_append_iff : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α (n + m)} {ys : Vector α n} {zs : Vector α m},
  xs.reverse = ys ++ zs ↔ xs = Vector.cast ⋯ (zs.reverse ++ ys.reverse)
-- Mathlib.Topology.Sheaves.Skyscraper
StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk_assoc : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] [inst_2 : CategoryTheory.Limits.HasTerminal C]
  [inst_3 : CategoryTheory.Limits.HasColimits C] {𝓕 : TopCat.Presheaf C X} {c : C} (f : 𝓕 ⟶ skyscraperPresheaf p₀ c)
  (U : TopologicalSpace.Opens ↑X) (hU : p₀ ∈ U) {Z : C} (h : c ⟶ Z),
  CategoryTheory.CategoryStruct.comp (𝓕.germ U p₀ hU)
      (CategoryTheory.CategoryStruct.comp (StalkSkyscraperPresheafAdjunctionAuxs.fromStalk p₀ f) h) =
    CategoryTheory.CategoryStruct.comp (f.app (Opposite.op U))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)
-- Lean.Compiler.LCNF.Types
/-- `tobject` is either an `object` or a `tagged` pointer.

Crucially the RC the RC operations for `tobject` are slightly more expensive because we
first need to test whether the `tobject` is really a pointer or not.
 -/
Lean.Compiler.LCNF.ImpureType.tobject : Lean.Expr
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.destruct_tail : ∀ {α : Type u} (s : Stream'.WSeq α), s.tail.destruct = s.destruct >>= Stream'.WSeq.tail.aux
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovary_neg_left`. -/
Monovary.of_neg_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {f : ι → α} {g : ι → β}, Monovary (-f) g → Antivary f g
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_alter_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, (m.alter k f).get? k = f (m.get? k)
-- Mathlib.Analysis.Complex.Basic
/-- We show that the partial order and the topology on `ℂ` are compatible.
We turn this into an instance scoped to `ComplexOrder`.  -/
Complex.orderClosedTopology : OrderClosedTopology ℂ
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.closedBall_eq_bInter_ball : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.closedBall x ε = ⋂ δ, ⋂ (_ : δ > ε), Metric.ball x δ
-- Mathlib.Algebra.Module.Rat
/-- A `ℚ≥0`-module is torsion-free as a group.

This instance will fire for any monoid `M`, so is local unless needed elsewhere.  -/
IsAddTorsionFree.of_module_rat : ∀ (M : Type u_1) [inst : AddCommGroup M] [Module ℚ M], IsAddTorsionFree M
-- Std.Http.Protocol.H1.Reader
/-- Marks the current message as complete and prepares for the next message.
 -/
Std.Http.Protocol.H1.Reader.markComplete : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → Std.Http.Protocol.H1.Reader dir
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.mk_right : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y : T} (f : X ⟶ Y), (CategoryTheory.Arrow.mk f).right = Y
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.coend.ι_map : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasCoend F]
  {F' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_3 : CategoryTheory.Limits.HasCoend F']
  (f : F ⟶ F') (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coend.ι F j) (CategoryTheory.Limits.coend.map f) =
    CategoryTheory.CategoryStruct.comp ((f.app (Opposite.op j)).app j) (CategoryTheory.Limits.coend.ι F' j)
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegular.instSum : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {ι : Type u_3}
  {μ : ι → MeasureTheory.Measure α} [∀ (i : ι), (μ i).InnerRegular] (a : Finset ι), (∑ i ∈ a, μ i).InnerRegular
-- Mathlib.Combinatorics.Hall.Basic
/-- This is the `hallMatchingsOn` sets assembled into a directed system.
 -/
hallMatchingsFunctor : {ι : Type u} → {α : Type v} → (ι → Finset α) → CategoryTheory.Functor (Finset ι)ᵒᵖ (Type (max u v))
-- Mathlib.Algebra.Homology.Factorizations.CM5a
CochainComplex.Plus.modelCategoryQuillen.exists_mono_quasiIso_injective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : CochainComplex C ℤ) [CategoryTheory.EnoughInjectives C] (n₀ n₁ : ℤ),
  autoParam (n₀ + 1 = n₁) CochainComplex.Plus.modelCategoryQuillen.exists_mono_quasiIso_injective._auto_1 →
    ∀ [K.IsStrictlyGE n₁],
      ∃ L i,
        ∃ (_ : CategoryTheory.Mono i) (_ : QuasiIso i) (_ : ∀ (n : ℤ), CategoryTheory.Injective (L.X n)),
          L.IsStrictlyGE n₀
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.instCoeFunForallSubtypeMemSubmoduleDomain : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        {σ : R →+* S} →
          {E : Type u_4} →
            [inst_2 : AddCommGroup E] →
              [inst_3 : Module R E] →
                {F : Type u_5} →
                  [inst_4 : AddCommGroup F] → [inst_5 : Module S F] → CoeFun (E →ₛₗ.[σ] F) fun f => ↥f.domain → F
-- Mathlib.Order.Filter.Pointwise
Filter.map₂_add : ∀ {α : Type u_2} [inst : Add α] {f g : Filter α}, Filter.map₂ (fun x1 x2 => x1 + x2) f g = f + g
-- Init.Omega.Int
Lean.Omega.Int.add_le_zero_iff_le_neg' : ∀ {a b : ℤ}, a + b ≤ 0 ↔ b ≤ -a
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
/-- If `ed` is an extra degeneracy for `X : SimplicialObject.Augmented C` and
`F : C ⥤ D` is a functor, then `ed.map F` is an extra degeneracy for the
augmented simplicial object in `D` obtained by applying `F` to `X`.  -/
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.map : {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] →
        {X : CategoryTheory.SimplicialObject.Augmented C} →
          X.ExtraDegeneracy →
            (F : CategoryTheory.Functor C D) →
              (((CategoryTheory.SimplicialObject.Augmented.whiskering C D).obj F).obj X).ExtraDegeneracy
-- Mathlib.Algebra.Lie.Abelian
LieModule.coe_maxTrivEquiv_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : LieRingModule L N]
  [inst_10 : LieModule R L N] (e : M ≃ₗ⁅R,L⁆ N) (m : ↥(LieModule.maxTrivSubmodule R L M)),
  ↑((LieModule.maxTrivEquiv e) m) = e ↑m
-- Mathlib.Data.Multiset.Find
Multiset.find?_zero : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p], Multiset.find? p 0 ⋯ = none
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instCommMonoidWithZeroOfMonoidWithZeroHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → CommMonoidWithZero (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), MonoidWithZeroHomClass (T h) (G i) (G j)] →
                      CommMonoidWithZero (DirectLimit G f)
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
CompleteLattice.MulticoequalizerDiagram.multispanIndex.match_1.congr_eq_1 : ∀ {ι : Type u_1} (motive : (CategoryTheory.Limits.MultispanShape.prod ι).L → Sort u_2)
  (x : (CategoryTheory.Limits.MultispanShape.prod ι).L) (h_1 : (i j : ι) → motive (i, j)) (i j : ι),
  x = (i, j) →
    (match x with
      | (i, j) => h_1 i j) ≍
      h_1 i j
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.map_equation : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) {S : Type s} [inst_1 : CommRing S]
  {f : R →+* S}, Function.Injective ⇑f → ∀ (P : Fin 3 → R), (W'.map f).Equation (⇑f ∘ P) ↔ W'.Equation P
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.coe_map : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (c : OmegaCompletePartialOrder.Chain α)
  (f : α →o β), ⇑(c.map f) = ⇑f ∘ ⇑c
-- Mathlib.Analysis.Normed.Group.Real
Real.norm_nnratCast : ∀ (q : ℚ≥0), ‖↑q‖ = ↑q
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.lowerBound?.eq_1 : ∀ {α : Type u_1} (cut : α → Ordering) (x : Option α), RBTree.RBNode.lowerBound? cut RBTree.RBNode.nil x = x
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.PreservesLimitsOfShape.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {F : CategoryTheory.Functor C D},
  autoParam (∀ {K : CategoryTheory.Functor J C}, CategoryTheory.Limits.PreservesLimit K F)
      CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit._autoParam →
    CategoryTheory.Limits.PreservesLimitsOfShape J F
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instContinuousAdd : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [inst_2 : ContinuousAdd M],
  ContinuousAdd (SeparationQuotient M)
-- Mathlib.Geometry.Manifold.ContMDiffMap
/-- The first projection of a product, as a `C^n` map.  -/
ContMDiffMap.fst : {𝕜 : 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
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mem_carrier : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α} {a : α}, a ∈ L.carrier ↔ a ∈ L
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
Real.hasDerivAt_fourierChar : ∀ (x : ℝ), HasDerivAt (fun x => ↑(Real.fourierChar x)) (2 * ↑Real.pi * Complex.I * ↑(Real.fourierChar x)) x
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.ι₁_snd_assoc : ∀ (X : TopCat) {Z : TopCat} (h : TopCat.I ⟶ Z),
  CategoryTheory.CategoryStruct.comp TopCat.ι₁
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X TopCat.I) h) =
    CategoryTheory.CategoryStruct.comp (TopCat.const 1) h
-- Init.Sym.Lemmas
Lean.Sym.Int8.le_eq_false : ∀ (a b : Int8), decide (a ≤ b) = false → (a ≤ b) = False
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The `faceOppositeCentroid` equals the average displacement from a vertex plus that vertex.  -/
Affine.Simplex.faceOppositeCentroid_eq_sum_vsub_vadd : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.faceOppositeCentroid i = (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i) +ᵥ s.points i
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H1_induction_on : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} {C : ↑(groupCohomology.H1 A) → Prop}
  (x : ↑(groupCohomology.H1 A)),
  (∀ (x : ↥(groupCohomology.cocycles₁ A)), C ((CategoryTheory.ConcreteCategory.hom (groupCohomology.H1π A)) x)) → C x
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.ext : ∀ {R : Type u} {M : Type v} [inst : SMul R M] {p q : SubMulAction R M}, (∀ (x : M), x ∈ p ↔ x ∈ q) → p = q
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.starProjection_orthogonalComplement_singleton_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (v : E), (𝕜 ∙ v)ᗮ.starProjection v = 0
-- Mathlib.Topology.Constructible
Topology.IsLocallyConstructible.biUnion : ∀ {X : Type u_2} [inst : TopologicalSpace X] {ι : Type u_4} {f : ι → Set X} {s : Set ι},
  s.Finite → (∀ i ∈ s, Topology.IsLocallyConstructible (f i)) → Topology.IsLocallyConstructible (⋃ i ∈ s, f i)
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.isRkFinite_iff : ∀ {α : Type u_1} {M : Matroid α} {X : Set α},
  autoParam (X ⊆ M.E) Matroid.isRkFinite_iff._auto_1 → (M.IsRkFinite X ↔ ∃ I, M.IsBasis I X ∧ I.Finite)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- Remap a simplex along an `Equiv` of index types.  -/
Affine.Simplex.reindex : {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] →
              {m n : ℕ} → Affine.Simplex k P m → Fin (m + 1) ≃ Fin (n + 1) → Affine.Simplex k P n
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_ne_mem_ball : ∀ {c : ℂ} {R : ℝ} {w : ℂ}, w ∈ Metric.ball c R → ∀ (θ : ℝ), circleMap c R θ ≠ w
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
ProbabilityTheory.BrownianReal.variance_eval_projectiveFamily : ∀ {I : Finset NNReal} (s : ↥I),
  ProbabilityTheory.variance (fun x => x s) (ProbabilityTheory.BrownianReal.projectiveFamily I) = ↑↑s
-- Mathlib.Data.Option.Basic
Option.pmap.hcongr_6 : ∀ (α α' : Type u_1),
  α = α' →
    ∀ (β β' : Type u_2),
      β = β' →
        ∀ (p : α → Prop) (p' : α' → Prop),
          p ≍ p' →
            ∀ (f : (a : α) → p a → β) (f' : (a : α') → p' a → β'),
              f ≍ f' →
                ∀ (o : Option α) (o' : Option α'),
                  o ≍ o' →
                    ∀ (a : ∀ (a : α), o = some a → p a) (a' : ∀ (a : α'), o' = some a → p' a),
                      a ≍ a' → Option.pmap f o a ≍ Option.pmap f' o' a'
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
ProbabilityTheory.Kernel.integrable_traj : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {E : Type u_2} [inst_2 : NormedAddCommGroup E] {a b : ℕ},
  a ≤ b →
    ∀ {f : ((n : ℕ) → X n) → E} (x₀ : (i : ↥(Finset.Iic a)) → X ↑i),
      MeasureTheory.Integrable f ((ProbabilityTheory.Kernel.traj κ a) x₀) →
        ∀ᵐ (x : (i : ℕ) → X i) ∂(ProbabilityTheory.Kernel.traj κ a) x₀,
          MeasureTheory.Integrable f ((ProbabilityTheory.Kernel.traj κ b) (Preorder.frestrictLe b x))
-- ProofWidgets.Compat
ProofWidgets.ExprWithCtx.mk : Lean.Elab.ContextInfo → Lean.LocalContext → Lean.LocalInstances → Lean.Expr → ProofWidgets.ExprWithCtx
-- Mathlib.GroupTheory.Sylow
Sylow.smul_def : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {g : G} {P : Sylow p G}, g • P = MulAut.conj g • P
-- Mathlib.RingTheory.Coprime.Lemmas
IsCoprime.of_prod_left : ∀ {R : Type u} {I : Type v} [inst : CommSemiring R] {x : R} {s : I → R} {t : Finset I},
  IsCoprime (∏ i ∈ t, s i) x → ∀ i ∈ t, IsCoprime (s i) x
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.IsBridge.of_not_reachable : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, ¬G.Reachable u v → G.IsBridge s(u, v)
-- Mathlib.Order.Interval.Set.Pi
Set.image_mulSingle_Ioo_left : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → One (α i)] (i : ι) (a : α i), Pi.mulSingle i '' Set.Ioo a 1 = Set.Ioo (Pi.mulSingle i a) 1
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.supported_mono : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {s t : Set α}, s ⊆ t → Finsupp.supported M R s ≤ Finsupp.supported M R t
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix'_toLin' : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  (M : Matrix m n R), LinearMap.toMatrix' (Matrix.toLin' M) = M
-- Mathlib.Algebra.Field.Periodic
/-- If a function `f` is `Periodic` with positive period `c`, then for all `x` there exists some
`y ∈ Ico a (a + c)` such that `f x = f y`.  -/
Function.Periodic.exists_mem_Ico : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddCommGroup α] [inst_1 : LinearOrder α]
  [IsOrderedAddMonoid α] [Archimedean α],
  Function.Periodic f c → 0 < c → ∀ (x a : α), ∃ y ∈ Set.Ico a (a + c), f x = f y
-- Mathlib.NumberTheory.Zsqrtd.ToReal
Zsqrtd.toReal_apply : ∀ {d : ℤ} (h : 0 ≤ d) (a : ℤ√d), (Zsqrtd.toReal h) a = ↑a.re + ↑a.im * √↑d
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
RightPreLieRing.assoc_symm' : ∀ {L : Type u_1} [self : RightPreLieRing L] (x y z : L), associator x y z = associator x z y
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.algHom_ext_iff : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {f g : MvPolynomial σ R →ₐ[R] A}, f = g ↔ ∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.not_mem_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering} {k : α}, k ∉ ∅
-- Init.Grind.Config
/-- When `true`, it enables **function-valued congruence closure**.
`grind` treats equalities of partially applied functions as first-class equalities
and propagates them through further applications.
Given an application `f a₁ a₂ … aₙ`, when `funCC := true` *and* function equality is enabled for `f`,
`grind` generates and tracks equalities for all partial applications:
- `f a₁`
- `f a₁ a₂`
- `…`
- `f a₁ a₂ … aₙ`

This allows equalities such as `f a₁ = g` to propagate to
`f a₁ a₂ = g a₂`.

**When is function equality enabled for a symbol?**
Function equality is automatically enabled in the following cases:
1. **`f` is not a constant.** (For example, a lambda expression, a local variable, or a function parameter.)
2. **`f` is a structure field projection**, *provided the structure is not a `class`.*
3. **`f` is a constant marked with the attribute:** `@[grind funCC]`

If none of the above conditions apply, function equality is disabled for `f`, and congruence
closure behaves almost like it does in SMT solvers for first-order logic.
Here is an example, `grind` can solve when `funCC := true`
```
example (a b : Nat) (g : Nat → Nat) (f : Nat → Nat → Nat) (h : f a = g) :
  f a b = g b := by
grind
```
 -/
Lean.Grind.Config.funCC : Lean.Grind.Config → Bool
-- Std.Time.Format.Modifier
/-- Exactly midnight (00:00:00)
 -/
Std.Time.DayPeriod.midnight : Std.Time.DayPeriod
-- Init.System.IO
/-- Returns the value of the environment variable `var`, or `none` if it is not present in the
environment.
 -/
IO.getEnv : String → BaseIO (Option String)
-- Init.Data.SInt.Lemmas
Int64.le_trans : ∀ {a b c : Int64}, a ≤ b → b ≤ c → a ≤ c
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
VonNeumannAlgebra.coe_toStarSubalgebra : ∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H]
  (S : VonNeumannAlgebra H), ↑S.toStarSubalgebra = ↑S
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.comap_id' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β),
  κ.comap (fun a => a) ⋯ = κ
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.OptionsPerPos.insertAt : Lean.PrettyPrinter.Delaborator.OptionsPerPos →
  Lean.SubExpr.Pos → Lean.Name → Lean.DataValue → Lean.PrettyPrinter.Delaborator.OptionsPerPos
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.norm_expSeries_summable_of_mem_ball : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸],
  ∀ x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius,
    Summable fun n => ‖(NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x‖
-- Mathlib.Order.Interval.Basic
/-- The starting point of an interval is smaller than the endpoint.  -/
NonemptyInterval.fst_le_snd : ∀ {α : Type u_6} [inst : LE α] (self : NonemptyInterval α), self.toProd.1 ≤ self.toProd.2
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.translationNumber_mul_of_commute : ∀ {f g : CircleDeg1Lift}, Commute f g → (f * g).translationNumber = f.translationNumber + g.translationNumber
-- Init.Data.UInt.Lemmas
UInt64.ofNat_sub : ∀ {a b : ℕ}, b ≤ a → UInt64.ofNat (a - b) = UInt64.ofNat a - UInt64.ofNat b
-- Mathlib.Algebra.Homology.Homotopy
HomologicalComplex.homotopyEquivalences.of_homotopy : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D},
  HomologicalComplex.homotopyEquivalences V c f → ∀ (hfg : Homotopy f g), HomologicalComplex.homotopyEquivalences V c g
-- Std.Sync.SharedMutex
/-- Creates a new shared mutex.  -/
Std.SharedMutex.new : {α : Type} → α → BaseIO (Std.SharedMutex α)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
UniqueFactorizationMonoid.exists_mem_factors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {x : α},
  x ≠ 0 → ¬IsUnit x → ∃ p, p ∈ UniqueFactorizationMonoid.factors x
-- Lean.Widget.InteractiveCode
/-- A tag indicating the diff status of the expression. Used when showing tactic diffs.  -/
Lean.Widget.DiffTag : Type
-- Mathlib.CategoryTheory.Category.TwoP
/-- Adding a second point is left adjoint to forgetting the second point.  -/
pointedToTwoPFstForgetCompBipointedToPointedFstAdjunction : pointedToTwoPFst ⊣ (CategoryTheory.forget₂ TwoP Bipointed).comp bipointedToPointedFst