mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.unop_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z P : Cᵒᵖ} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P}, CategoryTheory.IsPullback inr.unop inl.unop g.unop f.unop ↔ CategoryTheory.IsPushout f g inl inr
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.liftCycles_ιChainComplex_homologyπ_homology₀ε_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) [inst_3 : CategoryTheory.CategoryWithHomology C]
  (x : X.obj (Opposite.op { len := 0 })) {Z : C} (h : R ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (HomologicalComplex.liftCycles (X.chainComplex R) (X.ιChainComplex x) 0
        SSet.liftCycles_ιChainComplex_homologyπ_homology₀Iso_hom._proof_1 ⋯)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (X.chainComplex R) 0)
        (CategoryTheory.CategoryStruct.comp (X.homology₀ε R) h)) =
    h
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.reverse_of : ∀ {α : Type u_1} (a : α), (FreeAddMonoid.of a).reverse = FreeAddMonoid.of a
-- Init.Sym.Lemmas
Lean.Sym.Int32.lt_eq_true : ∀ (a b : Int32), decide (a < b) = true → (a < b) = True
-- Lean.Elab.Tactic.RenameInaccessibles
Lean.Elab.Tactic.renameInaccessibles : Lean.MVarId → Lean.TSyntaxArray `Lean.binderIdent → Lean.Elab.TermElabM Lean.MVarId
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.mul : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {φ ψ : MvPolynomial σ R} {m n : ℕ},
  φ.IsHomogeneous m → ψ.IsHomogeneous n → (φ * ψ).IsHomogeneous (m + n)
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y : CategoryTheory.Dial C} {x y : X ⟶ Y},
  x = y ↔ x.f = y.f ∧ x.F = y.F
-- Mathlib.Data.Seq.Computation
Computation.think_terminates : ∀ {α : Type u} (s : Computation α) [s.Terminates], s.think.Terminates
-- Mathlib.CategoryTheory.Dialectica.Monoidal
_private.Mathlib.CategoryTheory.Dialectica.Monoidal.0.CategoryTheory.Dial.«termπ(_,_)» : Lean.ParserDescr
-- Init.Data.String.Basic
String.data_empty : "".toList = []
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.comap_id : ∀ {α : Type u_1} {m : MeasurableSpace α}, MeasurableSpace.comap id m = m
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.weightedVSubOfPoint_apply : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (b : P),
  (s.weightedVSubOfPoint p b) w = ∑ i ∈ s, w i • (p i -ᵥ b)
-- Mathlib.RingTheory.FormalGroup.Basic
/-- An abbreviation of $F(0,X)$ for a formal group $F$.  -/
FormalGroup.zeroX : {R : Type u_1} → [inst : CommRing R] → FormalGroup R → PowerSeries R
-- Mathlib.Algebra.Homology.QuasiIso
isoOfQuasiIsoAt_inv_hom_id : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L)
  (i : ι) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [inst_4 : QuasiIsoAt f i],
  CategoryTheory.CategoryStruct.comp (isoOfQuasiIsoAt f i).inv (HomologicalComplex.homologyMap f i) =
    CategoryTheory.CategoryStruct.id (L.homology i)
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.mem_mk' : ∀ {R : Type u} [inst : NonAssocSemiring R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubmonoid R}
  (ha : ↑sa = s) {x : R}, x ∈ Subsemiring.mk' s sm hm sa ha ↔ x ∈ s
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.mem_iff : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : R} {a : A},
  r ∈ spectrum R a ↔ ¬IsUnit ((algebraMap R A) r - a)
-- Mathlib.RingTheory.KrullDimension.Module
Module.supportDim_self_eq_ringKrullDim : ∀ (R : Type u_1) [inst : CommRing R], Module.supportDim R R = ringKrullDim R
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.fromSubtype_toSubtype_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  (p : J → Prop) [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict p f)] {Z : C}
  (h : ⨁ Subtype.restrict p f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.fromSubtype f p)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.toSubtype f p) h) =
    h
-- Mathlib.RingTheory.AdicCompletion.Completeness
AdicCompletion.ker_evalOneₐ_eq_map : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R),
  I.FG → RingHom.ker (AdicCompletion.evalOneₐ I).toRingHom = Ideal.map (algebraMap R (AdicCompletion I R)) I
-- Lean.ExtraModUses
/-- Whether dependency must be imported as `meta`.  -/
Lean.ExtraModUse.isMeta : Lean.ExtraModUse → Bool
-- Mathlib.Algebra.GroupWithZero.Units.Basic
zpow_neg_mul_zpow_self : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} (n : ℤ), a ≠ 0 → a ^ (-n) * a ^ n = 1
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
/-- A `HomogeneousSubsemiring` is a `Subsemiring` that satisfies `IsHomogeneous`.  -/
HomogeneousSubsemiring : {ι : Type u_1} →
  {σ : Type u_2} →
    {A : Type u_3} →
      [inst : AddMonoid ι] →
        [inst_1 : Semiring A] →
          [inst_2 : SetLike σ A] →
            [inst_3 : AddSubmonoidClass σ A] → (𝒜 : ι → σ) → [inst_4 : DecidableEq ι] → [GradedRing 𝒜] → Type u_3
-- Mathlib.NumberTheory.Pell
/-- We define a solution to be *fundamental* if it has `x > 1` and `y > 0`
and its `x` is the smallest possible among solutions with `x > 1`.  -/
Pell.IsFundamental : {d : ℤ} → Pell.Solution₁ d → Prop
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- The sequence `n / (2 * n + 1)` tends to `1/2`  -/
Stirling.tendsto_self_div_two_mul_self_add_one : Filter.Tendsto (fun n => ↑n / (2 * ↑n + 1)) Filter.atTop (nhds (1 / 2))
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
setBasisOfLinearIndependentOfCardEqFinrank_repr_apply : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Set V}
  [inst_3 : Nonempty ↑s] [inst_4 : Fintype ↑s] (lin_ind : LinearIndependent K Subtype.val)
  (card_eq : s.toFinset.card = Module.finrank K V) (x : V),
  (setBasisOfLinearIndependentOfCardEqFinrank lin_ind card_eq).repr x =
    lin_ind.repr ((LinearMap.codRestrict (Submodule.span K (Set.range Subtype.val)) LinearMap.id ⋯) x)
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
IsGLB.add : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : Preorder G] [AddLeftMono G] [AddRightMono G] {s t : Set G} {a b : G},
  IsGLB s a → IsGLB t b → IsGLB (s + t) (a + b)
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.restrictScalars_inj : ∀ (R : Type u_1) {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module S M] [inst_7 : Module S M₂] [inst_8 : LinearMap.CompatibleSMul M M₂ R S] (fₗ gₗ : M →ₗ[S] M₂),
  ↑R fₗ = ↑R gₗ ↔ fₗ = gₗ
-- Mathlib.NumberTheory.Niven
/-- `cos(q * π)` for `q : ℚ` is algebraic over `ℤ`, using the complex `cos` function.  -/
Complex.isAlgebraic_cos_rat_mul_pi : ∀ (q : ℚ), IsAlgebraic ℤ (Complex.cos (↑q * ↑Real.pi))
-- Lean.Elab.Tactic.Basic
/-- Execute `x` using the main goal local context and instances  -/
Lean.Elab.Tactic.withMainContext : {α : Type} → Lean.Elab.Tactic.TacticM α → Lean.Elab.Tactic.TacticM α
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGE_map_hom₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) {X Y : C} (φ : X ⟶ Y),
  ((t.triangleLEGE a b h).map φ).hom₂ = φ
-- Mathlib.Data.PNat.Interval
PNat.card_Ioo : ∀ (a b : ℕ+), (Finset.Ioo a b).card = ↑b - ↑a - 1
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inl_isoPushout_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] {Q : C},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q inl)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q hP.isoPushout.hom) =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inl f g)
-- Init.Data.Float.Model.Float
/-- Determine whether `a` is equal to `b` according to IEEE rules.

This is not a reflexive relation.
 -/
Float.Model.beq : Float.Model → Float.Model → Bool
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.map_one : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] {f : α ↪ β}, Finset.map f 1 = {f 1}
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] (a : M),
  MulArchimedeanClass.mk a = toAntisymmetrization (fun x1 x2 => x1 ≤ x2) (MulArchimedeanOrder.of a)
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso_inv : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C) (D : Type uD)
  [inst_1 : CategoryTheory.Category.{uD', uD} D],
  (CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.counitIso W D).inv = CategoryTheory.eqToHom ⋯
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
CategoryTheory.Functor.mapHomotopyCategory.congr_simp : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {W : Type u_3} [inst_2 : CategoryTheory.Category.{v_1, u_3} W] [inst_3 : CategoryTheory.Preadditive W]
  (F F_1 : CategoryTheory.Functor V W) (e_F : F = F_1) [inst_4 : F.Additive] (c : ComplexShape ι),
  F.mapHomotopyCategory c = F_1.mapHomotopyCategory c
-- Mathlib.Order.BooleanGenerators
/-- An alternative constructor for Boolean algebras.

A set of *Boolean generators* in a compactly generated complete lattice is a subset `S` such that

* the elements of `S` are all atoms, and
* the set `S` satisfies an atomicity condition:
  any compact element below the supremum of a finite subset `s` of generators
  is equal to the supremum of a subset of `s`.

If the supremum of `S` is the whole lattice,
then the lattice is a Boolean algebra
(see `IsCompactlyGenerated.BooleanGenerators.booleanAlgebraOfSSupEqTop`).
 -/
IsCompactlyGenerated.BooleanGenerators : {α : Type u_1} → [CompleteLattice α] → Set α → Prop
-- Mathlib.LinearAlgebra.Matrix.Hadamard
/-- `Matrix.hadamard` (denoted as `⊙` within the Matrix namespace) defines the Hadamard product,
which is the pointwise product of two matrices of the same size.  -/
Matrix.«term_⊙_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_lt_iff_lt_mul : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulRightStrictMono α] {a b c : α}, a / c < b ↔ a < b * c
-- Batteries.Data.MLList.IO
/-- Give a list of tasks, return the monadic lazy list which
returns the values as they become available.
 -/
MLList.ofTaskList : {α : Type} → List (Task α) → MLList BaseIO α
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.inv_pow' : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  (A : Matrix n' n' R) (n : ℕ), A⁻¹ ^ n = (A ^ n)⁻¹
-- Mathlib.Algebra.SkewMonoidAlgebra.Support
SkewMonoidAlgebra.support_single : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {b : k} (a : G),
  b ≠ 0 → (SkewMonoidAlgebra.single a b).support = {a}
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddEquiv.withTopCongr_refl : ∀ {α : Type u} [inst : Add α], (AddEquiv.refl α).withTopCongr = AddEquiv.refl (WithTop α)
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.restrictFunctorComp_inv_app_app : ∀ {X Y Z : AlgebraicGeometry.Scheme} {U : X.Opens} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : AlgebraicGeometry.IsOpenImmersion f]
  [inst_1 : AlgebraicGeometry.IsOpenImmersion g] (M : Z.Modules),
  AlgebraicGeometry.Scheme.Modules.Hom.app ((AlgebraicGeometry.Scheme.Modules.restrictFunctorComp f g).inv.app M) U =
    M.presheaf.map (CategoryTheory.eqToHom ⋯).op
-- Mathlib.Order.Bounds.Image
mem_upperBounds_image2_of_mem_upperBounds_of_mem_lowerBounds : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β} {a : α} {b : β},
  (∀ (b : β), Monotone (Function.swap f b)) →
    (∀ (a : α), Antitone (f a)) → a ∈ upperBounds s → b ∈ lowerBounds t → f a b ∈ upperBounds (Set.image2 f s t)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.skipPrefix?_char_eq_some_iff : ∀ {c : Char} {s : String} {pos : s.Pos},
  s.skipPrefix? c = some pos ↔ ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ s.startPos.get h = c
-- Lean.DocString.Types
Lean.Doc.instInhabitedDescItem.default : {α : Type u} → {β : Type v} → Lean.Doc.DescItem α β
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
CategoryTheory.Limits.PreservesLimits.preservesCofilteredLimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesCofilteredLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.instInhabited : Inhabited CircleDeg1Lift
-- Mathlib.FieldTheory.IntermediateField.ExtendRight
IntermediateField.extendRight.algebra : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          (F : IntermediateField K L) →
            (M : Type u_3) →
              [inst_3 : Field M] →
                [inst_4 : Algebra K M] →
                  [inst_5 : Algebra L M] →
                    [inst_6 : IsScalarTower K L M] →
                      {S : Type u_5} →
                        [inst_7 : CommRing S] →
                          [inst_8 : Algebra S ↥F] →
                            [inst_9 : Algebra S M] → [IsScalarTower S (↥F) M] → Algebra S ↥(F.extendRight M)
-- Mathlib.Algebra.Group.Hom.Basic
AddMonoidHom.add.eq_1 : ∀ {M : Type u_2} {N : Type u_3} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N],
  AddMonoidHom.add = { add := fun f g => { toFun := fun m => f m + g m, map_zero' := ⋯, map_add' := ⋯ } }
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.lifting_property : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsSemisimpleModule R M] {P : Type u_6} [inst_6 : AddCommGroup P]
  [inst_7 : Module R P] (f : M →ₗ[R] N), Function.Surjective ⇑f → ∀ (g : P →ₗ[R] N), ∃ h, f ∘ₗ h = g
-- Mathlib.Order.Category.Lat
Lat.dual_map : ∀ {X Y : Lat} (f : X ⟶ Y), Lat.dual.map f = Lat.ofHom (LatticeHom.dual (Lat.Hom.hom f))
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.structuralAtom : Mathlib.Tactic.BicategoryLike.StructuralAtom → Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Mathlib.Analysis.Convex.Quasiconvex
QuasilinearOn.antitone_comp : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {β : Type u_6} {γ : Type u_7} [inst_4 : LinearOrder β] [inst_5 : Preorder γ] {s : Set E}
  {f : E → β} {g : β → γ}, Antitone g → QuasilinearOn 𝕜 s f → QuasilinearOn 𝕜 s (g ∘ f)
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.instMonoHomologyMapIntP : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n : ℤ),
  CategoryTheory.Mono
    (HomologicalComplex.homologyMap (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.p✝ f n) n)
-- Mathlib.Data.Nat.Totient
Nat.prod_primeFactors_pow_totient_ediv_dvd : ∀ {n : ℕ}, 0 < n → ∏ p ∈ n.primeFactors, p ^ (n.totient / (p - 1)) ∣ n ^ n.totient
-- Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Subalgebra.pointwise_smul_toSubsemiring : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {R' : Type u_3}
  [inst_3 : Semiring R'] [inst_4 : MulSemiringAction R' A] [inst_5 : SMulCommClass R' R A] (m : R')
  (S : Subalgebra R A), (m • S).toSubsemiring = m • S.toSubsemiring
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.instCompactSpaceSubtypeMem : ∀ (G : Type u) [inst : Group G] [inst_1 : TopologicalSpace G] [CompactSpace G] (H : ClosedSubgroup G), CompactSpace ↥H
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If `p₃` bisects the angle `∡ p₁ p₂ p₄` externally, and `p₃` and `p₄` lie on opposite sides of
the line `p₁ p₂`, then the unoriented angle `∠ p₁ p₂ p₃` is `π / 2` minus half `∠ p₁ p₂ p₄`.  -/
EuclideanGeometry.angle_eq_pi_sub_angle_div_two_of_oangle_eq_add_pi_of_sOppSide : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ : P},
  p₁ ≠ p₂ →
    EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₃ p₂ p₄ + ↑Real.pi →
      line[ℝ, p₁, p₂].SOppSide p₃ p₄ →
        EuclideanGeometry.angle p₁ p₂ p₃ = (Real.pi - EuclideanGeometry.angle p₁ p₂ p₄) / 2
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.comp_add : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  [inst_10 : AddCommGroup U] [inst_11 : Module R U] [inst_12 : TopologicalSpace U] [inst_13 : IsTopologicalAddGroup U]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} {π₃ : ContRepresentation R G U}
  (f : ContIntertwiningMap π₂ π₃) (g h : ContIntertwiningMap π₁ π₂), f.comp (g + h) = f.comp g + f.comp h
-- Mathlib.CategoryTheory.Localization.FiniteProducts
CategoryTheory.Limits.constLimAdj.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C],
  CategoryTheory.Limits.constLimAdj =
    CategoryTheory.Adjunction.mk'
      {
        homEquiv := fun c g =>
          { toFun := fun f => CategoryTheory.Limits.limit.lift g { pt := c, π := f },
            invFun := fun f =>
              { app := fun x => CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.limit.π g x),
                naturality := ⋯ },
            left_inv := ⋯, right_inv := ⋯ },
        unit :=
          {
            app := fun x =>
              CategoryTheory.Limits.limit.lift
                ((CategoryTheory.Functor.const J).obj ((CategoryTheory.Functor.id C).1 x))
                { pt := (CategoryTheory.Functor.id C).1 x,
                  π :=
                    CategoryTheory.CategoryStruct.id
                      ((CategoryTheory.Functor.const J).obj ((CategoryTheory.Functor.id C).1 x)) },
            naturality := ⋯ },
        counit := { app := fun g => { app := CategoryTheory.Limits.limit.π g, naturality := ⋯ }, naturality := ⋯ },
        homEquiv_unit := ⋯, homEquiv_counit := ⋯ }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α]
  {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
    ⟨k, v⟩ ∈ l → ∀ {h : k' ∈ m.insertMany l}, (m.insertMany l).get k' h = cast ⋯ v
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.LocQuiver.mk.inj : ∀ {C : Type uC} {inst : CategoryTheory.Category.{uC', uC} C} {W : CategoryTheory.MorphismProperty C} {obj obj_1 : C},
  { obj := obj } = { obj := obj_1 } → obj = obj_1
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.edgeDensity_empty_left : ∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] (t : Finset β),
  Rel.edgeDensity r ∅ t = 0
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.span_gramSchmidtNormed_range : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (f : ι → E),
  Submodule.span 𝕜 (Set.range (InnerProductSpace.gramSchmidtNormed 𝕜 f)) =
    Submodule.span 𝕜 (Set.range (InnerProductSpace.gramSchmidt 𝕜 f))
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- Auxiliary definition for `triangleFunctor`.  -/
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.triangleMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                (n : ℤ) →
                  {X Y : C} →
                    (X ⟶ Y) →
                      (CategoryTheory.Triangulated.TStructure.TruncAux.triangle✝ t n X ⟶
                        CategoryTheory.Triangulated.TStructure.TruncAux.triangle✝ t n Y)
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.objEquiv_symm_id_mem_nonDegenerate : ∀ (n : ℕ),
  SSet.stdSimplex.objEquiv.symm (CategoryTheory.CategoryStruct.id (Opposite.unop (Opposite.op { len := n }))) ∈
    (SSet.stdSimplex.obj { len := n }).nonDegenerate n
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.withDischarger : {α : Type} → (Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)) → Bool → Lean.Meta.SimpM α → Lean.Meta.SimpM α
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpEntry.thm.sizeOf_spec : ∀ (a : Lean.Meta.SimpTheorem), sizeOf (Lean.Meta.SimpEntry.thm a) = 1 + sizeOf a
-- Init.Data.List.Zip
List.unzip_eq_map : ∀ {α : Type u_1} {β : Type u_2} {l : List (α × β)}, l.unzip = (List.map Prod.fst l, List.map Prod.snd l)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_of_mul_lt_of_one_le_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b c : α}, a * b < c → 1 ≤ b → a < c
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- Homeomorphism `Ω^M X ≃ₜ Ω^N X` if `M ≃ N`.  -/
GenLoop.congr : {N : Type u_1} →
  {X : Type u_2} → [inst : TopologicalSpace X] → {M : Type u_3} → (x : X) → M ≃ N → ↑(GenLoop M X x) ≃ₜ ↑(GenLoop N X x)
-- Mathlib.GroupTheory.OrderOfElement
isOfFinAddOrder_iff_nsmul_eq_zero : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G}, IsOfFinAddOrder x ↔ ∃ n, 0 < n ∧ n • x = 0