mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.Galois.Profinite
/-- `algEquivToLimit` as a `MulEquiv`.  -/
InfiniteGalois.mulEquivToLimit : (k : Type u_3) →
  (K : Type u_4) →
    [inst : Field k] →
      [inst_1 : Field K] →
        [inst_2 : Algebra k K] →
          [IsGalois k K] →
            Gal(K/k) ≃* ↑(ProfiniteGrp.limit (InfiniteGalois.asProfiniteGaloisGroupFunctor k K)).toProfinite.toTop
-- Mathlib.CategoryTheory.Action.Monoidal
Action.instBraidedCategory : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    (G : Type u_2) →
      [inst_1 : Monoid G] →
        [inst_2 : CategoryTheory.MonoidalCategory V] →
          [CategoryTheory.BraidedCategory V] → CategoryTheory.BraidedCategory (Action V G)
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.ToLinear.State.vars : Lean.Meta.Simp.Arith.Int.ToLinear.State → Array Lean.Expr
-- Mathlib.FieldTheory.Separable
Polynomial.Separable.mul : ∀ {R : Type u} [inst : CommRing R] {f g : Polynomial R}, f.Separable → g.Separable → IsCoprime f g → (f * g).Separable
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
CategoryTheory.regularTopology.EqualizerCondition.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.Functor Cᵒᵖ (Type u_4)),
  (∀ (X B : C) (π : X ⟶ B) [CategoryTheory.EffectiveEpi π] [inst_2 : CategoryTheory.Limits.HasPullback π π],
      Function.Bijective
        ⇑(CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.regularTopology.mapToEqualizer P π (CategoryTheory.Limits.pullback.fst π π)
              (CategoryTheory.Limits.pullback.snd π π) ⋯))) →
    CategoryTheory.regularTopology.EqualizerCondition P
-- Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
/-- *Weak approximation for the infinite adele ring*

The number field $K$ is dense in the infinite adele ring $\prod_v K_v$.
 -/
NumberField.InfiniteAdeleRing.denseRange_algebraMap : ∀ (K : Type u_1) [inst : Field K] [NumberField K], DenseRange ⇑(algebraMap K (NumberField.InfiniteAdeleRing K))
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.orbitRel_subgroupOf : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (H K : Subgroup G),
  MulAction.orbitRel (↥(H.subgroupOf K)) α = MulAction.orbitRel (↥(H ⊓ K)) α
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α},
  (m₁ \ m₂).getD k fallback = if k ∈ m₂ then fallback else m₁.getD k fallback
-- Mathlib.Tactic.CategoryTheory.Coherence
/-- **Alias** of `Mathlib.Tactic.Coherence.monoidalCoherence`.

---

