mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Vector.Lemmas
Vector.push_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} {size : xs.size = n},
  (Vector.mk xs size).push = fun x => Vector.mk (xs.push x) ⋯
-- Mathlib.Analysis.Calculus.TangentCone.Defs
/-- A property ensuring that the tangent cone to `s` at `x` spans a dense subset of the whole space.
The main role of this property is to ensure that the differential within `s` at `x` is unique,
hence this name. The uniqueness it asserts is proved in `UniqueDiffWithinAt.eq` in
`Mathlib/Analysis/Calculus/FDeriv/Basic.lean`.
To avoid pathologies in dimension 0, we also require that `x` belongs to the closure of `s` (which
is automatic when `E` is not `0`-dimensional).  -/
UniqueDiffWithinAt : (R : Type u) →
  {E : Type v} →
    [inst : Semiring R] → [inst_1 : AddCommGroup E] → [Module R E] → [TopologicalSpace E] → Set E → E → Prop
-- Init.Data.BitVec.Basic
BitVec.hash.eq_def : ∀ {n : ℕ} (bv : BitVec n),
  bv.hash =
    if n ≤ 64 then (↑bv.toFin).toUInt64 else mixHash (↑bv.toFin).toUInt64 (BitVec.setWidth (n - 64) (bv >>> 64)).hash
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- When `A : Rep k G` is a trivial representation of `G`, `H¹(G, A)` is isomorphic to the
group homs `G → A`.  -/
groupCohomology.H1IsoOfIsTrivial : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → [A.IsTrivial] → groupCohomology.H1 A ≅ ModuleCat.of k (Additive G →+ ↑A)
-- Init.Data.SInt.Lemmas
USize.toISize_ofBitVec : ∀ (b : BitVec System.Platform.numBits), { toBitVec := b }.toISize = ISize.ofBitVec b
-- Init.Data.Order.Ord
Std.instOrientedOrdProd : ∀ {α : Type u_1} {β : Type u_2} [inst : Ord α] [inst_1 : Ord β] [Std.OrientedOrd α] [Std.OrientedOrd β],
  Std.OrientedOrd (α × β)
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.neg_iff : ∀ {α : Type u_1} [inst : Ring α] {a b : α}, FiniteMultiplicity a (-b) ↔ FiniteMultiplicity a b
-- Mathlib.Algebra.ContinuedFractions.Translations
_private.Mathlib.Algebra.ContinuedFractions.Translations.0.GenContFract.contsAux.match_3.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_2 ()
-- Mathlib.Logic.Function.Basic
Function.IsPartialInv.injective : ∀ {α : Type u_4} {β : Sort u_5} {f : α → β} {g : β → Option α}, Function.IsPartialInv f g → Function.Injective f
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.instAddCommGroupSubtypeMemAddSubmonoid.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M],
  AddSubmonoid.instAddCommGroupSubtypeMemAddSubmonoid = { toAddGroup := inferInstance, add_comm := ⋯ }
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.primeSpectrumProd_symm_inl : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] (x : PrimeSpectrum R),
  (PrimeSpectrum.primeSpectrumProd R S).symm (Sum.inl x) = PrimeSpectrum.comap (RingHom.fst R S) x
