mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
/-- If a normal cyclic Sylow `p`-subgroup `P` has a complement `K`, then either `⁅K, P⁆ = ⊥` or
`⁅K, P⁆ = P`.  -/
Sylow.commutator_eq_bot_or_commutator_eq_self : ∀ {G : Type u_1} [inst : Group G] {p : ℕ} [Fact (Nat.Prime p)] [Finite G] (P : Sylow p G) [IsCyclic ↥↑P] [(↑P).Normal]
  {K : Subgroup G}, K.IsComplement' ↑P → ⁅K, ↑P⁆ = ⊥ ∨ ⁅K, ↑P⁆ = ↑P
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- An independent set is a clique in the complement graph and vice versa.  -/
SimpleGraph.isClique_compl : ∀ {α : Type u_1} (G : SimpleGraph α) {s : Set α}, Gᶜ.IsClique s ↔ G.IsIndepSet s
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Morphisms of group objects preserve negations.  -/
CategoryTheory.AddGrpObj.neg_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddGrpObj A] [inst_3 : CategoryTheory.AddGrpObj B] (f : A ⟶ B)
  [CategoryTheory.IsAddMonHom f],
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg f =
    CategoryTheory.CategoryStruct.comp f CategoryTheory.AddGrpObj.neg
-- Mathlib.Topology.Algebra.Group.Basic
/-- **Alias** of `tendsto_inv_nhdsLE_inv`. -/
tendsto_inv_nhdsWithin_Iic_inv : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [inst_2 : PartialOrder H] [IsOrderedMonoid H]
  [ContinuousInv H] {a : H}, Filter.Tendsto Inv.inv (nhdsWithin a⁻¹ (Set.Iic a⁻¹)) (nhdsWithin a (Set.Ici a))
-- Mathlib.Order.Category.BddLat
bddLat_dual_comp_forget_to_bddOrd : BddLat.dual.comp (CategoryTheory.forget₂ BddLat BddOrd) = (CategoryTheory.forget₂ BddLat BddOrd).comp BddOrd.dual
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_compContinuous_linearIsometryEquiv : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (E₁ i)]
  [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : (i : ι) → E i ≃ₗᵢ[𝕜] E₁ i),
  ‖g.compContinuousLinearMap fun i => ↑↑(f i)‖ = ‖g‖
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_sub_le : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] (a b : E), ‖a - b‖₊ ≤ ‖a‖₊ + ‖b‖₊
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
/-- The union of a sequence of measurable sets is a measurable set. Use a more general
`MeasurableSet.iUnion` instead.  -/
MeasurableSpace.measurableSet_iUnion : ∀ {α : Type u_7} (self : MeasurableSpace α) (f : ℕ → Set α),
  (∀ (i : ℕ), MeasurableSpace.MeasurableSet' self (f i)) → MeasurableSpace.MeasurableSet' self (⋃ i, f i)
-- Mathlib.Data.ZMod.Units
ZMod.isUnit_inv : ∀ {m : ℕ} {n : ℤ}, IsUnit ↑n → IsUnit (↑n)⁻¹
-- Mathlib.CategoryTheory.Abelian.Projective.Extend
CategoryTheory.ProjectiveResolution.instIsGECochainComplexOfNatInt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  (R : CategoryTheory.ProjectiveResolution X), R.cochainComplex.IsGE 0
-- Mathlib.SetTheory.Cardinal.Free
instInfiniteFreeRing : ∀ (α : Type u_1), Infinite (FreeRing α)
-- Std.Async.System
/-- The group the user belongs to.
 -/
Std.Async.System.SystemUser.groupId : Std.Async.System.SystemUser → Option Std.Async.System.GroupId
-- Init.Data.List.MinMax
List.isSome_max?_of_ne_nil : ∀ {α : Type u_1} [inst : Max α] {l : List α}, l ≠ [] → l.max?.isSome = true
-- Mathlib.Order.Types.Arithmetic
OrderType.instHAdd : HAdd OrderType.{u} OrderType.{v} OrderType.{max u v}
-- Batteries.Util.ProofWanted
/-- `nm`'s own non-class wanted-dependencies, to be surfaced as binders on the enclosing
declaration and threaded into `nm`'s application. Empty unless `nm` was itself declared with a
body (or other `❰…❱` references) introducing chained dependencies.  -/
_private.Batteries.Util.ProofWanted.0.WantedRefInfo.deps : WantedRefInfo✝ → Array WantedDep✝
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- Restriction of a non-unital ring homomorphism to its range interpreted as a
non-unital subsemiring.

This is the bundled version of `Set.rangeFactorization`.  -/
NonUnitalRingHom.srangeRestrict : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocSemiring R] →
      {F : Type u_1} →
        [inst_1 : FunLike F R S] →
          [inst_2 : NonUnitalNonAssocSemiring S] →
            [inst_3 : NonUnitalRingHomClass F R S] → (f : F) → R →ₙ+* ↥(NonUnitalRingHom.srange f)
