mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Category.LightProfinite.AsLimit
/-- `S.asLimitConeAux` is indeed a limit cone.
(Auxiliary definition, use `S.asLimit` instead.)
 -/
LightProfinite.asLimitAux : (S : LightProfinite) → CategoryTheory.Limits.IsLimit S.asLimitConeAux
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.foldlM_list : ∀ {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {ps : Std.Do.PostShape} [inst : Monad m]
  [inst_1 : Std.Do.WPMonad m ps] {xs : List α} {init : β} {f : β → α → m β} (inv : Std.Do.Invariant xs β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f b cur ⦃(fun b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b'), inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs, property := ⋯ }, init)⦄
      List.foldlM f init xs ⦃(fun b => inv.1 ({ «prefix» := xs, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.NumberTheory.PythagoreanTriples
/-- A parameterization of the unit circle that is useful for classifying Pythagorean triples.
(To be applied in the case where `K = ℚ`.)  -/
circleEquivGen : {K : Type u_1} → [inst : Field K] → (∀ (x : K), 1 + x ^ 2 ≠ 0) → K ≃ { p // p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1 }
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- The product type `X × Y` is a binary product for `X` and `Y`.  -/
CategoryTheory.Limits.Types.binaryProductLimit : (X Y : Type u) → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Types.binaryProductCone X Y)
-- Mathlib.Control.Random
/-- Create a new random number generator distinct from the one stored in the state.  -/
Rand.split : {m : Type → Type u_1} → {g : Type} → [RandomGen g] → [Monad m] → RandGT g m g
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.forgetCreatesPullbackOfRight : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : AlgebraicGeometry.SheafedSpace C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] →
            CategoryTheory.CreatesLimit (CategoryTheory.Limits.cospan g f)
              AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.instContinuousSMulReal : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞}, ContinuousSMul ℝ (TestFunction Ω F n)
-- Mathlib.Topology.AlexandrovDiscrete
isOpen_iff_forall_specializes : ∀ {α : Type u_3} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {s : Set α},
  IsOpen s ↔ ∀ (x y : α), x ⤳ y → y ∈ s → x ∈ s
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.tprod_nil : ∀ {δ : Type u_4} {X : δ → Type u_5} [inst : (i : δ) → MeasurableSpace (X i)]
  (μ : (i : δ) → MeasureTheory.Measure (X i)), MeasureTheory.Measure.tprod [] μ = MeasureTheory.Measure.dirac PUnit.unit
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.instCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      CategoryTheory.Category.{v_1, max u_1 v_1} (CategoryTheory.ShortComplex C)
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
AlgebraicGeometry.IsPreimmersion.isEmbedding : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.IsPreimmersion f], Topology.IsEmbedding ⇑f
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabMutualDef.processDeriving : Array Lean.Elab.DefView → Array Lean.Elab.DefViewElabHeader → Lean.Elab.TermElabM Unit
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.Indep.of_isRestriction : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} {N : Matroid α}, N.Indep I → N.IsRestriction M → M.Indep I
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
/-- The induced functor `CofibrantObject.HoCat C ⥤ D`, when `D` is a localization
of `C` with respect to weak equivalences.  -/
HomotopicalAlgebra.CofibrantObject.HoCat.toLocalization : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          (L : CategoryTheory.Functor C D) →
            [L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] →
              CategoryTheory.Functor (HomotopicalAlgebra.CofibrantObject.HoCat C) D
-- Mathlib.Algebra.Order.Archimedean.Defs
Archimedean.mk : ∀ {R : Type u_2} [inst : AddCommMonoid R] [inst_1 : PartialOrder R],
  (∀ (x : R) {y : R}, 0 < y → ∃ n, x ≤ n • y) → Archimedean R
-- Batteries.Lean.EStateM
EStateM.run_seqRight : ∀ {ε σ α β : Type u_1} (x : EStateM ε σ α) (y : EStateM ε σ β) (s : σ),
  (x *> y).run s =
    match x.run s with
    | EStateM.Result.ok a s => y.run s
    | EStateM.Result.error e s => EStateM.Result.error e s
-- Mathlib.Computability.RegularExpressions
RegularExpression.brecOn.eq : ∀ {α : Type u} {motive : RegularExpression α → Sort u_1} (t : RegularExpression α)
  (F_1 : (t : RegularExpression α) → RegularExpression.below t → motive t),
  RegularExpression.brecOn t F_1 = F_1 t (RegularExpression.brecOn.go t F_1).2
-- Mathlib.Order.CompleteBooleanAlgebra
inf_iSup_eq : ∀ {α : Type u} {ι : Sort w} [inst : Order.Frame α] (a : α) (f : ι → α), a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.Functor.PreservesRightHomologyOf.congr_simp : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F F_1 : CategoryTheory.Functor C D) (e_F : F = F_1)
  [inst_4 : F.PreservesZeroMorphisms] (S S_1 : CategoryTheory.ShortComplex C),
  S = S_1 → F.PreservesRightHomologyOf S = F_1.PreservesRightHomologyOf S_1
-- Mathlib.Combinatorics.Matroid.Sum
Matroid.IsBase.eq_union_image_of_disjointSum : ∀ {α : Type u_1} {M N : Matroid α} {h : Disjoint M.E N.E} {B : Set α},
  (M.disjointSum N h).IsBase B → ∃ BM BN, M.IsBase BM ∧ N.IsBase BN ∧ Disjoint BM BN ∧ B = BM ∪ BN
-- Mathlib.Order.CompleteLattice.Defs
CompleteLattice.toPartialOrder' : {α : Type u_1} → [CompleteLattice α] → PartialOrder α
-- Init.Data.SInt.Lemmas
ISize.toInt_zero : ISize.toInt 0 = 0
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.descFSucc.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z) (n : ℕ)
  (g g_1 : J.cocomplex.X n ⟶ I.cocomplex.X n) (e_g : g = g_1) (g' : J.cocomplex.X (n + 1) ⟶ I.cocomplex.X (n + 1))
  (w :
    CategoryTheory.CategoryStruct.comp (J.cocomplex.d n (n + 1)) g' =
      CategoryTheory.CategoryStruct.comp g (I.cocomplex.d n (n + 1))),
  I.descFSucc J n g g' w = I.descFSucc J n g_1 g' ⋯
-- Std.Data.String.ToNat
Nat.toNat?_repr : ∀ (n : ℕ), n.repr.toNat? = some n
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (curr : ℕ) (h_1 : Unit → motive 0) (h_2 : (curr : ℕ) → motive curr.succ),
  (match curr.succ with
    | 0 => h_1 ()
    | curr.succ => h_2 curr) =
    h_2 curr
-- Init.Data.List.Nat.Prod
List.prod_replicate_nat : ∀ {n a : ℕ}, (List.replicate n a).prod = a ^ n
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
lt_iff_exists_one_lt_mul : ∀ {α : Type u} [inst : MulOneClass α] [inst_1 : Preorder α] [ExistsMulOfLE α] {a b : α} [MulLeftStrictMono α]
  [MulLeftReflectLT α], a < b ↔ ∃ c, 1 < c ∧ a * c = b
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.VersionedHtml.idx : ProofWidgets.RefreshComponent.VersionedHtml → ℕ
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.vadd_linear : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 →ᵃ[k] V2) (g : P1 →ᵃ[k] P2),
  (f +ᵥ g).linear = f.linear + g.linear
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_lt_add_right : ∀ {a b c : ENNReal}, a ≠ ⊤ → b < c → b + a < c + a
-- Init.Data.List.Sublist
List.getLast_filter_mem : ∀ {α : Type u_1} (xs : List α) (p : α → Bool) (h : List.filter p xs ≠ []), (List.filter p xs).getLast h ∈ xs
-- Mathlib.Util.Notation3
/-- Interpret a `prettyPrintOpt`. The default value is `true`.  -/
Mathlib.Notation3.getPrettyPrintOpt : Option (Lean.TSyntax `Mathlib.Notation3.prettyPrintOpt) → Bool
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.toSingleMk.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : K.X p ⟶ X) {n : ℤ}
  (x : p + n = q),
  CochainComplex.HomComplex.Cochain.toSingleMk f x =
    CochainComplex.HomComplex.Cochain.single
      (CategoryTheory.CategoryStruct.comp f (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) q X).inv) n
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- If `L` has well-defined support, then so does its comap along an embedding.  -/
SummationFilter.instHasSupportComap : ∀ {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) [L.HasSupport] (f : γ ↪ β), (L.comap f).HasSupport
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
/-- The left unitor isomorphism for the monoidal structure in `AugmentedSimplexCategory`  -/
AugmentedSimplexCategory.leftUnitor : (x : AugmentedSimplexCategory) → AugmentedSimplexCategory.tensorUnit.tensorObj x ≅ x
-- Std.Sync.SharedMutex
Std.instCoeOutSharedMutexBaseSharedMutex : {α : Type} → CoeOut (Std.SharedMutex α) Std.BaseSharedMutex
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.equivPair_tail : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (M i)] {i : ι} (p : Monoid.CoprodI.Word.Pair M i),
  (Monoid.CoprodI.Word.equivPair i) p.tail = { head := 1, tail := p.tail, fstIdx_ne := ⋯ }
-- Mathlib.Order.Filter.NAry
/-- If `b` is a right identity for `f : α → β → α`, then `pure b` is a right identity for
`Filter.map₂ f`.  -/
Filter.map₂_right_identity : ∀ {α : Type u_1} {β : Type u_3} {f : α → β → α} {b : β},
  (∀ (a : α), f a b = a) → ∀ (l : Filter α), Filter.map₂ f l (pure b) = l
-- Mathlib.Algebra.Group.Commute.Defs
Commute.on_refl : ∀ {G : Type u_1} {S : Type u_3} [inst : Mul S] {f : G → S}, Std.Refl fun a b => Commute (f a) (f b)
-- Mathlib.Analysis.Complex.ReImTopology
/-- **Alias** of `Complex.frontier_setOfPred_im_lt`. -/
Complex.frontier_setOf_im_lt : ∀ (a : ℝ), frontier {z | z.im < a} = {z | z.im = a}
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitMono.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {X Y : C} {f : X ⟶ Y} {x y : CategoryTheory.SplitMono f},
  x.retraction = y.retraction → x = y
-- Std.Tactic.BVDecide.LRAT.Internal.CNF
Std.Tactic.BVDecide.LRAT.Internal.Literal.sat_negate_iff_not_sat : ∀ {α : Type u_1} {p : α → Bool} {l : Std.Sat.Literal α},
  Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p l.negate ↔ ¬Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p l
-- Mathlib.Algebra.Homology.Embedding.Connect
/-- If `h : ConnectData K L`, then `h.cochainComplex` identifies to `L` in degrees `≥ 0`.  -/
CochainComplex.ConnectData.restrictionGEIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {K : ChainComplex C ℕ} →
        {L : CochainComplex C ℕ} →
          (h : CochainComplex.ConnectData K L) →
            HomologicalComplex.restriction h.cochainComplex (ComplexShape.embeddingUpIntGE 0) ≅ L
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.smul_def : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (T : CentroidHom α) (a : α), T • a = T a
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.PreDiscrTree.instAppend : {α : Type} → Append (Lean.Meta.LazyDiscrTree.PreDiscrTree α)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_hom_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {i i' j j' : E.I₀} (u₀ : E.I₀ → F.I₀)
  (u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)) (z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k))
  (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso hii' hjj' k).hom (z i j k) =
    CategoryTheory.CategoryStruct.comp (z i' j' ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj') k))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
        (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k)).hom)
-- Mathlib.Data.Countable.Defs
Finite.to_countable : ∀ {α : Sort u} [Finite α], Countable α
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_smul_left : ∀ {α : 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 α}
  [inst_4 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (c : ℝ)
  (f : ↥(MeasureTheory.Lp E 1 μ)), (MeasureTheory.L1.setToL1 ⋯) f = c • (MeasureTheory.L1.setToL1 hT) f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The complex hyperbolic cosine function is everywhere differentiable, with the derivative
`sinh x`.  -/
Complex.hasDerivAt_cosh : ∀ (x : ℂ), HasDerivAt Complex.cosh (Complex.sinh x) x
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.linkTarget.ref : Lean.Parser.ParserFn
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_add_eq_left_of_degree_lt : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, q.degree < p.degree → (p + q).natDegree = p.natDegree
-- Mathlib.Data.Fintype.Sum
Finset.toLeft_eq_univ : ∀ {α : Type u_3} {β : Type u_4} [inst : Fintype α] {u : Finset (α ⊕ β)},
  u.toLeft = Finset.univ ↔ Finset.map Function.Embedding.inl Finset.univ ⊆ u
-- Mathlib.Data.TypeVec
TypeVec.prod.snd.eq_1 : ∀ (n : ℕ) (α β : TypeVec.{u} n.succ) (i : Fin2 n), TypeVec.prod.snd i.fs = TypeVec.prod.snd i
-- Mathlib.Order.Basic
exists_forall_ge_and : ∀ {α : Type u_2} [inst : LinearOrder α] {p q : α → Prop},
  (∃ i, ∀ j ≥ i, p j) → (∃ i, ∀ j ≥ i, q j) → ∃ i, ∀ j ≥ i, p j ∧ q j
-- Mathlib.Topology.Sober
IsGenericPoint.specializes : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x y : α} {S : Set α}, IsGenericPoint x S → y ∈ S → x ⤳ y
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.symm_comp_rid_symm : ∀ {R : Type u_1} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ↑(TensorProduct.comm R M R) ∘ₗ ↑(TensorProduct.rid R M).symm = ↑(TensorProduct.lid R M).symm
-- Init.Data.Fin.Lemmas
Fin.lt_irrefl : ∀ {n : ℕ} (a : Fin n), ¬a < a
-- Init.Data.Repr
_private.Init.Data.Repr.0.Char.quoteCore.smallCharToHex : Char → String
-- Mathlib.FieldTheory.Relrank
IntermediateField.relrank_top_left : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A : IntermediateField F E),
  ⊤.relrank A = 1
-- Mathlib.CategoryTheory.Limits.Presentation
CategoryTheory.Limits.LimitPresentation.reindex_diag : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.Category.{t, w} J]
  {X : C} (P : CategoryTheory.Limits.LimitPresentation J X) {J' : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J'] (F : CategoryTheory.Functor J' J) [inst_3 : F.Initial],
  (P.reindex F).diag = F.comp P.diag
-- Mathlib.Analysis.ODE.ExistUnique
/-- **Picard-Lindelöf (Cauchy-Lipschitz) theorem**, differential form. This version shows the
existence of a local flow and that it is continuous on its domain as a (partial) map `E × ℝ → E`.  -/
IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_continuousOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E → E}
  {tmin tmax : ℝ} {t₀ : ↑(Set.Icc tmin tmax)} {x₀ : E} {a r L K : NNReal},
  IsPicardLindelof f t₀ x₀ a r L K →
    ∃ α,
      (∀ x ∈ Metric.closedBall x₀ ↑r,
          α (x, ↑t₀) = x ∧
            ∀ t ∈ Set.Icc tmin tmax, HasDerivWithinAt (fun x_1 => α (x, x_1)) (f t (α (x, t))) (Set.Icc tmin tmax) t) ∧
        ContinuousOn α (Metric.closedBall x₀ ↑r ×ˢ Set.Icc tmin tmax)
-- Mathlib.Algebra.HierarchyDesign
/-- The algebraic hierarchy is designed so that commutativity (e.g., of multiplication) is bundled
into the type class, so that we have, for example `Group` and `CommGroup`, `Ring` and `CommRing`,
etc.

It is often the case that one may desire to work with a commutative subobject inside an
ambient noncommutative type. In cases like `Subgroup.center` or `Subring.center`, the subobject is
*always* commutative, and in these cases one should simply imbue those subobjects (coerced to
`Type`) with the appropriate `Comm*` instance. However, in other cases, the commutativity of the
subobject may be conditional on commutativity of some other object. For example,
`Subgroup.closure s` is not always commutative, but it is when `s` is a commutative subset.
Likewise, if `S : Subgroup G` is a commutative subgroup, then `S.topologicalClosure` is also
commutative.

For such scenarios, users should prefer to use the unbundled `IsMulCommutative` typeclass, and to
provide theorems such as:
```
theorem isMulCommutative_closure {G : Type*} [Group G] {k : Set G}
    (hcomm : ∀ x ∈ k, ∀ y ∈ k, x * y = y * x) :
    IsMulCommutative (closure k)
```
or even *instances* such as
```
instance Subgroup.instIsMulCommutative_closure {S G : Type*} [Group G] [SetLike S G]
    [MulMemClass S G] (s : S) [IsMulCommutative s] :
    IsMulCommutative (closure (s : Set G))
```
and
```
instance Subgroup.isMulCommutative_topologicalClosure [T2Space G] (s : Subgroup G)
    [IsMulCommutative s] : IsMulCommutative s.topologicalClosure
```
Note that we prefer to name these instances manually because they are occasionally useful as
theorems. For example, the proof of the topological closure instance for subgroups above is proved
immediately from the one for monoids via: `s.toSubmonoid.isMulCommutative_topologicalClosure`.

In practice, we wish to be able to use the library of theorems about (bundled) commutativity for
subobjects as well, and so we also provide instances which take as input the unbundled
`Group G` and `IsMulCommutative G` and produce the bundled `CommGroup G`. However, to avoid
deleterious effects to type class synthesis for bundled commutativity (by forcing Lean to search
the entirery of both the bundled and unbundled hierarchies), these instances are only
available inside the `IsMulCommutative` scope and are simultaneously given the very low priority
`50`.
 -/
LibraryNote.commutative_subobjects : Batteries.Util.LibraryNote
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapNatIso_inverse_map_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S S' : CategoryTheory.Functor C D} (i : S ≅ S')
  {X Y : CategoryTheory.Comma S' (CategoryTheory.Functor.fromPUnit T)} (f : X ⟶ Y),
  ((CategoryTheory.CostructuredArrow.mapNatIso i).inverse.map f).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ x + y` is quasi-measure-preserving.  -/
MeasureTheory.quasiMeasurePreserving_add : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [ν.IsAddLeftInvariant],
  MeasureTheory.Measure.QuasiMeasurePreserving (fun p => p.1 + p.2) (μ.prod ν) ν
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Sized.rotateR_size : ∀ {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α}, l.Sized → (l.rotateR x r).size = l.size + r.size + 1
-- Mathlib.Algebra.Group.Basic
div_zpow : ∀ {α : Type u_1} [inst : DivisionCommMonoid α] (a b : α) (n : ℤ), (a / b) ^ n = a ^ n / b ^ n
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.one_le_prod : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : CommMonoid M] [inst_2 : Preorder M] [MulLeftMono M]
  {f : ι → M}, 1 ≤ f → 1 ≤ ∏ i, f i
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_abs : ∀ (x : ℝ), Real.log |x| = Real.log x
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.InductionCandidate.mk.injEq : ∀ (fvarId : Lean.FVarId) (val : Lean.InductiveVal) (fvarId_1 : Lean.FVarId) (val_1 : Lean.InductiveVal),
  ({ fvarId := fvarId, val := val } = { fvarId := fvarId_1, val := val_1 }) = (fvarId = fvarId_1 ∧ val = val_1)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.AddConstAsyncResult.mk.sizeOf_spec : ∀ (mainEnv asyncEnv : Lean.Environment) (constName : Lean.Name) (kind : Lean.ConstantKind)
  (exportedKind? : Option Lean.ConstantKind) (sigPromise : IO.Promise Lean.ConstantVal)
  (constPromise : IO.Promise Lean.Environment.ConstPromiseVal✝) (checkedEnvPromise : IO.Promise Lean.Kernel.Environment)
  (allRealizationsPromise : IO.Promise (Lean.NameMap Lean.AsyncConst✝)),
  sizeOf
      { mainEnv := mainEnv, asyncEnv := asyncEnv, constName := constName, kind := kind, exportedKind? := exportedKind?,
        sigPromise := sigPromise, constPromise := constPromise, checkedEnvPromise := checkedEnvPromise,
        allRealizationsPromise := allRealizationsPromise } =
    1 + sizeOf mainEnv + sizeOf asyncEnv + sizeOf constName + sizeOf kind + sizeOf exportedKind? + sizeOf sigPromise +
          sizeOf constPromise +
        sizeOf checkedEnvPromise +
      sizeOf allRealizationsPromise
