mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Basic
String.startInclusive_sliceTo : ∀ {s : String} {p : s.Pos}, (s.sliceTo p).startInclusive = s.startPos
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.DeclValue.extern.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {externAttrData externAttrData_1 : Lean.ExternAttrData},
  Lean.Compiler.LCNF.DeclValue.extern externAttrData = Lean.Compiler.LCNF.DeclValue.extern externAttrData_1 →
    externAttrData = externAttrData_1
-- Lean.Parser.Extension
Lean.Parser.registerBuiltinNodeKind : Lean.SyntaxNodeKind → IO Unit
-- Mathlib.CategoryTheory.Action.Basic
CategoryTheory.Functor.mapActionCongr_inv : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {W : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} W] (G : Type u_3) [inst_2 : Monoid G] {F F' : CategoryTheory.Functor V W}
  (e : F ≅ F'),
  (CategoryTheory.Functor.mapActionCongr G e).inv =
    { app := fun X => (Action.mkIso (e.app X.V) ⋯).inv, naturality := ⋯ }
-- Mathlib.Analysis.Normed.Group.Bounded
Bornology.IsBounded.exists_pos_norm_lt : ∀ {E : Type u_2} [inst : SeminormedAddGroup E] {s : Set E}, Bornology.IsBounded s → ∃ R > 0, ∀ x ∈ s, ‖x‖ < R
-- Aesop.Stats.Basic
Aesop.instInhabitedForwardRuleStateStats : Inhabited Aesop.ForwardRuleStateStats
-- Mathlib.CategoryTheory.ConcreteCategory.Bundled
CategoryTheory.Bundled.mk.inj : ∀ {c : Type u → Type v} {α : Type u} {str : autoParam (c α) CategoryTheory.Bundled.str._autoParam} {α_1 : Type u}
  {str_1 : autoParam (c α_1) CategoryTheory.Bundled.str._autoParam},
  { α := α, str := str } = { α := α_1, str := str_1 } → α = α_1 ∧ str ≍ str_1
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.map_natCast : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (n : ℕ), v ↑n = ↑n
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
/-- If `G` is a finite Galois group for `L/K` and `N` is a normal subgroup of `G` that is a
Galois group for `L/F`, then the quotient group `G ⧸ N` is a Galois group for `F/K`.  -/
IsGaloisGroup.instQuotientSubgroupSubtypeMemIntermediateFieldOfFinite : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] (F : IntermediateField K L) (N : Subgroup G)
  [inst_5 : N.Normal] [inst_6 : IsGaloisGroup (↥N) (↥F) L] [Finite G] [IsGaloisGroup G K L], IsGaloisGroup (G ⧸ N) K ↥F
-- Mathlib.Topology.UnitInterval
_private.Mathlib.Topology.UnitInterval.0.Set.Icc.eq_convexComb.zero_le : ∀ {a b : ℝ} {x y z : ↑(Set.Icc a b)}, x ≤ y → y ≤ z → 0 ≤ (↑y - ↑x) / (↑z - ↑x)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.notValue.injEq : ∀ (bvarIdx : ℕ) (strict : Bool) (bvarIdx_1 : ℕ) (strict_1 : Bool),
  (Lean.Meta.Grind.EMatchTheoremConstraint.notValue bvarIdx strict =
      Lean.Meta.Grind.EMatchTheoremConstraint.notValue bvarIdx_1 strict_1) =
    (bvarIdx = bvarIdx_1 ∧ strict = strict_1)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.locallyIntegrableOn_univ : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X},
  MeasureTheory.LocallyIntegrableOn f Set.univ μ ↔ MeasureTheory.LocallyIntegrable f μ
-- Mathlib.FieldTheory.Normal.Defs
Normal.out : ∀ {F : Type u_1} {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K],
  Normal F K → ∀ (x : K), IsIntegral F x ∧ (Polynomial.map (algebraMap F K) (minpoly F x)).Splits
