mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.Primrec.Basic
Primrec.option_get : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {f : α → Option β}
  {h : ∀ (a : α), (f a).isSome = true}, Primrec f → Primrec fun a => (f a).get ⋯
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.comp_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] (g : β →ᵈ γ) (f : α →ᵈ β) (x : α), (g.comp f) x = g (f x)
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.instInhabited : {α : Type u_2} → [inst : TopologicalSpace α] → Inhabited (TopologicalSpace.Opens α)
-- Lean.Parser.Basic
Lean.Parser.instDecidableEqRecoveryContext.decEq : (x x_1 : Lean.Parser.RecoveryContext) → Decidable (x = x_1)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.mk.congr_simp : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [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]
  (toContinuousMultilinearMap toContinuousMultilinearMap_1 : ContinuousMultilinearMap R (fun x => M) N)
  (e_toContinuousMultilinearMap : toContinuousMultilinearMap = toContinuousMultilinearMap_1)
  (map_eq_zero_of_eq' : ∀ (v : ι → M) (i j : ι), v i = v j → i ≠ j → toContinuousMultilinearMap.toFun v = 0),
  { toContinuousMultilinearMap := toContinuousMultilinearMap, map_eq_zero_of_eq' := map_eq_zero_of_eq' } =
    { toContinuousMultilinearMap := toContinuousMultilinearMap_1, map_eq_zero_of_eq' := ⋯ }
-- Lean.Elab.Tactic.Omega.Core
_private.Lean.Elab.Tactic.Omega.Core.0.Lean.Elab.Tactic.Omega.Justification.bullet : String → String
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.solveCnstrs.go : Lean.MVarId → Lean.Meta.Match.Alt → StateRefT' IO.RealWorld Lean.Meta.Match.State Lean.MetaM Unit
-- Mathlib.Data.Set.Prod
Set.fst_image_prod : ∀ {α : Type u_1} {β : Type u_2} (s : Set β) {t : Set α}, t.Nonempty → Prod.fst '' s ×ˢ t = s
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.Uniformizer.valuation_gt_one : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] {v : Valuation A Γ}
  [hv : v.IsRankOneDiscrete] (self : v.Uniformizer), v.IsUniformizer ↑self.val
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.map_mconv_monoidHom : ∀ {M : Type u_2} {M' : Type u_3} {mM : MeasurableSpace M} [inst : Monoid M] [MeasurableMul₂ M]
  {mM' : MeasurableSpace M'} [inst_2 : Monoid M'] [MeasurableMul₂ M'] {μ ν : MeasureTheory.Measure M}
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] (L : M →* M'),
  Measurable ⇑L →
    MeasureTheory.Measure.map (⇑L) (μ.mconv ν) =
      (MeasureTheory.Measure.map (⇑L) μ).mconv (MeasureTheory.Measure.map (⇑L) ν)
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.lapply_apply : ∀ {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] (i : ι) (f : Π₀ (i : ι), M i), (DFinsupp.lapply i) f = f i
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddCommSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddCommSemigroup α],
  Colex.instAddCommSemigroup = { toAddSemigroup := Colex.instAddSemigroup, add_comm := ⋯ }
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.IsCycle.existsUnique_cycle_nontrivial_subtype : ∀ {α : Type u_1} [Finite α] [inst : DecidableEq α] {f : Equiv.Perm α}, f.IsCycle → ∃! s, (↑s).formPerm ⋯ = f
-- Mathlib.Algebra.Group.Pi.Basic
Pi.commGroup.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → CommGroup (f i)],
  Pi.commGroup = { toGroup := Pi.group, mul_comm := ⋯ }