-- Mathlib.Topology.Algebra.Group.Matrix
/-- The natural inclusion of `SL n A` in `GL n A` is a closed embedding.  -/
Matrix.SpecialLinearGroup.isClosedEmbedding_toGL : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [IsTopologicalRing R] [T0Space R],
  Topology.IsClosedEmbedding ⇑Matrix.SpecialLinearGroup.toGL
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_eq_getKeyD : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {a fallback : α} {h : m.contains a = true}, m.getKey a h = m.getKeyD a fallback
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_eq_get!_getKey? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited α] {a : α}, m.getKey! a = (m.getKey? a).get!
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.perm_symm_mapsTo_iff_mapsTo : ∀ {α : Type u} {f : Equiv.Perm α} {s : Set α} [Finite ↑s], Set.MapsTo (⇑(Equiv.symm f)) s s ↔ Set.MapsTo (⇑f) s s
-- Lean.Parser.Term
Lean.Parser.Term.letConfigItem.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
/-- A nonempty irreducible root pairing is a root system.  -/
RootPairing.instIsRootSystemOfNonemptyOfNeZeroOfNatOfIsIrreducible : ∀ {ι : 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) [Nonempty ι]
  [NeZero 2] [P.IsIrreducible], P.IsRootSystem
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.id_map : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {X Y : B} (f : X ⟶ Y),
  (CategoryTheory.StrictPseudofunctor.id B).map f = f
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.zero_apply : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] (a : A), 0 a = 0
-- Mathlib.CategoryTheory.Abelian.Preradical.Radical
/-- A preradical `Φ` is *radical* if `Φ.colon Φ ≅ Φ`.  -/
CategoryTheory.Abelian.Preradical.isRadical : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Abelian C] → CategoryTheory.ObjectProperty (CategoryTheory.Abelian.Preradical C)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGEπ_comp_truncGEδLT_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C) {Z : C}
  (h : (CategoryTheory.shiftFunctor C 1).obj ((t.truncLT n).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X)
      (CategoryTheory.CategoryStruct.comp ((t.truncGEδLT n).app X) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.GroupTheory.Submonoid.Center
AddEquivClass.apply_mem_center : ∀ {M : Type u_3} {N : Type u_1} {F : Type u_2} [inst : EquivLike F M N] [inst_1 : Add M] [inst_2 : Add N]
  [AddEquivClass F M N] (e : F) {x : M}, x ∈ Set.addCenter M → e x ∈ Set.addCenter N
-- Mathlib.Data.Vector3
Fin2.insertPerm.eq_4 : ∀ (a : ℕ) (i : Fin2 a.succ) (j : Fin2 (a + 1)),
  i.fs.insertPerm j.fs =
    match i.insertPerm j with
    | Fin2.fz => Fin2.fz
    | k.fs => k.fs.fs
-- Mathlib.Topology.MetricSpace.Infsep
Set.le_einfsep_image_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : EDist α] {d : ENNReal} {f : β → α} {s : Set β},
  d ≤ (f '' s).einfsep ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≠ f y → d ≤ edist (f x) (f y)
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.lift_continuum : Cardinal.lift.{v, u_1} Cardinal.continuum = Cardinal.continuum
-- Mathlib.Data.Int.Interval
Int.card_Ico : ∀ (a b : ℤ), (Finset.Ico a b).card = (b - a).toNat
-- Mathlib.Data.Finset.Sym
Finset.image_diag_union_image_offDiag : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α],
  Finset.image (Function.uncurry Sym2.mk) s.diag ∪ Finset.image (Function.uncurry Sym2.mk) s.offDiag = s.sym2
-- Mathlib.Data.Bundle
Bundle.TotalSpace.eta : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} (z : Bundle.TotalSpace F E), ⟨z.proj, z.snd⟩ = z
-- Init.Data.List.Basic
List.replace_nil : ∀ {α : Type u} {a b : α} [inst : BEq α], [].replace a b = []
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_eq_some_getKey : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} (h : a ∈ m), m.getKey? a = some (m.getKey a h)
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_insertListConst : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)}
  {k : α},
  Std.Internal.List.containsKey k (Std.Internal.List.insertListConst l toInsert) =
    (Std.Internal.List.containsKey k l || (List.map Prod.fst toInsert).contains k)
-- Init.MetaTypes
/-- When `true` (default: `true`), reduces projections of structure constructors.
 -/
Lean.Meta.DSimp.Config.proj : Lean.Meta.DSimp.Config → Bool
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  Std.Internal.List.getKey? a (Std.Internal.List.insertEntry k v l) =
    if (k == a) = true then some k else Std.Internal.List.getKey? a l
-- Lean.Parser.Command
/-- Disable delimiting of local entries in ScopedEnvExtension within the current scope.
This command is for internal use only. It is intended for macros that implicitly introduce new
scopes, such as `expandInCmd` and `expandNamespacedDeclaration`. It allows local attributes to remain
accessible beyond those implicit scopes, even though they would normally be hidden from the user.
The numeric argument specifies how many scope levels to mark as non-delimiting.
 -/
Lean.Parser.Command.InternalSyntax.end_local_scope : Lean.ParserDescr
-- Lean.Meta.Tactic.Split
/-- Splits an `if-then-else` of `match`-expression in the goal target.
If `useNewSemantics` is `true`, the flag `backward.split` is ignored. Recall this flag only affects the split of `if-then-else` expressions.
 -/
