mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addETransformLeft_snd : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddGroup α] (e : α) (x : Finset α × Finset α),
  (Finset.addETransformLeft e x).2 = x.2 ∪ (-e +ᵥ x.2)
-- Mathlib.FieldTheory.CardinalEmb
_private.Mathlib.FieldTheory.CardinalEmb.0.Field.Emb.Cardinal.«termE⟮<_⟯_1» : Lean.ParserDescr
-- Lean.Parser.Term
Lean.Parser.Term.noindex.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Vector.Find
Vector.findSome?_eq_none_iff : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → Option β} {xs : Vector α n},
  Vector.findSome? f xs = none ↔ ∀ x ∈ xs, f x = none
-- Mathlib.Order.CompleteLattice.Defs
Equiv.supSet_def : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) [inst : SupSet β] (s : Set α), sSup s = e.symm (⨆ a ∈ s, e a)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.XClass.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Affine R) (x : R),
  WeierstrassCurve.Affine.CoordinateRing.XClass W' x =
    (WeierstrassCurve.Affine.CoordinateRing.mk W') (Polynomial.C (Polynomial.X - Polynomial.C x))
-- Init.Data.Rat.Basic
Rat.instNatCast : NatCast ℚ
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Real.measurable_arcsin : Measurable Real.arcsin
-- Batteries.Data.List.Interleave
List.interleave_ofFn_ofFn_odd : ∀ {α : Type u_1} {n : ℕ} {f : Fin (n + 1) → α} {g : Fin n → α},
  (List.ofFn f).interleave (List.ofFn g) = List.ofFn fun i => if hi : ↑i % 2 = 0 then f ⟨↑i / 2, ⋯⟩ else g ⟨↑i / 2, ⋯⟩
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the largest key in the tree map, panicking if the map is empty.
 -/
Std.TreeMap.Raw.maxKey! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.TreeMap.Raw α β cmp → α
-- Mathlib.Algebra.Divisibility.Basic
dvd_mul_of_dvd_left : ∀ {α : Type u_1} [inst : Semigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ b * c
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.union_insert_right_eq_insert_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {p : (a : α) × β a}, m₁ ∪ m₂.insert p.fst p.snd = (m₁ ∪ m₂).insert p.fst p.snd
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.IsClosedUnderBinaryCoproducts.closedUnderIsomorphisms : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [CategoryTheory.Limits.HasInitial C] [P.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete PEmpty.{1})]
  [P.IsClosedUnderBinaryCoproducts], P.IsClosedUnderIsomorphisms
-- Mathlib.Topology.Order.MonotoneConvergence
isGLB_of_tendsto_atTop : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder α] [OrderClosedTopology α]
  [inst_3 : Preorder β] [IsDirectedOrder β] [Nonempty β] {f : β → α} {a : α},
  Antitone f → Filter.Tendsto f Filter.atTop (nhds a) → IsGLB (Set.range f) a
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.mk.injEq : ∀ {α : Type u} {cmp : autoParam (α → α → Ordering) Std.ExtTreeSet._auto_1} (inner inner_1 : Std.ExtTreeMap α Unit cmp),
  ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.Data.List.Sigma
List.map_dlookup_eq_find : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (l : List (Sigma β)),
  Option.map (Sigma.mk a) (List.dlookup a l) = List.find? (fun s => decide (a = s.fst)) l
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.coe_coe : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N), ⇑e.toLieModuleHom = ⇑e
-- Mathlib.Algebra.Order.ToIntervalMod
self_sub_toIocMod : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), b - toIocMod hp a b = toIocDiv hp a b • p
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.inverse_comp_mapHomotopyCategory_snd : ∀ (X Y : SSet.Truncated 2),
  (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).comp
      (SSet.Truncated.mapHomotopyCategory (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)) =
    CategoryTheory.Prod.snd X.HomotopyCategory Y.HomotopyCategory
-- Mathlib.Algebra.Opposites
AddOpposite.unop_mul : ∀ {α : Type u_1} [inst : Mul α] (a b : αᵃᵒᵖ), AddOpposite.unop (a * b) = AddOpposite.unop a * AddOpposite.unop b
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt32.reduceAdd : Lean.Meta.Simp.DSimproc
-- Aesop.Forward.Match.Types
Aesop.instInhabitedForwardRuleMatch : Inhabited Aesop.ForwardRuleMatch
-- Init.Data.Option.Attach
_private.Init.Data.Option.Attach.0.Option.instDecidableEq.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (b : Option α) → (Unit → motive none) → ((val : α) → motive (some val)) → motive b
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp
GrpTypeEquivalenceGrp.grpGroup : (A : Type u) → [CategoryTheory.GrpObj A] → Group A
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp]
  (t t_1 : Std.DTreeMap.Raw α β cmp),
  t = t_1 → ∀ (a : α) (fallback fallback_1 : β a), fallback = fallback_1 → t.getD a fallback = t_1.getD a fallback_1