-- Init.Data.SInt.Lemmas
Int64.toInt16_toInt32 : ∀ (n : Int64), n.toInt32.toInt16 = n.toInt16
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.one_rpow : ∀ (x : ℝ), 1 ^ x = 1
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
/-- The second exterior derivative of a sufficiently smooth differential form is zero.  -/
extDeriv_extDeriv_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ} {r : WithTop ℕ∞}
  {ω : E → E [⋀^Fin n]→L[𝕜] F} {x : E}, ContDiffAt 𝕜 r ω x → minSmoothness 𝕜 2 ≤ r → extDeriv (extDeriv ω) x = 0
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.ext : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  ⦃f g : L.ElementaryEmbedding M N⦄, (∀ (x : M), f x = g x) → f = g
-- Init.Notation
/-- `stx` is a builtin syntax category for syntax. This is the abbreviated
parser notation used inside `syntax` and `macro` declarations.  -/
Lean.Parser.Category.stx : Lean.Parser.Category
-- Lean.Util.ShareCommon
Lean.ShareCommon.ShareCommonT.monadShareCommon : {m : Type u_1 → Type u_2} → [Monad m] → MonadShareCommon (Lean.ShareCommon.ShareCommonT m)
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.FiniteMeasure.self_eq_mass_smul_normalize : ∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.FiniteMeasure Ω),
  μ = μ.mass • μ.normalize.toFiniteMeasure
-- Mathlib.Algebra.Module.GradedModule
DirectSum.Gmodule.add_smul : ∀ {ιA : Type u_1} {ιB : Type u_2} {A : ιA → Type u_3} {M : ιB → Type u_4} {inst : AddMonoid ιA} {inst_1 : VAdd ιA ιB}
  {inst_2 : (i : ιA) → AddMonoid (A i)} {inst_3 : (i : ιB) → AddMonoid (M i)} {inst_4 : GradedMonoid.GMonoid A}
  [self : DirectSum.Gmodule A M] {i : ιA} {j : ιB} (a a' : A i) (b : M j),
  GradedMonoid.GSMul.smul (a + a') b = GradedMonoid.GSMul.smul a b + GradedMonoid.GSMul.smul a' b
-- Mathlib.Tactic.GRewrite.Core
/-- The value  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.GRewriteLemma.proof : Mathlib.Tactic.GRewrite.GRewriteLemma✝ → Lean.Expr
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.zeckendorf.eq_1 : Nat.zeckendorf 0 = []
-- Mathlib.Topology.UniformSpace.Cauchy
CauchySeq.prodMk : ∀ {α : Type u} {β : Type v} [uniformSpace : UniformSpace α] {γ : Type u_1} [inst : UniformSpace β] [inst_1 : Preorder γ]
  {u : γ → α} {v : γ → β}, CauchySeq u → CauchySeq v → CauchySeq fun x => (u x, v x)
-- Mathlib.Geometry.Manifold.Diffeomorph
ModelWithCorners.coe_transContinuousLinearEquiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_5}
  [inst_5 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) (e : E ≃L[𝕜] E'),
  ↑(I.transContinuousLinearEquiv e) = ⇑e ∘ ↑I
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_inter!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β k},
        Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.inter! m₂).getD k fallback = fallback
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of a quotient of `G` is less or equal the nilpotency class of `G`.  -/
Group.nilpotencyClass_quotient_le : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : H.Normal] [_h : Group.IsNilpotent G],
  Group.nilpotencyClass (G ⧸ H) ≤ Group.nilpotencyClass G
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.conePointsIsoOfNatIso.eq_1 : ∀ {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.Cone F} {t : CategoryTheory.Limits.Cone G}
  (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) (w : F ≅ G),
  P.conePointsIsoOfNatIso Q w =
    { hom := CategoryTheory.Limits.IsLimit.map s Q w.hom, inv := CategoryTheory.Limits.IsLimit.map t P w.inv,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.needEscape : String → Bool
-- Mathlib.ModelTheory.Basic
/-- The homomorphism sends related elements to related elements  -/
FirstOrder.Language.Hom.map_rel' : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (self : L.Hom M N) {n : ℕ} (r : L.Relations n) (x : Fin n → M),
  FirstOrder.Language.Structure.RelMap r x → FirstOrder.Language.Structure.RelMap r (self.toFun ∘ x)
-- Mathlib.Order.Interval.Multiset
Multiset.mem_Ioi : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] {a x : α}, x ∈ Multiset.Ioi a ↔ a < x
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.isoApp_right_unitor : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {X : (i : I) → C i} {i : I},
  CategoryTheory.Pi.isoApp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X) i =
    CategoryTheory.MonoidalCategoryStruct.rightUnitor (X i)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α}
  {f : Option β → Option β}, (t.alter k f)[k']? = if cmp k k' = Ordering.eq then f t[k]? else t[k']?
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_C_mul_eq_of_mul_eq_one : ∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R} {ai : R},
  ai * a = 1 → (Polynomial.C a * p).natDegree = p.natDegree
-- Mathlib.NumberTheory.LSeries.ZMod
/-- Functional equation for completed L-functions (odd case), valid for all `s`.  -/
ZMod.completedLFunction_one_sub_odd : ∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ},
  Function.Odd Φ →
    ∀ (s : ℂ), ZMod.completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * Complex.I * ZMod.completedLFunction (ZMod.dft Φ) s
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Walk.ofBoxProdLeft_boxProdLeft : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} [inst : DecidableEq β]
  [inst_1 : DecidableRel G.Adj] {a₁ a₂ : α} {b : β} (w : G.Walk a₁ a₂),
  (SimpleGraph.Walk.boxProdLeft H b w).ofBoxProdLeft = w