-- Batteries.Tactic.NoMatch
/-- The syntax `λ.` has been deprecated in favor of `nofun`.  -/
Batteries.Tactic.lambdaDot : Lean.ParserDescr
-- Lean.Meta.LazyDiscrTree
_private.Lean.Meta.LazyDiscrTree.0.Lean.Meta.LazyDiscrTree.getChildNgen.match_1.splitter : (motive : Lean.NameGenerator × Lean.NameGenerator → Sort u_1) →
  (x : Lean.NameGenerator × Lean.NameGenerator) → ((cngen ngen : Lean.NameGenerator) → motive (cngen, ngen)) → motive x
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderBaseChange.of_isPullback : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C}
  [self : P.IsStableUnderBaseChange] {X Y Y' S : C} {f : X ⟶ S} {g : Y ⟶ S} {f' : Y' ⟶ Y} {g' : Y' ⟶ X},
  CategoryTheory.IsPullback f' g' g f → P g → P g'
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- If `s : Finset (Fin n)` is a finite set of cardinality `k` and its complement has cardinality
`l`, then the space of continuous multilinear maps `G [×n]→L[𝕜] G'` of `n` variables is isomorphic
to the space of continuous multilinear maps `G [×k]→L[𝕜] G [×l]→L[𝕜] G'` of `k` variables taking
values in the space of continuous multilinear maps of `l` variables.  -/
ContinuousMultilinearMap.curryFinFinset : (𝕜 : Type u) →
  (G : Type wG) →
    (G' : Type wG') →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup G] →
          [inst_2 : NormedSpace 𝕜 G] →
            [inst_3 : NormedAddCommGroup G'] →
              [inst_4 : NormedSpace 𝕜 G'] →
                {k l n : ℕ} →
                  {s : Finset (Fin n)} → s.card = k → sᶜ.card = l → (G [×n]→L[𝕜] G') ≃ₗᵢ[𝕜] G [×k]→L[𝕜] G [×l]→L[𝕜] G'
-- Mathlib.Tactic.Simps.Basic
_private.Mathlib.Tactic.Simps.Basic.0.NameStruct.mk.sizeOf_spec : ∀ (parent : Lean.Name) (components : List String),
  sizeOf { parent := parent, components := components } = 1 + sizeOf parent + sizeOf components
-- Mathlib.NumberTheory.Dioph
IsPoly.add : ∀ {α : Type u_1} {f g : (α → ℕ) → ℤ}, IsPoly f → IsPoly g → IsPoly (f + g)
-- Mathlib.Data.Finsupp.Basic
Finsupp.comapDomain_surjective : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : Zero M] {f : α → β} (hf : Function.Injective f),
  Function.Surjective fun l => Finsupp.comapDomain f l ⋯
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation.unfold.eq_1 : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {op :
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl}
  (h : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation op)
  (hd? : Option (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl)),
  h.unfold hd? =
    Option.map
      (fun x =>
        match x with
        | ((exp, coef), op') => (exp, coef, op'))
      (Tactic.ComputeAsymptotics.Seq.FriendlyOperation.unfold h hd?)
-- Mathlib.Data.Set.Lattice
Set.iInter_subset_iInter₂ : ∀ {α : Type u_1} {ι : Sort u_5} (κ : ι → Sort u_12) (s : ι → Set α), ⋂ i, s i ⊆ ⋂ i, ⋂ x, s i
-- Mathlib.Topology.Algebra.WithZeroTopology
/-- The topology on a linearly ordered commutative group with a zero element adjoined.
A subset `U` is open if `0 ∉ U` or if there is an invertible element γ₀ such that
`{γ | γ < γ₀} ⊆ U`.  -/
WithZeroTopology.topologicalSpace : {Γ₀ : Type u_2} → [LinearOrderedCommGroupWithZero Γ₀] → TopologicalSpace Γ₀
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.tendsto_ae_map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β},
  AEMeasurable f μ → Filter.Tendsto f (MeasureTheory.ae μ) (MeasureTheory.ae (MeasureTheory.Measure.map f μ))
-- Init.Data.AC
_private.Init.Data.AC.0.Lean.Data.AC.evalList.match_1.eq_3 : ∀ (motive : List ℕ → Sort u_1) (x : ℕ) (xs : List ℕ) (h_1 : Unit → motive []) (h_2 : (x : ℕ) → motive [x])
  (h_3 : (x : ℕ) → (xs : List ℕ) → motive (x :: xs)),
  (xs = [] → False) →
    (match x :: xs with
      | [] => h_1 ()
      | [x] => h_2 x
      | x :: xs => h_3 x xs) =
      h_3 x xs
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.FullyFaithful.monObj.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C)
  [inst_5 : CategoryTheory.MonObj (F.obj X)],
  hF.monObj X =
    {
      one :=
        hF.preimage
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F) CategoryTheory.MonObj.one),
      mul :=
        hF.preimage
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X) CategoryTheory.MonObj.mul),
      one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