-- Mathlib.Tactic.Translate.ToDual
/-- The `insert_cast`/`insert_cast_fun` attributes create an abstraction boundary for the tagged
constant when translating it. For example, `Set.Icc`, `Monotone`, `DecidableLT`, `WCovBy` are all
morally self-dual, but their definition is not self-dual. So, in order to allow these constants
to be self-dual, we need to not unfold their definition in the proof term that we translate.  -/
Mathlib.Tactic.ToDual.unfoldBoundaries : Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaryExt
-- Mathlib.Algebra.WithConv
WithConv.addEquiv_symm_apply_ofConv : ∀ (A : Type u_2) [inst : AddMonoid A] (ofConv : A), ((WithConv.addEquiv A).symm ofConv).ofConv = ofConv
-- Mathlib.Algebra.Module.SpanRank
Cardinal.toNat.eq_1 : Cardinal.toNat = ENat.toNatHom.comp (MonoidWithZeroHom.ofClass Cardinal.toENat)
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.mk_one : ∀ {K : Type u_1} [inst : Field K], ⟨1, ⋯⟩ = 1
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
MeasureTheory.Measure.tendsto_IicSnd_atBot : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) [MeasureTheory.IsFiniteMeasure ρ]
  {s : Set α}, MeasurableSet s → Filter.Tendsto (fun r => (ρ.IicSnd ↑r) s) Filter.atBot (nhds 0)
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Comonad.ForgetCreatesLimits'.liftedCone_π_app_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {T : CategoryTheory.Comonad C} {D : CategoryTheory.Functor J T.Coalgebra}
  (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (t : CategoryTheory.Limits.IsLimit c)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor]
  [inst_3 : CategoryTheory.Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] (j : J),
  ((CategoryTheory.Comonad.ForgetCreatesLimits'.liftedCone c t).π.app j).f = c.π.app j
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_exists : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] {p : ι → Prop} {f : Exists p → α},
  ⨆ (ih : Exists p), f ih = ⨆ i, ⨆ (h : p i), f ⋯
-- Mathlib.Analysis.Normed.Algebra.Spectrum
AlgHom.instContinuousLinearMapClassOfAlgHomClass : ∀ {𝕜 : Type u_1} {A : Type u_2} {F : Type u_3} [inst : NormedField 𝕜] [inst_1 : NormedRing A]
  [inst_2 : NormedAlgebra 𝕜 A] [CompleteSpace A] [inst_4 : FunLike F A 𝕜] [AlgHomClass F 𝕜 A 𝕜],
  ContinuousLinearMapClass F 𝕜 A 𝕜
-- Lean.Meta.Tactic.Grind.Arith.ModelUtil
/-- Converts the given model into a sorted array of pairs `(e, v)` representing assignments `e := v`.
`isTarget` is a predicate used to detect terms that must be in the model but have not been assigned a value (see: `assignUnassigned`)
The pairs are sorted using `e`s generation and then `Expr.lt`.
Only terms s.t. `isInterpretedTerm e = false` are included into the resulting array.
 -/
Lean.Meta.Grind.Arith.finalizeModel : Lean.Meta.Grind.Goal →
  (Lean.Meta.Grind.ENode → Lean.MetaM Bool) → Std.HashMap Lean.Expr ℚ → Lean.MetaM (Array (Lean.Expr × ℚ))
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.map_bot : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X : C}, CategoryTheory.Presieve.map F ⊥ = ⊥
-- Mathlib.Data.List.Cycle
List.prev_eq_getElem_idxOf_pred_of_ne_head : ∀ {α : Type u_1} [inst : DecidableEq α] {l : List α} {a : α} (ha : a ∈ l),
  a ≠ l.head ⋯ → l.prev a ha = l[List.idxOf a l - 1]
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
minSmoothness_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n m : WithTop ℕ∞}, minSmoothness 𝕜 (n + m) = minSmoothness 𝕜 n + m
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Sized.induction : ∀ {α : Type u_1} {t : Ordnode α},
  t.Sized →
    ∀ {C : Ordnode α → Prop},
      C Ordnode.nil → (∀ (l : Ordnode α) (x : α) (r : Ordnode α), C l → C r → C (l.node' x r)) → C t
-- Mathlib.LinearAlgebra.LinearPMap
/-- Restrict a partially defined linear map to a submodule of `E` contained in `f.domain`.  -/
LinearPMap.domRestrict : {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] → (E →ₛₗ.[σ] F) → Submodule R E → E →ₛₗ.[σ] F
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.add_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f g : MeasureTheory.SimpleFunc α ENNReal),
  (f + g).lintegral μ = f.lintegral μ + g.lintegral μ
-- Std.Data.TreeMap.Lemmas
/-- Simpler variant of `getElem?_filterMap` when `LawfulEqCmp` is available.  -/
Std.TreeMap.getElem?_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → Option γ} {k : α}, (Std.TreeMap.filterMap f t)[k]? = t[k]?.bind fun x => f k x
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.functor_comp_inverse : ∀ (X Y : SSet.Truncated 2),
  (SSet.Truncated.HomotopyCategory.BinaryProduct.functor X Y).comp
      (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y) =
    CategoryTheory.Functor.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).HomotopyCategory
