mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_iff_injective_fintypeLinearCombination : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Fintype ι],
  LinearIndependent R v ↔ Function.Injective ⇑(Fintype.linearCombination R v)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
/-- This is the version one probably wants, which is why the pi's are there.  -/
pi_mul_cot_pi_q_exp : ∀ (z : UpperHalfPlane),
  ↑Real.pi * (↑Real.pi * ↑z).cot =
    ↑Real.pi * Complex.I - 2 * ↑Real.pi * Complex.I * ∑' (n : ℕ), Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ n
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.mapsTo_ofDigits : ∀ {b : ℕ}, 1 < b → ∀ (l : ℕ), Set.MapsTo (Nat.ofDigits b) {L | L.length = l ∧ ∀ x ∈ L, x < b} {n | n < b ^ l}
-- Mathlib.GroupTheory.HNNExtension
instGroupHNNExtension : {G : Type u_1} → [inst : Group G] → {A B : Subgroup G} → {φ : ↥A ≃* ↥B} → Group (HNNExtension G A B φ)
-- Init.Data.List.Perm
List.Perm.subset : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Perm l₂ → l₁ ⊆ l₂
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.fac_pull_assoc : ∀ {Δ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) {Δ' : SimplexCategoryᵒᵖ}
  (θ : Δ ⟶ Δ') {Z : SimplexCategory} (h : Opposite.unop A.fst ⟶ Z),
  CategoryTheory.CategoryStruct.comp (A.pull θ).e
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp θ.unop A.e)) h) =
    CategoryTheory.CategoryStruct.comp θ.unop (CategoryTheory.CategoryStruct.comp A.e h)
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.coord_reindex : ∀ {ι : Type u_1} {ι' : Type u_2} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V]
  [inst_1 : AddTorsor V P] [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) (e : ι ≃ ι') (i : ι'),
  (b.reindex e).coord i = b.coord (e.symm i)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ ∩ m₂).getKey? k = none
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) (s : Set α)
  (a b : α),
  variationOnFromTo f s a b =
    if a ≤ b then (eVariationOn f (s ∩ Set.Icc a b)).toReal else -(eVariationOn f (s ∩ Set.Icc b a)).toReal
-- Lean.Elab.Tactic.Conv.Pattern
/-- Is this pattern interested in accepting the next match?  -/
Lean.Elab.Tactic.Conv.PatternMatchState.isReady : Lean.Elab.Tactic.Conv.PatternMatchState → Bool
-- Mathlib.Algebra.Polynomial.Derivative
/-- `derivative p` is the formal derivative of the polynomial `p`  -/
Polynomial.derivative : {R : Type u} → [inst : Semiring R] → Polynomial R →ₗ[R] Polynomial R
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE_X₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceCyclesE._auto_3),
  (X.cokernelSequenceCyclesE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).X₂ = X.cycles f₁ f₂ n₁
-- Mathlib.Lean.Meta.CongrTheorems
Lean.Meta.instFastSubsingletonOfFastIsEmpty : ∀ {α : Type u} [inst : Lean.Meta.FastIsEmpty α], Lean.Meta.FastSubsingleton α
-- Mathlib.Algebra.Order.Group.Unbundled.Int
Int.abs_natCast : ∀ (n : ℕ), |↑n| = ↑n
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- See also `Finset.prod_dite_eq'`.  -/
Fintype.prod_dite_eq' : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i : ι)
  (f : (j : ι) → j = i → M), (∏ j, if h : j = i then f j h else 1) = f i ⋯
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.restrictAdjunction_unit_app_app : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules)
  (U : Y.Opens),
  AlgebraicGeometry.Scheme.Modules.Hom.app ((AlgebraicGeometry.Scheme.Modules.restrictAdjunction f).unit.app M) U =
    M.presheaf.map (CategoryTheory.homOfLE ⋯).op
-- Mathlib.Logic.Equiv.Sum
/-- Four-way commutativity of `sum`. The name matches `add_add_add_comm`.  -/
Equiv.sumSumSumComm : (α : Type u_9) → (β : Type u_10) → (γ : Type u_11) → (δ : Type u_12) → (α ⊕ β) ⊕ γ ⊕ δ ≃ (α ⊕ γ) ⊕ β ⊕ δ
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.getCast!_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : Std.DHashMap.Internal.AssocList α β} {a : α}
  [inst_2 : Inhabited (β a)], Std.DHashMap.Internal.AssocList.getCast! a l = Std.Internal.List.getValueCast! a l.toList
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rcc.toArray_iter_eq_toArray : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_4 : Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rcc α}, r.iter.toArray = r.toArray
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
/-- **Alias** of `ModelWithCorners.contMDiffOn_symm`. -/
contMDiffOn_model_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) {n : WithTop ℕ∞},
  ContMDiffOn (modelWithCornersSelf 𝕜 E) I n (↑I.symm) (Set.range ↑I)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.addSemigroup : {R : Type u} → {M : Type v} → [AddSemigroup R] → [AddSemigroup M] → AddSemigroup (TrivSqZeroExt R M)