Coherence tactic for monoidal categories.  -/
Mathlib.Tactic.Coherence.monoidal_coherence : Lean.MVarId → Lean.Elab.TermElabM Unit
-- Mathlib.MeasureTheory.Function.LpSeminorm.SMul
MeasureTheory.MemLp.const_smul' : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {𝕜 : Type u_3}
  [inst : NormedRing 𝕜] {ε : Type u_4} [inst_1 : TopologicalSpace ε] [inst_2 : ESeminormedAddMonoid ε]
  [inst_3 : SMul 𝕜 ε] [ENormSMulClass 𝕜 ε] {f : α → ε} [ContinuousConstSMul 𝕜 ε],
  MeasureTheory.MemLp f p μ → ∀ (c : 𝕜), MeasureTheory.MemLp (c • f) p μ
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.tfaeHaveDecl.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.SInt.Lemmas
Int64.toUInt64_sub : ∀ (a b : Int64), (a - b).toUInt64 = a.toUInt64 - b.toUInt64
-- Mathlib.Topology.MetricSpace.Infsep
Set.le_einfsep : ∀ {α : Type u_1} [inst : EDist α] {s : Set α} {d : ENNReal}, (∀ x ∈ s, ∀ y ∈ s, x ≠ y → d ≤ edist x y) → d ≤ s.einfsep
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lift_aleph : ∀ (o : Ordinal.{u}), Cardinal.lift.{v, u} (Cardinal.aleph o) = Cardinal.aleph (Ordinal.lift.{v, u} o)
-- Mathlib.Lean.Expr.Basic
/-- Given `f a₀ a₁ ... aₙ₋₁`, returns the `i`th argument or none if out of bounds.  -/
Lean.Expr.getArg? : (e : Lean.Expr) → ℕ → optParam ℕ e.getAppNumArgs → Option Lean.Expr
-- Mathlib.Data.List.Sublists
/-- **Alias** of the forward direction of `List.nodup_sublists`. -/
List.Nodup.of_sublists : ∀ {α : Type u} {l : List α}, l.sublists.Nodup → l.Nodup
-- Mathlib.Data.List.Sigma
List.NodupKeys.nodup : ∀ {α : Type u} {β : α → Type v} {l : List (Sigma β)}, l.NodupKeys → l.Nodup
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Occasionally useful for rewriting in the backwards direction.  -/
CategoryTheory.MorphismProperty.Over.forget_comp_forget_map : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T) (X : T)
  [inst_1 : Q.IsMultiplicative] {A B : P.Over Q X} (f : A ⟶ B),
  ((CategoryTheory.MorphismProperty.Over.forget P Q X).comp (CategoryTheory.Over.forget X)).map f = f.left
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isRat_add : ∀ {α : Type u_1} [inst : Ring α] {f : α → α → α} {a b : α} {na nb nc : ℤ} {da db dc k : ℕ},
  f = HAdd.hAdd →
    Mathlib.Meta.NormNum.IsRat a na da →
      Mathlib.Meta.NormNum.IsRat b nb db →
        (na.mul ↑db).add (nb.mul ↑da) = (↑k).mul nc → da.mul db = k.mul dc → Mathlib.Meta.NormNum.IsRat (f a b) nc dc
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.pullbackCone_snd_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z)
  (g : Y ⟶ Z)
  (pb :
    (i : Function.Pullback f.f g.f) →
      CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯))
        (g.φ (↑i).2))
  (i : (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).pt.I),
  (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).snd.f i = (↑i).2
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.nil.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α], sizeOf Batteries.BinomialHeap.Imp.HeapNode.nil = 1
-- Mathlib.Order.Interval.Set.OrdConnected
Set.OrdConnected.preimage_anti : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : β → α},
  s.OrdConnected → Antitone f → (f ⁻¹' s).OrdConnected
-- Init.Data.List.MinMaxOn
List.maxOn_eq_get_maxOn? : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α} (h : xs ≠ []),
  List.maxOn f xs h = (List.maxOn? f xs).get ⋯
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.mk : {α : Type} →
  Std.HashMap Lean.Meta.RefinedDiscrTree.Key Lean.Meta.RefinedDiscrTree.TrieIndex →
    Array (Lean.Meta.RefinedDiscrTree.Trie α) → Lean.Meta.RefinedDiscrTree α
-- Mathlib.NumberTheory.LSeries.HurwitzZetaValues
/-- Explicit formula for `ζ (2 * k)`, for `k ∈ ℕ` with `k ≠ 0`, in terms of the Bernoulli number
`bernoulli (2 * k)`.

Compare `hasSum_zeta_nat` for a version formulated in terms of a sum over `1 / n ^ (2 * k)`, and
`riemannZeta_neg_nat_eq_bernoulli` for values at negative integers (equivalent to the above via
the functional equation).  -/
riemannZeta_two_mul_nat : ∀ {k : ℕ},
  k ≠ 0 →
    riemannZeta (2 * ↑k) =
      (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * ↑Real.pi ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k).factorial
-- Mathlib.Geometry.Convex.Hull
/-- The convex hull of a set `s` is the minimal convex set that includes `s`.  -/
Convexity.convexHull : (R : Type u_1) →
  {X : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsStrictOrderedRing R] → [Convexity.ConvexSpace R X] → ClosureOperator (Set X)
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
/-- The evaluation map `(f : E →SLₚₜ[σ] F) ↦ f a` for `a : E` as a continuous linear map.  -/
PointwiseConvergenceCLM.evalCLM : {𝕜₁ : Type u_4} →
  {𝕜₂ : Type u_5} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          {E : Type u_7} →
            (F : Type u_8) →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : AddCommGroup F] →
                    [inst_5 : TopologicalSpace F] →
                      [inst_6 : IsTopologicalAddGroup F] →
                        [inst_7 : Module 𝕜₁ E] →
                          [inst_8 : Module 𝕜₂ F] → [inst_9 : ContinuousConstSMul 𝕜₂ F] → E → (E →SLₚₜ[σ] F) →L[𝕜₂] F
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_diff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_contains : Std.DTreeMap.Internal.Impl.contains k (m₁.diff m₂ ⋯) = true},
  Std.DTreeMap.Internal.Impl.Const.get (m₁.diff m₂ ⋯) k h_contains = Std.DTreeMap.Internal.Impl.Const.get m₁ k ⋯
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_ite_eq : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (a : ι) (b : ι → M),
  (∑ x ∈ s, if a = x then b x else 0) = if a ∈ s then b a else 0
