mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Search.Expansion
_private.Aesop.Search.Expansion.0.Aesop.runFirstUnsafeRule.loop : {Q : Type} →
  [inst : Aesop.Queue Q] → Aesop.GoalRef → Aesop.UnsafeQueue → Aesop.SearchM Q (Aesop.UnsafeQueue × Aesop.RuleResult)
-- Mathlib.Algebra.Group.Semiconj.Basic
AddSemiconjBy.neg_neg_symm_iff : ∀ {G : Type u_1} [inst : SubtractionMonoid G] {a x y : G}, AddSemiconjBy (-a) (-x) (-y) ↔ AddSemiconjBy a y x
-- Mathlib.RingTheory.HahnSeries.Basic
/-- `single a r` is the Hahn series which has coefficient `r` at `a` and zero otherwise.  -/
HahnSeries.single : {Γ : Type u_1} → {R : Type u_3} → [inst : PartialOrder Γ] → [inst_1 : Zero R] → Γ → ZeroHom R (HahnSeries Γ R)
-- Mathlib.NumberTheory.ModularForms.Petersson
UpperHalfPlane.petersson_slash_SL : ∀ (k : ℤ) (f f' : UpperHalfPlane → ℂ) (g : Matrix.SpecialLinearGroup (Fin 2) ℤ) (τ : UpperHalfPlane),
  UpperHalfPlane.petersson k (SlashAction.map k g f) (SlashAction.map k g f') τ =
    UpperHalfPlane.petersson k f f' (g • τ)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map_mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {Y : C} {S : CategoryTheory.Functor C D} {f : S.obj Y ⟶ T} (g : T ⟶ T'),
  (CategoryTheory.CostructuredArrow.map g).obj (CategoryTheory.CostructuredArrow.mk f) =
    CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.preservesLimitsOfShape_presheafToSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{t, w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1}
  {CD : D → Type t} [inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_5 : CategoryTheory.ConcreteCategory D FD]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [inst_7 : (CategoryTheory.forget D).ReflectsIsomorphisms]
  [inst_8 :
    ∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  (K : Type w') [inst_9 : CategoryTheory.SmallCategory K] [CategoryTheory.FinCategory K]
  [CategoryTheory.Limits.HasLimitsOfShape K D] [CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget D)]
  [∀ (X : C), Small.{t, max u v} (J.Cover X)ᵒᵖ],
  CategoryTheory.Limits.PreservesLimitsOfShape K (CategoryTheory.plusPlusSheaf J D)
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.instInhabitedBuiltinSimprocs.default : Lean.Meta.Simp.BuiltinSimprocs
-- Mathlib.Tactic.CategoryTheory.Reassoc
/-- Given an equation `f = g` between morphisms `X ⟶ Y` in a category,
produce the equation `∀ {Z} (h : Y ⟶ Z), f ≫ h = g ≫ h`,
but with compositions fully right associated and identities removed.
Also returns the category `C` and any instance metavariables that need to be solved for.
 -/
Mathlib.Tactic.Reassoc.reassocExprHom : Lean.Expr → Lean.MetaM (Lean.Expr × Array Lean.MVarId)
-- Mathlib.GroupTheory.Focal
Subgroup.focalSubgroupOf_eq_closure : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.focalSubgroupOf = Subgroup.closure {g | ∃ x ∈ H, ∃ u, ↑g = ⁅x, u⁆}
-- Init.Data.Array.Find
Array.isSome_findSome? : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Option β},
  (Array.findSome? f xs).isSome = xs.any fun x => (f x).isSome
-- Mathlib.Condensed.TopCatAdjunction
/-- The unit of the adjunction `condensedSetToTopCat ⊣ topCatToCondensedSet`  -/
CondensedSet.topCatAdjunctionUnit : (X : CondensedSet) → X ⟶ X.toTopCat.toCondensedSet
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.QInfty_comp_PInfty_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {Z : ChainComplex C ℕ}
  (h : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.QInfty
      (CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Tactic.ITauto
/-- Insert a proposition and its proof into the context, as in `have : A := p`. This will eagerly
apply all level 1 rules on the spot, which are rules that don't split the goal and are validity
preserving: specifically, we drop `⊤` and `A → ⊤` hypotheses, close the goal if we find a `⊥`
hypothesis, split all conjunctions, and also simplify `⊥ → A` (drop), `⊤ → A` (simplify to `A`),
`A ∧ B → C` (curry to `A → B → C`) and `A ∨ B → C` (rewrite to `(A → C) ∧ (B → C)` and split).  -/
Mathlib.Tactic.ITauto.Context.add : Mathlib.Tactic.ITauto.IProp →
  Mathlib.Tactic.ITauto.Proof →
    Mathlib.Tactic.ITauto.Context →
      Except (Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.Proof) Mathlib.Tactic.ITauto.Context
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueData_t : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (i j : ↑X.affineOpens), I.glueData.t i j = I.glueDataT i j
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainBotCoeff_add_chainTopCoeff_le_three : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι} [P.IsReduced],
  RootPairing.chainBotCoeff i j + RootPairing.chainTopCoeff i j ≤ 3
-- Mathlib.NumberTheory.NumberField.AdeleRing
NumberField.AdeleRing.instInhabited : (R : Type u_1) →
  (K : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : IsDedekindDomain R] →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] → [inst_4 : IsFractionRing R K] → Inhabited (NumberField.AdeleRing R K)
-- Lean.Elab.BuiltinNotation
/-- Return `true` if `lhs` is a free variable and `rhs` does not depend on it.  -/
_private.Lean.Elab.BuiltinNotation.0.Lean.Elab.Term.isSubstCandidate : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Init.Data.List.Basic
/-- If one list is a permutation of the other, adding the same element as the head of each yields
lists that are permutations of each other: `l₁ ~ l₂ → x::l₁ ~ x::l₂`.
 -/
List.Perm.cons : ∀ {α : Type u} (x : α) {l₁ l₂ : List α}, l₁.Perm l₂ → (x :: l₁).Perm (x :: l₂)
-- Mathlib.Order.SuccPred.Limit
Order.isSuccPrelimit_toDual_iff : ∀ {α : Type u_1} {a : α} [inst : LT α], Order.IsSuccPrelimit (OrderDual.toDual a) ↔ Order.IsPredPrelimit a
-- Init.Data.SInt.Lemmas
ISize.toInt32_ofIntClamp : ∀ {n : ℤ},
  -2 ^ (System.Platform.numBits - 1) ≤ n →
    n < 2 ^ (System.Platform.numBits - 1) → (ISize.ofIntClamp n).toInt32 = Int32.ofInt n
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.IfInput.rhs : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → {w : ℕ} → Std.Sat.AIG.RefVec.IfInput aig w → aig.RefVec w
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.toProp.eq_7 : ∀ (K : Type u_2) [inst : Add K] [inst_1 : Mul K] [inst_2 : Neg K] [inst_3 : Zero K] [inst_4 : One K],
  FirstOrder.Field.FieldAxiom.toProp K FirstOrder.Field.FieldAxiom.existsInv = ∀ (x : K), x ≠ 0 → ∃ y, x * y = 1
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- The presheaf of smooth functions from `M` to `R`, for `R` a smooth ring, as a presheaf
of rings.  -/
smoothPresheafRing : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              ModelWithCorners 𝕜 EM HM →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [ChartedSpace HM M] →
                                  (R : Type u) →
                                    [inst_9 : TopologicalSpace R] →
                                      [inst_10 : ChartedSpace H R] →
                                        [inst_11 : Ring R] →
                                          [ContMDiffRing I (↑⊤) R] → TopCat.Presheaf RingCat (TopCat.of M)
-- Mathlib.Analysis.CStarAlgebra.Matrix
Matrix.l2_opNNNorm_conjTranspose : ∀ {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] [inst_4 : DecidableEq m] (A : Matrix m n 𝕜), ‖A.conjTranspose‖₊ = ‖A‖₊
-- Mathlib.Algebra.Order.IsBotOne
/-- **Alias** of `pos_of_gt`. -/
LT.lt.pos : ∀ {α : Type u_1} {a b : α} [inst : Preorder α] [inst_1 : Zero α] [IsBotZeroClass α], a < b → 0 < b
-- Lean.Elab.PreDefinition.TerminationMeasure
_private.Lean.Elab.PreDefinition.TerminationMeasure.0.Lean.Elab.TerminationMeasure.delab.go.match_1.splitter : (motive : ℕ → Lean.TSyntaxArray `ident → Sort u_1) →
  (x : ℕ) →
    (x_1 : Lean.TSyntaxArray `ident) →
      ((vars : Lean.TSyntaxArray `ident) → motive 0 vars) →
        ((i : ℕ) → (vars : Lean.TSyntaxArray `ident) → motive i.succ vars) → motive x x_1
-- Mathlib.Algebra.Lie.Rank
LieAlgebra.exists_isRegular : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] [IsDomain R] [Infinite R], ∃ x, LieAlgebra.IsRegular R x
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- the numerator of a left fraction  -/
CategoryTheory.MorphismProperty.LeftFraction.f : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → (self : W.LeftFraction X Y) → X ⟶ self.Y'
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
WeakFEPair.mk.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f f_1 : ℝ → E) (e_f : f = f_1)
  (g g_1 : ℝ → E) (e_g : g = g_1) (k k_1 : ℝ) (e_k : k = k_1) (ε ε_1 : ℂ) (e_ε : ε = ε_1) (f₀ f₀_1 : E)
  (e_f₀ : f₀ = f₀_1) (g₀ g₀_1 : E) (e_g₀ : g₀ = g₀_1)
  (hf_int : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume)
  (hg_int : MeasureTheory.LocallyIntegrableOn g (Set.Ioi 0) MeasureTheory.volume) (hk : 0 < k) (hε : ε ≠ 0)
  (h_feq : ∀ x ∈ Set.Ioi 0, f (1 / x) = (ε * ↑(x ^ k)) • g x)
  (hf_top : ∀ (r : ℝ), (fun x => f x - f₀) =O[Filter.atTop] fun x => x ^ r)
  (hg_top : ∀ (r : ℝ), (fun x => g x - g₀) =O[Filter.atTop] fun x => x ^ r),
  { f := f, g := g, k := k, ε := ε, f₀ := f₀, g₀ := g₀, hf_int := hf_int, hg_int := hg_int, hk := hk, hε := hε,
      h_feq := h_feq, hf_top := hf_top, hg_top := hg_top } =
    { f := f_1, g := g_1, k := k_1, ε := ε_1, f₀ := f₀_1, g₀ := g₀_1, hf_int := ⋯, hg_int := ⋯, hk := ⋯, hε := ⋯,
      h_feq := ⋯, hf_top := ⋯, hg_top := ⋯ }
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearMap.injective_of_linearIndependent : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_6}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N} {ι : Type u_7} {v : ι → M},
  Submodule.span R (Set.range v) = ⊤ → LinearIndependent R (⇑f ∘ v) → Function.Injective ⇑f
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_mono_of_nonneg : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E]
  [ClosedIciTopology E] {f g : α → E},
  0 ≤ᵐ[μ] f → MeasureTheory.Integrable g μ → f ≤ᵐ[μ] g → ∫ (a : α), f a ∂μ ≤ ∫ (a : α), g a ∂μ