/-- Given a continuous function `f` in a subalgebra of `C(X, ℝ)`, postcomposing by a polynomial
gives another function in `A`.

This lemma proves something slightly more subtle than this:
we take `f`, and think of it as a function into the restricted target `Set.Icc (-‖f‖) ‖f‖)`,
and then postcompose with a polynomial function on that interval.
This is in fact the same situation as above, and so also gives a function in `A`.
 -/
ContinuousMap.polynomial_comp_attachBound_mem : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (f : ↥A)
  (g : Polynomial ℝ), (g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound ∈ A
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.map_lie₂ : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} {P : Type w₂} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : AddCommGroup P] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : LieRingModule L M] [inst_9 : LieRingModule L N]
  [inst_10 : LieRingModule L P] [inst_11 : LieAlgebra R L] [inst_12 : LieModule R L N] [inst_13 : LieModule R L P]
  (f : M →ₗ⁅R,L⁆ N →ₗ[R] P) (x : L) (m : M) (n : N), ⁅x, (f m) n⁆ = (f ⁅x, m⁆) n + (f m) ⁅x, n⁆
-- Mathlib.Order.Directed
DirectedOn.of_linearOrder : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Set α), DirectedOn (fun x1 x2 => x1 ≤ x2) s
-- Mathlib.Algebra.Module.Torsion.Basic
Module.IsTorsionBy.mk_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {r : R}
  [inst_3 : (Ideal.span {r}).IsTwoSided] (hM : Module.IsTorsionBy R M r) (b : R) (x : M),
  (Ideal.Quotient.mk (Ideal.span {r})) b • x = b • x
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Given a pair of additive monoid homomorphisms `f`, `g` such that `g.comp f = id`
and `f.comp g = id`, returns an additive equivalence with `toFun = f` and `invFun = g`.  This
constructor is useful if the underlying type(s) have specialized `ext` lemmas for additive
monoid homomorphisms.  -/
AddMonoidHom.toAddEquiv : {M : Type u_4} →
  {N : Type u_5} →
    [inst : AddZeroClass M] →
      [inst_1 : AddZeroClass N] →
        (f : M →+ N) → (g : N →+ M) → g.comp f = AddMonoidHom.id M → f.comp g = AddMonoidHom.id N → M ≃+ N
-- Mathlib.Analysis.Complex.Circle
Circle.instContinuousSMul : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MulAction ℂ α] [ContinuousSMul ℂ α], ContinuousSMul Circle α
-- Mathlib.RingTheory.Flat.Tensor
/-- An `R`-module `M` is flat if for all finitely generated ideals `I` of `R`,
the canonical map `I ⊗ M →ₗ M` is injective.  -/
Module.Flat.iff_lift_lsmul_comp_subtype_injective : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.Flat R M ↔
    ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(TensorProduct.lift (LinearMap.lsmul R M ∘ₗ Submodule.subtype I))
-- Mathlib.GroupTheory.GroupAction.Pointwise
/-- `preimage_smul_setₛₗ` when both scalars act by unit  -/
preimage_smul_setₛₗ_of_isUnit_isUnit : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [inst : Monoid M]
  [inst_1 : Monoid N] [inst_2 : MulAction M α] [inst_3 : MulAction N β] [inst_4 : FunLike F α β]
  [MulActionSemiHomClass F σ α β] {c : M} (f : F),
  IsUnit c → IsUnit (σ c) → ∀ (t : Set β), ⇑f ⁻¹' (σ c • t) = c • ⇑f ⁻¹' t