-- Mathlib.Order.Heyting.Hom
BiheytingHom.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β] [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (toLatticeHom : LatticeHom α β)
  (map_himp' : ∀ (a b : α), toLatticeHom.toFun (a ⇨ b) = toLatticeHom.toFun a ⇨ toLatticeHom.toFun b)
  (map_sdiff' : ∀ (a b : α), toLatticeHom.toFun (a \ b) = toLatticeHom.toFun a \ toLatticeHom.toFun b),
  sizeOf { toLatticeHom := toLatticeHom, map_himp' := map_himp', map_sdiff' := map_sdiff' } = 1 + sizeOf toLatticeHom
-- Init.Data.List.Monadic
List.mapM'.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → m β), List.mapM' f [] = pure []
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasFDerivAt.ccosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E},
  HasFDerivAt f f' x → HasFDerivAt (fun x => Complex.cosh (f x)) (Complex.sinh (f x) • f') x
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_div_nhds_one_iff : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {α : Type u_1} {l : Filter α}
  {x : G} {u : α → G}, Filter.Tendsto (fun x_1 => u x_1 / x) l (nhds 1) ↔ Filter.Tendsto u l (nhds x)
-- Mathlib.CategoryTheory.Preadditive.EndoFunctor
CategoryTheory.Endofunctor.algebraPreadditive_homGroup_sub_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.Algebra F) (α β : A₁ ⟶ A₂),
  (α - β).f = α.f - β.f
-- Mathlib.Analysis.Calculus.Deriv.Star
/-- A function `f` has derivative `f'` at `z` iff `star ∘ f ∘ conj` has derivative `star f'` at
`conj z`.  -/
hasDerivAt_star_conj_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace 𝕜 F] [inst_4 : StarAddMonoid F] [StarModule 𝕜 F] [ContinuousStar F] [NormedStarGroup 𝕜]
  {f : 𝕜 → F} {x : 𝕜} {f' : F},
  HasDerivAt (star ∘ f ∘ ⇑(starRingEnd 𝕜)) f' x ↔ HasDerivAt f (star f') ((starRingEnd 𝕜) x)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.keyAtIdx?.eq_2 : ∀ {α : Type u} {β : α → Type v} (x size : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v l r).keyAtIdx? x =
    match compare x l.size with
    | Ordering.lt => l.keyAtIdx? x
    | Ordering.eq => some k
    | Ordering.gt => r.keyAtIdx? (x - l.size - 1)
-- Mathlib.Data.Num.Basic
/-- The number of bits of a `PosNum`, as a `Nat`.  -/
PosNum.natSize : PosNum → ℕ
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- The above data together form a topological group.  -/
ProfiniteGrp.topologicalGroup : ∀ (self : ProfiniteGrp.{u}), IsTopologicalGroup ↑self.toProfinite.toTop
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z)
  (H :
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base)),
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift f g H =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.Limits.pullback.snd f g))
      (CategoryTheory.Limits.pullback.fst f g)
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.maxEntry?.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size k v l
                          (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =>
      h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h) =
    h_1 ()
-- Init.Data.String.Iterate
String.Slice.RevByteIterator.s : String.Slice.RevByteIterator → String.Slice
-- Lean.DocString.Parser
/-- Parses a link reference target.
 -/
Lean.Doc.Parser.linkRef : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Mathlib.NumberTheory.Height.EllipticCurve
/-- If `W` is a Weierstrass curve over `K`, then the map `F : ℙ² → ℙ²` given by `addSubMap W`
is a morphism.