-- Mathlib.Topology.Perfect
perfect_def : ∀ {α : Type u_1} [inst : TopologicalSpace α] (C : Set α), Perfect C ↔ IsClosed C ∧ Preperfect C
-- Mathlib.Computability.NFA
NFA.accepts_iff_exists_path : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} {x : List α},
  x ∈ M.accepts ↔ ∃ s ∈ M.start, ∃ t ∈ M.accept, Nonempty (M.Path s t x)
-- Mathlib.Data.Multiset.Sym
Multiset.mem_sym2_iff : ∀ {α : Type u_1} {m : Multiset α} {z : Sym2 α}, z ∈ m.sym2 ↔ ∀ y ∈ z, y ∈ m
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termG₃ : Lean.ParserDescr
-- Mathlib.Algebra.Ring.Prod
RingHom.snd_comp_prod : ∀ {R : Type u_1} {S : Type u_3} {T : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : NonAssocSemiring T] (f : R →+* S) (g : R →+* T), (RingHom.snd S T).comp (f.prod g) = g
-- Mathlib.AlgebraicGeometry.Geometrically.Integral
AlgebraicGeometry.instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian_1 : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.GeometricallyIntegral g]
  [AlgebraicGeometry.Flat g] [AlgebraicGeometry.UniversallyOpen g] [AlgebraicGeometry.IsIntegral X]
  [AlgebraicGeometry.IsLocallyNoetherian X], AlgebraicGeometry.IsIntegral (CategoryTheory.Limits.pullback f g)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
