mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Basic
/-- For every arity, a `Type v` of relations of that arity  -/
FirstOrder.Language.Relations : FirstOrder.Language → ℕ → Type v
-- Mathlib.Algebra.Tropical.Basic
Tropical.add_eq_left : ∀ {R : Type u} [inst : LinearOrder R] ⦃x y : Tropical R⦄, x ≤ y → x + y = x
-- Mathlib.Order.Category.FinBddDistLat
_private.Mathlib.Order.Category.FinBddDistLat.0.FinBddDistLat.Hom.mk.inj : ∀ {X Y : FinBddDistLat} {hom' hom'_1 : BoundedLatticeHom ↑X.toDistLat ↑Y.toDistLat},
  { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- A constructor for chain maps between `ℕ`-indexed chain complexes,
working by induction on commutative squares.

You need to provide the components of the chain map in degrees 0 and 1,
show that these form a commutative square,
and then give a construction of each component,
and the fact that it forms a commutative square with the previous component,
using as an inductive hypothesis the data (and commutativity) of the previous two components.
 -/
ChainComplex.mkHom : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (P Q : ChainComplex V ℕ) →
        (zero : P.X 0 ⟶ Q.X 0) →
          (one : P.X 1 ⟶ Q.X 1) →
            CategoryTheory.CategoryStruct.comp one (Q.d 1 0) = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero →
              ((n : ℕ) →
                  (p :
                      (f : P.X n ⟶ Q.X n) ×'
                        (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×'
                          CategoryTheory.CategoryStruct.comp f' (Q.d (n + 1) n) =
                            CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f) →
                    (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
                      CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 2) (n + 1)) =
                        CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst) →
                (P ⟶ Q)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.uset : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.FVarId →
    ℕ →
      Lean.FVarId →
        Lean.Compiler.LCNF.Code pu →
          autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_9 → Lean.Compiler.LCNF.Code pu
-- Mathlib.Data.Multiset.UnionInter
Multiset.union.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s.union t = s - t + t
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- Embedding of a subalgebra into the algebra, as an algebra homomorphism.  -/
SubalgebraClass.val : {S : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : SetLike S A] → [inst_4 : SubsemiringClass S A] → [hSR : SMulMemClass S R A] → (s : S) → ↥s →ₐ[R] A
-- Mathlib.Topology.Category.Profinite.Basic
/-- The natural functor from `Fintype` to `Profinite`, endowing a finite type with the
discrete topology.  -/
FintypeCat.toProfinite : CategoryTheory.Functor FintypeCat Profinite
-- Mathlib.Tactic.Linter.Style
/-- If `stx` is syntax describing an `open` command, `extractOpenNames stx`
returns an array of the syntax corresponding to the opened names,
omitting any renamed or hidden items.

This only checks independent `open` commands: for `open ... in ...` commands,
this linter returns an empty array.
 -/
Mathlib.Linter.Style.openClassical.extractOpenNames : Lean.Syntax → Array (Lean.TSyntax `ident)
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
/-- `Restriction N M` means that `N = M ↾ R` for some subset `R` of `M.E`  -/
Matroid.IsRestriction : {α : Type u_1} → Matroid α → Matroid α → Prop
-- Mathlib.Topology.MetricSpace.Infsep
Set.infsep.eq_1 : ∀ {α : Type u_1} [inst : EDist α] (s : Set α), s.infsep = s.einfsep.toReal
-- Mathlib.Topology.Order.LocalExtr
IsLocalMaxOn.max : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {a : α} {s : Set α},
  IsLocalMaxOn f s a → IsLocalMaxOn g s a → IsLocalMaxOn (fun x => max (f x) (g x)) s a
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.rule_expr_ : Lean.ParserDescr
-- Std.Data.HashSet.Lemmas
Std.HashSet.get_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k a : α} {h' : a ∈ m.erase k}, (m.erase k).get a h' = m.get a ⋯
-- Init.Data.Int.Gcd
Int.gcd_dvd_left : ∀ (a b : ℤ), ↑(a.gcd b) ∣ a
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.zero_term : ∀ {α : Type u_1} [inst : AddCommMonoid α] (x a : α), Mathlib.Tactic.Abel.term 0 x a = a
-- Init.Data.BitVec.Lemmas
BitVec.signExtend_or : ∀ {w v : ℕ} {x y : BitVec w}, BitVec.signExtend v (x ||| y) = BitVec.signExtend v x ||| BitVec.signExtend v y
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mapIso_counitIso_hom_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S S' : D} {T : CategoryTheory.Functor C D} (i : S ≅ S')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S') T),
  ((CategoryTheory.StructuredArrow.mapIso i).counitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.Ref.content : {α : Sort u_1} → Lean.Doc.Ref✝ α → α
-- Mathlib.Topology.Algebra.UniformConvergence
instCommGroupUniformOnFun : {α : Type u_1} → {β : Type u_2} → {𝔖 : Set (Set α)} → [CommGroup β] → CommGroup (UniformOnFun α β 𝔖)
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
CategoryTheory.PreZeroHypercoverFamily.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {x y : CategoryTheory.PreZeroHypercoverFamily C},
  x = y ↔ x.property = y.property
-- Mathlib.Algebra.Ring.Subring.Basic
RingEquiv.coe_subringCongr_apply : ∀ {R : Type u} [inst : NonAssocRing R] {s t : Subring R} (h : s = t) (x : ↥s), ↑((RingEquiv.subringCongr h) x) = ↑x
-- Lean.Meta.Eqns
/-- Returns equation theorems for the given declaration.
 -/
Lean.Meta.getEqnsFor? : Lean.Name → Lean.MetaM (Option (Array Lean.Name))
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y)
  [inst_2 : K.HasPullbacks], P f ↔ ∀ (i : 𝒰.I₀), P (CategoryTheory.Limits.pullback.snd f (𝒰.f i))
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
CategoryTheory.Idempotents.app_comp_p_assoc : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C]
  {P Q : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C)} (f : P ⟶ Q) (X : J) {Z : C}
  (h : Q.X.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f.f.app X) (CategoryTheory.CategoryStruct.comp (Q.p.app X) h) =
    CategoryTheory.CategoryStruct.comp (f.f.app X) h
-- Mathlib.Tactic.CategoryTheory.Reassoc
/-- An option to tag the lemma generated by `@[reassoc]` with `to_dual none`.  -/
Mathlib.Tactic.Reassoc.toDualOpt : Lean.ParserDescr
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
Algebra.GrothendieckAddGroup.eq_1 : ∀ (M : Type u_1) [inst : AddCommMonoid M], Algebra.GrothendieckAddGroup M = AddLocalization ⊤
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.instBEqSimprocEntry : BEq Lean.Meta.Simp.SimprocEntry
-- Std.Tactic.Do.Syntax
/-- `mclear` is like `clear`, but operating on a stateful `Std.Do.SPred` goal.
```lean
example (P Q : SPred σs) : P ⊢ₛ Q → Q := by
  mintro HP
  mintro HQ
  mclear HP
  mexact HQ
```
 -/
Lean.Parser.Tactic.mclear : Lean.ParserDescr
-- Init.Data.UInt.Lemmas
UInt8.ofFin_mul : ∀ (a b : Fin UInt8.size), UInt8.ofFin (a * b) = UInt8.ofFin a * UInt8.ofFin b
-- Init.Data.SInt.Basic
Int64.ofUInt64.sizeOf_spec : ∀ (toUInt64 : UInt64), sizeOf { toUInt64 := toUInt64 } = 1 + sizeOf toUInt64
-- Mathlib.Algebra.Category.FGModuleCat.Limits
FGModuleCat.instHasFiniteLimits : ∀ {k : Type u} [inst : Ring k] [IsNoetherianRing k], CategoryTheory.Limits.HasFiniteLimits (FGModuleCat k)
-- Mathlib.Topology.Spectral.Prespectral
PrespectralSpace.isBasis_opens : ∀ (X : Type u_1) [inst : TopologicalSpace X] [PrespectralSpace X], TopologicalSpace.Opens.IsBasis {U | IsCompact ↑U}
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_neg : ∀ {a : UInt8}, (-a).toBitVec = -a.toBitVec
-- Mathlib.Data.Set.Lattice
Set.biInter_const : ∀ {α : Type u_1} {β : Type u_2} {s : Set α}, s.Nonempty → ∀ (t : Set β), ⋂ a ∈ s, t = t
-- Init.Data.BitVec.Bitblast
/-- The denominator is positive.  -/
BitVec.DivModState.Lawful.hdPos : ∀ {w : ℕ} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w}, BitVec.DivModState.Lawful args qr → 0 < args.d
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functorObjObj_comon_comul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (A : CategoryTheory.Functor C D) [inst_3 : CategoryTheory.ComonObj A]
  (X : C), CategoryTheory.ComonObj.comul = CategoryTheory.ComonObj.comul.app X
-- Mathlib.LinearAlgebra.Multilinear.TensorProduct
/-- Given two multilinear maps `(ι₁ → N) → N₁` and `(ι₂ → N) → N₂`, this produces the map
`(ι₁ ⊕ ι₂ → N) → N₁ ⊗ N₂` by taking the coproduct of the domain and the tensor product
of the codomain.

This can be thought of as combining `Equiv.sumArrowEquivProdArrow.symm` with
`TensorProduct.map`, noting that the two operations can't be separated as the intermediate result
is not a `MultilinearMap`.

While this can be generalized to work for dependent `Π i : ι₁, N'₁ i` instead of `ι₁ → N`, doing so
introduces `Sum.elim N'₁ N'₂` types in the result which are difficult to work with and not defeq
to the simple case defined here. See
[this zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/Instances.20on.20.60sum.2Eelim.20A.20B.20i.60/near/218484619).
 -/
MultilinearMap.domCoprod : {R : Type u_1} →
  {ι₁ : Type u_2} →
    {ι₂ : Type u_3} →
      [inst : CommSemiring R] →
        {N₁ : Type u_6} →
          [inst_1 : AddCommMonoid N₁] →
            [inst_2 : Module R N₁] →
              {N₂ : Type u_7} →
                [inst_3 : AddCommMonoid N₂] →
                  [inst_4 : Module R N₂] →
                    {N : Type u_8} →
                      [inst_5 : AddCommMonoid N] →
                        [inst_6 : Module R N] →
                          MultilinearMap R (fun x => N) N₁ →
                            MultilinearMap R (fun x => N) N₂ → MultilinearMap R (fun x => N) (TensorProduct R N₁ N₂)
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atBot_pow : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedMonoid M] {l : Filter α}
  {f : α → M}, Filter.Tendsto f l Filter.atBot → ∀ {n : ℕ}, 0 < n → Filter.Tendsto (fun x => f x ^ n) l Filter.atBot
-- Init.Data.String.Lemmas.FindPos
String.Slice.posLE.induct_unfolding : ∀ (s : String.Slice) (motive : String.Pos.Raw → s.Pos → Prop),
  (∀ (x : String.Pos.Raw) (h : String.Pos.Raw.IsValidForSlice s x), motive x (s.pos x h)) →
    (∀ (x : String.Pos.Raw),
        ¬String.Pos.Raw.IsValidForSlice s x → x ≠ 0 → motive x.dec (s.posLE x.dec) → motive x (s.posLE x.dec)) →
      ∀ (offset : String.Pos.Raw), motive offset (s.posLE offset)
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.zeroth_contAux_eq_one_zero : ∀ {K : Type u_1} {g : GenContFract K} [inst : DivisionRing K], g.contsAux 0 = { a := 1, b := 0 }
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_eq_false_iff_exists_contains_eq_true : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → (m.isEmpty = false ↔ ∃ a, m.contains a = true)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- The second right fraction.  -/
CategoryTheory.MorphismProperty.RightFraction₂.snd : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → W.RightFraction₂ X Y → W.RightFraction X Y
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.instHasZeroMorphisms : CategoryTheory.Limits.HasZeroMorphisms SemiNormedGrp₁
-- Mathlib.RingTheory.Coalgebra.Basic
Finsupp.comul_comp_lsingle : ∀ (R : Type u) (ι : Type v) (A : Type w) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A] (i : ι),
  CoalgebraStruct.comul ∘ₗ Finsupp.lsingle i =
    TensorProduct.map (Finsupp.lsingle i) (Finsupp.lsingle i) ∘ₗ CoalgebraStruct.comul