-- Mathlib.Analysis.InnerProductSpace.l2Space
OrthonormalBasis.coe_toHilbertBasis : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] [inst_4 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E),
  ⇑b.toHilbertBasis = ⇑b
-- Mathlib.RingTheory.WittVector.IsPoly
/-- Addition of Witt vectors is a polynomial function.  -/
WittVector.addIsPoly₂ : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)], WittVector.IsPoly₂ p fun x x_1 x1 x2 => x1 + x2
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_insertNth : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (i : Fin (n + 1)) (x : M) (p : Fin n → M),
  ∑ j, i.insertNth x p j = x + ∑ j, p j
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.toOneHypercover_toPreOneHypercover : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} [inst_2 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] {X : C}
  (data : F.OneHypercoverDenseData J₀ J X), data.toOneHypercover.toPreOneHypercover = data.toPreOneHypercover
-- Mathlib.Tactic.NormNum.Core
Mathlib.Meta.NormNum.NormNumExt.mk.injEq : ∀ (pre post : Bool)
  (eval : {u : Lean.Level} → {α : Q(Type u)} → (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.NormNum.Result e))
  (name : autoParam Lean.Name Mathlib.Meta.NormNum.NormNumExt.name._autoParam) (pre_1 post_1 : Bool)
  (eval_1 : {u : Lean.Level} → {α : Q(Type u)} → (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.NormNum.Result e))
  (name_1 : autoParam Lean.Name Mathlib.Meta.NormNum.NormNumExt.name._autoParam),
  ({ pre := pre, post := post, eval := eval, name := name } =
      { pre := pre_1, post := post_1, eval := eval_1, name := name_1 }) =
    (pre = pre_1 ∧ post = post_1 ∧ eval = eval_1 ∧ name = name_1)
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
/-- If each component of the unit is a monomorphism, then the left adjoint is faithful.  -/
CategoryTheory.Adjunction.faithful_L_of_mono_unit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R)
  [∀ (X : C), CategoryTheory.Mono (h.unit.app X)], L.Faithful
-- Mathlib.Tactic.Abel
/-- Normalize a term `orig` of the form `smul e₁ e₂` or `smulg e₁ e₂`.
Normalized terms use `smul` for monoids and `smulg` for groups,
so there are actually four cases to handle:
* Using `smul` in a monoid just simplifies the pieces using `subst_into_smul`
* Using `smulg` in a group just simplifies the pieces using `subst_into_smulg`
* Using `smul a b` in a group requires converting `a` from a nat to an int and
  then simplifying `smulg ↑a b` using `subst_into_smul_upcast`
* Using `smulg` in a monoid is impossible (or at least out of scope),
  because you need a group argument to write a `smulg` term  -/
Mathlib.Tactic.Abel.evalSMul' : (Lean.Expr → Mathlib.Tactic.Abel.M (Mathlib.Tactic.Abel.NormalExpr × Lean.Expr)) →
  Bool → Lean.Expr → Lean.Expr → Lean.Expr → Mathlib.Tactic.Abel.M (Mathlib.Tactic.Abel.NormalExpr × Lean.Expr)
-- Init.Grind.Config
/-- The configuration for `grind`.
Passed to `grind` using, for example, the `grind (config := { matchEqs := true })` syntax.
 -/
