mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.compatible_familyOfElements : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {α : ι' → ι}
  {p' : (j : ι') → X' j ⟶ X (α j)} (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = f' j)
  {D₁ D₂ : F.DescentData f}
  (φ :
    (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₁ ⟶
      (CategoryTheory.Pseudofunctor.DescentData.pullFunctor F ⋯).obj D₂)
  (i : ι), (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.familyOfElements✝ w φ i).Compatible
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factorThru_add_sub_factorThru_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {P : CategoryTheory.Subobject Y} (f g : X ⟶ Y) (w : P.Factors (f + g)) (wg : P.Factors g),
  P.factorThru (f + g) w - P.factorThru g wg = P.factorThru f ⋯
-- Mathlib.Order.Filter.AtTopBot.Disjoint
Filter.disjoint_atTop_atBot : ∀ {α : Type u_3} [inst : PartialOrder α] [Nontrivial α], Disjoint Filter.atTop Filter.atBot
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.ker_addSubgroupMap : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H : AddSubgroup G) (f : G →+ N),
  (f.addSubgroupMap H).ker = f.ker.addSubgroupOf H
-- Mathlib.ModelTheory.Types
FirstOrder.Language.Theory.CompleteType.setOfPred_subset_eq_univ_iff : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} (S : (L.withConstants α).Theory),
  {p | S ⊆ ↑p} = Set.univ ↔ ∀ φ ∈ S, (L.lhomWithConstants α).onTheory T ⊨ᵇ φ
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L)
  {Z : HomologicalComplex C (ComplexShape.up ℤ)}
  (h :
    (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).obj
        (CochainComplex.mappingCone.triangle (CochainComplex.mappingCone.inr φ)).obj₁ ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.rotateHomotopyEquiv φ).hom
      (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle (CochainComplex.mappingCone.inr φ)).mor₃
        h) =
    CategoryTheory.CategoryStruct.comp (-(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map φ) h
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_mul_C : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ) (a : R), (p * Polynomial.C a).coeff n = p.coeff n * a
-- Mathlib.Topology.Maps.Proper.Basic
/-- The composition of two proper maps is proper.  -/
IsProperMap.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y} {g : Y → Z}, IsProperMap g → IsProperMap f → IsProperMap (g ∘ f)
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.IsVonNBounded.smul_tendsto_zero : ∀ {𝕜 : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {S : Set E} {ε : ι → 𝕜} {x : ι → E} {l : Filter ι},
  Bornology.IsVonNBounded 𝕜 S →
    (∀ᶠ (n : ι) in l, x n ∈ S) → Filter.Tendsto ε l (nhds 0) → Filter.Tendsto (ε • x) l (nhds 0)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.surjective : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (x : A.N), ∃ s, x = h.type₁ s ∨ x = h.type₂ s
-- Mathlib.Algebra.Category.Grp.Images
AddCommGrpCat.image.lift_fac : ∀ {G H : AddCommGrpCat} {f : G ⟶ H} (F' : CategoryTheory.Limits.MonoFactorisation f),
  CategoryTheory.CategoryStruct.comp (AddCommGrpCat.image.lift F') F'.m = AddCommGrpCat.image.ι f
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.triangle_obj₃ : ∀ {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]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  (h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  (h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  (h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃),
  (CategoryTheory.Triangulated.Octahedron'.triangle comm h₁₂ h₂₃ h₁₃ h).obj₃ = Z₂₃
-- Init.Data.Vector.Lemmas
Vector.foldrM_append : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n k : ℕ} [inst : Monad m] [LawfulMonad m] {f : α → β → m β}
  {b : β} {xs : Vector α n} {ys : Vector α k},
  Vector.foldrM f b (xs ++ ys) = do
    let b ← Vector.foldrM f b ys
    Vector.foldrM f b xs
-- Mathlib.Algebra.Group.TransferInstance
Equiv.vadd.eq_1 : ∀ (M : Type u_1) {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : VAdd M β],
  Equiv.vadd M e = { vadd := fun n x => e.invFun (n +ᵥ e.toFun x) }
-- Mathlib.Data.Fintype.Inv
Fintype.choose_subtype_eq : ∀ {α : Type u_4} (p : α → Prop) [inst : Fintype { a // p a }] [inst_1 : DecidableEq α] (x : { a // p a })
  (h : optParam (∃! a, ↑a = ↑x) ⋯), Fintype.choose (fun y => ↑y = ↑x) h = x
-- Mathlib.Algebra.Group.Conj
AddConjClasses.quotient_mk_eq_mk : ∀ {α : Type u} [inst : AddMonoid α] (a : α), ⟦a⟧ = AddConjClasses.mk a
-- Init.Sym.Lemmas
Lean.Sym.Int.dvd_eq_false : ∀ (a b : ℤ), decide (a ∣ b) = false → (a ∣ b) = False
-- Lean.Elab.ParseImportsFast
Lean.ParseImports.manyImports : Lean.ParseImports.Parser → Lean.ParseImports.Parser
-- Mathlib.Data.Fin.Basic
Fin.ne_iff_vne : ∀ {n : ℕ} (a b : Fin n), a ≠ b ↔ ↑a ≠ ↑b
-- Mathlib.Data.Stream.Init
Stream'.interleave_eq : ∀ {α : Type u} (s₁ s₂ : Stream' α), s₁ ⋈ s₂ = Stream'.cons s₁.head (Stream'.cons s₂.head (s₁.tail ⋈ s₂.tail))
-- Batteries.Linter.UnnecessarySeqFocus
/-- The `<;>` node itself.  -/
Batteries.Linter.UnnecessarySeqFocus.Entry.stx : Batteries.Linter.UnnecessarySeqFocus.Entry → Lean.Syntax
-- Mathlib.Order.Defs.LinearOrder
min_eq_left_of_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a < b → min a b = a
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeSemigroup.toFreeMonoid_injective : ∀ {α : Type u_1}, Function.Injective ⇑FreeSemigroup.toFreeMonoid
-- Mathlib.GroupTheory.RegularWreathProduct
/-- The element of Q  -/
RegularWreathProduct.right : {D : Type u_1} → {Q : Type u_2} → D ≀ᵣ Q → Q
-- Init.Data.List.Sublist
List.sublist_cons_iff : ∀ {α : Type u_1} {a : α} {l l' : List α}, l.Sublist (a :: l') ↔ l.Sublist l' ∨ ∃ r, l = a :: r ∧ r.Sublist l'
-- Mathlib.Topology.UniformSpace.Cauchy
TotallyBounded.exists_subset : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α},
  TotallyBounded s → ∀ {U : SetRel α α}, U ∈ uniformity α → ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.aleph_one_le_iff : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph 1 ≤ c ↔ Cardinal.aleph0 < c
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
modularCyclotomicCharacter.eq_1 : ∀ (L : Type u) [inst : CommRing L] [inst_1 : IsDomain L] {n : ℕ} [inst_2 : NeZero n]
  (hn : Nat.card ↥(rootsOfUnity n L) = n),
  modularCyclotomicCharacter L hn =
    (Units.mapEquiv (ZMod.ringEquivCongr hn).toMulEquiv).toMonoidHom.comp (modularCyclotomicCharacter' L n)
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.Name.mangleAux : Lean.Name → String
-- Mathlib.Algebra.Homology.ModelCategory.Injective
CochainComplex.Plus.modelCategoryQuillen.instHasLiftingPropertyOfMonoOfFibrationOfWeakEquivalence : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {A B X Y : CochainComplex.Plus C} (i : A ⟶ B) (p : X ⟶ Y) [CategoryTheory.Mono i] [HomotopicalAlgebra.Fibration p]
  [HomotopicalAlgebra.WeakEquivalence p], CategoryTheory.HasLiftingProperty i p
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- If `{Uᵢ}` covers `Y`, this is the pre-`0`-hypercover of `X ×[Z] Y` given by `{X ×[Z] Uᵢ}`.  -/
CategoryTheory.PreZeroHypercover.pullbackCoverOfRight : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {Y : C} →
      (E : CategoryTheory.PreZeroHypercover Y) →
        {X Z : C} →
          (f : X ⟶ Z) →
            (g : Y ⟶ Z) →
              [inst_1 : CategoryTheory.Limits.HasPullback f g] →
                [∀ (i : E.I₀), CategoryTheory.Limits.HasPullback f (CategoryTheory.CategoryStruct.comp (E.f i) g)] →
                  CategoryTheory.PreZeroHypercover (CategoryTheory.Limits.pullback f g)
-- Mathlib.Algebra.Group.Submonoid.Membership
/-- An induction principle for elements of `⨆ i, S i`.
If `C` holds for `1` and all elements of `S i` for all `i`, and is preserved under multiplication,
then it holds for all elements of the supremum of `S`.  -/
Submonoid.iSup_induction : ∀ {M : Type u_1} [inst : MulOneClass M] {ι : Sort u_4} (S : ι → Submonoid M) {motive : M → Prop} {x : M},
  x ∈ ⨆ i, S i →
    (∀ (i : ι), ∀ x ∈ S i, motive x) → motive 1 → (∀ (x y : M), motive x → motive y → motive (x * y)) → motive x
-- Mathlib.Algebra.Group.Action.Defs
SMulCommClass.mk : ∀ {M : Type u_9} {N : Type u_10} {α : Type u_11} [inst : SMul M α] [inst_1 : SMul N α],
  (∀ (m : M) (n : N) (a : α), m • n • a = n • m • a) → SMulCommClass M N α
-- Mathlib.RingTheory.TensorProduct.IsBaseChangePi
/-- Base change commutes with binary products.  -/
IsBaseChange.prodMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {M : Type u_3}
  {N : Type u_4} {M' : Type u_5} {N' : Type u_6} [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : AddCommMonoid M'] [inst_8 : AddCommMonoid N']
  [inst_9 : Module R M'] [inst_10 : Module R N'] [inst_11 : Module S M'] [inst_12 : Module S N']
  [inst_13 : IsScalarTower R S M'] [inst_14 : IsScalarTower R S N'] (f : M →ₗ[R] M') (g : N →ₗ[R] N'),
  IsBaseChange S f → IsBaseChange S g → IsBaseChange S (f.prodMap g)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearMap.IsInvertible.inverse_comp_self : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace M₂]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {f : M →L[R] M₂}, f.IsInvertible → f.inverse ∘SL f = ContinuousLinearMap.id R M
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopicWith.trans : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {P : C(X, Y) → Prop}
  ⦃f g h : C(X, Y)⦄, f.HomotopicWith g P → g.HomotopicWith h P → f.HomotopicWith h P
-- Mathlib.Data.Sym.Sym2
/-- Mapping an unordered pair on the diagonal to a finite set produces a finset of size `1`.  -/
Sym2.card_toFinset_of_isDiag : ∀ {α : Type u_1} [inst : DecidableEq α] (z : Sym2 α), z.IsDiag → z.toFinset.card = 1
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- The fact that `χ` factors through `χ₀` of level `d`  -/
DirichletCharacter.FactorsThrough.eq_changeLevel : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} {χ : DirichletCharacter R n} {d : ℕ} (h : χ.FactorsThrough d),
  χ = (DirichletCharacter.changeLevel ⋯) h.χ₀
-- Mathlib.Combinatorics.SimpleGraph.Circulant
SimpleGraph.instDecidableRelAdjCirculantGraphOfDecidableEqOfDecidablePredMemSet : {G : Type u_1} →
  [inst : AddGroup G] →
    (s : Set G) → [DecidableEq G] → [DecidablePred fun x => x ∈ s] → DecidableRel (SimpleGraph.circulantGraph s).Adj
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- The pointwise inversion of set `s⁻¹` is defined as `{x | x⁻¹ ∈ s}` in scope `Pointwise`. It is
equal to `{x⁻¹ | x ∈ s}`, see `Set.image_inv_eq_inv`.  -/
Set.inv : {α : Type u_2} → [Inv α] → Inv (Set α)
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.coneOfPreserves_π_app_left : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (F : CategoryTheory.Functor J (CategoryTheory.Comma L R))
  [inst_4 : CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R]
  (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R)))
  {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂)
  (j : J), ((CategoryTheory.Comma.coneOfPreserves F c₁ t₂).π.app j).left = c₁.π.app j
-- Mathlib.Topology.UniformSpace.Cauchy
CompleteSpace.fst_of_prod : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] [inst : UniformSpace β] [CompleteSpace (α × β)]
  [h : Nonempty β], CompleteSpace α
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeIsoApp.eq_3 : ∀ (C : Type u) (x : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C)
  (X a : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C (X.tensor a) x =
    (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.FreeMonoidalCategory.inclusion.obj { as := x.as })
          X a).symm ≪≫
      CategoryTheory.MonoidalCategory.whiskerRightIso (CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C X x) a ≪≫
        CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C a { as := X.normalizeObj x.as }