-- Mathlib.Computability.Primrec.Basic
Primrec.option_iget : ∀ {α : Type u_1} [inst : Primcodable α] [inst_1 : Inhabited α], Primrec Option.iget
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.Hom.mk.hcongr_11 : ∀ (C C' : Type u_1),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v_1, u_1} C) (inst' : CategoryTheory.Category.{v_1, u_1} C'),
      inst ≍ inst' →
        ∀ (Wₗ : CategoryTheory.MorphismProperty C) (Wₗ' : CategoryTheory.MorphismProperty C'),
          Wₗ ≍ Wₗ' →
            ∀ (Wᵣ : CategoryTheory.MorphismProperty C) (Wᵣ' : CategoryTheory.MorphismProperty C'),
              Wᵣ ≍ Wᵣ' →
                ∀ (c : C) (c' : C'),
                  c ≍ c' →
                    ∀ (c'_1 : C) (c'' : C'),
                      c'_1 ≍ c'' →
                        ∀ (S₁ : CategoryTheory.Span Wₗ Wᵣ c c'_1) (S₁' : CategoryTheory.Span Wₗ' Wᵣ' c' c''),
                          S₁ ≍ S₁' →
                            ∀ (S₂ : CategoryTheory.Span Wₗ Wᵣ c c'_1) (S₂' : CategoryTheory.Span Wₗ' Wᵣ' c' c''),
                              S₂ ≍ S₂' →
                                ∀ (hom : S₁.apex ⟶ S₂.apex) (hom' : S₁'.apex ⟶ S₂'.apex),
                                  hom ≍ hom' →
                                    ∀ (hom_l : CategoryTheory.CategoryStruct.comp hom S₂.l = S₁.l)
                                      (hom_l' : CategoryTheory.CategoryStruct.comp hom' S₂'.l = S₁'.l),
                                      hom_l ≍ hom_l' →
                                        ∀ (hom_r : CategoryTheory.CategoryStruct.comp hom S₂.r = S₁.r)
                                          (hom_r' : CategoryTheory.CategoryStruct.comp hom' S₂'.r = S₁'.r),
                                          hom_r ≍ hom_r' →
                                            { hom := hom, hom_l := hom_l, hom_r := hom_r } ≍
                                              { hom := hom', hom_l := hom_l', hom_r := hom_r' }
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.ext : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
  [inst_3 : MulZeroOneClass β] {f g : α →*₀o β}, (∀ (a : α), f a = g a) → f = g
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasEqualizers C]
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasImage f] {Y' : C} (h : Y ⟶ Y') [inst_3 : CategoryTheory.IsIso h]
  {Z : C} (h_1 : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f h).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp f h)).arrow
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv h) h_1)
-- Mathlib.Order.RelClasses
/-- A bounded or final set. Not to be confused with `Bornology.IsBounded`.  -/
Set.Bounded : {α : Type u} → (α → α → Prop) → Set α → Prop
-- Lean.Meta.Tactic.Grind.MatchCond
/-- Propagates `MatchCond` downwards  -/
Lean.Meta.Grind.propagateMatchCondDown : Lean.Meta.Grind.Propagator
-- Mathlib.Data.Fintype.Fin
Fin.card_filter_univ_succ : ∀ {n : ℕ} (p : Fin (n + 1) → Prop) [inst : DecidablePred p],
  {x | p x}.card = if p 0 then {x | p x.succ}.card + 1 else {x | p x.succ}.card
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.equiv_refl : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M), b.equiv b (Equiv.refl ι) = LinearEquiv.refl R M
-- Lean.Elab.Import
Lean.Elab.checkModuleNamePortability : Lean.Name → Lean.Parser.InputContext → String.Pos.Raw → Lean.MessageLog → Lean.MessageLog
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.coe_def : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} (J : hI.SubDPIdeal), ↑J = J.carrier
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.sheafPushforwardContinuousId_hom_app_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (A : Type u) [inst_1 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) (X : CategoryTheory.Sheaf J A) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Functor.sheafPushforwardContinuousId A J).hom.app X).hom.app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj.obj X_1)
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.semiring : {α : Type u_1} →
  [inst : Semiring α] →
    [inst_1 : PartialOrder α] → [ZeroLEOneClass α] → [AddLeftMono α] → [PosMulMono α] → Semiring { x // 0 ≤ x }
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.instHasOfPostcompPropertySchemeIsProperIsSeparated : CategoryTheory.MorphismProperty.HasOfPostcompProperty @AlgebraicGeometry.IsProper @AlgebraicGeometry.IsSeparated
-- Mathlib.Data.Finsupp.Multiset
Finsupp.toMultiset_toFinsupp : ∀ {α : Type u_1} [inst : DecidableEq α] (f : α →₀ ℕ), Multiset.toFinsupp (Finsupp.toMultiset f) = f
-- Mathlib.Algebra.Group.Action.Defs
VAddCommClass.op_right : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} [inst : VAdd M α] [inst_1 : VAdd N α] [inst_2 : VAdd Nᵃᵒᵖ α]
  [IsCentralVAdd N α] [VAddCommClass M N α], VAddCommClass M Nᵃᵒᵖ α
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
/-- **Turán's theorem**. `turanGraph n r` is, up to isomorphism, the unique
`r + 1`-cliquefree Turán-maximal graph on `n` vertices.  -/
SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {r : ℕ},
  0 < r → (G.IsTuranMaximal r ↔ Nonempty (G ≃g SimpleGraph.turanGraph (Fintype.card V) r))