-- Mathlib.Order.Disjoint
IsCompl.inf_eq_bot : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] {x y : α}, IsCompl x y → x ⊓ y = ⊥
-- Mathlib.CategoryTheory.Adjunction.Additive
CategoryTheory.Adjunction.homAddEquiv_symm_apply : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D] {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (adj : F ⊣ G) [inst_4 : F.Additive] (X : C) (Y : D) (f : X ⟶ G.obj Y),
  (adj.homAddEquiv X Y).symm f = (adj.homEquiv X Y).symm f
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsRestriction.isStrictRestriction_of_ground_ne : ∀ {α : Type u_1} {M N : Matroid α}, N.IsRestriction M → N.E ≠ M.E → N.IsStrictRestriction M
-- Mathlib.Order.Filter.AtTopBot.Monoid
Filter.Tendsto.atBot_of_const_le_add : ∀ {α : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelAddMonoid M]
  {l : Filter α} {f g : α → M},
  (∃ C, ∀ (x : α), C ≤ f x) → Filter.Tendsto (fun x => f x + g x) l Filter.atBot → Filter.Tendsto g l Filter.atBot
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.IsMultiplicative.map_div_of_coprime : ∀ {R : Type u_1} [inst : GroupWithZero R] {f : ArithmeticFunction R},
  f.IsMultiplicative → ∀ {l d : ℕ}, d ∣ l → (l / d).Coprime d → f d ≠ 0 → f (l / d) = f l / f d
-- Batteries.Data.BinomialHeap.Lemmas
_private.Batteries.Data.BinomialHeap.Lemmas.0.Batteries.BinomialHeap.Imp.Heap.realSize.match_1.splitter : {α : Type u_1} →
  (motive : Batteries.BinomialHeap.Imp.Heap α → Sort u_2) →
    (x : Batteries.BinomialHeap.Imp.Heap α) →
      (Unit → motive Batteries.BinomialHeap.Imp.Heap.nil) →
        ((rank : ℕ) →
            (val : α) →
              (c : Batteries.BinomialHeap.Imp.HeapNode α) →
                (s : Batteries.BinomialHeap.Imp.Heap α) → motive (Batteries.BinomialHeap.Imp.Heap.cons rank val c s)) →
          motive x
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Hom.ext : ∀ {R : Type u} {S : Type v} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S} {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} {inst_3 : CommRing R'} {inst_4 : CommRing S'} {inst_5 : Algebra R' S'}
  {P' : Algebra.Extension R' S'} {inst_6 : Algebra R R'} {inst_7 : Algebra S S'} {x y : P.Hom P'},
  x.toRingHom = y.toRingHom → x = y
-- Mathlib.SetTheory.Lists
Lists.instSizeOf : {α : Type u_1} → [SizeOf α] → SizeOf (Lists α)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.single_le_prod' : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] {f : ι → N} {s : Finset ι} [MulLeftMono N],
  (∀ i ∈ s, 1 ≤ f i) → ∀ {a : ι}, a ∈ s → f a ≤ ∏ x ∈ s, f x
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.pderiv_inl_universalFactorizationMap_X : ∀ (R : Type u_1) [inst : CommRing R] (n m k : ℕ) (hn : n = m + k) (i : Fin m) (j : Fin n),
  (MvPolynomial.pderiv (Sum.inl i))
      ((MvPolynomial.tensorEquivSum R (Fin m) (Fin k) R)
        ((MvPolynomial.universalFactorizationMap R n m k hn) (MvPolynomial.X j))) =
    if ↑j < ↑i then 0
    else if h : ↑j - ↑i < k then MvPolynomial.X (Sum.inr ⟨↑j - ↑i, h⟩) else if ↑j - ↑i = k then 1 else 0
-- Init.Data.Nat.Lemmas
Nat.instAssociativeMin : Std.Associative min
-- Init.Data.SInt.Basic
Int16.ofUInt16.sizeOf_spec : ∀ (toUInt16 : UInt16), sizeOf { toUInt16 := toUInt16 } = 1 + sizeOf toUInt16
-- Std.Http.Server.Config
/-- The maximum size that the connection can receive in a single recv call.
 -/