-- Std.Async.System
Std.Async.System.instReprCPUInfo : Repr Std.Async.System.CPUInfo
-- Mathlib.GroupTheory.GroupAction.Jordan
/-- A criterion due to Jordan for being 2-pretransitive (Wielandt, 13.1)  -/
MulAction.IsPreprimitive.is_two_pretransitive : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
  MulAction.IsPreprimitive G α →
    ∀ {s : Set α} {n : ℕ},
      s.ncard = n + 1 →
        n + 2 < Nat.card α →
          MulAction.IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
            MulAction.IsMultiplyPretransitive G α 2
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_range_comp : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {ι : Sort u_5} (f : ι → α) (g : α → M),
  (Set.range f).indicator g ∘ f = g ∘ f
-- Mathlib.Computability.TuringMachine.Tape
Turing.Dir.noConfusionType : Sort v✝ → Turing.Dir → Turing.Dir → Sort v✝
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The composition of the isomorphism `pullbackSpecIso R S T` (from the pullback of
`Spec S ⟶ Spec R` and `Spec T ⟶ Spec R` to `Spec (S ⊗[R] T)`) with the morphism
`Spec (S ⊗[R] T) ⟶ Spec T` obtained by applying `Spec.map` to the ring morphism `t ↦ 1 ⊗ₜ[R] t`
is the second projection.
 -/