-- Mathlib.RingTheory.Artinian.Module
/-- This is the Fitting decomposition of the module `M` with respect to the endomorphism `f`.

See also `LinearMap.isCompl_iSup_ker_pow_iInf_range_pow` for an alternative spelling.  -/
LinearMap.eventually_isCompl_ker_pow_range_pow : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsArtinian R M]
  [IsNoetherian R M] (f : Module.End R M), ∀ᶠ (n : ℕ) in Filter.atTop, IsCompl (f ^ n).ker (f ^ n).range
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.builder? : Aesop.Frontend.RuleConfig → Option Aesop.Frontend.DBuilderName
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.coendFunctor_map : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] (C : Type u') [inst_1 : CategoryTheory.Category.{v', u'} C]
  [inst_2 : ∀ (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)), CategoryTheory.Limits.HasCoend F]
  {X Y : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} (f : X ⟶ Y),
  (CategoryTheory.Limits.coendFunctor J C).map f = CategoryTheory.Limits.coend.map f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constGetEntryGTD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : α × β},
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.getEntryGTD t₁ k fallback = Std.DTreeMap.Raw.Const.getEntryGTD t₂ k fallback
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiffWithinAt_pi : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {x : E} {n : WithTop ℕ∞} {ι : Type u_3} [inst_3 : Fintype ι]
  {F' : ι → Type u_5} [inst_4 : (i : ι) → NormedAddCommGroup (F' i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (F' i)]
  {Φ : E → (i : ι) → F' i}, ContDiffWithinAt 𝕜 n Φ s x ↔ ∀ (i : ι), ContDiffWithinAt 𝕜 n (fun x => Φ x i) s x
-- Mathlib.FieldTheory.Normal.Closure
normalClosure.algebra : (F : Type u_1) →
  (K : Type u_2) →
    (L : Type u_3) →
      [inst : Field F] →
        [inst_1 : Field K] →
          [inst_2 : Field L] →
            [inst_3 : Algebra F K] →
              [inst_4 : Algebra F L] →
                [inst_5 : Algebra K L] → [IsScalarTower F K L] → Algebra K ↥(IntermediateField.normalClosure F K L)
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- **Alias** of `linearIndependent_finSnoc`. -/
linearIndependent_fin_snoc : ∀ {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {x : V} {n : ℕ}
  {v : Fin n → V}, LinearIndependent K (Fin.snoc v x) ↔ LinearIndependent K v ∧ x ∉ Submodule.span K (Set.range v)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.MonadSetTermId : (Type → Type) → Type
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- The weight space representation of automorphisms  -/
RootPairing.Equiv.weightHom : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (P : RootPairing ι R M N) → P.Aut →* M ≃ₗ[R] M
-- Mathlib.Algebra.Homology.HomotopyCategory.KProjective
CochainComplex.isKProjective_iff_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K₁ K₂ : CochainComplex C ℤ} (e : K₁ ≅ K₂), K₁.IsKProjective ↔ K₂.IsKProjective
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.map_fromSpec : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {V : X.Opens}
  (hV : AlgebraicGeometry.IsAffineOpen V) (f : Opposite.op U ⟶ Opposite.op V),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (X.presheaf.map f)) hU.fromSpec = hV.fromSpec
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
/-- If a property on finitely generated modules over a Noetherian ring satisfies that:

- it holds for zero module (it's formalized as it holds for any module which is subsingleton),
- it holds for `A ⧸ p` for every prime ideal `p` of `A` (to avoid universe problem,
  it's formalized as it holds for any module isomorphic to `A ⧸ p`),
- it is stable by short exact sequences,

then the property holds for every finitely generated modules.

NOTE: This should be the induction principle for `M`, but due to the bug
https://github.com/leanprover/lean4/issues/4246
currently it is induction for `Module.Finite A M`.  -/
IsNoetherianRing.induction_on_isQuotientEquivQuotientPrime : ∀ (A : Type u) [inst : CommRing A] [IsNoetherianRing A] ⦃M : Type v⦄ [inst_2 : AddCommGroup M] [inst_3 : Module A M]
  (x : Module.Finite A M)
  {motive : (N : Type v) → [inst_4 : AddCommGroup N] → [inst_5 : Module A N] → [Module.Finite A N] → Prop},
  (∀ (N : Type v) [inst_4 : AddCommGroup N] [inst_5 : Module A N] [inst : Module.Finite A N] [Subsingleton N],
      motive N) →
    (∀ (N : Type v) [inst_4 : AddCommGroup N] [inst_5 : Module A N] [inst_6 : Module.Finite A N] (p : PrimeSpectrum A)
        (a : N ≃ₗ[A] A ⧸ p.asIdeal), motive N) →
      (∀ (N₁ : Type v) [inst_4 : AddCommGroup N₁] [inst_5 : Module A N₁] [inst_6 : Module.Finite A N₁] (N₂ : Type v)
          [inst_7 : AddCommGroup N₂] [inst_8 : Module A N₂] [inst_9 : Module.Finite A N₂] (N₃ : Type v)
          [inst_10 : AddCommGroup N₃] [inst_11 : Module A N₃] [inst_12 : Module.Finite A N₃] (f : N₁ →ₗ[A] N₂)
          (g : N₂ →ₗ[A] N₃),
          Function.Injective ⇑f → Function.Surjective ⇑g → Function.Exact ⇑f ⇑g → motive N₁ → motive N₃ → motive N₂) →
        motive M