This implies that `|logHeight (F x) - 2 * logHeight x| ≤ C` for a constant `C`,
where `x = ![s, t, u]` and `F` acts on the coordinate vector.  -/
WeierstrassCurve.abs_logHeight_addSubMap_sub_two_mul_logHeight_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (W : WeierstrassCurve K) [W.IsElliptic],
  ∃ C,
    ∀ (x : Fin 3 → K), |(Height.logHeight fun i => (MvPolynomial.eval x) (W.addSubMap i)) - 2 * Height.logHeight x| ≤ C
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
Real.contDiff_exp : ∀ {n : WithTop ℕ∞}, ContDiff ℝ n Real.exp
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.image_symm_eq_preimage : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [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₂]
  (e : P₁ ≃ᴬ[k] P₂) (s : Set P₂), ⇑e.symm '' s = ⇑e ⁻¹' s
-- Mathlib.Algebra.Order.Module.Defs
IsStrictOrderedRing.toIsStrictOrderedModule : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α], IsStrictOrderedModule α α
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.ι_ofι : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {P : C} (ι : P ⟶ X)
  (w : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g),
  (CategoryTheory.Limits.Fork.ofι ι w).ι = ι
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.ofArrows_le_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {ι : Type u_1} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  {R : CategoryTheory.Presieve X}, CategoryTheory.Presieve.ofArrows Y f ≤ R ↔ ∀ (i : ι), R (f i)
-- Mathlib.CategoryTheory.ObjectProperty.CompleteLattice
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsTop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], ⊤.IsClosedUnderIsomorphisms
-- Mathlib.Probability.Distributions.Bernoulli
ProbabilityTheory.integral_bernoulliMeasure : ∀ {X : Type u_1} [inst : MeasurableSpace X] {E : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [CompleteSpace E] [MeasurableSingletonClass X] (x y : X) (p : ↑unitInterval) (f : X → E),
  ∫ (z : X), f z ∂ProbabilityTheory.bernoulliMeasure x y p = ↑p • f x + (1 - ↑p) • f y
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidSaveTextDocumentParams.text? : Lean.Lsp.DidSaveTextDocumentParams → Option String
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.toList_ofList : ∀ {α : Type u_1} (l : List α), FreeMonoid.toList (FreeMonoid.ofList l) = l
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
AlgebraicIndependent.aeval_comp_repr : ∀ {ι : Type u_1} {R : Type u_3} {A : Type u_5} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] (hx : AlgebraicIndependent R x),
  (MvPolynomial.aeval x).comp hx.repr = (Algebra.adjoin R (Set.range x)).val
-- Mathlib.Algebra.Quaternion
Quaternion.instStarRing : {R : Type u_3} → [inst : CommRing R] → StarRing (Quaternion R)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.of.inj : ∀ {η η_1 : Mathlib.Tactic.BicategoryLike.AtomIso},
  Mathlib.Tactic.BicategoryLike.Mor₂Iso.of η = Mathlib.Tactic.BicategoryLike.Mor₂Iso.of η_1 → η = η_1
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionHom : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {c c' : Cᴹᵒᵖ} {d d_1 : D} (f : c ⟶ c')
  (g : d ⟶ d_1),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f g =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom g f.unmop
-- Lean.Parser.Syntax
Lean.Parser.Command.elabTail : Lean.Parser.Parser
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.associator_inv_apply_2 : ∀ {X Y Z : TopCat}
  {x : ↑(CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))},
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv) x).2 = x.2.2
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.exists_pow_neg_lt : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {ε : ℝ}, 0 < ε → ∃ k, ↑p ^ (-↑k) < ε
-- Mathlib.Algebra.Algebra.Hom
MulSemiringAction.toAlgHom_injective : ∀ {M : Type u_1} (R : Type u_3) (A : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] [inst_4 : MulSemiringAction M A] [inst_5 : SMulCommClass M R A] [FaithfulSMul M A],
  Function.Injective (MulSemiringAction.toAlgHom R A)