AlgebraicGeometry.pullbackSpecIso_hom_snd_assoc : ∀ (R S T : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T] {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of T) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso R S T).hom
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight)) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R S)))
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R T))))
      h
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instReprPower : Repr Lean.Grind.CommRing.Power
-- Mathlib.Algebra.Star.StarAlgHom
/-- Reinterpret a star algebra equivalence as a `StarRingEquiv` by forgetting the interaction with
the scalar multiplication.  -/
StarAlgEquiv.toStarRingEquiv : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : Add A] →
        [inst_1 : Add B] →
          [inst_2 : Mul A] →
            [inst_3 : Mul B] →
              [inst_4 : SMul R A] →
                [inst_5 : SMul R B] → [inst_6 : Star A] → [inst_7 : Star B] → (A ≃⋆ₐ[R] B) → A ≃⋆+* B
-- Mathlib.Algebra.Group.Subgroup.Defs
InvMemClass.coe_inv : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} {H : S} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G] (x : ↥H),
  ↑x⁻¹ = (↑x)⁻¹
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
expNegInvGlue.zero_iff_nonpos : ∀ {x : ℝ}, expNegInvGlue x = 0 ↔ x ≤ 0
-- Mathlib.Data.Finite.Defs
Finite.false : ∀ {α : Sort u_1} [Infinite α], Finite α → False
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.swap_mem_interedges_iff : ∀ {α : Type u_4} {r : α → α → Prop} [inst : DecidableRel r] {s t : Finset α} [Std.Symm r] {x : α × α},
  x.swap ∈ Rel.interedges r s t ↔ x ∈ Rel.interedges r t s
