mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.map_hom_ofInv_id_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (W : CategoryTheory.MorphismProperty C) {X Y : C} (s : Y ⟶ X)
  (hs : W s) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) {Z : D} (h : L.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (L.map s)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.RightFraction.ofInv s hs).map L hL) h) =
    h
-- Mathlib.Analysis.PSeries
/-- Test for convergence of the `p`-series: the real-valued series `∑' n : ℕ, (n ^ p)⁻¹` converges
if and only if `1 < p`.  -/
Real.summable_nat_pow_inv : ∀ {p : ℕ}, (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Bicategory.mateEquiv.eq_1 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d e f : B} {g : c ⟶ e} {h : d ⟶ f} {l₁ : c ⟶ d} {r₁ : d ⟶ c}
  {l₂ : e ⟶ f} {r₂ : f ⟶ e} (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁)
  (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂),
  CategoryTheory.Bicategory.mateEquiv adj₁ adj₂ =
    adj₂.homEquiv₂.trans
      (((CategoryTheory.Iso.refl g).homCongr (CategoryTheory.Bicategory.associator l₁ h r₂)).trans adj₁.homEquiv₁)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.instDistribMulAction : {ι : Type v} →
  {M₁ : ι → Type w₁} →
    {M₂ : Type w₂} →
      {R' : Type u_1} →
        {A : Type u_3} →
          [inst : Monoid R'] →
            [inst_1 : Semiring A] →
              [inst_2 : (i : ι) → AddCommMonoid (M₁ i)] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : (i : ι) → TopologicalSpace (M₁ i)] →
                    [inst_5 : TopologicalSpace M₂] →
                      [inst_6 : (i : ι) → Module A (M₁ i)] →
                        [inst_7 : Module A M₂] →
                          [inst_8 : DistribMulAction R' M₂] →
                            [ContinuousConstSMul R' M₂] →
                              [SMulCommClass A R' M₂] →
                                [inst_11 : ContinuousAdd M₂] → DistribMulAction R' (ContinuousMultilinearMap A M₁ M₂)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.coe_toEquiv_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β), ⇑e.symm = ⇑e.symm
-- Init.Data.Array.Lemmas
Array.getElem_extract : ∀ {α : Type u_1} {i : ℕ} {xs : Array α} {start stop : ℕ} (h : i < (xs.extract start stop).size),
  (xs.extract start stop)[i] = xs[start + i]
-- Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky
/-- The set of ideals of a semiring `R` that are disjoint from a given subsemigroup `S`.  -/
_private.Mathlib.RingTheory.UniqueFactorizationDomain.Kaplansky.0.UniqueFactorizationMonoid.kaplanskySet : {R : Type u_1} → [inst : Semiring R] → Subsemigroup R → Set (Ideal R)
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_congr_smul_measure : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C C' : ℝ} (c : ENNReal),
  c ≠ ⊤ →
    ∀ (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
      (hT_smul : MeasureTheory.DominatedFinMeasAdditive (c • μ) T C') (f : α → E),
      MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun (c • μ) T hT_smul f
-- Mathlib.Data.List.Sort
List.sortedGT_reverse : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.reverse.SortedGT ↔ l.SortedLT
-- Init.WFExtrinsicFix
WellFounded.extrinsicFix₂_eq_apply : ∀ {α : Sort u_2} {β : α → Sort u_3} {C₂ : (a : α) → β a → Sort u_1} [inst : ∀ (a : α) (b : β a), Nonempty (C₂ a b)]
  {R : (a : α) ×' β a → (a : α) ×' β a → Prop}
  {F : (a : α) → (b : β a) → ((a' : α) → (b' : β a') → R ⟨a', b'⟩ ⟨a, b⟩ → C₂ a' b') → C₂ a b},
  WellFounded R →
    ∀ {a : α} {b : β a}, WellFounded.extrinsicFix₂ R F a b = F a b fun a' b' x => WellFounded.extrinsicFix₂ R F a' b'
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.add_leftNegEquiv : ∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S.leftNeg),
  ↑x + ↑((S.leftNegEquiv hS) x) = 0
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
/-- The composite `A ⨯ A ⟶ cokernel (diag A) ⟶ A` given by the natural projection into the cokernel
followed by the inverse of `r`. In the category of modules, using the normal kernels and
cokernels, this map is equal to the map `(a, b) ↦ a - b`, hence the name `σ` for "subtraction".  -/
CategoryTheory.NonPreadditiveAbelian.σ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [inst_1 : CategoryTheory.NonPreadditiveAbelian C] → {A : C} → A ⨯ A ⟶ A
-- Mathlib.Algebra.Lie.TraceForm
LieIdeal.restrict_killingForm : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
  (killingForm R L).restrict (LieIdeal.toLieSubalgebra R L I).toSubmodule = LieModule.traceForm R (↥I) L
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
/-- Given an embedding `e : c.Embedding c'` of complex shapes, the
functor `e.extendHomotopyFunctor C` on homotopy categories is
induced by the functor `e.extendFunctor C` on homological complexes.  -/
ComplexShape.Embedding.extendHomotopyFunctorFactors : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        (e : c.Embedding c') →
          [inst : e.IsRelIff] →
            (C : Type u_3) →
              [inst_1 : CategoryTheory.Category.{v_1, u_3} C] →
                [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
                  [inst_3 : CategoryTheory.Preadditive C] →
                    (HomotopyCategory.quotient C c).comp (e.extendHomotopyFunctor C) ≅
                      (e.extendFunctor C).comp (HomotopyCategory.quotient C c')
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.liftToPathCategory_obj : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {D : Type uD}
  [inst_1 : CategoryTheory.Category.{uD', uD} D] (G : CategoryTheory.Functor C D) (hG : W.IsInvertedBy G)
  (X : CategoryTheory.Paths (CategoryTheory.Localization.Construction.LocQuiver W)),
  (CategoryTheory.Localization.Construction.liftToPathCategory G hG).obj X = G.obj X.obj
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.dist_toLp_single_same : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_2 : DecidableEq ι] (i : ι) (b₁ b₂ : β i),
  dist (WithLp.toLp p (Pi.single i b₁)) (WithLp.toLp p (Pi.single i b₂)) = dist b₁ b₂
-- Mathlib.Logic.Basic
Decidable.forall_or_left : ∀ {α : Sort u_1} {q : Prop} {p : α → Prop} [Decidable q], (∀ (x : α), q ∨ p x) ↔ q ∨ ∀ (x : α), p x
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.instInhabitedSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers : {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) →
                Inhabited ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.ofIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X : C}
  [inst_2 : CategoryTheory.AddMonObj M] (e : M ≅ X),
  CategoryTheory.AddMonObj.ofIso e =
    { zero := CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero e.hom,
      add :=
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.inv e.inv)
          (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add e.hom),
      zero_add := ⋯, add_zero := ⋯, add_assoc := ⋯ }
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.one_sub_le_one : ∀ {β : Type u_2} [inst : Ring β] [inst_1 : PartialOrder β] [IsOrderedRing β] (x : ↑(Set.Icc 0 1)), 1 - ↑x ≤ 1
-- Init.Data.UInt.Lemmas
UInt64.ofNatLT_uInt8ToNat : ∀ (n : UInt8), UInt64.ofNatLT n.toNat ⋯ = n.toUInt64
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.inr_comp_binaryCoproductIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
      (CategoryTheory.FunctorToTypes.binaryCoproductIso F G).hom =
    CategoryTheory.FunctorToTypes.coprod.inr
-- Lean.Exception
/-- Return true if `ex` was generated by `throwMaxRecDepthAt`.
This function is a bit hackish. The max rec depth exception should probably be an internal exception,
but it is also produced by `MacroM` which implemented in the prelude, and internal exceptions have not
been defined yet.
 -/
Lean.Exception.isMaxRecDepth : Lean.Exception → Bool
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.MorphismProperty.le_isColocal_isColocal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C),
  W ≤ W.isColocal.isColocal
-- Lean.Log
/-- Log a new warning message using the given message data. The position is provided by `ref`.  -/
Lean.logWarningAt : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] → [Lean.AddMessageContext m] → [Lean.MonadOptions m] → Lean.Syntax → Lean.MessageData → m Unit
-- Init.Data.BitVec.Lemmas
BitVec.getElem_allOnes : ∀ {v : ℕ} (i : ℕ) (h : i < v), (BitVec.allOnes v)[i] = true
-- Mathlib.Analysis.Complex.Schwarz
/-- The **Schwarz Lemma**: if `f : ℂ → E` is complex analytic
on an open disk with center `c` and a positive radius `R₁`,
and it sends this disk to a closed ball with center `f c` and radius `R₂`,
then the norm of the derivative of `f` at `c` is at most the ratio `R₂ / R₁`.  -/
Complex.norm_deriv_le_div_of_mapsTo_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R₁ R₂ : ℝ} {f : ℂ → E} {c : ℂ},
  DifferentiableOn ℂ f (Metric.ball c R₁) →
    Set.MapsTo f (Metric.ball c R₁) (Metric.closedBall (f c) R₂) → 0 < R₁ → ‖deriv f c‖ ≤ R₂ / R₁
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.toAut_isHomeomorph : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] (G : Type u_1) [inst_2 : Group G]
  [inst_3 : (X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.FiberFunctor F]
  [inst_5 : TopologicalSpace G] [inst_6 : IsTopologicalGroup G] [inst_7 : CompactSpace G]
  [inst_8 : CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G],
  IsHomeomorph ⇑(CategoryTheory.PreGaloisCategory.toAut F G)
-- Mathlib.GroupTheory.IsPerfect
/-- The trivial group is perfect.  -/
Group.IsPerfect.instOfSubsingleton : ∀ {G : Type u_1} [inst : Group G] [Subsingleton G], Group.IsPerfect G
-- Mathlib.Analysis.Normed.Lp.MeasurableSpace
PiLp.topologicalSpace.eq_1 : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [inst : (i : ι) → TopologicalSpace (β i)],
  PiLp.topologicalSpace p β = TopologicalSpace.induced WithLp.ofLp Pi.topologicalSpace
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.CongrInfo.interlaced.sizeOf_spec : ∀ (rewritable : Array Bool), sizeOf (Lean.Meta.Sym.CongrInfo.interlaced rewritable) = 1 + sizeOf rewritable
-- Mathlib.RingTheory.Ideal.Int
Int.ringChar_idealQuot : ∀ (n : ℕ), ringChar (ℤ ⧸ Ideal.span {↑n}) = n
-- Mathlib.RingTheory.Smooth.AdicCompletion
/-- If `A` is formally smooth over `R`, the projection from the adic completion of
`S` at the kernel of `f : S →ₐ[R] A` has a section.  -/
Algebra.FormallySmooth.exists_kerProj_comp_eq_id : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {S : Type u_3}
  [inst_3 : CommRing S] [inst_4 : Algebra R S] [Algebra.FormallySmooth R A] (f : S →ₐ[R] A)
  (hf : Function.Surjective ⇑f), ∃ g, (AdicCompletion.kerProj hf).comp g = AlgHom.id R A
-- Aesop.Frontend.Tactic
Aesop.Frontend.TacticConfig.enabledRuleSets : Aesop.Frontend.TacticConfig → Std.HashSet Aesop.RuleSetName
-- Mathlib.LinearAlgebra.TensorProduct.Associator
/-- Given linear maps `f : M → Q`, `g : N → S`, and `h : P → T`, if we identify `(M ⊗ N) ⊗ P`
with `M ⊗ (N ⊗ P)` and `(Q ⊗ S) ⊗ T` with `Q ⊗ (S ⊗ T)`, then this lemma states that
`f ⊗ (g ⊗ h) = (f ⊗ g) ⊗ h`.  -/
TensorProduct.map_map_comp_assoc_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9}
  {T : Type u_10} [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P]
  [inst_4 : AddCommMonoid Q] [inst_5 : AddCommMonoid S] [inst_6 : AddCommMonoid T] [inst_7 : Module R M]
  [inst_8 : Module R N] [inst_9 : Module R Q] [inst_10 : Module R S] [inst_11 : Module R T] [inst_12 : Module R P]
  (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T),
  TensorProduct.map f (TensorProduct.map g h) ∘ₗ ↑(TensorProduct.assoc R M N P) =
    ↑(TensorProduct.assoc R Q S T) ∘ₗ TensorProduct.map (TensorProduct.map f g) h
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleRing.ideal_eq_span_idempotent : ∀ {R : Type u_2} [inst : Ring R] [IsSemisimpleRing R] (I : Ideal R), ∃ e, IsIdempotentElem e ∧ I = Ideal.span {e}
-- Mathlib.Order.Interval.Set.Basic
Set.self_notMem_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, a ∉ Set.Ioi a
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.isClassImp? : Lean.Expr → Lean.MetaM (Option Lean.Name)
-- Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy
/-- A simplicial homotopy between `f` and `g` induces a chain homotopy
between the induced morphisms on the alternating face map complexes.  -/
CategoryTheory.SimplicialObject.Homotopy.toChainHomotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : CategoryTheory.SimplicialObject C} →
        {f g : X ⟶ Y} →
          CategoryTheory.SimplicialObject.Homotopy f g →
            Homotopy ((AlgebraicTopology.alternatingFaceMapComplex C).map f)
              ((AlgebraicTopology.alternatingFaceMapComplex C).map g)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableOn.smul_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F] [IsBoundedSMul 𝕜' F]
  [IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'}, DifferentiableOn 𝕜 c s → ∀ (f : F), DifferentiableOn 𝕜 (fun y => c y • f) s
-- Lean.Compiler.IR.Basic
Lean.IR.instReprCtorInfo.repr : Lean.IR.CtorInfo → ℕ → Std.Format
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.sum_comm : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : Countable ι]
  (κ : ι → ι → ProbabilityTheory.Kernel α β),
  (ProbabilityTheory.Kernel.sum fun n => ProbabilityTheory.Kernel.sum (κ n)) =
    ProbabilityTheory.Kernel.sum fun m => ProbabilityTheory.Kernel.sum fun n => κ n m
-- Mathlib.Topology.UniformSpace.CompareReals
/-- The metric space uniform structure on ℚ (which presupposes the existence
of real numbers) agrees with the one coming directly from (abs : ℚ → ℚ).  -/
Rat.uniformSpace_eq : AbsoluteValue.abs.uniformSpace = PseudoMetricSpace.toUniformSpace
-- Mathlib.FieldTheory.Galois.Abelian
instIsAbelianGaloisSubtypeMemIntermediateField : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [IsAbelianGalois K L]
  (K' : IntermediateField K L), IsAbelianGalois K ↥K'
-- Std.Data.HashMap.Basic
Std.HashMap.Equiv.mk : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β},
  m₁.inner.Equiv m₂.inner → m₁.Equiv m₂
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHomClass.toLatticeHomClass : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} {inst : Lattice α} {inst_1 : Lattice β} {inst_2 : BoundedOrder α}
  {inst_3 : BoundedOrder β} {inst_4 : FunLike F α β} [self : BoundedLatticeHomClass F α β], LatticeHomClass F α β
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.ext_iff : ∀ {α : Type u₁} {x y : CategoryTheory.Discrete α}, x = y ↔ x.as = y.as
-- Init.Data.Float.Model.Unpacked.Operations.ToNat
/-- Converts an `UnpackedFloat` to an `ISize`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.UnpackedFloat.toISize : Float.Model.UnpackedFloat → ISize
-- Mathlib.CategoryTheory.Abelian.Subcategory
CategoryTheory.ObjectProperty.preservesEpimorphisms_ι_of_isNormalMonoCategory : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFiniteProducts C]
  [CategoryTheory.Limits.HasKernels C] [CategoryTheory.Limits.HasCokernels C] [CategoryTheory.IsNormalMonoCategory C]
  [CategoryTheory.Limits.HasZeroObject C] [P.ContainsZero] [P.IsClosedUnderCokernels], P.ι.PreservesEpimorphisms
-- Mathlib.GroupTheory.CommutingProbability
DihedralGroup.commProb_cons : ∀ (n : ℕ) (l : List ℕ),
  commProb (DihedralGroup.Product (n :: l)) = commProb (DihedralGroup n) * commProb (DihedralGroup.Product l)
-- Mathlib.RingTheory.SimpleRing.DivisionRing
isSimpleModule_iff_eq_zero_or_injective : ∀ (R : Type u) (M : Type v) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsSimpleModule R M ↔
    Nontrivial M ∧
      ∀ (N : Type v) [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N), f = 0 ∨ Function.Injective ⇑f
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousWithinAt_neg_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {s : Set α} {a : α} [inst_1 : PartialOrder β]
  [inst_2 : AddCommGroup β] [IsOrderedAddMonoid β],
  UpperSemicontinuousWithinAt (-f) s a ↔ LowerSemicontinuousWithinAt f s a
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientGroup.discreteTopology_iff : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] {N : Subgroup G},
  DiscreteTopology (G ⧸ N) ↔ IsOpen ↑N
-- Mathlib.CategoryTheory.Comma.Arrow
/-- Given a square from an isomorphism `i` to an arrow `p`, express the target part of `sq`
in terms of the inverse of `i`.  -/
CategoryTheory.Arrow.square_from_iso_invert : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {X Y : T} (i : X ≅ Y) (p : CategoryTheory.Arrow T)
  (sq : CategoryTheory.Arrow.mk i.hom ⟶ p),
  CategoryTheory.CategoryStruct.comp i.inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) p.hom) =
    CategoryTheory.Arrow.Hom.right sq