Std.Http.Config.maximumRecvSize : Std.Http.Config → ℕ
-- Mathlib.Topology.Order.DenselyOrdered
/-- **Alias** of `nhdsLT_neBot_of_exists_lt`. -/
nhdsWithin_Iio_self_neBot' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {b : α},
  (∃ a, a < b) → (nhdsWithin b (Set.Iio b)).NeBot
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.root_coroot'_eq_pairing : ∀ {ι : 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) (i j : ι),
  (P.coroot' i) (P.root j) = P.pairing j i
-- Mathlib.CategoryTheory.Action.Limits
/-- `F : C ⥤ SingleObj G ⥤ V` preserves the limit of some `K : J ⥤ C` if it does
evaluated at `SingleObj.star G`.  -/
_private.Mathlib.CategoryTheory.Action.Limits.0.Action.SingleObj.preservesLimit : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} C]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor (CategoryTheory.SingleObj G) V)) {J : Type u_4}
  [inst_3 : CategoryTheory.Category.{v_3, u_4} J] (K : CategoryTheory.Functor J C),
  CategoryTheory.Limits.PreservesLimit K
      (F.comp ((CategoryTheory.evaluation (CategoryTheory.SingleObj G) V).obj (CategoryTheory.SingleObj.star G))) →
    CategoryTheory.Limits.PreservesLimit K F
-- Mathlib.Order.Std
/-- = is decidable. This can always be automatically derived from `decidableLE`.  -/
LinearOrder.OfStdArgs.decidableEq : {α : Type u_1} →
  (self : LinearOrder.OfStdArgs α) →
    let this := self.toPartialOrderArgs;
    let this := self.decidableLE;
    DecidableEq α
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.unopFunctor_map : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : Bᵒᵖ) {X Y : a ⟶ b} (η : X ⟶ Y),
  (Bicategory.Opposite.unopFunctor a b).map η = η.unop2
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_sum : ∀ {R : Type u} {ι : Type y} [inst : Semiring R] (k : ℕ) (s : Finset ι) (f : ι → Polynomial R),
  (⇑Polynomial.derivative)^[k] (∑ b ∈ s, f b) = ∑ b ∈ s, (⇑Polynomial.derivative)^[k] (f b)
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.commShiftIso_unopUnop_hom_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖᵒᵖ)
  (n m : ℤ) (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.commShiftIso_unopUnop_hom_app._auto_1) {Z : C}
  (h : (CategoryTheory.shiftFunctor C n).obj ((CategoryTheory.unopUnop C).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso (CategoryTheory.unopUnop C) n).hom.app X) h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso Cᵒᵖ n m hnm).hom.app X).unop.unop
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).inv.app (Opposite.unop X)).unop h)
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Multipliable.one_lt_tprod : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommGroup α] [inst_1 : PartialOrder α]
  [IsOrderedMonoid α] [inst_3 : TopologicalSpace α] [IsTopologicalGroup α] [OrderClosedTopology α] {g : ι → α}
  [L.LeAtTop] [L.NeBot], Multipliable g L → (∀ (i : ι), 1 ≤ g i) → ∀ (i : ι), 1 < g i → 1 < ∏'[L] (i : ι), g i
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
/-- If `B` is a faithfully flat `A`-algebra, the preimage of the pushforward of any
ideal `I` is again `I`.  -/
Ideal.comap_map_eq_self_of_faithfullyFlat : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [Module.FaithfullyFlat A B] (I : Ideal A), Ideal.comap (algebraMap A B) (Ideal.map (algebraMap A B) I) = I
-- Mathlib.Combinatorics.SetFamily.Compression.UV
_private.Mathlib.Combinatorics.SetFamily.Compression.UV.0.UV.aux : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {u v : Finset α},
  (∀ x ∈ u, ∃ y ∈ v, UV.IsCompressed (u.erase x) (v.erase y) 𝒜) → v = ∅ → u = ∅
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- `t` is in the shadow of `𝒜` iff there is a `s ∈ 𝒜` from which we can remove one element to
get `t`.  -/
Finset.mem_shadow_iff : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} {t : Finset α},
  t ∈ 𝒜.shadow ↔ ∃ s ∈ 𝒜, ∃ a ∈ s, s.erase a = t
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- A split equalizer diagram consists of morphisms

```
      ι   f
    W → X ⇉ Y
          g
```

satisfying `ι ≫ f = ι ≫ g` together with morphisms

```
      r   t
    W ← X ← Y
```