-- Init.Data.List.Lemmas
List.getLast.congr_simp : ∀ {α : Type u} (as as_1 : List α) (e_as : as = as_1) (a : as ≠ []), as.getLast a = as_1.getLast ⋯
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.vaddInvariantMeasure_map : ∀ {M : Type uM} {α : Type uα} {β : Type uβ} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [inst_2 : VAdd M α]
  [inst_3 : VAdd M β] [MeasurableConstVAdd M β] (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure M α μ]
  (f : α → β),
  (∀ (m : M) (a : α), f (m +ᵥ a) = m +ᵥ f a) →
    Measurable f → MeasureTheory.VAddInvariantMeasure M β (MeasureTheory.Measure.map f μ)
-- Mathlib.Topology.PartitionOfUnity
/-- If `X` is a locally compact T2 topological space and `U` is a locally finite open covering of a
compact set `s`, then there exists a `PartitionOfUnity ι X s` that is subordinate to `U`.  -/
PartitionOfUnity.exists_isSubordinate_of_locallyFinite_t2space : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} [LocallyCompactSpace X] [T2Space X],
  IsCompact s →
    ∀ (U : ι → Set X),
      (∀ (i : ι), IsOpen (U i)) →
        LocallyFinite U → s ⊆ ⋃ i, U i → ∃ f, f.IsSubordinate U ∧ ∀ (i : ι), HasCompactSupport ⇑(f i)
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.mk.injEq : ∀ {α α₂ β : Type w} {m : Type w → Type u_1} (it₁ : Std.IterM m (Std.IterM m β)) (it₂ : Option (Std.IterM m β))
  (it₁_1 : Std.IterM m (Std.IterM m β)) (it₂_1 : Option (Std.IterM m β)),
  ({ it₁ := it₁, it₂ := it₂ } = { it₁ := it₁_1, it₂ := it₂_1 }) = (it₁ = it₁_1 ∧ it₂ = it₂_1)
-- Mathlib.NumberTheory.SmoothNumbers
/-- `m` is `s`-factored if and only if all prime divisors of `m` are in `s`.  -/
Nat.mem_factoredNumbers' : ∀ {s : Finset ℕ} {m : ℕ}, m ∈ Nat.factoredNumbers s ↔ ∀ (p : ℕ), Nat.Prime p → p ∣ m → p ∈ s
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instDiv : {ι : Type u_1} → {G : ι → Type u_4} → [(i : ι) → Div (G i)] → Div ((i : ι) → G i)
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight₁_div_eq_mulHeight : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x y : K),
  Height.mulHeight₁ (x / y) = Height.mulHeight ![x, y]