MeasureTheory.probReal_add_probReal_compl : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  [MeasureTheory.IsProbabilityMeasure μ], MeasurableSet s → μ.real s + μ.real sᶜ = 1
-- Mathlib.LinearAlgebra.Dimension.Constructions
Pi.dim_spanSubset : ∀ {R : Type u} {ι : Type w} [inst : Semiring R] [StrongRankCondition R] [inst_2 : Finite ι] [Nontrivial R] {s : Set ι},
  Module.finrank R ↥(Pi.spanSubset R s) = s.ncard
-- Mathlib.Algebra.Notation.Support
Function.mem_support : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] {f : ι → M} {x : ι}, x ∈ Function.support f ↔ f x ≠ 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblU_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P : Fin 3 → R},
  P 2 = 0 → W'.dblU P = -3 * P 0 ^ 2
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- A convenience class, for a completely metrizable space endowed with a complete metric.
No instance of this class should be registered: It should be used as
`letI := upgradeIsCompletelyMetrizable X` to endow a completely metrizable
space with a complete metric.  -/
TopologicalSpace.UpgradedIsCompletelyMetrizableSpace : Type u_3 → Type u_3
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.extend.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) {X : C} (f : X ⟶ c.pt),
  c.extend f = { pt := X, π := CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const J).map f) c.π }
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.ConeMorphism.ext : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (f g : c ⟶ c'), f.hom = g.hom → f = g
-- Mathlib.LinearAlgebra.Alternating.Basic
LinearMap.compAlternatingMap_smul : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {S : Type u_10} {N₂ : Type u_11}
  [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] [inst_7 : Monoid S] [inst_8 : DistribMulAction S N]
  [inst_9 : DistribMulAction S N₂] [inst_10 : SMulCommClass R S N] [inst_11 : SMulCommClass R S N₂]
  [LinearMap.CompatibleSMul N N₂ S R] (g : N →ₗ[R] N₂) (s : S) (f : M [⋀^ι]→ₗ[R] N),
  g.compAlternatingMap (s • f) = s • g.compAlternatingMap f
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.artanh_lt_artanh_iff : ∀ {x y : ℝ}, x ∈ Set.Ioo (-1) 1 → y ∈ Set.Ioo (-1) 1 → (Real.artanh x < Real.artanh y ↔ x < y)
-- Init.Data.Float.Model.Unpacked.Sign
/-- Negative (`-`) sign.  -/
Float.Model.UnpackedFloat.Sign.negative : Float.Model.UnpackedFloat.Sign
-- Lean.Meta.SizeOf
_private.Lean.Meta.SizeOf.0.Lean.Meta.ignoreField : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Order.Filter.Pointwise
Filter.bot_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {g : Filter β}, ⊥ • g = ⊥
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_roc : ∀ {m n i : ℕ}, (m<...=n).toArray[i]? = if i < n - m then some (m + 1 + i) else none
-- Mathlib.LinearAlgebra.Basis.SMul
/-- A version of `unitsSMul` that uses `IsUnit`.  -/
Module.Basis.isUnitSMul : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → Module.Basis ι R M → {w : ι → R} → (∀ (i : ι), IsUnit (w i)) → Module.Basis ι R M
-- Mathlib.Algebra.Squarefree.Basic
squarefree_iff_irreducible_sq_not_dvd_of_ne_zero : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [WfDvdMonoid R] {r : R},
  r ≠ 0 → (Squarefree r ↔ ∀ (x : R), Irreducible x → ¬x * x ∣ r)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.orderBot : {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] → OrderBot (E →ₛₗ.[σ] F)
-- Mathlib.Analysis.Complex.MeanValue
/-- The **Mean Value Property** of complex differentiable functions: If `f : ℂ → E` is complex
differentiable at all points of a closed disc of radius `R` and center `c`, then the circle average
`circleAverage f c R` equals `f c`.
 -/
DiffContOnCl.circleAverage : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {R : ℝ} {c : ℂ},
  DiffContOnCl ℂ f (Metric.ball c |R|) → Real.circleAverage f c R = f c
-- Init.Data.Int.Bitwise.Lemmas
Int.negSucc_shiftRight : ∀ (m n : ℕ), Int.negSucc m >>> n = Int.negSucc (m >>> n)
-- Mathlib.Order.UpperLower.Principal
LowerSet.Iio.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] (a : α), LowerSet.Iio a = { carrier := Set.Iio a, lower' := ⋯ }
-- Mathlib.Order.Filter.Pointwise
Filter.isScalarTower'' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SMul α β] [inst_1 : SMul α γ] [inst_2 : SMul β γ]
  [IsScalarTower α β γ], IsScalarTower (Filter α) (Filter β) (Filter γ)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.not_specializes_infty_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, ¬OnePoint.infty ⤳ ↑x