satisfying `ι ≫ r = 𝟙 W`, `g ≫ t = 𝟙 X` and `f ≫ t = r ≫ ι`.

The name "equalizer" is appropriate, since any split equalizer is an equalizer, see
`CategoryTheory.IsSplitEqualizer.isEqualizer`.
Split equalizers are also absolute, since a functor preserves all the structure above.
 -/
CategoryTheory.IsSplitEqualizer : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (X ⟶ Y) → (X ⟶ Y) → {W : C} → (W ⟶ X) → Type v
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveCodiscrete
CategoryTheory.Codiscrete.equivFun_apply : ∀ {X : Type u} {n : ℕ} (f : (CategoryTheory.nerve (CategoryTheory.Codiscrete X)).obj (Opposite.op { len := n }))
  (k : Fin (n + 1)), CategoryTheory.Codiscrete.equivFun f k = (f.obj k).as
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.seq : Lean.Syntax → Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.Code
-- Mathlib.CategoryTheory.EqToHom
/-- If `T ≃ D` is a bijection and `D` is a category, then
`InducedCategory D e` is equivalent to `D`.  -/
CategoryTheory.Equivalence.induced : {D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] → {T : Type u_2} → (e : T ≃ D) → CategoryTheory.InducedCategory D ⇑e ≌ D
-- Mathlib.Combinatorics.Quiver.Path.Vertices
/-- The head of the vertices list is the start vertex.  -/
Quiver.Path.vertices_head_eq : ∀ {V : Type u_1} [inst : Quiver V] {a b : V} (p : Quiver.Path a b) (h : optParam (p.vertices ≠ []) ⋯),
  p.vertices.head h = a
-- Mathlib.Data.EReal.Inv
EReal.mul_div_right : ∀ (a b c : EReal), a / b * c = a * c / b
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.thm : Lean.ParserDescr
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.instCategoryStructuredArrow : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : D} →
          {T : CategoryTheory.Functor C D} →
            CategoryTheory.Category.{v₁, max u₁ v₂} (CategoryTheory.StructuredArrow S T)