-- Mathlib.Algebra.Module.SnakeLemma
SnakeLemma.δ_eq : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6}
  {N₃ : Type u_7} [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁] [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂]
  [inst_5 : AddCommGroup M₃] [inst_6 : Module R M₃] [inst_7 : AddCommGroup N₁] [inst_8 : Module R N₁]
  [inst_9 : AddCommGroup N₂] [inst_10 : Module R N₂] [inst_11 : AddCommGroup N₃] [inst_12 : Module R N₃]
  (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (i₃ : M₃ →ₗ[R] N₃) (f₁ : M₁ →ₗ[R] M₂) (f₂ : M₂ →ₗ[R] M₃)
  (hf : Function.Exact ⇑f₁ ⇑f₂) (g₁ : N₁ →ₗ[R] N₂) (g₂ : N₂ →ₗ[R] N₃) (hg : Function.Exact ⇑g₁ ⇑g₂)
  (h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁) (h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂) (σ : M₃ → M₂) (hσ : ⇑f₂ ∘ σ = id) (ρ : N₂ → N₁)
  (hρ : ρ ∘ ⇑g₁ = id) {K₃ : Type u_9} {C₁ : Type u_10} [inst_13 : AddCommGroup K₃] [inst_14 : Module R K₃]
  [inst_15 : AddCommGroup C₁] [inst_16 : Module R C₁] (ι₃ : K₃ →ₗ[R] M₃) (hι₃ : Function.Exact ⇑ι₃ ⇑i₃)
  (π₁ : N₁ →ₗ[R] C₁) (hπ₁ : Function.Exact ⇑i₁ ⇑π₁) (x : K₃) (y : M₂), f₂ y = ι₃ x → ∀ (z : N₁), ⋯ = ⋯ → ⋯ = ⋯
-- Lean.Expr
_private.Lean.Expr.0.Lean.Expr.updateApp!Impl : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.eq_of_subset_indep : ∀ {α : Type u_1} {M : Matroid α} {B I : Set α}, M.IsBase B → M.Indep I → B ⊆ I → B = I
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
addMonoidAlgebraEquivDirectSum_apply : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring M] [inst_2 : (m : M) → Decidable (m ≠ 0)],
  ⇑addMonoidAlgebraEquivDirectSum = AddMonoidAlgebra.toDirectSum
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The direction of the affine span is the `vectorSpan`.  -/
direction_affineSpan : ∀ (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] (s : Set P), (affineSpan k s).direction = vectorSpan k s
-- Mathlib.LinearAlgebra.TensorProduct.Defs
/-- Note that this provides the default `CompatibleSMul R R M N` instance through
`IsScalarTower.left`.  -/
TensorProduct.CompatibleSMul.isScalarTower : ∀ {R : Type u_1} {R' : Type u_4} [inst : CommSemiring R] [inst_1 : Monoid R'] {M : Type u_7} {N : Type u_8}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : DistribMulAction R' M] [inst_5 : Module R M]
  [inst_6 : Module R N] [inst_7 : SMul R' R] [IsScalarTower R' R M] [inst_9 : DistribMulAction R' N]
  [IsScalarTower R' R N], TensorProduct.CompatibleSMul R R' M N
-- Std.Data.HashSet.Lemmas
Std.HashSet.toList_emptyWithCapacity : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {c : ℕ}, (Std.HashSet.emptyWithCapacity c).toList = []
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.toList_ric : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α β),
  t.Ordered →
    ∀ (bound : α),
      Std.Slice.toList (Std.Ric.Sliceable.mkSlice t *...=bound) =
        List.filter (fun e => (compare e.fst bound).isLE) t.toList
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Group.mulRightReflectLE_of_mulRightMono : ∀ {N : Type u_2} [inst : Group N] [inst_1 : LE N] [MulRightMono N], MulRightReflectLE N
-- Mathlib.Analysis.Normed.Module.Basic
/-- Produces a `NormedAddCommGroup E` instance from a `NormedSpace.Core` on a type
that already has a preexisting uniform space structure and a preexisting bornology. This requires
proofs that the uniformity induced by the norm is equal to the preexisting uniformity, and likewise
for the bornology. See note [reducible non-instances].  -/
NormedAddCommGroup.ofCoreReplaceAll : {𝕜 : Type u_6} →
  {E : Type u_7} →
    [inst : NormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module 𝕜 E] →
          [inst_3 : Norm E] →
            [U : UniformSpace E] →
              [B : Bornology E] →
                (core : NormedSpace.Core 𝕜 E) →
                  uniformity E = uniformity E →
                    (∀ (s : Set E), Bornology.IsBounded s ↔ Bornology.IsBounded s) → NormedAddCommGroup E
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.rename_injective : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (e : σ ↪ τ),
  Function.Injective ⇑(MvPowerSeries.rename ⇑e)
-- Lean.Compiler.ExternAttr
Lean.ExternAttrData.mk.injEq : ∀ (entries entries_1 : List Lean.ExternEntry),
  ({ entries := entries } = { entries := entries_1 }) = (entries = entries_1)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false →
    Std.ExtDHashMap.Const.get! (Std.ExtDHashMap.Const.insertMany m l) k = Std.ExtDHashMap.Const.get! m k
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.instSingletonOfT1Space : {α : Type u_2} → [inst : TopologicalSpace α] → [T1Space α] → Singleton α (TopologicalSpace.IrreducibleCloseds α)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.coe_pow : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  (x : ↥S) (n : ℕ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
HasFDerivAt.clm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {x : E}
  {H : Type u_5} [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {c' : E →L[𝕜] G →L[𝕜] H}
  {u : E → G} {u' : E →L[𝕜] G},
  HasFDerivAt c c' x → HasFDerivAt u u' x → HasFDerivAt (fun y => (c y) (u y)) (c x ∘SL u' + c'.flip (u x)) x
-- Mathlib.Algebra.Order.ToIntervalMod
Ico_eq_locus_Ioc_eq_iUnion_Ioo : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) {a : α}, {b | toIcoMod hp a b = toIocMod hp a b} = ⋃ z, Set.Ioo (a + z • p) (a + p + z • p)
-- Mathlib.Algebra.IsPrimePow
IsPrimePow.pow : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : R}, IsPrimePow n → ∀ {k : ℕ}, k ≠ 0 → IsPrimePow (n ^ k)
-- Mathlib.RingTheory.ChainOfDivisors
DivisorChain.element_of_chain_eq_pow_second_of_chain : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [UniqueFactorizationMonoid M] {q r : Associates M} {n : ℕ},
  n ≠ 0 →
    ∀ {c : Fin (n + 1) → Associates M},
      StrictMono c → (∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i) → r ∣ q → q ≠ 0 → ∃ i, r = c 1 ^ ↑i
-- Mathlib.Computability.DFA
Language.IsRegular.of_compl : ∀ {T : Type u} {L : Language T}, Lᶜ.IsRegular → L.IsRegular
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inv_ofPred : ∀ {α : Type u_2} [inst : Inv α] (p : α → Prop), {x | p x}⁻¹ = {x | p x⁻¹}
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Strong normalization monoid: multiplying with `normUnit` gives a normal form for associated
elements. It is stronger in that it ensures the normalization map is a monoid homomorphism.  -/
StrongNormalizationMonoid : (α : Type u_2) → [CommMonoidWithZero α] → Type u_2
-- Mathlib.Order.Interval.Set.OrdConnected
OrderEmbedding.image_Ioo : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ↪o β),
  (Set.range ⇑e).OrdConnected → ∀ (x y : α), ⇑e '' Set.Ioo x y = Set.Ioo (e x) (e y)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.mul_vle_mul_right : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R}, x ≤ᵥ y → ∀ (z : R), z * x ≤ᵥ z * y
-- Mathlib.Analysis.Real.Pi.Irrational
/-- Auxiliary for the proof that `π` is irrational.
The first of the two integer-coefficient polynomials that describe the behaviour of the
sequence of integrals `I`.
While not given in the informal proof, these are easy to deduce from the recursion formulae.
 -/
_private.Mathlib.Analysis.Real.Pi.Irrational.0.sinPoly : ℕ → Polynomial ℤ
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.instAdd : {R : Type u} →
  {L : Type v} → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → Add (LieSubalgebra R L)
-- Mathlib.Analysis.Convex.Segment
mem_segment_iff_div : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semifield 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {x y z : E},
  x ∈ segment 𝕜 y z ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x
-- Mathlib.RingTheory.Finiteness.Basic
Module.Finite.of_finite : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Finite M],
  Module.Finite R M
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
Submodule.finrank_sup_span_singleton : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [Module.Finite K V]
  {p : Submodule K V} {v : V}, v ∉ p → Module.finrank K ↥(p ⊔ K ∙ v) = Module.finrank K ↥p + 1
