mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.fromAffine_some_ne_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [inst_1 : Nontrivial R] {X Y : R}
  (h : W'.toAffine.Nonsingular X Y),
  WeierstrassCurve.Projective.Point.fromAffine (WeierstrassCurve.Affine.Point.some X Y h) ≠ 0
-- ProofWidgets.Presentation.Expr
ProofWidgets.GetExprPresentationParams.mk.inj : ∀ {expr : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx} {name : Lean.Name}
  {expr_1 : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx} {name_1 : Lean.Name},
  { expr := expr, name := name } = { expr := expr_1, name := name_1 } → expr = expr_1 ∧ name = name_1
-- Mathlib.Algebra.Order.Kleene
Prod.kstar_def : ∀ {α : Type u_1} {β : Type u_2} [inst : KleeneAlgebra α] [inst_1 : KleeneAlgebra β] (a : α × β),
  KStar.kstar a = (KStar.kstar a.1, KStar.kstar a.2)
-- Mathlib.CategoryTheory.Filtered.Basic
/-- a filtered category must be non-empty  -/
CategoryTheory.IsFiltered.nonempty : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.IsFiltered C], Nonempty C
-- Lean.Elab.Tactic.Doc
Lean.Elab.Tactic.Doc.TacticDoc.mk.sizeOf_spec : ∀ (internalName : Lean.Name) (userName : String) (tags : Lean.NameSet) (docString : Option String)
  (extensionDocs : Array String),
  sizeOf
      { internalName := internalName, userName := userName, tags := tags, docString := docString,
        extensionDocs := extensionDocs } =
    1 + sizeOf internalName + sizeOf userName + sizeOf tags + sizeOf docString + sizeOf extensionDocs
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.toAddSubmonoid_mono : ∀ {R : Type u} [inst : NonAssocSemiring R], Monotone Subsemiring.toAddSubmonoid
-- Mathlib.Topology.UniformSpace.Cauchy
UniformContinuous.comp_cauchySeq : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Type u_1} [inst : UniformSpace β] [inst_1 : Preorder γ]
  {f : α → β}, UniformContinuous f → ∀ {u : γ → α}, CauchySeq u → CauchySeq (f ∘ u)