Lean.Meta.splitTarget? : Lean.MVarId → optParam Bool true → optParam Bool false → Lean.MetaM (Option (List Lean.MVarId))
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue!_modifyKey_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {k : α} [inst_2 : Inhabited β] {f : β → β}
  (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValue! k (Std.Internal.List.Const.modifyKey k f l) =
      (Option.map f (Std.Internal.List.getValue? k l)).get!
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.mapComp_inv_app_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z)
  (X_1 : CategoryTheory.Over X),
  ((CategoryTheory.Over.mapComp f g).inv.app X_1).left = CategoryTheory.CategoryStruct.id X_1.left
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cocone F} {t : CategoryTheory.Limits.Cocone G}
  (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) (w : F ≅ G) (j : J),
  CategoryTheory.CategoryStruct.comp (s.ι.app j) (P.coconePointsIsoOfNatIso Q w).hom =
    CategoryTheory.CategoryStruct.comp (w.hom.app j) (t.ι.app j)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.length_tail_add_one : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, ¬p.Nil → p.tail.length + 1 = p.length
-- Mathlib.Topology.Maps.Basic
Topology.IsEmbedding.continuous : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsEmbedding f → Continuous f
-- Mathlib.GroupTheory.OrderOfElement
zpow_pow_orderOf : ∀ {G : Type u_1} [inst : Group G] {x : G} {i : ℤ}, (x ^ i) ^ orderOf x = 1
-- Init.Data.Int.LemmasAux
Int.max_self_assoc : ∀ {m n : ℤ}, max m (max m n) = max m n
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.Hom.right_act_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} {M N : Bimod A B} (self : M.Hom N),
  CategoryTheory.CategoryStruct.comp M.actRight self.hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.hom B.X) N.actRight
-- Lean.Server.Requests
Lean.Server.StatefulRequestHandler.onDidChange : Lean.Server.StatefulRequestHandler → Lean.Lsp.DidChangeTextDocumentParams → Lean.Server.RequestM Unit
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.addCommMonoid : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_4} →
      {ι : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] →
                    [inst_6 : TopologicalSpace N] → [ContinuousAdd N] → AddCommMonoid (M [⋀^ι]→L[R] N)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesIsoX₂_inv_hom_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] (hf : S.f = 0),
  CategoryTheory.CategoryStruct.comp S.pOpcycles (S.opcyclesIsoX₂ hf).hom = CategoryTheory.CategoryStruct.id S.X₂
-- Batteries.Data.Fin.Lemmas
Fin.find?_le_findRev? : ∀ {n : ℕ} {p : Fin n → Bool}, Fin.find? p ≤ Fin.findRev? p
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.SubmersivePresentation.basisKaehler_apply : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) (k : ↑(Set.range P.map)ᶜ),
  P.basisKaehler k = (KaehlerDifferential.D R S) (P.val ↑k)
-- Mathlib.Dynamics.OmegaLimit
omegaLimit_eq_iInter : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α),
  omegaLimit f ϕ s = ⋂ u, closure (Set.image2 ϕ (↑u) s)
-- Mathlib.Algebra.GCDMonoid.Basic
Associates.lcm_mk_mk : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b : α},
  lcm (Associates.mk a) (Associates.mk b) = Associates.mk (lcm a b)
-- Mathlib.Topology.UniformSpace.HeineCantor
/-- In a product space `α × β`, assume that a function `f` is continuous on `s × k` where `k` is
compact. Then, along the fiber above any `q ∈ s`, `f` is transversely uniformly continuous, i.e.,
if `p ∈ s` is close enough to `q`, then `f p x` is uniformly close to `f q x` for all `x ∈ k`.  -/
IsCompact.mem_uniformity_of_prod : ∀ {α : Type u_4} {β : Type u_5} {E : Type u_6} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : UniformSpace E] {f : α → β → E} {s : Set α} {k : Set β} {q : α} {u : Set (E × E)},
  IsCompact k →
    ContinuousOn (Function.uncurry f) (s ×ˢ k) →
      q ∈ s → u ∈ uniformity E → ∃ v ∈ nhdsWithin q s, ∀ p ∈ v, ∀ x ∈ k, (f p x, f q x) ∈ u
-- Mathlib.Data.List.Destutter
/-- `destutter` of `≠` gives a list of maximal length over any chain.

