mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Maps.Basic
IsOpenMap.image_mem_nhds : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f → ∀ {x : X} {s : Set X}, s ∈ nhds x → f '' s ∈ nhds (f x)
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.coe_toAlgHom : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] {f : A →⋆ₐ[R] B}, ⇑↑f = ⇑f
-- Mathlib.Topology.DiscreteSubset
Continuous.discrete_of_tendsto_cofinite_cocompact : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} [T1Space X]
  [WeaklyLocallyCompactSpace Y],
  Continuous f → Filter.Tendsto f Filter.cofinite (Filter.cocompact Y) → DiscreteTopology X
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.get?.match_1.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.lt = Ordering.lt → motive Ordering.lt)
  (h_2 : Ordering.lt = Ordering.gt → motive Ordering.gt) (h_3 : Ordering.lt = Ordering.eq → motive Ordering.eq),
  (match h : Ordering.lt with
    | Ordering.lt => h_1 h
    | Ordering.gt => h_2 h
    | Ordering.eq => h_3 h) =
    h_1 ⋯
-- Init.Data.Bool
Subtype.beq_iff : ∀ {α : Type u} [inst : BEq α] {p : α → Prop} {x y : { a // p a }}, (x == y) = (↑x == ↑y)
-- Lean.Server.AsyncList
/-- Spawns a `Task` acting like `List.find?` but which will wait for tail evaluation
when necessary to traverse the list. If the tail terminates before a matching element
is found, the task throws the terminating value.  -/
Lean.AsyncList.waitFind? : {α : Type u_1} → {ε : Type u_2} → (α → Bool) → Lean.AsyncList ε α → Lean.Server.ServerTask (Except ε (Option α))
-- Init.Data.Range.Polymorphic.Basic
/-- Checks whether the range contains any value.

This function returns a meaningful value given `LawfulUpwardEnumerable` and
`LawfulUpwardEnumerableLE` instances.
 -/
Std.Rcc.isEmpty : {α : Type u} → [inst : LE α] → [DecidableLE α] → [Std.PRange.UpwardEnumerable α] → Std.Rcc α → Bool
-- Mathlib.Data.Set.Sigma
Set.mk_preimage_sigma : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι},
  i ∈ s → Sigma.mk i ⁻¹' s.sigma t = t i
-- Batteries.Data.List.Count
List.leftInverse_sigmaCountToIdx_idxToSigmaCount : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : ReflBEq α] {xs : List α},
  Function.LeftInverse xs.sigmaCountToIdx xs.idxToSigmaCount
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.lowerCentralSeries_eq_bot_iff_nilpotencyClass_le : ∀ {G : Type u_1} [inst : AddGroup G] [hG : AddGroup.IsNilpotent G] {n : ℕ},
  ⊤.lowerCentralSeries n = ⊥ ↔ AddGroup.nilpotencyClass G ≤ n
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
DerivedCategory.instIsLEObjSingleFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (X : C) (n : ℤ), ((DerivedCategory.singleFunctor C n).obj X).IsLE n
-- Mathlib.CategoryTheory.Limits.Constructions.EpiMono
/-- If `F` preserves pushouts, then it preserves epimorphisms.  -/
CategoryTheory.preserves_epi_of_preservesColimit : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y)
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f f) F] [CategoryTheory.Epi f],
  CategoryTheory.Epi (F.map f)
-- Mathlib.Algebra.Lie.OfAssociative
LieAlgebra.ad_pow_lie : ∀ (R : Type u) {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x y z : L) (n : ℕ),
  ((LieAlgebra.ad R L) x ^ n) ⁅y, z⁆ =
    ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n,
      n.choose ij.1 • ⁅((LieAlgebra.ad R L) x ^ ij.1) y, ((LieAlgebra.ad R L) x ^ ij.2) z⁆