-- Mathlib.NumberTheory.FactorisationProperties
Nat.instDecidableDeficient : (n : ℕ) → Decidable n.Deficient
-- Mathlib.Algebra.Group.WithOne.Basic
WithZero.coeAddHom.eq_1 : ∀ {α : Type u} [inst : Add α], WithZero.coeAddHom = { toFun := WithZero.coe, map_add' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.initial_op_of_final : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Final], F.op.Initial
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffWithinAt.of_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {m n : WithTop ℕ∞}, ContMDiffWithinAt I I' n f s x → m ≤ n → ContMDiffWithinAt I I' m f s x
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, returning `none` if no such pair exists.
 -/
Std.DTreeMap.Const.getEntryGE? : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap α (fun x => β) cmp → α → Option (α × β)
-- Init.Data.Range.Polymorphic.PRange
Std.instDecidableEqRii : {α : Type u_1} → [DecidableEq α] → DecidableEq (Std.Rii α)
-- Mathlib.Algebra.Group.Torsion
pow_eq_one_iff : ∀ {M : Type u_1} [inst : Monoid M] [IsMulTorsionFree M] {n : ℕ} {a : M}, a ^ n = 1 ↔ a = 1 ∨ n = 0
-- Mathlib.Topology.Constructions
/-- The product of a neighborhood of `s` and a neighborhood of `t` is a neighborhood of `s ×ˢ t`,
formulated in terms of a filter inequality.  -/
nhdsSet_prod_le : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (s : Set X) (t : Set Y),
  nhdsSet (s ×ˢ t) ≤ nhdsSet s ×ˢ nhdsSet t
-- Mathlib.Analysis.Convex.Deriv
ConcaveOn.leftDeriv_le_slope : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  ConcaveOn ℝ S f →
    x ∈ S → y ∈ S → x < y → DifferentiableWithinAt ℝ f (Set.Iio y) y → derivWithin f (Set.Iio y) y ≤ slope f x y
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.instInhabitedRefreshState : Inhabited ProofWidgets.RefreshComponent.RefreshState
-- Init.Data.String.Legacy
_private.Init.Data.String.Legacy.0.String.splitOnAux.eq_def : ∀ (s sep : String) (b i j : String.Pos.Raw) (r : List String),
  s.splitOnAux sep b i j r =
    if String.Pos.Raw.atEnd s i = true then
      have r := String.Pos.Raw.extract s b i :: r;
      r.reverse
    else
      if (String.Pos.Raw.get s i == String.Pos.Raw.get sep j) = true then
        have i := String.Pos.Raw.next s i;
        have j := String.Pos.Raw.next sep j;
        if String.Pos.Raw.atEnd sep j = true then
          s.splitOnAux sep i i 0 (String.Pos.Raw.extract s b (i.unoffsetBy j) :: r)
        else s.splitOnAux sep b i j r
      else s.splitOnAux sep b (String.Pos.Raw.next s (i.unoffsetBy j)) 0 r
-- Mathlib.RingTheory.Localization.BaseChange
/-- The `S`-isomorphism `S ⊗[R] Rᵣ ≃ₐ Sᵣ`.  -/
IsLocalization.Away.tensorRightEquiv : {R : Type u_7} →
  (S : Type u_8) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (r : R) →
            (A : Type u_9) →
              [inst_3 : CommSemiring A] →
                [inst_4 : Algebra R A] →
                  [IsLocalization.Away r A] → TensorProduct R A S ≃ₐ[S] Localization.Away ((algebraMap R S) r)
-- Mathlib.AlgebraicGeometry.Gluing
_private.Mathlib.AlgebraicGeometry.Gluing.0.AlgebraicGeometry.Scheme.IsLocallyDirected.«term↓_» : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isTrail_cons : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w),
  (SimpleGraph.Walk.cons h p).IsTrail ↔ p.IsTrail ∧ s(u, v) ∉ p.edges
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
/-- Forgetting functor to `Cat`  -/
CategoryTheory.Grpd.forgetToCat : CategoryTheory.Functor CategoryTheory.Grpd CategoryTheory.Cat
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instInhabited : {G : Type u_1} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → Inhabited (OpenAddSubgroup G)
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.leftNegEquiv_symm_fromLeftNeg : ∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S.leftNeg),
  (S.leftNegEquiv hS).symm (S.fromLeftNeg x) = x
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.norm_toBCF_eq_norm : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  {f : ZeroAtInftyContinuousMap α β}, ‖f.toBCF‖ = ‖f‖
-- Lean.Meta.Match.MatcherApp.Basic
Lean.Meta.MatcherApp.mk : Lean.Meta.MatcherInfo →
  Lean.Name →
    Array Lean.Level →
      Array Lean.Expr → Lean.Expr → Array Lean.Expr → Array Lean.Expr → Array Lean.Expr → Lean.Meta.MatcherApp
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of an inner regular measure under map of a left action is again inner regular.  -/
MeasureTheory.innerRegular_map_smul : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  {α : Type u_3} [inst_3 : Monoid α] [inst_4 : MulAction α G] [ContinuousConstSMul α G] [μ.InnerRegular] (a : α),
  (MeasureTheory.Measure.map (fun x => a • x) μ).InnerRegular