In other words, `l.destutter (· ≠ ·)` is a `≠`-chain sublist of `l`, and is at least as long as any
other `≠`-chain sublist.  -/
List.IsChain.length_le_length_destutter_ne : ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : DecidableEq α],
  l₁.Sublist l₂ → List.IsChain (fun x1 x2 => x1 ≠ x2) l₁ → l₁.length ≤ (List.destutter (fun x1 x2 => x1 ≠ x2) l₂).length
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_prod_finset : ∀ {R : Type u} {ι : Type y} [inst : CommSemiring R] [inst_1 : DecidableEq ι] {s : Finset ι} {f : ι → Polynomial R},
  Polynomial.derivative (∏ b ∈ s, f b) = ∑ a ∈ s, (∏ b ∈ s.erase a, f b) * Polynomial.derivative (f a)
-- Mathlib.Topology.Bases
Dense.exists_countable_dense_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} [TopologicalSpace.SeparableSpace ↑s],
  Dense s → ∃ t ⊆ s, t.Countable ∧ Dense t
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.mem_support_ofFinset_iff : ∀ {α : Type u_1} {f : α → ENNReal} {s : Finset α} (h : ∑ a ∈ s, f a = 1) (h' : ∀ a ∉ s, f a = 0) (a : α),
  a ∈ (PMF.ofFinset f s h h').support ↔ a ∈ s ∧ f a ≠ 0
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
/-- Dedekind's linear independence of characters  -/
linearIndependent_monoidHom : ∀ (G : Type u_6) [inst : MulOneClass G] (L : Type u_7) [inst_1 : CommRing L] [IsDomain L],
  LinearIndependent L fun f => ⇑f
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- The multiplicative kernel of a monoid homomorphism is the subgroup of elements `x : G` such that
`f x = 1`  -/
MonoidHom.ker : {G : Type u_1} → [inst : Group G] → {M : Type u_7} → [inst_1 : MulOneClass M] → (G →* M) → Subgroup G
-- Mathlib.Dynamics.OmegaLimit
/-- The ω-limit w.r.t. `Filter.atBot`.  -/
omegaLimit.«termω⁻» : Lean.ParserDescr
-- Std.Data.Internal.List.Associative
Std.Internal.List.mem_map_toProd_iff_mem : ∀ {α : Type u} {β : Type v} {k : α} {v : β} {l : List ((_ : α) × β)},
  ⟨k, v⟩ ∈ l ↔ (k, v) ∈ List.map (fun x => (x.fst, x.snd)) l
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- Cyclotomic extensions are abelian.  -/
IsCyclotomicExtension.isAbelianGalois : ∀ (S : Set ℕ) (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [IsCyclotomicExtension S K L], IsAbelianGalois K L
-- Mathlib.Tactic.ClickSuggestions.TryPremises
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.runSuggestions.go : Mathlib.Tactic.ClickSuggestions.SectionKind →
  {α β : Type} →
    [Ord α] →
      [Inhabited α] →
        String →
          (α → α → Lean.MetaM Bool) →
            Array β →
              (β → Mathlib.Tactic.ClickSuggestions.Premise) →
                (β → Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM (Mathlib.Tactic.ClickSuggestions.Result α)) →
                  Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM ProofWidgets.Html
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.preimage_zeroLocus : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U : Y.Opens} (s : Set ↑(Y.presheaf.obj (Opposite.op U))),
  ⇑f ⁻¹' Y.zeroLocus s = X.zeroLocus (⇑(CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f U)) '' s)
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_onFinset : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {s : Finset α} {f : α → R} (g : α → M) (hf : ∀ (a : α), f a ≠ 0 → a ∈ s),
  (Finsupp.linearCombination R g) (Finsupp.onFinset s f hf) = ∑ x ∈ s, f x • g x
-- Mathlib.Algebra.Lie.Ideal
/-- A morphism of Lie algebras `f : L → L'` pulls back Lie ideals of `L'` to Lie ideals of `L`.

Note that `f` makes `L'` into a Lie module over `L` (turning `f` into a morphism of Lie modules)
and so this is a special case of `LieSubmodule.comap` but we do not exploit this fact.  -/
LieIdeal.comap : {R : Type u} →
  {L : Type v} →
    {L' : Type w₂} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieRing L'] →
            [inst_3 : LieAlgebra R L'] → [inst_4 : LieAlgebra R L] → (L →ₗ⁅R⁆ L') → LieIdeal R L' → LieIdeal R L
-- Init.Data.Vector.Erase
Vector.eraseIdx_append : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m} {k : ℕ} (h : k < n + m),
  (xs ++ ys).eraseIdx k h =
    if h' : k < n then Vector.cast ⋯ (xs.eraseIdx k h' ++ ys) else Vector.cast ⋯ (xs ++ ys.eraseIdx (k - n) ⋯)
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.leftRelDecidable.eq_1 : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) [inst_1 : DecidablePred fun x => x ∈ s] (x y : α),
  QuotientGroup.leftRelDecidable s x y = ⋯.mpr (inst_1 (x⁻¹ * y))