-- Mathlib.Order.CompleteBooleanAlgebra
/-- A completely distributive lattice is a complete lattice whose `⨅` and `⨆`
distribute over each other.  -/
CompletelyDistribLattice : Type u → Type u
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G]
  {ν : MeasureTheory.Measure α},
  MeasureTheory.IsFundamentalDomain G s μ →
    ν.AbsolutelyContinuous μ → (MeasureTheory.Measure.sum fun g => ν.restrict (g • s)) = ν
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
/-- The parallelepiped spanned by a basis, as a compact set with nonempty interior.  -/
Module.Basis.parallelepiped : {ι : Type u_1} →
  {E : Type u_3} →
    [Fintype ι] →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] → Module.Basis ι ℝ E → TopologicalSpace.PositiveCompacts E
-- Mathlib.Analysis.Normed.Module.FiniteDimension
/-- The set of injective continuous linear maps `E → F` is open,
if `E` is finite-dimensional over a complete field.  -/
ContinuousLinearMap.isOpen_injective : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace 𝕜]
  [FiniteDimensional 𝕜 E], IsOpen {L | Function.Injective ⇑L}
-- Mathlib.Data.Rel
SetRel.isSymm_comp_self : ∀ {α : Type u_1} {R : SetRel α α} [R.IsSymm], (R.comp R).IsSymm
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.Monoidal.ε_of_cartesianMonoidalCategory : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] [inst_5 : CategoryTheory.Limits.PreservesFiniteProducts F],
  CategoryTheory.Functor.LaxMonoidal.ε F = (CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso F).inv
-- Mathlib.Algebra.Star.Basic
StarRing.toStarMul : {R : Type u} → {inst : NonUnitalNonAssocSemiring R} → [self : StarRing R] → StarMul R
-- Mathlib.Analysis.Seminorm
Seminorm.instIsOrderedSMulOfIsOrderedModuleReal : ∀ {R : Type u_1} {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E]
  [inst_3 : SMul R ℝ] [inst_4 : SMul R NNReal] [inst_5 : IsScalarTower R NNReal ℝ] [inst_6 : Preorder R]
  [inst_7 : Zero R] [IsOrderedModule R ℝ], IsOrderedSMul R (Seminorm 𝕜 E)
-- Lean.Meta.Match.Match
/-- Try to solve the problem by using the first alternative whose pending constraints can be resolved.
 -/
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.processLeaf : Lean.Meta.Match.Problem → StateRefT' IO.RealWorld Lean.Meta.Match.State Lean.MetaM Unit
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_mul_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : StrongNormalizedGCDMonoid α] (a b c : α),
  lcm (b * a) (c * a) = lcm b c * normalize a
-- Mathlib.Analysis.Complex.Norm
Complex.lim_eq_lim_im_add_lim_re : ∀ (f : CauSeq ℂ fun x => ‖x‖), f.lim = ↑(Complex.cauSeqRe f).lim + ↑(Complex.cauSeqIm f).lim * Complex.I
-- Mathlib.Computability.Halting
ComputablePred.rice₂ : ∀ (C : Set Nat.Partrec.Code),
  (∀ (cf cg : Nat.Partrec.Code), cf.eval = cg.eval → (cf ∈ C ↔ cg ∈ C)) →
    ((ComputablePred fun c => c ∈ C) ↔ C = ∅ ∨ C = Set.univ)