Lean.Grind.Config : Type
-- Mathlib.Algebra.Homology.BifunctorShift
/-- The inclusion of a summand `(F.obj (K₁.X n₁)).obj (K₂.X n₂) ⟶ (mapBifunctor K₁ K₂ F).X n`
of the total cochain complex when `n₁ + n₂ = n`.  -/
CochainComplex.ιMapBifunctor : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
              [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                (K₁ : CochainComplex C₁ ℤ) →
                  (K₂ : CochainComplex C₂ ℤ) →
                    [inst_5 : CategoryTheory.Preadditive D] →
                      (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                        [inst_6 : F.PreservesZeroMorphisms] →
                          [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] →
                            [inst_8 : K₁.HasMapBifunctor K₂ F] →
                              (n₁ n₂ n : ℤ) →
                                n₁ + n₂ = n → ((F.obj (K₁.X n₁)).obj (K₂.X n₂) ⟶ (K₁.mapBifunctor K₂ F).X n)
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.update : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : CommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalGroup α] {f : β → α} [L.LeAtTop],
  Multipliable f L → ∀ (b : β) [inst_4 : DecidableEq β] (a : α), Multipliable (Function.update f b a) L
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.instIsClosedImmersionLiftCoborder : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsImmersion f],
  AlgebraicGeometry.IsClosedImmersion (AlgebraicGeometry.Scheme.Hom.liftCoborder f)
-- Mathlib.CategoryTheory.Bicategory.End
CategoryTheory.whiskerLeft_def : ∀ {C : Type u} [inst : CategoryTheory.Bicategory C] (X : C) {f x x_1 : X ⟶ X} (η : x ⟶ x_1),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft f η = CategoryTheory.Bicategory.whiskerLeft f η
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.dvd_of_mem_cycleType : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {σ : Equiv.Perm α} {n : ℕ}, n ∈ σ.cycleType → n ∣ orderOf σ
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.Proj.stalkIso'_symm_mk : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (x : ↑(ProjectiveSpectrum.top 𝒜))
  (f : HomogeneousLocalization.NumDenSameDeg 𝒜 x.asHomogeneousIdeal.toIdeal.primeCompl),
  (AlgebraicGeometry.Proj.stalkIso' 𝒜 x).symm (HomogeneousLocalization.mk f) =
    (CategoryTheory.ConcreteCategory.hom
        ((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).presheaf.germ
          (ProjectiveSpectrum.basicOpen 𝒜 ↑f.den) x ⋯))
      (AlgebraicGeometry.sectionInBasicOpen 𝒜 x f)
-- Mathlib.Topology.Category.CompHaus.Basic
/-- The category of compact Hausdorff spaces.  -/
CompHaus : Type (u_1 + 1)
-- Mathlib.Algebra.Field.Defs
DivisionSemiring.toInv : {K : Type u_2} → [self : DivisionSemiring K] → Inv K
-- Mathlib.Data.Set.Card
Set.nonempty_of_encard_ne_zero : ∀ {α : Type u_1} {s : Set α}, s.encard ≠ 0 → s.Nonempty
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.dual_involutive : ∀ {α : Type u_1}, Function.Involutive Matroid.dual
-- Init.Data.SInt.Lemmas
Int32.ofInt_tmod : ∀ {a b : ℤ},
  Int32.minValue.toInt ≤ a →
    a ≤ Int32.maxValue.toInt →
      Int32.minValue.toInt ≤ b → b ≤ Int32.maxValue.toInt → Int32.ofInt (a.tmod b) = Int32.ofInt a % Int32.ofInt b
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.inv_mul_eq_iff_eq_mul_of_invertible : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  (A : Matrix n n α) [Invertible A] (B C : Matrix n m α), A⁻¹ * B = C ↔ B = A * C
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.support_copy : ∀ {V : Type u} {G : SimpleGraph V} {u v u' v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v'),
  (p.copy hu hv).support = p.support
-- Mathlib.Data.ZMod.Basic
ZMod.cast_intCast : ∀ {n : ℕ} {R : Type u_1} [inst : Ring R] {m : ℕ} [CharP R m], m ∣ n → ∀ (k : ℤ), (↑k).cast = ↑k
-- Mathlib.Order.Filter.Pointwise
/-- `Filter α` is a `Semigroup` under pointwise operations if `α` is.  -/
Filter.semigroup : {α : Type u_2} → [Semigroup α] → Semigroup (Filter α)
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.isSymmetric_linearIsometryEquiv_conj_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (T : E →ₗ[𝕜] E) (f : E ≃ₗᵢ[𝕜] F),
  (↑f.toLinearEquiv ∘ₗ T ∘ₗ ↑f.symm.toLinearEquiv).IsSymmetric ↔ T.IsSymmetric
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.mapGlueData_U : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [inst_2 : ∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F]
  (i : D.J), (D.mapGlueData F).U i = F.obj (D.U i)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.leftUnitor_neg_zero_tensor_add_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X₁ : C}
  [inst_2 : CategoryTheory.AddMonObj M] (f : X₁ ⟶ M) {Z : C} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₁).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.AddMonObj.zero f)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.univBall_symm_apply_center : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {P : Type u_2}
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor E P] (c : P) (r : ℝ),
  ↑(OpenPartialHomeomorph.univBall c r).symm c = 0
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
min_mul_distrib' : ∀ {α : Type u} [inst : Monoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedMul α] (a b c : α),
  min (a * b) c = min (min a c * min b c) c