-- Mathlib.Data.Semiquot
Semiquot.mem_bind : ∀ {α : Type u_1} {β : Type u_2} (q : Semiquot α) (f : α → Semiquot β) (b : β), b ∈ q.bind f ↔ ∃ a ∈ q, b ∈ f a
-- Mathlib.Algebra.Order.Pi
Function.one_le_const : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] [inst_1 : Preorder α] {a : α} [Nonempty β],
  1 ≤ Function.const β a ↔ 1 ≤ a
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
IsSemilinearSet.biInter : ∀ {M : Type u_1} {ι : Type u_3} [inst : AddCommMonoid M] [AddMonoid.FG M] {s : Set ι} {t : ι → Set M},
  s.Finite → (∀ i ∈ s, IsSemilinearSet (t i)) → IsSemilinearSet (⋂ i ∈ s, t i)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.norm_comm_apply : ∀ {k : Type u} [inst : Semiring k] {G : Type v} [inst_1 : Group G] [inst_2 : Fintype G] {A B : Rep.{u_1, u, v} k G}
  (f : A ⟶ B) (x : ↑A),
  B.ρ.norm ((CategoryTheory.ConcreteCategory.hom f) x) = (CategoryTheory.ConcreteCategory.hom f) (A.ρ.norm x)
-- Mathlib.Order.Category.Frm
Frm.ofHom_apply : ∀ {X Y : Type u} [inst : Order.Frame X] [inst_1 : Order.Frame Y] (f : FrameHom X Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (Frm.ofHom f)) x = f x
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.abs_div_tendsto_atBot_atTop_of_degree_gt : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P Q : Polynomial 𝕜)
  [OrderTopology 𝕜],
  Q.degree < P.degree →
    Q ≠ 0 → Filter.Tendsto (fun x => |Polynomial.eval x P / Polynomial.eval x Q|) Filter.atBot Filter.atTop
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.op2_associator : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  (CategoryTheory.Bicategory.associator f g h).op2 = (CategoryTheory.Bicategory.associator h.op g.op f.op).symm
-- Mathlib.Data.Finset.Max
Finset.max_empty : ∀ {α : Type u_2} [inst : LinearOrder α], ∅.max = ⊥
-- Mathlib.Probability.Distributions.Pareto
ProbabilityTheory.paretoPDFReal.eq_1 : ∀ (t r x : ℝ), ProbabilityTheory.paretoPDFReal t r x = if t ≤ x then r * t ^ r * x ^ (-(r + 1)) else 0
-- Init.Data.Option.Lemmas
Option.pelim_congr_left : ∀ {α : Type u_1} {β : Sort u_2} {o o' : Option α} {b : β} {f : (a : α) → a ∈ o → β} (h : o = o'),
  o.pelim b f = o'.pelim b fun a ha => f a ⋯
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given Localization maps `f : M →+ N, k : P →+ Q` for AddSubmonoids `S, T` respectively if an
`AddCommMonoid` homomorphism `g : M →+ P` induces a `f.map hy k : N →+ Q`, then for all `z : N`,
we have `k (g y) + f.map hy k z = k (g x)` where `x : M, y ∈ S` are such that
`z + f y = f x`.  -/
AddSubmonoid.LocalizationMap.map_add_left : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : AddCommMonoid Q] {k : T.LocalizationMap Q} (z : N),
  k (g ↑(f.sec z).2) + (f.map hy k) z = k (g (f.sec z).1)
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.instPartialOrder : {α : Type u_2} → {β : Type u_3} → [inst : InfSet α] → {x : CompleteLattice β} → PartialOrder (sInfHom α β)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.mem_toNonUnitalSubalgebra : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S : Subalgebra R A}
  {x : A}, x ∈ S.toNonUnitalSubalgebra ↔ x ∈ S
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.instFaithfulSMul : ∀ {R : Type u_2} {S : Type u_3} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [FaithfulSMul R S], FaithfulSMul (MvPolynomial σ R) (MvPolynomial σ S)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_left_inj₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : LinearOrder G₀] {a b : G₀} {n : ℤ} [PosMulStrictMono G₀]
  [MulPosMono G₀], 0 ≤ a → 0 ≤ b → n ≠ 0 → (a ^ n = b ^ n ↔ a = b)
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.comap_incl_self : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L),
  LieIdeal.comap I.incl I = ⊤
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.anyM_pure : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β}
  {p : β → ULift.{w, 0} Bool}, Std.IterM.anyM (fun x => pure (p x)) it = Std.IterM.any (fun x => (p x).down) it
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.sPolynomial.eq_1 : ∀ {σ : Type u_1} (m : MonomialOrder σ) {R : Type u_2} [inst : CommRing R] (f g : MvPolynomial σ R),
  m.sPolynomial f g =
    (MvPolynomial.monomial (m.degree g - m.degree f)) (m.leadingCoeff g) * f -
      (MvPolynomial.monomial (m.degree f - m.degree g)) (m.leadingCoeff f) * g
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.instInhabitedBasicMeasure.default : Lean.Elab.WF.GuessLex.BasicMeasure
-- Mathlib.Algebra.Ring.Equiv
/-- Product of ring equivalences. This is `Equiv.prodCongr` as a `RingEquiv`.  -/
RingEquiv.prodCongr : {R : Type u_7} →
  {R' : Type u_8} →
    {S : Type u_9} →
      {S' : Type u_10} →
        [inst : NonUnitalNonAssocSemiring R] →
          [inst_1 : NonUnitalNonAssocSemiring R'] →
            [inst_2 : NonUnitalNonAssocSemiring S] →
              [inst_3 : NonUnitalNonAssocSemiring S'] → R ≃+* R' → S ≃+* S' → R × S ≃+* R' × S'
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
/-- Map from `Lp F p (μ.trim hm)` to `lpMeas`, inverse of `Lp_meas_to_Lp_trim`.  -/
MeasureTheory.lpTrimToLpMeas : {α : Type u_1} →
  (F : Type u_2) →
    (𝕜 : Type u_3) →
      (p : ENNReal) →
        [inst : RCLike 𝕜] →
          [inst_1 : NormedAddCommGroup F] →
            [inst_2 : NormedSpace 𝕜 F] →
              {m m0 : MeasurableSpace α} →
                (μ : MeasureTheory.Measure α) →
                  (hm : m ≤ m0) → ↥(MeasureTheory.Lp F p (μ.trim hm)) → ↥(MeasureTheory.lpMeas F 𝕜 m p μ)
-- Mathlib.Order.LiminfLimsup
Filter.inf_liminf : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteDistribLattice α] {f : Filter β} {u : β → α} [f.NeBot] (a : α),
  a ⊓ Filter.liminf u f = Filter.liminf (fun x => a ⊓ u x) f
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Differentiable.sigmoid : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ},
  Differentiable ℝ f → Differentiable ℝ (Real.sigmoid ∘ f)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.coe_disjoint : ∀ {α : Type u_2} [inst : TopologicalSpace α] {s t : TopologicalSpace.Clopens α}, Disjoint ↑s ↑t ↔ Disjoint s t
-- Mathlib.Algebra.Star.Module
StarModule.decomposeProdAdjoint_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : Semiring R] [inst_1 : StarMul R] [inst_2 : TrivialStar R]
  [inst_3 : AddCommGroup A] [inst_4 : Module R A] [inst_5 : StarAddMonoid A] [inst_6 : StarModule R A]
  [inst_7 : Invertible 2] (i : A),
  (StarModule.decomposeProdAdjoint R A) i = ((selfAdjointPart R) i, (skewAdjointPart R) i)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
inv_mul_le_iff_le_mul' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LE α] [MulLeftMono α] {a b c : α}, c⁻¹ * a ≤ b ↔ a ≤ b * c
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- A limit kernel fork is mapped to a limit kernel fork by a functor `G` when this functor
preserves the corresponding limit.  -/
CategoryTheory.Limits.KernelFork.mapIsLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {X Y : C} →
              {f : X ⟶ Y} →
                (c : CategoryTheory.Limits.KernelFork f) →
                  CategoryTheory.Limits.IsLimit c →
                    (G : CategoryTheory.Functor C D) →
                      [inst_4 : G.PreservesZeroMorphisms] →
                        [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G] →
                          CategoryTheory.Limits.IsLimit (c.map G)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.coeFn_injective : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  {P : C(X, Y) → Prop}, Function.Injective DFunLike.coe
-- Mathlib.Data.PNat.Basic
PNat.natPred.eq_1 : ∀ (i : ℕ+), i.natPred = ↑i - 1
-- Lean.DocString.Parser
Lean.Doc.Parser.instReprUnorderedListType.repr : Lean.Doc.Parser.UnorderedListType → ℕ → Std.Format
-- Mathlib.LinearAlgebra.Matrix.Swap
/-- The swap matrix `swap R i j` is the identity matrix with the
`i`-th and `j`-th rows modified such that multiplying by it on the
left (resp. right) corresponds to swapping the `i`-th and `j`-th row (resp. column).  -/
Matrix.swap : (R : Type u_1) → {n : Type u_2} → [Zero R] → [One R] → [DecidableEq n] → n → n → Matrix n n R
-- Mathlib.Order.UpperLower.Closure
lowerClosure_iUnion : ∀ {α : Type u_1} {ι : Sort u_3} [inst : Preorder α] (f : ι → Set α), lowerClosure (⋃ i, f i) = ⨆ i, lowerClosure (f i)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.brecOn_5.eq : ∀ {motive_1 : Lean.Elab.Term.Do.Code → Sort u}
  {motive_2 : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u}
  {motive_3 : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u}
  {motive_4 : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u}
  {motive_5 : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u}
  {motive_6 : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code → Sort u}
  {motive_7 : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code → Sort u}
  (t : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) (F_1 : (t : Lean.Elab.Term.Do.Code) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_1 t → motive_2 t)
  (F_3 : (t : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_2 t → motive_3 t)
  (F_4 : (t : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_4 t → motive_5 t)
  (F_6 : (t : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code.below_5 t → motive_6 t)
  (F_7 : (t : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code.below_6 t → motive_7 t),
  Lean.Elab.Term.Do.Code.brecOn_5 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 =
    F_6 t (Lean.Elab.Term.Do.Code.brecOn_5.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- Intersection of two pre-`1`-hypercovers.  -/
CategoryTheory.PreOneHypercover.inter : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {S : C} →
      (E : CategoryTheory.PreOneHypercover S) →
        (F : CategoryTheory.PreOneHypercover S) →
          [∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)] →
            [∀ (i j : E.I₀) (k : E.I₁ i j) (a b : F.I₀) (l : F.I₁ a b),
                  CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (E.p₁ k) (E.f i))
                    (CategoryTheory.CategoryStruct.comp (F.p₁ l) (F.f a))] →
              CategoryTheory.PreOneHypercover S
-- Init.Data.Bool
Bool.or_eq_false_iff : ∀ {x y : Bool}, (x || y) = false ↔ x = false ∧ y = false
-- Mathlib.Order.Interval.Lex
NonemptyInterval.instLinearOrderLex : {α : Type u_1} → [inst : LinearOrder α] → LinearOrder (Lex (NonemptyInterval α))
-- Mathlib.Topology.Gluing
TopCat.GlueData.MkCore.mk.inj : ∀ {J : Type u} {U : J → TopCat} {V : (i : J) → J → TopologicalSpace.Opens ↑(U i)}
  {t :
    (i j : J) →
      (TopologicalSpace.Opens.toTopCat (U i)).obj (V i j) ⟶ (TopologicalSpace.Opens.toTopCat (U j)).obj (V j i)}
  {V_id : ∀ (i : J), V i i = ⊤} {t_id : ∀ (i : J), ⇑(CategoryTheory.ConcreteCategory.hom (t i i)) = id}
  {t_inter :
    ∀ ⦃i j : J⦄ (k : J) (x : ↥(V i j)), ↑x ∈ V i k → ↑((CategoryTheory.ConcreteCategory.hom (t i j)) x) ∈ V j k}
  {cocycle :
    ∀ (i j k : J) (x : ↥(V i j)) (h : ↑x ∈ V i k),
      ↑((CategoryTheory.ConcreteCategory.hom (t j k)) ⟨↑((CategoryTheory.ConcreteCategory.hom (t i j)) x), ⋯⟩) =
        ↑((CategoryTheory.ConcreteCategory.hom (t i k)) ⟨↑x, h⟩)}
  {J_1 : Type u} {U_1 : J_1 → TopCat} {V_1 : (i : J_1) → J_1 → TopologicalSpace.Opens ↑(U_1 i)}
  {t_1 :
    (i j : J_1) →
      (TopologicalSpace.Opens.toTopCat (U_1 i)).obj (V_1 i j) ⟶ (TopologicalSpace.Opens.toTopCat (U_1 j)).obj (V_1 j i)}
  {V_id_1 : ∀ (i : J_1), V_1 i i = ⊤} {t_id_1 : ∀ (i : J_1), ⇑(CategoryTheory.ConcreteCategory.hom (t_1 i i)) = id}
  {t_inter_1 :
    ∀ ⦃i j : J_1⦄ (k : J_1) (x : ↥(V_1 i j)),
      ↑x ∈ V_1 i k → ↑((CategoryTheory.ConcreteCategory.hom (t_1 i j)) x) ∈ V_1 j k}
  {cocycle_1 :
    ∀ (i j k : J_1) (x : ↥(V_1 i j)) (h : ↑x ∈ V_1 i k),
      ↑((CategoryTheory.ConcreteCategory.hom (t_1 j k)) ⟨↑((CategoryTheory.ConcreteCategory.hom (t_1 i j)) x), ⋯⟩) =
        ↑((CategoryTheory.ConcreteCategory.hom (t_1 i k)) ⟨↑x, h⟩)},
  { J := J, U := U, V := V, t := t, V_id := V_id, t_id := t_id, t_inter := t_inter, cocycle := cocycle } =
      { J := J_1, U := U_1, V := V_1, t := t_1, V_id := V_id_1, t_id := t_id_1, t_inter := t_inter_1,
        cocycle := cocycle_1 } →
    J = J_1 ∧ U ≍ U_1 ∧ V ≍ V_1 ∧ t ≍ t_1
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.Hom.normNoninc : ∀ {M N : SemiNormedGrp₁} (self : M.Hom N), self.hom'.NormNoninc
-- Mathlib.RingTheory.SimpleModule.Isotypic
LinearEquiv.isIsotypicOfType_iff_type : ∀ {R : Type u_2} {M : Type u} {N : Type u_3} {S : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup S] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R S]
  (e : N ≃ₗ[R] S), IsIsotypicOfType R M N ↔ IsIsotypicOfType R M S
-- Mathlib.Order.RelIso.Basic
RelIso.default_def : ∀ {α : Type u_1} (r : α → α → Prop), default = RelIso.refl r
-- Mathlib.Topology.Algebra.Group.Pointwise
closure_subset_mul_self_of_mem_nhds_one : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {U : Set G},
  U ∈ nhds 1 → closure U ⊆ U * U