-- Std.Sat.AIG.Lemmas
/-- The AIG produced by `AIG.mkGate` agrees with the input AIG on all indices that are valid for both.
 -/
Std.Sat.AIG.mkGate_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (idx : ℕ) (aig : Std.Sat.AIG α) (input : aig.BinaryInput)
  {h : idx < aig.decls.size},
  have this := ⋯;
  (aig.mkGate input).aig.decls[idx] = aig.decls[idx]
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.isReal_iff : ∀ {K : Type u_1} [inst : Field K] {φ : K →+* ℂ},
  NumberField.ComplexEmbedding.IsReal φ ↔ NumberField.ComplexEmbedding.conjugate φ = φ
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
inv_lt_div_iff_lt_mul : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] [MulRightStrictMono α] {a b c : α},
  a⁻¹ < b / c ↔ c < a * b
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasFDerivAt.csinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E},
  HasFDerivAt f f' x → HasFDerivAt (fun x => Complex.sinh (f x)) (Complex.cosh (f x) • f') x
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.length_of : ∀ {α : Type u_1} (m : α), (FreeAddMonoid.of m).length = 1
-- Mathlib.Data.Finset.Fin
Finset.coe_attachFin : ∀ {n : ℕ} {s : Finset ℕ} (h : ∀ m ∈ s, m < n), ↑(s.attachFin h) = Fin.val ⁻¹' ↑s
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.map_div : ∀ {R : Type u} {k : Type y} [inst : Field R] {p q : Polynomial R} [inst_1 : Field k] (f : R →+* k),
  Polynomial.map f (p / q) = Polynomial.map f p / Polynomial.map f q
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Stream'.cons.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pushforward_bot : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X),
  CategoryTheory.Sieve.pushforward f ⊥ = ⊥
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.div_subset_div : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s₁ s₂ t₁ t₂ : Finset α}, s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ / t₁ ⊆ s₂ / t₂
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey!_eq_default : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)}, l.isEmpty = true → Std.Internal.List.minKey! l = default
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.continuousWithinAt_of_dominated : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {X : Type u_6} [inst_2 : TopologicalSpace X] [FirstCountableTopology X] {F : X → α → G}
  {x₀ : X} {bound : α → ℝ} {s : Set X},
  (∀ᶠ (x : X) in nhdsWithin x₀ s, MeasureTheory.AEStronglyMeasurable (F x) μ) →
    (∀ᶠ (x : X) in nhdsWithin x₀ s, ∀ᵐ (a : α) ∂μ, ‖F x a‖ ≤ bound a) →
      MeasureTheory.Integrable bound μ →
        (∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x => F x a) s x₀) →
          ContinuousWithinAt (fun x => ∫ (a : α), F x a ∂μ) s x₀