-- Mathlib.Analysis.Normed.Group.Continuity
closure_zero_eq : ∀ {E : Type u_4} [inst : SeminormedAddGroup E], closure {0} = {x | ‖x‖ = 0}
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.toIntSubmodule_toAddSubgroup : ∀ {R : Type u_4} {M : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M),
  AddSubgroup.toIntSubmodule N.toAddSubgroup = Submodule.restrictScalars ℤ N
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.standardσ_comp_standardσ : ∀ (L₁ L₂ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + L₂.length = m₂),
  CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.standardσ L₁ h) (SimplexCategoryGenRel.standardσ L₂ h') =
    SimplexCategoryGenRel.standardσ (L₂ ++ L₁) ⋯
-- Mathlib.Data.Vector.Defs
/-- The empty vector with elements of type `α`  -/
List.Vector.nil : {α : Type u_1} → List.Vector α 0
-- Mathlib.Order.ScottContinuity
ScottContinuousOn.fst : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {D : Set (Set (α × β))},
  ScottContinuousOn D Prod.fst
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.ComonObj.comul_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} (X : C)
  [self : CategoryTheory.ComonObj X],
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.ComonObj.comul) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.ComonObj.comul X)
        (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {A B : CategoryTheory.CommMon C} {f g : A ⟶ B},
  f = g ↔ f.hom.hom = g.hom.hom
-- Mathlib.LinearAlgebra.TensorPower.Symmetric
SymmetricPower.instAddCommGroup : (ι R : Type u) →
  [inst : CommRing R] →
    (M : Type v) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → AddCommGroup (SymmetricPower R ι M)
-- Mathlib.Topology.MetricSpace.Isometry
/-- An isometry from a complete emetric space is a closed embedding  -/
Isometry.isClosedEmbedding : ∀ {α : Type u} {γ : Type w} [inst : EMetricSpace α] [CompleteSpace α] [inst_2 : EMetricSpace γ] {f : α → γ},
  Isometry f → Topology.IsClosedEmbedding f
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- Another auxiliary lemma for `Basis.le_span`, which does not require assuming the basis is finite,
but still assumes we have a finite spanning set.
 -/
basis_le_span' : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [RankCondition R]
  {ι : Type u_2} (b : Module.Basis ι R M) {w : Set M} [inst_4 : Fintype ↑w],
  Submodule.span R w = ⊤ → Cardinal.mk ι ≤ ↑(Fintype.card ↑w)
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeSigma.match_3.eq_2 : ∀ (motive : (n : ℕ) → (f : Fin n → ℕ) → (i : Fin n) × Fin (f i) → Sort u_1) (n : ℕ) (f : Fin (n + 1) → ℕ) (i : ℕ)
  (hi : i + 1 < n + 1) (j : Fin (f ⟨i + 1, hi⟩))
  (h_1 : (a : ℕ) → (f : Fin (a + 1) → ℕ) → (j : Fin (f 0)) → motive a.succ f ⟨⟨0, ⋯⟩, j⟩)
  (h_2 :
    (n : ℕ) →
      (f : Fin (n + 1) → ℕ) →
        (i : ℕ) → (hi : i + 1 < n + 1) → (j : Fin (f ⟨i + 1, hi⟩)) → motive n.succ f ⟨⟨i.succ, hi⟩, j⟩),
  (match n.succ, f, ⟨⟨i.succ, hi⟩, j⟩ with
    | a.succ, f, ⟨⟨0, ⋯⟩, j⟩ => h_1 a f j
    | n.succ, f, ⟨⟨i.succ, hi⟩, j⟩ => h_2 n f i hi j) =
    h_2 n f i hi j
-- Mathlib.MeasureTheory.Group.Arithmetic
measurable_add_unop : ∀ {α : Type u_2} [inst : MeasurableSpace α], Measurable AddOpposite.unop
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.instLinearOrder : LinearOrder Ordinal.{u_1}
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.instCategoryAffineScheme : CategoryTheory.Category.{u_1, u_1 + 1} AlgebraicGeometry.AffineScheme
-- Mathlib.Topology.Sheaves.Flasque
/-- Given a short exact sequence of sheaves, `0 ⟶ 𝓕 ⟶ 𝓖 ⟶ 𝓗 ⟶ 0`, if `𝓕` is flasque then
`𝓖(U) ⟶ 𝓗(U)` is surjective, for any open `U`.  -/
TopCat.Sheaf.IsFlasque.epi_of_shortExact : ∀ {X : TopCat} {U : TopologicalSpace.Opens ↑X} {S : CategoryTheory.ShortComplex (TopCat.Sheaf AddCommGrpCat X)},
  S.ShortExact → ∀ [S.X₁.IsFlasque], CategoryTheory.Epi (S.g.hom.app (Opposite.op U))
-- Init.Data.BitVec.Lemmas
BitVec.neg_ne_iff_ne_neg : ∀ {w : ℕ} {x y : BitVec w}, -x ≠ y ↔ x ≠ -y
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lift_eq_aleph_one : ∀ {c : Cardinal.{u}}, Cardinal.lift.{v, u} c = Cardinal.aleph 1 ↔ c = Cardinal.aleph 1
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.coe_mem_source : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (e' : Bundle.Pretrivialization F Bundle.TotalSpace.proj) {b : B} {y : E b}, ⟨b, y⟩ ∈ e'.source ↔ b ∈ e'.baseSet
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
/-- If `f` and `g` are monic and splits, then `Res(f, g) = ∏ (α - β)`,
where `α` and `β` runs through the roots of `f` and `g` respectively.  -/
Polynomial.resultant_eq_prod_roots_sub : ∀ {K : Type u_3} [inst : Field K] (f g : Polynomial K),
  f.Monic →
    g.Monic → f.Splits → g.Splits → f.resultant g = (Multiset.map (fun ij => ij.1 - ij.2) (f.roots ×ˢ g.roots)).prod
-- Mathlib.Topology.MetricSpace.Thickening
Metric.thickening_biUnion : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {ι : Type u_2} (δ : ℝ) (f : ι → Set α) (I : Set ι),
  Metric.thickening δ (⋃ i ∈ I, f i) = ⋃ i ∈ I, Metric.thickening δ (f i)
-- Mathlib.Geometry.Euclidean.Similarity
/-- In two similar triangles, all three corresponding angles are equal.  -/
Similar.angle_eq_all : ∀ {V₁ : Type u_2} {V₂ : Type u_3} {P₁ : Type u_4} {P₂ : Type u_5} [inst : NormedAddCommGroup V₁]
  [inst_1 : NormedAddCommGroup V₂] [inst_2 : InnerProductSpace ℝ V₁] [inst_3 : InnerProductSpace ℝ V₂]
  [inst_4 : MetricSpace P₁] [inst_5 : MetricSpace P₂] [inst_6 : NormedAddTorsor V₁ P₁] [inst_7 : NormedAddTorsor V₂ P₂]
  {a b c : P₁} {a' b' c' : P₂},
  Similar ![a, b, c] ![a', b', c'] →
    EuclideanGeometry.angle a b c = EuclideanGeometry.angle a' b' c' ∧
      EuclideanGeometry.angle b c a = EuclideanGeometry.angle b' c' a' ∧
        EuclideanGeometry.angle c a b = EuclideanGeometry.angle c' a' b'
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.mvars.delayed : Lean.Option Bool