-- Init.Data.Vector.Monadic
Vector.mapM_pure : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {xs : Vector α n}
  (f : α → β), Vector.mapM (fun x => pure (f x)) xs = pure (Vector.map f xs)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the sign of the angle between three points is negative, the first and third points are not
equal.  -/
EuclideanGeometry.left_ne_right_of_oangle_sign_eq_neg_one : ∀ {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}, (EuclideanGeometry.oangle p₁ p₂ p₃).sign = -1 → p₁ ≠ p₃
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.w_mk_right_assoc : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f : CategoryTheory.Arrow T} {X Y : T} {g : X ⟶ Y}
  (sq : f ⟶ CategoryTheory.Arrow.mk g) {Z : T} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left sq) (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right sq) h)
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.hom_inv_id_left_assoc : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (e : f ≅ g) {Z : T}
  (h : f.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left e.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left e.inv) h) =
    h
-- Init.Data.Int.Order
Int.sign_of_add_one : ∀ (x : ℕ), (↑x + 1).sign = 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss.0.Polynomial.Chebyshev.sumZeroes.eq_1 : ∀ (n : ℕ) (P : Polynomial ℝ),
  Polynomial.Chebyshev.sumZeroes n P =
    Real.pi / ↑n * ∑ i ∈ Finset.range n, Polynomial.eval (Real.cos ((2 * ↑i + 1) / (2 * ↑n) * Real.pi)) P
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorPushforward_comp : ∀ {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} {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  (G : CategoryTheory.Functor D E) (R : CategoryTheory.Sieve X),
  CategoryTheory.Sieve.functorPushforward (F.comp G) R =
    CategoryTheory.Sieve.functorPushforward G (CategoryTheory.Sieve.functorPushforward F R)
-- Mathlib.Data.Fintype.Pi
/-- Finite product of finite sets is finite. Note this is a variant of `Set.Finite.pi` without the
extra `i ∈ univ` binder.  -/
Set.Finite.pi' : ∀ {ι : Type u_3} [Finite ι] {κ : ι → Type u_4} {t : (i : ι) → Set (κ i)},
  (∀ (i : ι), (t i).Finite) → {f | ∀ (i : ι), f i ∈ t i}.Finite
-- Mathlib.Topology.UniformSpace.UniformEmbedding
totallyBounded_image_iff : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {f : α → β} {s : Set α},
  IsUniformInducing f → (TotallyBounded (f '' s) ↔ TotallyBounded s)
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.h1Cotangentι_injective : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Extension R S}, Function.Injective ⇑Algebra.Extension.h1Cotangentι
-- Mathlib.Topology.Order.WithTop
WithTop.tendsto_untopA : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] [inst_3 : Nonempty ι]
  {a : WithTop ι}, a ≠ ⊤ → Filter.Tendsto WithTop.untopA (nhds a) (nhds a.untopA)
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.getD_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {fallback : β}, m₁.Equiv m₂ → m₁.getD k fallback = m₂.getD k fallback
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.sum_sq_norm_inner_right : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (x : E),
  ∑ i, ‖inner 𝕜 (b i) x‖ ^ 2 = ‖x‖ ^ 2