-- Mathlib.GroupTheory.Exponent
Monoid.exponent_eq_iSup_orderOf' : ∀ {G : Type u} [inst : CommMonoid G], Monoid.exponent G = if ∃ g, orderOf g = 0 then 0 else ⨆ g, orderOf g
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.CondIndepSets.condIndepSet_of_mem : ∀ {Ω : Type u_1} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ} {s t : Set Ω}
  (S T : Set (Set Ω)),
  s ∈ S →
    t ∈ T →
      MeasurableSet s →
        MeasurableSet t →
          ∀ (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
            ProbabilityTheory.CondIndepSets m' hm' S T μ → ProbabilityTheory.CondIndepSet m' hm' s t μ
-- Mathlib.Order.Filter.Basic
Filter.EventuallyEq.diff : ∀ {α : Type u} {s t s' t' : Set α} {l : Filter α}, s =ᶠ[l] t → s' =ᶠ[l] t' → s \ s' =ᶠ[l] t \ t'
-- Mathlib.Topology.LocallyFinite
LocallyFinite.continuousOn_iUnion' : ∀ {ι : Type u_1} {X : Type u_4} {Y : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : ι → Set X}
  {g : X → Y},
  LocallyFinite f → (∀ (i : ι), ∀ x ∈ closure (f i), ContinuousWithinAt g (f i) x) → ContinuousOn g (⋃ i, f i)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.ι_range_map_map : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {Q₁ : QuadraticForm R M₁}
  {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂),
  Submodule.map (CliffordAlgebra.map f).toLinearMap (CliffordAlgebra.ι Q₁).range =
    Submodule.map (CliffordAlgebra.ι Q₂) f.range
-- Mathlib.Tactic.FieldSimp
/-- Given `x` in a commutative group-with-zero, construct a new expression in the standard form
*** / *** (all denominators at the end) which is equal to `x`.  -/
Mathlib.Tactic.FieldSimp.reduceExpr : ({u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) → Lean.Expr → Mathlib.Tactic.AtomM Lean.Meta.Simp.Result
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.singleCompEvalIsoSelf_hom_app : ∀ (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (X : V), (HomologicalComplex.singleCompEvalIsoSelf V c j).hom.app X = (HomologicalComplex.singleObjXSelf c j X).hom
-- Init.PropLemmas
not_and_self_iff : ∀ (a : Prop), ¬a ∧ a ↔ False
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.isLocal_ringHomProperty : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme)
  {Q : outParam ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop)}
  [self : AlgebraicGeometry.HasRingHomProperty P Q], RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q
-- Lean.Declaration
Lean.DefinitionSafety.noConfusionType : Sort v✝ → Lean.DefinitionSafety → Lean.DefinitionSafety → Sort v✝
-- Mathlib.Algebra.Order.Quantale
AddQuantale.add_sup_distrib : ∀ {α : Type u_1} {x y z : α} [inst : AddSemigroup α] [inst_1 : CompleteLattice α] [IsAddQuantale α],
  x + y ⊔ z = (x + y) ⊔ (x + z)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonParameterInformation.fromJson : Lean.Json → Except String Lean.Lsp.ParameterInformation
-- Mathlib.RingTheory.Jacobson.Radical
Ring.jacobson.eq_1 : ∀ (R : Type u_1) [inst : Ring R], Ring.jacobson R = Module.jacobson R R
-- Mathlib.Data.PEquiv
PEquiv.coe_mk : ∀ {α : Type u} {β : Type v} (f₁ : α → Option β) (f₂ : β → Option α)
  (h : ∀ (a : α) (b : β), f₂ b = some a ↔ f₁ a = some b), ⇑{ toFun := f₁, invFun := f₂, inv := h } = f₁
-- Mathlib.Tactic.ClickSuggestions.Rewrite
/-- The expression that is being rewritten. This may not be the same as the selected expression,
because we also suggest rewriting partial applications.  -/
Mathlib.Tactic.ClickSuggestions.RwInfo.pos : Mathlib.Tactic.ClickSuggestions.RwInfo → Lean.SubExpr.Pos
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castSucc_Iic : ∀ {n : ℕ} (i : Fin n), Finset.image Fin.castSucc (Finset.Iic i) = Finset.Iic i.castSucc
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
IsometricContinuousFunctionalCalculus.isGreatest_spectrum : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A] [inst_3 : PartialOrder A]
  [StarOrderedRing A] [IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [Nontrivial A]
  (a : A),
  autoParam (0 ≤ a) IsometricContinuousFunctionalCalculus.isGreatest_spectrum._auto_1 →
    IsGreatest (spectrum NNReal a) ‖a‖₊
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (x : ↥U),
  hU.isoSpec.hom x =
    (AlgebraicGeometry.Spec.map (X.presheaf.germ U ↑x ⋯)) (IsLocalRing.closedPoint ↑(X.presheaf.stalk ↑x))