-- Mathlib.Data.Subtype
Subtype.map_ne : ∀ {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} {f g : α → β} (h₁ : ∀ (a : α), p a → q (f a))
  (h₂ : ∀ (a : α), p a → q (g a)) {x y : Subtype p}, Subtype.map f h₁ x ≠ Subtype.map g h₂ y ↔ f ↑x ≠ g ↑y
-- Init.Data.Option.Lemmas
Option.all_guard : ∀ {α : Type u_1} {q p : α → Bool} (a : α), Option.all q (Option.guard p a) = (!p a || q a)
-- Mathlib.Order.CompleteLattice.Basic
sSup_sdiff_singleton_bot : ∀ {α : Type u_1} [inst : CompleteLattice α] (s : Set α), sSup (s \ {⊥}) = sSup s
-- Mathlib.Algebra.Module.Presentation.Free
Module.Relations.solutionFinsupp_var : ∀ {A : Type u} [inst : Ring A] (relations : Module.Relations A) [inst_1 : IsEmpty relations.R] (g : relations.G),
  relations.solutionFinsupp.var g = fun₀ | g => 1
-- Mathlib.Data.Finsupp.Basic
Finsupp.curry_apply : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] (f : α × β →₀ M) (x : α) (y : β),
  (f.curry x) y = f (x, y)
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mapMahlerMeasure_pos_of_ne_zero : ∀ {A : Type u_2} [inst : NormedRing A] {p : Polynomial A} (v : A →+* ℂ), Isometry ⇑v → p ≠ 0 → 0 < p.mapMahlerMeasure v
-- Mathlib.Topology.Algebra.Monoid
AddSubsemigroup.continuousAdd : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddSemigroup M] [ContinuousAdd M] (S : AddSubsemigroup M),
  ContinuousAdd ↥S
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntry?.eq_2 : ∀ {α : Type u} {β : Type v} (size : ℕ) (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.maxEntry?
      (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) =
    some (k, v)
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- A factorisation of a morphism `f = e ≫ m`, with `m` monic.  -/
CategoryTheory.Limits.MonoFactorisation.m : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → {f : X ⟶ Y} → (self : CategoryTheory.Limits.MonoFactorisation f) → self.I ⟶ Y
-- Mathlib.Data.Finsupp.Defs
Finsupp.mapRange_apply : ∀ {α : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] {f : M → N} {hf : f 0 = 0} {g : α →₀ M}
  {a : α}, (Finsupp.mapRange f hf g) a = f (g a)
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- A variant of `incl_lift` with `Z` an initial object.  -/
CategoryTheory.WithInitial.inclLiftToInitial : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        {Z : D} →
          (F : CategoryTheory.Functor C D) →
            (hZ : CategoryTheory.Limits.IsInitial Z) →
              CategoryTheory.WithInitial.incl.comp (CategoryTheory.WithInitial.liftToInitial F hZ) ≅ F
-- Mathlib.NumberTheory.Divisors
Nat.divisorsAntidiagonalList.eq_1 : ∀ (n : ℕ),
  n.divisorsAntidiagonalList =
    List.filterMap
      (fun x =>
        have y := n / x;
        if x * y = n then some (x, y) else none)
      (List.range' 1 n)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.addCommSemigroup : {α : Type u} → [AddCommSemigroup α] → AddCommSemigroup (WithTop α)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k a : α},
  Std.DTreeMap.Const.get? (t.erase k) a = if cmp k a = Ordering.eq then none else Std.DTreeMap.Const.get? t a
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- This is another version of `conjAct_smul_ι_mem_range_ι` which uses `involute`.  -/
spinGroup.involute_act_ι_mem_range_ι : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ},
  ↑x ∈ spinGroup Q →
    ∀ [Invertible 2] (y : M), CliffordAlgebra.involute ↑x * (CliffordAlgebra.ι Q) y * ↑x⁻¹ ∈ (CliffordAlgebra.ι Q).range
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.diag_replicateCol_mul_replicateRow : ∀ {n : Type u_3} {α : Type v} {ι : Type u_6} [inst : Mul α] [inst_1 : AddCommMonoid α] [inst_2 : Unique ι]
  (a b : n → α), (Matrix.replicateCol ι a * Matrix.replicateRow ι b).diag = a * b
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
/-- The base change of `B[M]` to an `R`-algebra `A` is isomorphic to `(A ⊗[R] B)[M]`
as an `A`-algebra.  -/
AddMonoidAlgebra.rTensorEquivAlgEquiv : (R : Type u_1) →
  {M : Type u_2} →
    (S : Type u_4) →
      (A : Type u_5) →
        (B : Type u_6) →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring S] →
              [inst_2 : CommSemiring A] →
                [inst_3 : CommSemiring B] →
                  [inst_4 : Algebra R S] →
                    [inst_5 : Algebra R A] →
                      [inst_6 : Algebra R B] →
                        [inst_7 : Algebra S A] →
                          [inst_8 : IsScalarTower R S A] →
                            [inst_9 : AddCommMonoid M] →
                              TensorProduct R A (AddMonoidAlgebra B M) ≃ₐ[S] AddMonoidAlgebra (TensorProduct R A B) M