-- Qq.SortLocalDecls
Qq.SortLocalDecls.Context.mk : Lean.NameMap Lean.LocalDecl → Qq.SortLocalDecls.Context
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.instLT : {ι : Type u_1} → LT (AbstractSimplicialComplex ι)
-- Mathlib.Data.Matrix.Basic
Matrix.zero_le_one_row : ∀ {n : Type u_3} {α : Type u_11} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α] [inst_3 : Preorder α]
  [ZeroLEOneClass α] (i : n), 0 ≤ 1 i
-- Mathlib.Analysis.Analytic.Composition
AnalyticOn.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : F → G} {g : E → F} {s : Set F} {t : Set E},
  AnalyticOn 𝕜 f s → AnalyticOn 𝕜 g t → Set.MapsTo g t s → AnalyticOn 𝕜 (f ∘ g) t
-- Mathlib.Data.NNReal.Defs
NNReal.ne_iff : ∀ {x y : NNReal}, ↑x ≠ ↑y ↔ x ≠ y
-- Std.Data.HashMap.Basic
/-- Inserts multiple mappings into the hash map by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`.
The `insertMany` function on `HashSet` and `HashSet.Raw` behaves differently: it will prefer the first
appearance.
 -/
Std.HashMap.insertMany : {α : Type u} →
  {β : Type v} →
    {x : BEq α} → {x_1 : Hashable α} → {ρ : Type w} → [ForIn Id ρ (α × β)] → Std.HashMap α β → ρ → Std.HashMap α β
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.instPreservesLimitsOfSizeFunctorOppositeTypeShrinkYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w', v, u} C],
  CategoryTheory.Limits.PreservesLimitsOfSize.{t, w, v, max u w', u, max (max u v) (w' + 1)}
    CategoryTheory.shrinkYoneda.{w', v, u}
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.im_ofNat : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddCommGroupWithOne R] (n : ℕ) [inst_1 : n.AtLeastTwo], (OfNat.ofNat n).im = 0
-- Init.Data.SInt.Lemmas
Int8.zero_ne_one : 0 ≠ 1