-- Mathlib.LinearAlgebra.FixedSubmodule
/-- The fixed submodule of a linear map.  -/
LinearMap.fixedSubmodule : {R : Type u_1} →
  [inst : Semiring R] →
    {V : Type u_3} → [inst_1 : AddCommMonoid V] → [inst_2 : Module R V] → (V →ₗ[R] V) → Submodule R V
-- Mathlib.NumberTheory.ModularForms.SlashActions
SlashAction.slash_mul : ∀ {β : Type u_1} {G : Type u_2} {α : Type u_3} {inst : Monoid G} {inst_1 : AddMonoid α} [self : SlashAction β G α]
  (k : β) (g h : G) (a : α), SlashAction.map k (g * h) a = SlashAction.map k h (SlashAction.map k g a)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.coe_inf' : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] {s : Finset β} (H : s.Nonempty) (f : β → α),
  ↑(s.inf' H f) = s.inf (WithTop.some ∘ f)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGTD.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β) (fallback : (a : α) × β a),
  Std.DTreeMap.Internal.Impl.getEntryGTD k t fallback = (Std.DTreeMap.Internal.Impl.getEntryGT? k t).getD fallback
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.mem_iff_isSome_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, a ∈ m ↔ (Std.ExtDHashMap.Const.get? m a).isSome = true
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.pow_const : ∀ {β : Type u_2} {γ : Type u_3} {α : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace γ]
  [inst_2 : Pow β γ] [MeasurablePow β γ] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β},
  AEMeasurable f μ → ∀ (c : γ), AEMeasurable (fun x => f x ^ c) μ
-- Mathlib.Combinatorics.SimpleGraph.Sum
/-- The disjoint sum is associative up to isomorphism. `Iso.sumAssoc` as a graph isomorphism.  -/
SimpleGraph.Iso.sumAssoc : {U : Type u_1} →
  {V : Type u_3} →
    {W : Type u_5} → {G : SimpleGraph V} → {H : SimpleGraph W} → {I : SimpleGraph U} → G ⊕g H ⊕g I ≃g G ⊕g (H ⊕g I)