-- Init.Data.Dyadic.Basic
Rat.mkRat_one : ∀ (x : ℤ), mkRat x 1 = ↑x
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.toLinearMap.congr_simp : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f f_1 : MultilinearMap R M₁ M₂),
  f = f_1 →
    ∀ {inst_5 : DecidableEq ι} [inst_6 : DecidableEq ι] (m m_1 : (i : ι) → M₁ i),
      m = m_1 → ∀ (i : ι), f.toLinearMap m i = f_1.toLinearMap m_1 i
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.over_map_coverPreserving : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {X Y : C}
  (f : X ⟶ Y), CategoryTheory.CoverPreserving (J.over X) (J.over Y) (CategoryTheory.Over.map f)
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mul_left_mem_nonZeroDivisorsLeft_eq_zero_iff : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {r x : M₀}, r ∈ nonZeroDivisorsLeft M₀ → (r * x = 0 ↔ x = 0)
-- Init.Data.Rat.Lemmas
Rat.lt_div_iff : ∀ {a b c : ℚ}, 0 < c → (a < b / c ↔ a * c < b)
-- Lean.Meta.Sym.AlphaShareBuilder
_private.Lean.Meta.Sym.AlphaShareBuilder.0.Lean.Meta.Sym.Internal.mkAppRevRangeS.go : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] → [Monad m] → Array Lean.Expr → ℕ → Lean.Expr → ℕ → m Lean.Expr
-- Init.Omega.Constraint
/-- The trivial constraint, satisfied everywhere.  -/
Lean.Omega.Constraint.trivial : Lean.Omega.Constraint
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.eHomFunctor_obj_map : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] (C : Type u)
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] (X : Cᵒᵖ)
  {X_1 Y : C} (φ : X_1 ⟶ Y),
  ((CategoryTheory.eHomFunctor V C).obj X).map φ = CategoryTheory.eHomWhiskerLeft V (Opposite.unop X) φ
-- Init.Data.SInt.Lemmas
Int64.toInt_bmod : ∀ (x : Int64), x.toInt.bmod 18446744073709551616 = x.toInt
-- Mathlib.Logic.Equiv.Fintype
/-- If `e` is an equivalence between two subtypes of a type `α`, `e.toCompl`
is an equivalence between the complement of those subtypes.

See also `Equiv.compl`, for a computable version when a term of type
`{e' : α ≃ α // ∀ x : {x // p x}, e' x = e x}` is known.  -/
Equiv.toCompl : {α : Type u_1} → {p q : α → Prop} → [Finite ↑{x | p x}] → ↑{x | p x} ≃ ↑{x | q x} → ↑{x | ¬p x} ≃ ↑{x | ¬q x}
-- Mathlib.Data.Opposite
Opposite.op_surjective : ∀ {α : Sort u}, Function.Surjective Opposite.op
-- Mathlib.Condensed.TopComparison
/-- `TopCat.toCondensedSet` yields a functor from `TopCat.{u + 1}` to `CondensedSet.{u}`.
 -/
topCatToCondensedSet : CategoryTheory.Functor TopCat CondensedSet
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_smul_le_map : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : CommSemiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (p : Submodule R M) [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (c : R₂),
  Submodule.map (c • f) p ≤ Submodule.map f p