-- Mathlib.Order.RelClasses
/-- Derive a `WellFoundedRelation` instance from an `isWellFounded` instance.  -/
IsWellFounded.toWellFoundedRelation : {α : Type u} → (r : α → α → Prop) → [IsWellFounded α r] → WellFoundedRelation α
-- Aesop.Index.Basic
Aesop.IndexMatchLocation.instOrd : Ord Aesop.IndexMatchLocation
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
LinearEquiv.coe_ofInjectiveOfFinrankEq : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {V' : Type u_1}
  [inst_3 : AddCommGroup V'] [inst_4 : Module K V'] [inst_5 : FiniteDimensional K V'] (f : V →ₗ[K] V')
  (hinj : Function.Injective ⇑f) (hrank : Module.finrank K V = Module.finrank K V'),
  ↑(LinearEquiv.ofInjectiveOfFinrankEq f hinj hrank) = f
-- Lean.Meta.Tactic.Grind.Main
_private.Lean.Meta.Tactic.Grind.Main.0.Lean.Meta.Grind.countersToMessageData : String → Lean.Name → Array (Lean.Name × ℕ) → Lean.MetaM Lean.MessageData
-- Mathlib.Algebra.Algebra.Basic
/-- The `CommRing` structure on a `CommSemiring` induced by a ring morphism from a `CommRing`.  -/
RingHom.commSemiringToCommRing : {R : Type u_4} → {A : Type u_5} → [inst : CommRing R] → [inst_1 : CommSemiring A] → (R →+* A) → CommRing A
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_extract : ∀ {n : ℕ} (hi lo : ℕ) (x : BitVec n) (i : ℕ),
  (BitVec.extractLsb hi lo x).getLsbD i = (decide (i ≤ hi - lo) && x.getLsbD (lo + i))
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
addOrderOf_eq_card_of_forall_mem_zmultiples : ∀ {α : Type u_1} [inst : AddGroup α] {g : α}, (∀ (x : α), x ∈ AddSubgroup.zmultiples g) → addOrderOf g = Nat.card α
-- Mathlib.Algebra.Group.TransferInstance
Equiv.pow.eq_1 : ∀ (M : Type u_1) {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : Pow β M],
  Equiv.pow M e = { pow := fun x n => e.invFun (e.toFun x ^ n) }
-- Init.Data.UInt.Basic
instXorOpUInt32 : XorOp UInt32
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.OmissionReason.proof : Lean.PrettyPrinter.Delaborator.OmissionReason
-- Mathlib.Topology.IsLocalHomeomorph
IsLocalHomeomorphOn.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {g : Y → Z} {f : X → Y} {s : Set X} {t : Set Y},
  IsLocalHomeomorphOn g t → IsLocalHomeomorphOn f s → Set.MapsTo f s t → IsLocalHomeomorphOn (g ∘ f) s
-- Mathlib.Combinatorics.Matroid.Map
Matroid.map_emptyOn : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), (Matroid.emptyOn α).map f ⋯ = Matroid.emptyOn β
-- Init.Data.BitVec.Lemmas
BitVec.toNat_allOnes : ∀ {v : ℕ}, (BitVec.allOnes v).toNat = 2 ^ v - 1
-- Mathlib.Topology.LocallyConstant.Basic
/-- Given two closed sets covering a topological space, and locally constant maps on these two sets,
then if these two locally constant maps agree on the intersection, we get a piecewise defined
locally constant map on the whole space.

TODO: Generalise this construction to `ContinuousMap`.  -/
LocallyConstant.piecewise : {X : Type u_1} →
  {Z : Type u_3} →
    [inst : TopologicalSpace X] →
      {C₁ C₂ : Set X} →
        IsClosed C₁ →
          IsClosed C₂ →
            C₁ ∪ C₂ = Set.univ →
              (f : LocallyConstant (↑C₁) Z) →
                (g : LocallyConstant (↑C₂) Z) →
                  (∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩) →
                    [DecidablePred fun x => x ∈ C₁] → LocallyConstant X Z
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.tensorObj_ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X R : C}
  {S T : CategoryTheory.Over X} (f₁ f₂ : R ⟶ (CategoryTheory.MonoidalCategoryStruct.tensorObj S T).left),
  CategoryTheory.CategoryStruct.comp f₁ (CategoryTheory.Limits.pullback.fst S.hom T.hom) =
      CategoryTheory.CategoryStruct.comp f₂ (CategoryTheory.Limits.pullback.fst S.hom T.hom) →
    CategoryTheory.CategoryStruct.comp f₁ (CategoryTheory.Limits.pullback.snd S.hom T.hom) =
        CategoryTheory.CategoryStruct.comp f₂ (CategoryTheory.Limits.pullback.snd S.hom T.hom) →
      f₁ = f₂
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- The completed Riemann zeta function, `Λ(s)`, which satisfies
`Λ(s) = π ^ (-s / 2) Γ(s / 2) ζ(s)` (up to a minor correction at `s = 0`).  -/
completedRiemannZeta : ℂ → ℂ
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.mkDiscr : Lean.Name → Lean.Elab.TermElabM (Lean.TSyntax `Lean.Parser.Term.matchDiscr)
-- Mathlib.Order.Concept
Concept.instLattice : {α : Type u_2} → {β : Type u_3} → {r : α → β → Prop} → Lattice (Concept α β r)
-- Init.Grind.Ring.Basic
Lean.Grind.IsCharP.intCast_ext_iff : ∀ (p : ℕ) {α : Type u} [inst : Lean.Grind.Ring α] [Lean.Grind.IsCharP α p] {x y : ℤ}, ↑x = ↑y ↔ x % ↑p = y % ↑p
-- Mathlib.Data.Finsupp.Notation
Finsupp.fun₀.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instDivisionMonoid.eq_1 : ∀ {α : Type u_1} [inst : DivisionMonoid α],
  OrderDual.instDivisionMonoid =
    { toDivInvMonoid := OrderDual.instDivInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯ }
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomMulAct.instMulDistribMulActionAEEqFun : {M : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : MeasurableSpace α] →
        {μ : MeasureTheory.Measure α} →
          [inst_1 : TopologicalSpace β] →
            [inst_2 : Monoid M] →
              [inst_3 : MulAction M α] →
                [MeasurableConstSMul M α] →
                  [MeasureTheory.SMulInvariantMeasure M α μ] →
                    [inst_6 : Monoid β] → [inst_7 : ContinuousMul β] → MulDistribMulAction Mᵈᵐᵃ (α →ₘ[μ] β)
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- Suppose `f` is a sequence of functions that converges in measure to `g`. If `f` is
`UniformIntegrable`, then `g` is in `Lp`.  -/
MeasureTheory.UniformIntegrable.memLp_of_tendstoInMeasure : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {p : ENNReal} {κ : Type u_4} {u : Filter κ} [u.NeBot] [u.IsCountablyGenerated] {f : κ → α → β} {g : α → β},
  MeasureTheory.UniformIntegrable f p μ → MeasureTheory.TendstoInMeasure μ f u g → MeasureTheory.MemLp g p μ
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.exists_coroot_ne : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  (S : Type u_5) [inst_6 : CommRing S] [IsDomain R] [IsDomain S] [inst_9 : Algebra S R] [inst_10 : FaithfulSMul S R]
  [inst_11 : P.IsValuedIn S] [inst_12 : Module S M] [inst_13 : IsScalarTower S R M] [inst_14 : Module S N]
  [IsScalarTower S R N] [P.IsAnisotropic] {x : ↥(P.rootSpan S)}, x ≠ 0 → ∃ i, (P.coroot'In S i) x ≠ 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → γ a} {k : α}
  {h' : k ∈ Std.DTreeMap.Raw.map f t} (h : t.WF), (Std.DTreeMap.Raw.map f t).get k h' = f k (t.get k ⋯)
-- Init.Data.Vector.Lemmas
Vector.flatten_singleton : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n}, #v[xs].flatten = Vector.cast ⋯ xs
-- Mathlib.Data.Nat.PrimeFin
Nat.primeFactors_mono : ∀ {m n : ℕ}, m ∣ n → n ≠ 0 → m.primeFactors ⊆ n.primeFactors
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `antivaryOn_neg`. -/
AntivaryOn.neg : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] {s : Set ι} {f : ι → α} {g : ι → β},
  AntivaryOn f g s → AntivaryOn (-f) (-g) s
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.mk.injEq : ∀ {α : Type u} {β : Type v} {cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw._auto_1}
  (inner inner_1 : Std.DTreeMap.Raw α (fun x => β) cmp), ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.Computability.Primrec.Basic
/-- A subtype of a primitive recursive predicate is `Primcodable`.  -/
Primcodable.subtype : {α : Type u_1} → [inst : Primcodable α] → {p : α → Prop} → [DecidablePred p] → PrimrecPred p → Primcodable (Subtype p)
-- Mathlib.Combinatorics.Tiling.Tile
/-- An induction principle to deduce results for `PlacedTile` from those given an index and an
element of `G`, used with `induction pt using PlacedTile.induction_on`.  -/
DiscreteTiling.PlacedTile.induction_on : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} {ppt : DiscreteTiling.PlacedTile ps → Prop} (pt : DiscreteTiling.PlacedTile ps),
  (∀ (i : ιₚ) (gx : G), ppt { index := i, groupElts := ↑gx }) → ppt pt
-- Mathlib.Data.List.Basic
List.exists_mem_cons_of : ∀ {α : Type u} {p : α → Prop} {a : α} (l : List α), p a → ∃ x ∈ a :: l, p x
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.AdicCauchySequence.instNeg : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Neg (AdicCompletion.AdicCauchySequence I M)
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofReal_one : ENNReal.ofReal 1 = 1
-- Mathlib.Algebra.Order.Star.Basic
smul_mem_closure_star_mul : ∀ {R : Type u_1} {A : Type u_2} [inst : Semiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [StarModule R A] [IsScalarTower R A A] [SMulCommClass R A A] {r : R},
  r ∈ AddSubmonoid.closure (Set.range fun s => star s * s) →
    ∀ {a : A},
      a ∈ AddSubmonoid.closure (Set.range fun s => star s * s) →
        r • a ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.proj.sizeOf_spec : ∀ (i : ℕ) (x : Lean.IR.VarId), sizeOf (Lean.IR.Expr.proj i x) = 1 + sizeOf i + sizeOf x
-- Mathlib.Algebra.Group.TypeTags.Hom
MonoidHom.toAdditiveLeft_apply_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : MulOneClass α] [inst_1 : AddZeroClass β] (a : α →* Multiplicative β)
  (a_1 : Additive α), (MonoidHom.toAdditiveLeft a) a_1 = Multiplicative.toAdd (a (Additive.toMul a_1))
-- Mathlib.Order.Directed
directedOn_univ : ∀ {α : Type u_1} {r : α → α → Prop} [IsDirected α r], DirectedOn r Set.univ
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- Range of an `AlgHom` as a subalgebra.  -/
AlgHom.range : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] → [inst_3 : Semiring B] → [inst_4 : Algebra R B] → (A →ₐ[R] B) → Subalgebra R B
-- Mathlib.Analysis.Calculus.Deriv.Star
/-- If `f` has derivative `f'` at `z`, then `star ∘ f ∘ conj` has derivative `star f'` at
`conj z`.  -/
HasDerivAt.star_conj : ∀ {𝕜 : 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] {x : 𝕜} [NormedStarGroup 𝕜]
  {f : 𝕜 → F} {f' : F}, HasDerivAt f f' x → HasDerivAt (star ∘ f ∘ ⇑(starRingEnd 𝕜)) (star f') ((starRingEnd 𝕜) x)
-- Std.Data.DTreeMap.Internal.Cell
/-- Type for representing the place in a tree map where a mapping for `k` could live.
Internal implementation detail of the tree map.
 -/
Std.DTreeMap.Internal.Cell : (α : Type u) → [Ord α] → (α → Type v) → (α → Ordering) → Type (max u v)
-- Mathlib.Data.Nat.Init
/-- Given `P : ℕ → ℕ → Sort*`, if we have `P m 0` and `P 0 n` for all `m n : ℕ`, and for any
`m n : ℕ` we can extend `P` from `(m, n + 1)` and `(m + 1, n)` to `(m + 1, n + 1)` then we have
`P m n` for all `m n : ℕ`.

Note that for non-`Prop` output it is preferable to use the equation compiler directly if possible,
since this produces equation lemmas.  -/
Nat.pincerRecursion : {P : ℕ → ℕ → Sort u_1} →
  ((m : ℕ) → P m 0) → ((n : ℕ) → P 0 n) → ((x y : ℕ) → P x y.succ → P x.succ y → P x.succ y.succ) → (n m : ℕ) → P n m
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.Iterators.Types.Map.instProductive : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad n] [inst_1 : Std.Iterator α m β]
  {lift : ⦃α : Type w⦄ → m α → n α} {f : β → Std.Iterators.PostconditionT n γ} [Std.Iterators.Productive α m],
  Std.Iterators.Productive (Std.Iterators.Types.Map α m n lift f) n
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Section.mk.inj : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} {inst : Group N} {inst_1 : Group E} {inst_2 : Group G}
  {S : GroupExtension N E G} {toFun : G → E} {rightInverse_rightHom : Function.RightInverse toFun ⇑S.rightHom}
  {toFun_1 : G → E} {rightInverse_rightHom_1 : Function.RightInverse toFun_1 ⇑S.rightHom},
  { toFun := toFun, rightInverse_rightHom := rightInverse_rightHom } =
      { toFun := toFun_1, rightInverse_rightHom := rightInverse_rightHom_1 } →
    toFun = toFun_1
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pullback_inter : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} (S R : CategoryTheory.Sieve X),
  CategoryTheory.Sieve.pullback f (S ⊓ R) = CategoryTheory.Sieve.pullback f S ⊓ CategoryTheory.Sieve.pullback f R
-- Init.Data.UInt.Lemmas
UInt32.toNat_ofNatTruncate_of_lt : ∀ {n : ℕ}, n < UInt32.size → (UInt32.ofNatClamp n).toNat = n
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.prod_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  {C : Type u_4} [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : TopologicalSpace C] (f₁ : A →A[R] B)
  (f₂ : A →A[R] C) (x : A), (f₁.prod f₂) x = (f₁ x, f₂ x)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.step_supports : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Λ] [inst_1 : Inhabited Γ]
  (M : Λ → Turing.TM1.Stmt Γ Λ σ) {S : Finset Λ},
  Turing.TM1.Supports M S →
    ∀ {c c' : Turing.TM1.Cfg Γ Λ σ}, c' ∈ Turing.TM1.step M c → c.l ∈ Finset.insertNone S → c'.l ∈ Finset.insertNone S
-- Mathlib.Algebra.Category.MonCat.Limits
MonCat.hasLimits : CategoryTheory.Limits.HasLimits MonCat
-- Init.Data.List.Impl
List.findRev?.eq_2 : ∀ {α : Type u} (p : α → Bool) (a : α) (as : List α),
  List.findRev? p (a :: as) =
    match List.findRev? p as with
    | some b => some b
    | none => if p a = true then some a else none
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.continuousSMul : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {p : SeminormFamily 𝕜 E ι}, WithSeminorms p → ContinuousSMul 𝕜 E
-- Mathlib.Data.Multiset.MapFold
Multiset.map_zero : ∀ {α : Type u_1} {β : Type v} (f : α → β), Multiset.map f 0 = 0
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn_ric : ∀ {α β : Type u} {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred]
  [inst_4 : Std.PRange.Least? α] [inst_5 : LE α] [inst_6 : DecidableLE α] [inst_7 : Std.PRange.UpwardEnumerable α]
  [inst_8 : Std.Rxc.IsAlwaysFinite α] [inst_9 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_10 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_11 : Std.PRange.LawfulUpwardEnumerableLE α]
  {xs : Std.Ric α} {init : β} {f : α → β → m (ForInStep β)} (inv : Std.Internal.Do.Invariant xs.toList β Pred)
  {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Adjunction.functorialityUnit_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {J : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} J] (K : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cocone K),
  ((adj.functorialityUnit K).app c).hom = adj.unit.app c.pt