-- Aesop.Tracing
Aesop.traceSimpTheoremTreeContents : Lean.Meta.SimpTheoremTree → Aesop.TraceOption → Lean.CoreM Unit
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
IsFreeGroupoid.SpanningTree.treeHom.eq_1 : ∀ {G : Type u} [inst : CategoryTheory.Groupoid G] [inst_1 : IsFreeGroupoid G]
  (T : WideSubquiver (Quiver.Symmetrify (IsFreeGroupoid.Generators G)))
  [inst_2 : Quiver.Arborescence (WideSubquiver.toType (Quiver.Symmetrify (IsFreeGroupoid.Generators G)) T)] (a : G),
  IsFreeGroupoid.SpanningTree.treeHom T a = IsFreeGroupoid.SpanningTree.homOfPath T default
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp_inv_app_fst_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  {A₂ : Type u₇} {B₂ : Type u₈} {C₂ : Type u₉} [inst_6 : CategoryTheory.Category.{v₇, u₇} A₂]
  [inst_7 : CategoryTheory.Category.{v₈, u₈} B₂] [inst_8 : CategoryTheory.Category.{v₉, u₉} C₂]
  {F₂ : CategoryTheory.Functor A₂ B₂} {G₂ : CategoryTheory.Functor C₂ B₂} (X : Type u₁₀)
  [inst_9 : CategoryTheory.Category.{v₁₀, u₁₀} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (ψ' : CategoryTheory.Limits.CatCospanTransform F₁ G₁ F₂ G₂)
  (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (x : X),
  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp X ψ ψ').inv.app X_1).fst.app x =
    CategoryTheory.CategoryStruct.id (ψ'.left.obj (ψ.left.obj (X_1.fst.obj x)))
-- Mathlib.Algebra.Category.HopfAlgCat.Monoidal
HopfAlgCat.tensorUnit_carrier : ∀ (R : Type u) [inst : CommRing R], (CategoryTheory.MonoidalCategoryStruct.tensorUnit (HopfAlgCat R)).carrier = R
-- Mathlib.Algebra.CubicDiscriminant
Cubic.toPoly_injective : ∀ {R : Type u_1} [inst : Semiring R] (P Q : Cubic R), P.toPoly = Q.toPoly ↔ P = Q
-- Mathlib.GroupTheory.SpecificGroups.Alternating
Equiv.Perm.mul_mem_alternatingGroup_of_isSwap : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {g g' : Equiv.Perm α},
  g.IsSwap → g'.IsSwap → g * g' ∈ alternatingGroup α
-- Mathlib.Tactic.Choose
Mathlib.Tactic.Choose.ElimStatus.success : Mathlib.Tactic.Choose.ElimStatus
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curry_map_app_app : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E] {X Y : CategoryTheory.Functor (C × D) E} (T : X ⟶ Y)
  (X_1 : C) (Y_1 : D), ((CategoryTheory.Functor.curry.map T).app X_1).app Y_1 = T.app (X_1, Y_1)
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coequalizer.isoTargetOfSelf_inv : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f : X ⟶ Y),
  (CategoryTheory.Limits.coequalizer.isoTargetOfSelf f).inv = CategoryTheory.Limits.coequalizer.π f f
-- Mathlib.Analysis.Real.Sqrt
Real.le_sqrt' : ∀ {x y : ℝ}, 0 < x → (x ≤ √y ↔ x ^ 2 ≤ y)
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.inftyValued.def : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)] {x : RatFunc F},
  Valued.v x = RatFunc.inftyValuationDef F x
-- Mathlib.Order.BooleanAlgebra.Set
Set.disjoint_of_subset_iff_left_eq_empty : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → (Disjoint s t ↔ s = ∅)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.id_whiskerLeft_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) f) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
      (CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv h))
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.neg_def : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddGroup X] [inst_3 : DistribMulAction R X] (r : X) (s : ↥S), -(r /ₒ s) = -r /ₒ s
-- Mathlib.MeasureTheory.Function.LpOrder
MeasureTheory.Lp.instLattice : {α : Type u_1} →
  {E : Type u_2} →
    {m : MeasurableSpace α} →
      {μ : MeasureTheory.Measure α} →
        {p : ENNReal} →
          [inst : NormedAddCommGroup E] →
            [inst_1 : Lattice E] → [HasSolidNorm E] → [IsOrderedAddMonoid E] → Lattice ↥(MeasureTheory.Lp E p μ)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
/-- The functor sending a `G`-representation `A` to `Hⁿ(G, A)`.  -/
groupCohomology.functor : (k G : Type u) → [inst : CommRing k] → [inst_1 : Group G] → ℕ → CategoryTheory.Functor (Rep.{u, u, u} k G) (ModuleCat k)