-- Mathlib.Topology.CWComplex.Classical.Finite
Topology.RelCWComplex.mkFiniteType_cell : ∀ {X : Type u} [inst : TopologicalSpace X] (C : Set X) (D : outParam (Set X)) (cell : ℕ → Type u)
  (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X) (finite_cell : ∀ (n : ℕ), Finite (cell n))
  (source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1)
  (continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1))
  (continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target)
  (pairwiseDisjoint' : Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1)
  (disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' Metric.ball 0 1) D)
  (mapsTo :
    ∀ (n : ℕ) (i : cell n),
      Set.MapsTo (↑(map n i)) (Metric.sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1))
  (closed' :
    ∀ A ⊆ C,
      (∀ (n : ℕ) (j : cell n), IsClosed (A ∩ ↑(map n j) '' Metric.closedBall 0 1)) ∧ IsClosed (A ∩ D) → IsClosed A)
  (isClosedBase : IsClosed D) (union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C) (n : ℕ),
  Topology.RelCWComplex.cell C n = cell n
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.codeSupp'.match_1.eq_5 : ∀ (motive : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Sort u_1) (f g : Turing.ToPartrec.Code)
  (k : Turing.PartrecToTM2.Cont')
  (h_1 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.zero' → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.zero' k)
  (h_2 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.succ → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.succ k)
  (h_3 :
    (c : Turing.ToPartrec.Code) →
      c = Turing.ToPartrec.Code.tail → (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.tail k)
  (h_4 : (c f fs : Turing.ToPartrec.Code) → c = f.cons fs → (k : Turing.PartrecToTM2.Cont') → motive (f.cons fs) k)
  (h_5 : (c f g : Turing.ToPartrec.Code) → c = f.comp g → (k : Turing.PartrecToTM2.Cont') → motive (f.comp g) k)
  (h_6 : (c f g : Turing.ToPartrec.Code) → c = f.case g → (k : Turing.PartrecToTM2.Cont') → motive (f.case g) k)
  (h_7 : (c f : Turing.ToPartrec.Code) → c = f.fix → (k : Turing.PartrecToTM2.Cont') → motive f.fix k),
  (match f.comp g, k with
    | c@h:Turing.ToPartrec.Code.zero', k => h_1 c h k
    | c@h:Turing.ToPartrec.Code.succ, k => h_2 c h k
    | c@h:Turing.ToPartrec.Code.tail, k => h_3 c h k
    | c@h:(f.cons fs), k => h_4 c f fs h k
    | c@h:(f.comp g), k => h_5 c f g h k
    | c@h:(f.case g), k => h_6 c f g h k
    | c@h:f.fix, k => h_7 c f h k) =
    h_5 (f.comp g) f g ⋯ k
-- Lean.ErrorExplanation
Lean.getErrorExplanationsSorted : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → m (Array (Lean.Name × Lean.ErrorExplanation))
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.restrictStalkIso_hom_eq_germ_apply : ∀ {U : TopCat} (X : AlgebraicGeometry.LocallyRingedSpace) {f : U ⟶ X.toTopCat}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U)
  (hx : x ∈ V) (y : ↑((X.restrict h).presheaf.obj (Opposite.op V))),
  (CategoryTheory.ConcreteCategory.hom (X.restrictStalkIso h x).hom)
      ((CategoryTheory.ConcreteCategory.hom ((X.restrict h).presheaf.germ V x hx)) y) =
    (CategoryTheory.ConcreteCategory.hom
        (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯))
      y
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
map_mem_nonZeroDivisors : ∀ {F : Type u_1} {M₀ : Type u_2} {M₀' : Type u_3} [inst : MonoidWithZero M₀] [inst_1 : MonoidWithZero M₀']
  [inst_2 : FunLike F M₀ M₀'] [Nontrivial M₀] [NoZeroDivisors M₀'] [ZeroHomClass F M₀ M₀'] (g : F),
  Function.Injective ⇑g → ∀ {x : M₀}, x ∈ nonZeroDivisors M₀ → g x ∈ nonZeroDivisors M₀'
-- Mathlib.Tactic.FunProp.Mor
/-- `mkAppN f #[a₀, ..., aₙ]` ==> `f a₀ a₁ .. aₙ` where `f` can be bundled morphism.  -/
Mathlib.Meta.FunProp.Mor.mkAppN : Lean.Expr → Array Mathlib.Meta.FunProp.Mor.Arg → Lean.Expr
-- Mathlib.Data.Fintype.Card
Finite.injective_iff_bijective : ∀ {α : Type u_1} [Finite α] {f : α → α}, Function.Injective f ↔ Function.Bijective f
-- Mathlib.Topology.Algebra.Support
HasCompactSupport.neg : ∀ {α : Type u_9} {β : Type u_10} [inst : TopologicalSpace α] [inst_1 : SubtractionMonoid β] {f : α → β},
  HasCompactSupport f → HasCompactSupport (-f)
-- Std.Async.System
Std.Async.System.instReprGroupInfo.repr : Std.Async.System.GroupInfo → ℕ → Std.Format
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.lift_comp_map : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {E : Type u_9} [inst_3 : AddCommMonoid E] [inst_4 : Module R E]
  {t : ι → Type u_11} [inst_5 : (i : ι) → AddCommMonoid (t i)] [inst_6 : (i : ι) → Module R (t i)]
  (f : (i : ι) → s i →ₗ[R] t i) (h : MultilinearMap R t E),
  PiTensorProduct.lift h ∘ₗ PiTensorProduct.map f = PiTensorProduct.lift (h.compLinearMap f)
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.isBitVecValueTransition : Lean.Meta.Match.Problem → Lean.MetaM Bool
-- Mathlib.MeasureTheory.Function.UnifTight
/-- Forward direction of Vitali's convergence theorem, with a.e. instead of `InMeasure`
convergence  -/
MeasureTheory.tendsto_Lp_of_tendsto_ae : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup β] {μ : MeasureTheory.Measure α}
  {p : ENNReal},
  1 ≤ p →
    p ≠ ⊤ →
      ∀ {f : ℕ → α → β} {g : α → β},
        (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
          MeasureTheory.MemLp g p μ →
            MeasureTheory.UnifIntegrable f p μ →
              MeasureTheory.UnifTight f p μ →
                (∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) →
                  Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0)
-- Init.Grind.Lemmas
Lean.Grind.eq_true_of_and_eq_true_left : ∀ {a b : Prop}, (a ∧ b) = True → a = True
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_diff! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α}
  {h_contains : Std.DTreeMap.Internal.Impl.contains k (m₁.diff! m₂) = true}, (m₁.diff! m₂).get k h_contains = m₁.get k ⋯
-- Std.Do.Triple.SpecLemmas
getThe.eq_1 : ∀ (σ : Type u) {m : Type u → Type v} [inst : MonadStateOf σ m], getThe σ = MonadStateOf.get
-- Mathlib.NumberTheory.ArithmeticFunction.Carmichael
ArithmeticFunction.carmichael_eq_exponent : ∀ {n : ℕ}, n ≠ 0 → ArithmeticFunction.carmichael n = Monoid.exponent (ZMod n)ˣ
-- Mathlib.Topology.Constructions
IsOpen.preimage_val : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsOpen t → IsOpen (Subtype.val ⁻¹' t)
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedAddSubmonoid.instPartialOrder.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M],
  SaturatedAddSubmonoid.instPartialOrder = PartialOrder.ofSetLike (SaturatedAddSubmonoid M) M
-- Mathlib.CategoryTheory.Subfunctor.Finite
CategoryTheory.Subfunctor.IsGeneratedBy.ofSection_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  {G : CategoryTheory.Subfunctor F} {ι : Type w'} {X : ι → Cᵒᵖ} {x : (i : ι) → F.obj (X i)},
  G.IsGeneratedBy x → ∀ (i : ι), CategoryTheory.Subfunctor.ofSection (x i) ≤ G
-- Mathlib.GroupTheory.Submonoid.Center
/-- The center of an addition with zero `M` is the set of elements that commute with everything in
`M`  -/
AddSubmonoid.center : (M : Type u_1) → [inst : AddZeroClass M] → AddSubmonoid M
-- Init.SimpLemmas
instAssociativeBoolOr : Std.Associative fun x1 x2 => x1 || x2
-- Mathlib.Data.Finset.Option
Finset.eraseNone_empty : ∀ {α : Type u_1}, Finset.eraseNone ∅ = ∅
-- Mathlib.Topology.DenseEmbedding
/-- The product of two dense embeddings is a dense embedding.  -/
IsDenseEmbedding.prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : TopologicalSpace δ] {e₁ : α → β} {e₂ : γ → δ},
  IsDenseEmbedding e₁ → IsDenseEmbedding e₂ → IsDenseEmbedding fun p => (e₁ p.1, e₂ p.2)
-- Mathlib.Algebra.Group.Equiv.Opposite
MulEquiv.op_apply_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : Mul α] [inst_1 : Mul β] (f : α ≃* β) (a : αᵐᵒᵖ),
  (MulEquiv.op f) a = (MulOpposite.op ∘ ⇑f ∘ MulOpposite.unop) a
-- Init.Grind.Norm
Lean.Grind.imp_true_eq : ∀ (p : Prop), (p → True) = True
-- Mathlib.Data.List.AList
AList.toAList_cons : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (b : β a) (xs : List (Sigma β)),
  (⟨a, b⟩ :: xs).toAList = AList.insert a b xs.toAList
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instSemigroup : {α : Type u_1} → [Semigroup α] → Semigroup αᵃᵒᵖ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_filter_le_size : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {f : α → β → Bool}, (Std.ExtDTreeMap.filter f t).size ≤ t.size
-- Std.Http.Data.Status
/-- Checks if the type of the status code is a server error, meaning that the server failed to fulfill
an apparently valid request.

Reference: https://httpwg.org/specs/rfc9110.html#status.codes
 -/
Std.Http.Status.isServerError : Std.Http.Status → Bool
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.ofHom_apply : ∀ {X Y : Type u} [inst : Group X] [inst_1 : Group Y] (f : X →* Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (GrpCat.ofHom f)) x = f x
-- Mathlib.Order.WithBot
WithBot.eq_bot_iff_forall_lt : ∀ {α : Type u_1} [inst : Preorder α] {x : WithBot α}, x = ⊥ ↔ ∀ (b : α), x < ↑b
-- Mathlib.Algebra.Star.StarAlgHom
/-- Reinterpret a non-unital star algebra homomorphism as a non-unital algebra homomorphism
by forgetting the interaction with the star operation.  -/
NonUnitalStarAlgHom.toNonUnitalAlgHom : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : Monoid R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : DistribMulAction R A] →
            [inst_3 : Star A] →
              [inst_4 : NonUnitalNonAssocSemiring B] →
                [inst_5 : DistribMulAction R B] → [inst_6 : Star B] → (A →⋆ₙₐ[R] B) → A →ₙₐ[R] B
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
/-- Integration by parts of Schwartz functions for the Laplacian.

Version for scalar multiplication.  -/
SchwartzMap.integral_smul_laplacian_right_eq_left : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace ℝ F] [inst_3 : InnerProductSpace ℝ E] [inst_4 : FiniteDimensional ℝ E]
  [inst_5 : MeasurableSpace E] {μ : MeasureTheory.Measure E} [BorelSpace E] [μ.IsAddHaarMeasure] [inst_8 : RCLike 𝕜]
  [inst_9 : NormedSpace 𝕜 F] (f : SchwartzMap E 𝕜) (g : SchwartzMap E F),
  ∫ (x : E), f x • (Laplacian.laplacian g) x ∂μ = ∫ (x : E), (Laplacian.laplacian f) x • g x ∂μ
-- Mathlib.Tactic.ProdAssoc
/-- Given `P : ProdTree` representing an iterated product and `e : Expr` which
should correspond to a term of the iterated product, this will return
a list, whose items correspond to the leaves of `P` (i.e. the types appearing in the product),
where each item is the appropriate composition of `Prod.fst` and `Prod.snd` applied to `e`
resulting in an element of the type corresponding to the leaf.

For example, if `P` corresponds to `(X × Y) × Z` and `t : (X × Y) × Z`, then this
should return `[t.fst.fst, t.fst.snd, t.snd]`.
 -/
Lean.Expr.ProdTree.unpack : Lean.Expr → Lean.Expr.ProdTree → Lean.MetaM (List Lean.Expr)
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.renameEquiv_refl : ∀ {σ : Type u_1} {R : Type u_4} [inst : CommSemiring R], MvPowerSeries.renameEquiv R (Equiv.refl σ) = AlgEquiv.refl
-- Mathlib.Order.CompleteLattice.Basic
Equiv.biSup_comp : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_8} {ι' : Type u_9} {g : ι' → α} (e : ι ≃ ι') (s : Set ι'),
  ⨆ i ∈ ⇑e.symm '' s, g (e i) = ⨆ i ∈ s, g i
-- Mathlib.Algebra.BigOperators.Finprod
map_finsum : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {f : α → M}
  {G : Type u_7} [inst_2 : FunLike G M N] [AddMonoidHomClass G M N] (g : G),
  Function.HasFiniteSupport f → g (∑ᶠ (i : α), f i) = ∑ᶠ (i : α), g (f i)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.rpow_intCast : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] (a : Aˣ) (n : ℤ), autoParam (0 ≤ ↑a) CFC.rpow_intCast._auto_1 → ↑a ^ ↑n = ↑(a ^ n)
-- Mathlib.RingTheory.WittVector.Identities
WittVector.mul_pow_charP_coeff_zero : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p] (x : WittVector p R) {m n : ℕ},
  m < n → (x * ↑p ^ n).coeff m = 0
-- Mathlib.Analysis.Quaternion
Quaternion.coeComplex_zero : ↑0 = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  k ∈ Std.TreeMap.Raw.unitOfList l cmp ↔ l.contains k = true
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.coe_lt_coe : ∀ {α : Type u_1} [inst : LT α] {a b : α}, ↑a < ↑b ↔ a < b
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.stdPart_coe : ∀ (x : ℝ), ArchimedeanClass.stdPart ↑x = x
-- Init.Grind.Ring.Basic
Lean.Grind.Semiring.natCast_add : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a b : ℕ), ↑(a + b) = ↑a + ↑b
-- Mathlib.Topology.Bases
TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open : ∀ {α : Type u} [t : TopologicalSpace α] {b : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis b → ∀ {a : α} {u : Set α}, a ∈ u → IsOpen u → ∃ v ∈ b, a ∈ v ∧ v ⊆ u
-- Init.Data.Order.MinMaxOn
apply_maxOn_le_iff : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β} {x y : α}
  {b : β}, f (maxOn f x y) ≤ b ↔ f x ≤ b ∧ f y ≤ b
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.sum_right : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (B : LinearMap.BilinForm R M) {α : Type u_7} (t : Finset α) (w : M) (g : α → M),
  (B w) (∑ i ∈ t, g i) = ∑ i ∈ t, (B w) (g i)
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
Module.rank_zero_iff_of_free : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Free R M], Module.rank R M = 0 ↔ Subsingleton M
-- Batteries.Data.Nat.Lemmas
/-- **Alias** of `List.sum_append_nat`. -/
Nat.sum_append : ∀ {l₁ l₂ : List ℕ}, (l₁ ++ l₂).sum = l₁.sum + l₂.sum
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- Because the state transition function uses the alphabet and machine states in both the input
and output, to map a machine from one alphabet and machine state space to another we need functions
in both directions, essentially an `Equiv` without the laws.  -/
Turing.TM0.Machine.map : {Γ : Type u_1} →
  [inst : Inhabited Γ] →
    {Γ' : Type u_2} →
      [inst_1 : Inhabited Γ'] →
        {Λ : Type u_3} →
          [inst_2 : Inhabited Λ] →
            {Λ' : Type u_4} →
              [inst_3 : Inhabited Λ'] →
                Turing.TM0.Machine Γ Λ →
                  Turing.PointedMap Γ Γ' → Turing.PointedMap Γ' Γ → (Λ → Λ') → (Λ' → Λ) → Turing.TM0.Machine Γ' Λ'
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k k' fallback : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → (Std.DHashMap.ofList l).getKeyD k' fallback = k
-- Mathlib.LinearAlgebra.Matrix.WithConv
instNonAssocCommSemiringWithConvMatrix : {m : Type u_1} →
  {n : Type u_2} → {α : Type u_3} → [NonAssocCommSemiring α] → NonAssocCommSemiring (WithConv (Matrix m n α))
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.instPartialOrder : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → {hI : DividedPowers I} → PartialOrder hI.SubDPIdeal
-- Lean.Elab.DocString
/-- Whether suggestions should be provided interactively.  -/
Lean.Doc.Context.suggestionMode : Lean.Doc.Context → Lean.Doc.SuggestionMode
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivial.trivialization_source : ∀ (B : Type u_1) (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F],
  (Bundle.Trivial.trivialization B F).source = Set.univ
-- Mathlib.Analysis.Normed.Group.Bounded
HasCompactMulSupport.exists_bound_of_continuous : ∀ {α : Type u_1} {E : Type u_2} [inst : SeminormedGroup E] [inst_1 : TopologicalSpace α] {f : α → E},
  HasCompactMulSupport f → Continuous f → ∃ C, ∀ (x : α), ‖f x‖ ≤ C
-- Mathlib.CategoryTheory.Preadditive.EndoFunctor
CategoryTheory.Endofunctor.coalgebraPreadditive_homGroup_zero_f : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (F : CategoryTheory.Functor C C) [inst_2 : F.Additive] (A₁ A₂ : CategoryTheory.Endofunctor.Coalgebra F),
  CategoryTheory.Endofunctor.Coalgebra.Hom.f 0 = 0
-- Mathlib.CategoryTheory.Monoidal.Bimon_
CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : CategoryTheory.Bimon C),
  M.equivMonComonUnitIsoAppXAux.hom = CategoryTheory.CategoryStruct.id M.X.X
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.Hom.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] {V W : HopfAlgCat R} [inst_1 : SizeOf R] (toBialgHom' : V.carrier →ₐc[R] W.carrier),
  sizeOf { toBialgHom' := toBialgHom' } = 1 + sizeOf toBialgHom'
-- Mathlib.Algebra.Star.Subalgebra
/-- Restrict the scalar ring of a star algebra equivalence.  -/
StarAlgEquiv.restrictScalars : (R : Type u_1) →
  {S : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : NonUnitalNonAssocSemiring A] →
              [inst_3 : NonUnitalNonAssocSemiring B] →
                [inst_4 : MulAction R S] →
                  [inst_5 : Module S A] →
                    [inst_6 : Module S B] →
                      [inst_7 : Module R A] →
                        [inst_8 : Module R B] →
                          [IsScalarTower R S A] →
                            [IsScalarTower R S B] → [inst_11 : Star A] → [inst_12 : Star B] → (A ≃⋆ₐ[S] B) → A ≃⋆ₐ[R] B
-- Mathlib.LinearAlgebra.Matrix.DotProduct
Matrix.self_mul_conjTranspose_mul_eq_zero : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : PartialOrder R]
  [inst_3 : NonUnitalRing R] [inst_4 : StarRing R] [StarOrderedRing R] [NoZeroDivisors R] {p : Type u_5}
  (A : Matrix m n R) (B : Matrix m p R), A * A.conjTranspose * B = 0 ↔ A.conjTranspose * B = 0
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.triangleMap_hom₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} (φ₁ : K₁ ⟶ L₁)
  (φ₂ : K₂ ⟶ L₂) (a : K₁ ⟶ K₂) (b : L₁ ⟶ L₂)
  (comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂),
  (CochainComplex.mappingCone.triangleMap φ₁ φ₂ a b comm).hom₃ = CochainComplex.mappingCone.map φ₁ φ₂ a b comm
-- Mathlib.Topology.Algebra.Module.IsWeak
/-- A map `f : α → E` is continuous if all the maps `fun a ↦ B (f a) y` are continuous
for each `y : F`.  -/
LinearMap.IsWeak.continuous_of_continuous_eval : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [hB : B.IsWeak] {α : Type u_7} [inst_7 : TopologicalSpace α]
  {f : α → E}, (∀ (y : F), Continuous fun x => (B (f x)) y) → Continuous f
-- Init.Data.UInt.Lemmas
UInt16.ofFin_bitVecToFin : ∀ (n : BitVec 16), UInt16.ofFin n.toFin = { toBitVec := n }
-- Mathlib.GroupTheory.Divisible
/-- A group is `ℕ`-rootable if it is `ℤ`-rootable
 -/
Group.rootableByNatOfRootableByInt : (A : Type u_1) → [inst : Group A] → [RootableBy A ℤ] → RootableBy A ℕ
-- Aesop.Forward.RuleInfo
/-- Common variables shared between this slot and the previous slots.  -/
Aesop.Slot.common : Aesop.Slot → Std.HashSet Aesop.PremiseIndex
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The induced map `∐ I.left ⟶ ∐ I.right` via `I.fst` for colimiting cofans.  -/
CategoryTheory.Limits.MultispanIndex.fstSigmaMapOfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      (I : CategoryTheory.Limits.MultispanIndex J C) →
        {c : CategoryTheory.Limits.Cofan I.left} →
          (d : CategoryTheory.Limits.Cofan I.right) → CategoryTheory.Limits.IsColimit c → (c.pt ⟶ d.pt)
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instAddCommGroup : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] → [inst_6 : LieModule R L M] → AddCommGroup (LieDerivation R L M)