-- Init.Data.Array.Find
Array.findFinIdx?_congr : ∀ {α : Type u_1} {p : α → Bool} {xs ys : Array α} (w : xs = ys),
  Array.findFinIdx? p xs = Option.map (fun i => Fin.cast ⋯ i) (Array.findFinIdx? p ys)
-- Std.Do.WP.Basic
_private.Std.Do.WP.Basic.0.Std.Do.EStateM.instWP.match_1.eq_2 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (e : ε) (s' : σ)
  (h_1 : (a : α) → (s' : σ) → motive (EStateM.Result.ok a s'))
  (h_2 : (e : ε) → (s' : σ) → motive (EStateM.Result.error e s')),
  (match EStateM.Result.error e s' with
    | EStateM.Result.ok a s' => h_1 a s'
    | EStateM.Result.error e s' => h_2 e s') =
    h_2 e s'
-- Mathlib.Topology.EMetricSpace.Defs
/-- The `WeakEMetric` space induced by pulling back a topology along an injective function.  -/
WeakEMetricSpace.induced : {α : Type u_2} →
  {β : Type u_3} →
    [n : TopologicalSpace β] → {f : α → β} → Function.Injective f → WeakEMetricSpace β → WeakEMetricSpace α
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Modification.instInhabited : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η : F ⟶ G} → Inhabited (CategoryTheory.Oplax.OplaxTrans.Modification η η)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
StrictMono.const_add : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α}
  [AddLeftStrictMono α], StrictMono f → ∀ (c : α), StrictMono fun x => c + f x