-- Mathlib.Data.Set.Lattice
/-- `sUnion` is monotone under taking a superset of each set.  -/
Set.sUnion_mono_supsets : ∀ {α : Type u_1} {s : Set (Set α)} {f : Set α → Set α}, (∀ (t : Set α), f t ⊆ t) → ⋃₀ (f '' s) ⊆ ⋃₀ s
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- For any monomorphism `U ⟶ X`, there is an associated characteristic map `X ⟶ Ω`.  -/
CategoryTheory.Subobject.Classifier.χ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (self : CategoryTheory.Subobject.Classifier C) → {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ self.Ω
-- Mathlib.Data.Seq.Computation
Computation.eq_of_bisim : ∀ {α : Type u} (R : Computation α → Computation α → Prop),
  Computation.IsBisimulation R → ∀ {s₁ s₂ : Computation α}, R s₁ s₂ → s₁ = s₂
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- Reformulate in the `StructureGroupoid` namespace the compatibility condition of charts in a
charted space admitting a structure groupoid, to make it more easily accessible with dot
notation.  -/
StructureGroupoid.compatible : ∀ {H : Type u_5} [inst : TopologicalSpace H] (G : StructureGroupoid H) {M : Type u_6} [inst_1 : TopologicalSpace M]
  [inst_2 : ChartedSpace H M] [HasGroupoid M G] {e e' : OpenPartialHomeomorph M H},
  e ∈ atlas H M → e' ∈ atlas H M → e.symm.trans e' ∈ G
-- Mathlib.Tactic.Linter.MinImports
/-- The `minImports` linter incrementally computes the minimal imports needed for each file to build.
Whenever it detects that a new command requires an increase in the (transitive) imports that it
computed so far, it emits a warning mentioning the bigger minimal imports.

Unlike the related `#min_imports` command, the linter takes into account notation and tactic
information.
It also works incrementally, providing information that is better suited, for instance, to split
files.

Another important difference is that the `minImports` *linter* starts counting imports from
where the option is set to `true` *downwards*, whereas the `#min_imports` *command* looks at the
imports needed from the command *upwards*.
 -/
Mathlib.Linter.linter.minImports : Lean.Option Bool
-- Init.Data.List.Basic
List.lookup_cons : ∀ {α : Type u} {β : Type u_1} {b : β} {as : List (α × β)} {a : α} [inst : BEq α] {k : α},
  List.lookup a ((k, b) :: as) =
    match a == k with
    | true => some b
    | false => List.lookup a as
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.idealQuotientMk : ∀ {R : Type u_6} [inst : CommRing R] {I : Ideal R} {x y : R},
  x ≡ y [SMOD I] ↔ (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
-- Mathlib.Tactic.Positivity.Finset
/-- Extension for `Finset.card`. `#s` is positive if `s` is nonempty.

It calls `Mathlib.Meta.proveFinsetNonempty` to attempt proving that the finset is nonempty.  -/
Mathlib.Meta.Positivity.evalFinsetCard : Mathlib.Meta.Positivity.PositivityExt
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.Equiv.of_keys_perm : ∀ {α : Type u} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => Unit}, t₁.keys.Perm t₂.keys → t₁.Equiv t₂
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.injective_πs' : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o₁ o₂ : Ordinal.{u}}
  (h : o₁ ≤ o₂), Function.Injective ⇑(Profinite.NobelingProof.πs' C h)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticForm.discr'_comp : ∀ {R : Type u_3} {n : Type w} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [inst_3 : Invertible 2]
  {Q : QuadraticForm R (n → R)} (f : (n → R) →ₗ[R] n → R),
  QuadraticForm.discr' (QuadraticMap.comp Q f) = (LinearMap.toMatrix' f).det * (LinearMap.toMatrix' f).det * Q.discr'
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
isLUB_neg : ∀ {G : Type u_2} [inst : AddGroup G] [inst_1 : Preorder G] [AddLeftMono G] [AddRightMono G] {s : Set G} {a : G},
  IsLUB (-s) a ↔ IsGLB s (-a)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.mul_assoc_flip : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.MonObj M],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M CategoryTheory.MonObj.mul)
      CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M M).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul M) CategoryTheory.MonObj.mul)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.notMem_neighborFinset_self : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)], v ∉ G.neighborFinset v
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.instRing : {R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : Ring A] →
          [inst_2 : Algebra R A] → [inst_3 : Semiring B] → [inst_4 : Algebra R B] → Ring (TensorProduct R A B)
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
algebraicIndependent_adjoin : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  AlgebraicIndependent R x → AlgebraicIndependent R fun i => ⟨x i, ⋯⟩
-- Init.Data.List.Zip
List.getElem?_zip_eq_some : ∀ {α : Type u_1} {β : Type u_2} {l₁ : List α} {l₂ : List β} {z : α × β} {i : ℕ},
  (l₁.zip l₂)[i]? = some z ↔ l₁[i]? = some z.1 ∧ l₂[i]? = some z.2
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.instNormHom : {V W : SemiNormedGrp} → Norm (V ⟶ W)
-- Mathlib.Order.Preorder.Chain
IsChain.image_iso : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} [inst : LE α] [inst_1 : LE β],
  IsChain (fun x1 x2 => x1 ≤ x2) s → ∀ (φ : α ≃o β), IsChain (fun x1 x2 => x1 ≤ x2) (⇑φ '' s)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.basicOpen_eq_iSup_proj : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A),
  AlgebraicGeometry.Proj.basicOpen 𝒜 f = ⨆ i, AlgebraicGeometry.Proj.basicOpen 𝒜 ((GradedRing.proj 𝒜 i) f)
-- Mathlib.AlgebraicGeometry.Sites.MorphismProperty
AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme)
  [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P] [P.IsStableUnderBaseChange],
  (AlgebraicGeometry.Scheme.precoverage P).IsStableUnderBaseChange
-- Mathlib.Data.Nat.BitIndices
/-- **Alias** of `Nat.bitIndices_sum_map_two_pow`.

---

Together with `Nat.sum_map_bitIndices_two_pow`, this implies a bijection between `ℕ` and `Finset ℕ`.
See `Finset.equivBitIndices` for this bijection.
 -/
Nat.bitIndices_twoPowsum : ∀ {L : List ℕ}, L.SortedLT → (List.map (fun i => 2 ^ i) L).sum.bitIndices = L
-- Lean.Data.Position
Lean.instFromJsonPosition.fromJson : Lean.Json → Except String Lean.Position
-- Mathlib.RepresentationTheory.Basic
/-- Given a representation `(V, ρ)` of a finite group `G`, `norm ρ` is the linear map `V →ₗ[k] V`
defined by `x ↦ ∑ ρ g x` for `g` in `G`.  -/
Representation.norm : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : Semiring k] →
        [inst_1 : Group G] →
          [Fintype G] → [inst_3 : AddCommMonoid V] → [inst_4 : Module k V] → Representation k G V → Module.End k V