-- Std.Data.DHashMap.Basic
/-- Inserts multiple mappings into the hash map by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the last occurrence takes precedence.

Note: this precedence behavior is true for `HashMap`, `DHashMap`, `HashMap.Raw` and `DHashMap.Raw`.
The `insertMany` function on `HashSet` and `HashSet.Raw` behaves differently: it will prefer the first
appearance.
 -/
Std.DHashMap.insertMany : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} → {ρ : Type w} → [ForIn Id ρ ((a : α) × β a)] → Std.DHashMap α β → ρ → Std.DHashMap α β
-- Init.Data.Int.Gcd
Int.lcm_eq_one_iff : ∀ {m n : ℤ}, m.lcm n = 1 ↔ m ∣ 1 ∧ n ∣ 1
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.eval.eq_1 : Nat.Partrec.Code.zero.eval = pure 0
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.hasCoequalizer_of_common_section : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasReflexiveCoequalizers C] {A B : C}
  {f g : A ⟶ B} (r : B ⟶ A),
  CategoryTheory.CategoryStruct.comp r f = CategoryTheory.CategoryStruct.id B →
    CategoryTheory.CategoryStruct.comp r g = CategoryTheory.CategoryStruct.id B →
      CategoryTheory.Limits.HasCoequalizer f g
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The affine subspace seen as a subset.  -/
AffineSubspace.carrier : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] → [inst_2 : Module k V] → [inst_3 : AddTorsor V P] → AffineSubspace k P → Set P
-- Init.Data.Repr
instReprSigma : {α : Type u_1} → {β : α → Type v} → [Repr α] → [(x : α) → Repr (β x)] → Repr (Sigma β)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.continuous_toFun : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_4} {V₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (self : P₁ ≃ᴬ[k] P₂), Continuous (↑self).toFun
-- Init.Data.Array.Perm
Array.Perm.push_comm : ∀ {α : Type u_1} (x y : α) {xs ys : Array α}, xs.Perm ys → ((xs.push x).push y).Perm ((ys.push y).push x)
-- Mathlib.LinearAlgebra.CrossProduct
cross_anticomm' : ∀ {R : Type u_1} [inst : CommRing R] (v w : Fin 3 → R), (crossProduct v) w + (crossProduct w) v = 0
-- Std.Http.Data.URI.Basic
Std.Http.URI.instReprQuery : Repr Std.Http.URI.Query
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k k' fallback : α} {f : β → β},
  (t.modify k f).getKeyD k' fallback =
    if cmp k k' = Ordering.eq then if k ∈ t then k else fallback else t.getKeyD k' fallback
-- Lean.Widget.Basic
Lean.Widget.instTypeNameTermInfo : TypeName Lean.Elab.TermInfo
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.differentiableAt_sin : ∀ {x : ℂ}, DifferentiableAt ℂ Complex.sin x
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
AffineSubspace.smul_mem_smul_iff : ∀ {k : Type u_2} {V : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {s : AffineSubspace k V}
  {p : V} {G : Type u_9} [inst_3 : Group G] [inst_4 : DistribMulAction G V] [inst_5 : SMulCommClass G k V] {a : G},
  a • p ∈ a • s ↔ p ∈ s
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAt.domChart_mem_maximalAtlas : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAt I J n f x), h.domChart ∈ IsManifold.maximalAtlas I n M
-- Mathlib.RingTheory.Valuation.Discrete.Basic
/-- The integer underlying a `Uniformizer`  -/
Valuation.Uniformizer.val : {Γ : Type u_1} →
  [inst : LinearOrderedCommGroupWithZero Γ] →
    {A : Type u_2} → [inst_1 : Ring A] → {v : Valuation A Γ} → [hv : v.IsRankOneDiscrete] → v.Uniformizer → ↥v.integer
-- Mathlib.Data.Finsupp.Weight
/-- **Alias** of `Finsupp.degree_mapDomain`. -/
Finsupp.degree_mapDomain_eq_of_subsingletonAddUnits : ∀ {σ : Type u_1} {M : Type u_2} {τ : Type u_5} (f : σ → τ) [inst : AddCommMonoid M] (x : σ →₀ M),
  Finsupp.degree (Finsupp.mapDomain f x) = Finsupp.degree x