-- Lean.Elab.Command
Lean.Elab.Command.getCurrMacroScope : Lean.Elab.Command.CommandElabM ℕ
-- Mathlib.Order.Bounds.Basic
isGLB_le_isLUB_of_nonempty_inter : ∀ {α : Type u_1} [inst : Preorder α] {s s' : Set α} {a b : α}, (s ∩ s').Nonempty → IsGLB s a → IsLUB s' b → a ≤ b
-- Mathlib.ModelTheory.Definability
Set.DefinableFun.proj : ∀ {M : Type u_1} (L : FirstOrder.Language) [inst : L.Structure M] {α : Type u_2} {A : Set M} {i : α},
  Set.DefinableFun L A fun v => v i
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
/-- A bicategory structure on the lax functors between bicategories, with lax transformations.  -/
CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory : (B : Type u₁) →
  [inst : CategoryTheory.Bicategory B] →
    (C : Type u₂) → [inst_1 : CategoryTheory.Bicategory C] → CategoryTheory.Bicategory (CategoryTheory.LaxFunctor B C)
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card.eq_1 : ∀ (α : Type u_3), ENat.card α = Cardinal.toENat (Cardinal.mk α)
-- Mathlib.Order.Basic
Subtype.coe_le_coe : ∀ {α : Type u_2} [inst : LE α] {p : α → Prop} {x y : Subtype p}, ↑x ≤ ↑y ↔ x ≤ y