-- Init.Data.Array.Extract
Array.extract_extract : ∀ {α : Type u_1} {as : Array α} {i j k l : ℕ}, (as.extract i j).extract k l = as.extract (i + k) (min (i + l) j)
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atBot_add_atBot : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedAddMonoid M] {l : Filter α}
  {f g : α → M},
  Filter.Tendsto f l Filter.atBot → Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x + g x) l Filter.atBot
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Extract
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {newWidth : ℕ} →
        (aig : Std.Sat.AIG α) →
          Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget aig newWidth → Std.Sat.AIG.RefVecEntry α newWidth
-- Mathlib.FieldTheory.SeparableDegree
/-- If `x` is a separable element, then `x⁻¹` is also a separable element.  -/
Field.isSeparable_inv : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  IsSeparable F x → IsSeparable F x⁻¹
-- Lean.Meta.Sym.Pattern
/-- Returns `true` if the metavariable `mvarId` can be assigned in the current context.
When `unify` is `true`, uses the default condition (not read-only nor synthetic opaque).
When `unify` is `false`, only metavariables in `mvarsNew` can be assigned. That is,
only metavariables associated with pattern variables can be assigned.
 -/
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.isAssignableMVar : Lean.MVarId → Lean.Meta.Sym.DefEqM✝ Bool
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.diff_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {t₃ t₄ : Std.DTreeMap.Raw α β cmp},
  t₁.WF → t₂.WF → t₃.WF → t₄.WF → t₁.Equiv t₃ → t₂.Equiv t₄ → (t₁ \ t₂).Equiv (t₃ \ t₄)