mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Submersion
/-- If `f: M → N` and `g: M' → N'` are submersions at `x` and `x'`, respectively,
then `f × g: M × M' → N × N'` is a submersion at `(x, x')`.  -/
Manifold.IsSubmersionAt.prodMap : ∀ {𝕜 : Type u_1} {E' : Type u_2} {E'' : Type u_3} {E''' : Type u_4} {H : Type u_7} {H' : Type u_8} {G : Type u_9}
  {G' : Type u_10} {E : Type u} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  [inst_5 : NormedAddCommGroup E''] [inst_6 : NormedSpace 𝕜 E''] [inst_7 : NormedAddCommGroup E''']
  [inst_8 : NormedSpace 𝕜 E'''] [inst_9 : TopologicalSpace H] [inst_10 : TopologicalSpace H']
  [inst_11 : TopologicalSpace G] [inst_12 : TopologicalSpace G'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 E'' G} {J' : ModelWithCorners 𝕜 E''' G'} {M : Type u_11}
  {M' : Type u_12} {N : Type u_13} {N' : Type u_14} [inst_13 : TopologicalSpace M] [inst_14 : ChartedSpace H M]
  [inst_15 : TopologicalSpace M'] [inst_16 : ChartedSpace H' M'] [inst_17 : TopologicalSpace N]
  [inst_18 : ChartedSpace G N] [inst_19 : TopologicalSpace N'] [inst_20 : ChartedSpace G' N'] {n : WithTop ℕ∞} {x : M}
  {f : M → N} {g : M' → N'} {x' : M'} [IsManifold I n M] [IsManifold I' n M'] [IsManifold J n N] [IsManifold J' n N'],
  Manifold.IsSubmersionAt I J n f x →
    Manifold.IsSubmersionAt I' J' n g x' → Manifold.IsSubmersionAt (I.prod I') (J.prod J') n (Prod.map f g) (x, x')
-- Batteries.Lean.AttributeExtra
Lean.instInhabitedParametricAttributeExtra : {a : Type} → Inhabited (Lean.ParametricAttributeExtra a)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get!_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], (t₁ ∩ t₂).get! k = if k ∈ t₂ then t₁.get! k else default
-- Mathlib.Algebra.Group.TransferInstance
Equiv.one.eq_1 : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) [inst : One β], e.one = { one := e.invFun 1 }
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If the angle ∠ABC at a point is π, the angle ∠BCA is 0.  -/
EuclideanGeometry.angle_eq_zero_of_angle_eq_pi_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi → EuclideanGeometry.angle p₂ p₃ p₁ = 0
-- Mathlib.Analysis.Calculus.LagrangeMultipliers
/-- Lagrange multipliers theorem. Let `f : ι → E → ℝ` be a finite family of functions.
Suppose that `φ : E → ℝ` has a local extremum on the set `{x | ∀ i, f i x = f i x₀}` at `x₀`.
Suppose that all functions `f i` as well as `φ` are strictly differentiable at `x₀`.
Then the derivatives `f' i : E → L[ℝ] ℝ` and `φ' : StrongDual ℝ E` are linearly dependent.

See also `IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt` for a version that
that states existence of Lagrange multipliers `Λ` and `Λ₀` instead of using
`¬LinearIndependent ℝ _`  -/
IsLocalExtrOn.linear_dependent_of_hasStrictFDerivAt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {φ : E → ℝ} {x₀ : E}
  {φ' : StrongDual ℝ E} {ι : Type u_3} [Finite ι] {f : ι → E → ℝ} {f' : ι → StrongDual ℝ E},
  IsLocalExtrOn φ {x | ∀ (i : ι), f i x = f i x₀} x₀ →
    (∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀) →
      HasStrictFDerivAt φ φ' x₀ → ¬LinearIndependent ℝ (Option.elim' φ' f')
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.PreservesLE.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.UpwardEnumerable β]
  [inst_2 : LE α] [inst_3 : LE β] {f : Std.PRange.UpwardEnumerable.Map α β},
  (∀ {a b : α}, a ≤ b ↔ f.toFun a ≤ f.toFun b) → f.PreservesLE
-- Mathlib.Analysis.Normed.Group.InfiniteSum
/-- If `∑' i, ‖f i‖₊` is summable, then `‖∑' i, f i‖₊ ≤ ∑' i, ‖f i‖₊`. Note that
we do not assume that `∑' i, f i` is summable, and it might not be the case if `α` is not a complete
space.  -/
nnnorm_tsum_le : ∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ι → E},
  (Summable fun i => ‖f i‖₊) → ‖∑' (i : ι), f i‖₊ ≤ ∑' (i : ι), ‖f i‖₊
-- Mathlib.Topology.Compactness.CompactSystem
/-- Inserting `univ` into a compact system gives a compact system.  -/
IsCompactSystem.insert_univ : ∀ {α : Type u_1} {S : Set (Set α)}, IsCompactSystem S → IsCompactSystem (insert Set.univ S)
-- Mathlib.NumberTheory.ModularForms.DedekindEta
ModularForm.eta_tprod_ne_zero : ∀ {z : ℂ}, z ∈ UpperHalfPlane.upperHalfPlaneSet → ∏' (n : ℕ), (1 - ModularForm.eta_q n z) ≠ 0
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.msymm_zero : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] [inst_2 : DecidableEq σ],
  MvPolynomial.msymm σ R (Nat.Partition.indiscrete 0) = 1
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- When lowered to a prop, `Matrix.diagonalInvertibleEquivInvertible` forms an `iff`.  -/
Matrix.isUnit_diagonal : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {v : n → α},
  IsUnit (Matrix.diagonal v) ↔ IsUnit v
-- Mathlib.Combinatorics.Enumerative.Bell
Multiset.bell_mul_eq : ∀ (m : Multiset ℕ),
  m.bell * (Multiset.map (fun j => j.factorial) m).prod * ∏ j ∈ m.toFinset.erase 0, (Multiset.count j m).factorial =
    m.sum.factorial
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.holderConjugate_div_div : ∀ {p q r : NNReal}, p.HolderTriple q r → (p / r).HolderConjugate (q / r)
-- Mathlib.Algebra.Lie.SemiDirect
/-- `LieAlgebra.SemiDirectSum.toProd` as a linear equivalence.  -/
LieAlgebra.SemiDirectSum.toProdl : {R : Type u_1} →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : LieRing K] →
        [inst_2 : LieAlgebra R K] →
          {L : Type u_3} →
            [inst_3 : LieRing L] →
              [inst_4 : LieAlgebra R L] → (ψ : L →ₗ⁅R⁆ LieDerivation R K K) → (K ⋊⁅ψ⁆ L) ≃ₗ[R] K × L
-- Init.Data.List.Basic
/-- Returns the index of the first element for which `p` returns `true`, or `none` if there is no such
element.

Examples:
* `[7, 6, 5, 8, 1, 2, 6].findIdx (· < 5) = some 4`
* `[7, 6, 5, 8, 1, 2, 6].findIdx (· < 1) = none`
 -/
List.findIdx? : {α : Type u} → (α → Bool) → List α → Option ℕ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyPrepareParams.mk.sizeOf_spec : ∀ (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams),
  sizeOf { toTextDocumentPositionParams := toTextDocumentPositionParams } = 1 + sizeOf toTextDocumentPositionParams
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.instVAddInvariantMeasureHausdorffMeasureOfIsIsometricVAdd : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] {α : Type u_4}
  [inst_3 : AddGroup α] [inst_4 : AddAction α X] [IsIsometricVAdd α X] {d : ℝ},
  MeasureTheory.VAddInvariantMeasure α X (MeasureTheory.Measure.hausdorffMeasure d)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.subsingleton : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] (𝒜 : ι → σ) {x : Submonoid A},
  0 ∈ x → Subsingleton (HomogeneousLocalization 𝒜 x)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.top_prod : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  (s : NonUnitalSubring S), ⊤.prod s = NonUnitalSubring.comap (NonUnitalRingHom.snd R S) s
-- Mathlib.Topology.Sion
_private.Mathlib.Topology.Sion.0.Sion.sublevelLeft.eq_1 : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : LinearOrder β] (X : Set E) (f : E → F → β) (b : β) (z : F),
  Sion.sublevelLeft✝ X f b z = ((fun x => f x z) ∘ fun x => ↑x) ⁻¹' Set.Iic b
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.comp_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {P Q R : C} (f : P ⟶ Q)
  (g g' : Q ⟶ R),
  CategoryTheory.CategoryStruct.comp f (g - g') =
    CategoryTheory.CategoryStruct.comp f g - CategoryTheory.CategoryStruct.comp f g'
-- Mathlib.Data.Vector.Defs
/-- nth element of a vector, indexed by a `Fin` type.  -/
List.Vector.get : {α : Type u_1} → {n : ℕ} → List.Vector α n → Fin n → α
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the forward direction of `lipschitzWith_iff_norm_inv_mul_le`. -/
LipschitzWith.norm_inv_mul_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F] {f : E → F} {C : NNReal},
  LipschitzWith C f → ∀ (x y : E), ‖(f x)⁻¹ * f y‖ ≤ ↑C * ‖x⁻¹ * y‖
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp : ∀ (n : Type u) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y)
  (g : Y ⟶ AlgebraicGeometry.Spec (CommRingCat.of (MvPolynomial n (ULift.{u, 0} ℤ)))) (i : n),
  (AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv n) (CategoryTheory.CategoryStruct.comp f g) i =
    (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f))
      ((AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv n) g i)
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.lift.congr_simp : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} {K : Type u_4} [inst : Monoid K] [inst_1 : (i : ι) → Monoid (G i)]
  [inst_2 : Monoid H] {φ : (i : ι) → H →* G i} (f f_1 : (i : ι) → G i →* K) (e_f : f = f_1) (k k_1 : H →* K)
  (e_k : k = k_1) (hf : ∀ (i : ι), (f i).comp (φ i) = k), Monoid.PushoutI.lift f k hf = Monoid.PushoutI.lift f_1 k_1 ⋯
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_set_coe_iff : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], (LinearIndependent R fun (x : ↑s) => v ↑x) ↔ LinearIndepOn R v s
-- Mathlib.Topology.Piecewise
continuousOn_piecewise_ite : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → β} {s s' t : Set α}
  [inst_2 : (x : α) → Decidable (x ∈ t)],
  ContinuousOn f s →
    ContinuousOn g s' →
      s ∩ frontier t = s' ∩ frontier t → Set.EqOn f g (s ∩ frontier t) → ContinuousOn (t.piecewise f g) (t.ite s s')
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The function `Real.sinh` is real analytic.  -/
Real.analyticWithinAt_sinh : ∀ {x : ℝ} {s : Set ℝ}, AnalyticWithinAt ℝ Real.sinh s x
-- Mathlib.Topology.MetricSpace.Antilipschitz
AntilipschitzWith.injective : ∀ {α : Type u_4} {β : Type u_5} [inst : EMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
  AntilipschitzWith K f → Function.Injective f
-- Mathlib.Data.Nat.Squarefree
Nat.MinSqFacProp.eq_2 : ∀ (n d : ℕ), n.MinSqFacProp (some d) = (Nat.Prime d ∧ d * d ∣ n ∧ ∀ (p : ℕ), Nat.Prime p → p * p ∣ n → d ≤ p)
-- Lean.LocalContext
/-- Set the kind of a `LocalDecl`.
 -/
Lean.LocalDecl.setKind : Lean.LocalDecl → Lean.LocalDeclKind → Lean.LocalDecl
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.upcrossingsBefore_zero' : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ}, MeasureTheory.upcrossingsBefore a b f 0 = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign_coe_pi_div_two : (↑(Real.pi / 2)).sign = 1
-- Mathlib.Algebra.Opposites
AddOpposite.instNeg : {α : Type u_1} → [Neg α] → Neg αᵃᵒᵖ
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.of_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) {X Y : C} {f : X ⟶ Y},
  P f →
    ∀ {X' Y' : C} {f' : X' ⟶ Y'} (hX : X = X') (hY : Y = Y'),
      f' =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom hY)) →
        P f'
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.SubseqResult.suffix.injEq : ∀ (s s_1 : Lean.Grind.AC.Seq), (Lean.Grind.AC.SubseqResult.suffix s = Lean.Grind.AC.SubseqResult.suffix s_1) = (s = s_1)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.nonUnitalSemiring : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → [AddSemigroup M] → NonUnitalSemiring (AddMonoidAlgebra R M)
-- Mathlib.Order.Filter.Basic
Filter.filter_eq_bot_of_isEmpty : ∀ {α : Type u} [IsEmpty α] (f : Filter α), f = ⊥
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Walk.ofBoxProdRight.eq_def : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} [inst : DecidableEq α]
  [inst_1 : DecidableRel H.Adj] {x y : α × β} (x_1 : (G □ H).Walk x y),
  x_1.ofBoxProdRight =
    match y, x_1 with
    | .(x), SimpleGraph.Walk.nil => SimpleGraph.Walk.nil
    | y, SimpleGraph.Walk.cons h w =>
      ⋯.by_cases (fun hH => SimpleGraph.Walk.cons ⋯ w.ofBoxProdRight) fun hG => ⋯ ▸ w.ofBoxProdRight
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.div_conj_eq_sub_one : ∀ {p q : ENNReal} [h : p.HolderConjugate q], p / q = p - 1
-- Mathlib.Algebra.Regular.Defs
/-- A left-regular element is an element `c` such that multiplication on the left by `c`
is injective.  -/
IsLeftRegular : {R : Type u_1} → [Mul R] → R → Prop
-- Init.Data.List.Lemmas
List.any_flatten : ∀ {α : Type u_1} {f : α → Bool} {l : List (List α)}, l.flatten.any f = l.any fun x => x.any f
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.LambdaTheorem.mk.sizeOf_spec : ∀ (funPropName thmName : Lean.Name) (thmArgs : Mathlib.Meta.FunProp.LambdaTheoremArgs),
  sizeOf { funPropName := funPropName, thmName := thmName, thmArgs := thmArgs } =
    1 + sizeOf funPropName + sizeOf thmName + sizeOf thmArgs
-- Mathlib.Analysis.Normed.Order.Hom.Basic
/-- Constructs a `NormedAddGroup` structure from an `AddGroupNormClass` on an
`AddGroup`.  -/
AddGroupNormClass.toNormedAddGroup : {F : Type u_1} →
  {α : Type u_2} → [inst : FunLike F α ℝ] → [inst_1 : AddGroup α] → [AddGroupNormClass F α ℝ] → F → NormedAddGroup α
-- Mathlib.Topology.Order.LocalExtr
IsLocalMax.comp_antitone : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f : α → β} {a : α}, IsLocalMax f a → ∀ {g : β → γ}, Antitone g → IsLocalMin (g ∘ f) a
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.instDistribMulActionOfSMulCommClass : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {X : Type u_4} →
        {Y : Type u_5} →
          {σ : M → N} →
            [inst : AddMonoid Y] →
              [inst_1 : Monoid R] →
                [inst_2 : SMul M X] →
                  [inst_3 : DistribSMul N Y] →
                    [inst_4 : DistribMulAction R Y] → [SMulCommClass N R Y] → DistribMulAction R (X →ₑ[σ] Y)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.cancelAux.eq_1 : ∀ (m₁ m₂ r₁ r₂ : Nat.Internal.Linear.Poly),
  Nat.Internal.Linear.Poly.cancelAux 0 m₁ m₂ r₁ r₂ = (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_inv_hom₁ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C),
  (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp T).inv.hom₁ =
    CategoryTheory.CategoryStruct.id (Opposite.op (F.obj T.obj₃))
-- Mathlib.Algebra.Order.Ring.Archimedean
/-- Multiplication in `R` transfers to addition in `ArchimedeanClass R`.  -/
ArchimedeanClass.instAdd : {R : Type u_1} →
  [inst : LinearOrder R] → [inst_1 : CommRing R] → [inst_2 : IsStrictOrderedRing R] → Add (ArchimedeanClass R)
-- Mathlib.Combinatorics.Quiver.Basic
Quiver.homOfEq.congr_simp : ∀ {V : Type u_1} [inst : Quiver V] {X Y X' Y' : V} (f f_1 : X ⟶ Y),
  f = f_1 → ∀ (hX : X = X') (hY : Y = Y'), Quiver.homOfEq f hX hY = Quiver.homOfEq f_1 hX hY
-- Mathlib.Topology.NhdsWithin
tendsto_nhdsWithin_mono_right : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : β → α} {l : Filter β} {a : α} {s t : Set α},
  s ⊆ t → Filter.Tendsto f l (nhdsWithin a s) → Filter.Tendsto f l (nhdsWithin a t)
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.popWhile.eq_def : ∀ {α : Type u} (p : α → Bool) (as : Array α),
  Array.popWhile p as = if h : as.size > 0 then if p as[as.size - 1] = true then Array.popWhile p as.pop else as else as
-- Batteries.Data.List.Basic
/-- Apply `f` to the last element of `l`, if it exists.  -/
List.modifyLast : {α : Type u_1} → (α → α) → List α → List α
-- Mathlib.Analysis.Complex.HasPrimitives
/-- A function `f` `IsExactOn` in `U` if it is the complex derivative of a function on `U`.

In complex variable theory, this is also referred to as "having a primitive".  -/
Complex.IsExactOn : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → (ℂ → E) → Set ℂ → Prop
-- Init.Data.BitVec.Lemmas
BitVec.zeroExtend_eq_setWidth : ∀ {w v : ℕ} {x : BitVec w}, BitVec.zeroExtend v x = BitVec.setWidth v x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Replicate
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorReplicateTargetBlastReplicate : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Tactic.BVDecide.BVExpr.bitblast.ReplicateTarget fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastReplicate
-- Mathlib.RingTheory.Teichmuller
Perfection.mk_teichmuller : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommRing R] {I : Ideal R} [inst_2 : CharP (R ⧸ I) p]
  [inst_3 : IsAdicComplete I R] (x : Perfection (R ⧸ I) p),
  (Ideal.Quotient.mk I) ((Perfection.teichmuller p I) x) = (Perfection.coeff (R ⧸ I) p 0) x
-- Mathlib.Order.Filter.Basic
Filter.frequently_congr : ∀ {α : Type u} {p q : α → Prop} {f : Filter α},
  (∀ᶠ (x : α) in f, p x ↔ q x) → ((∃ᶠ (x : α) in f, p x) ↔ ∃ᶠ (x : α) in f, q x)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.toContinuousLinearMap_inj : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] {f g : E →ₛₗᵢ[σ₁₂] E₂}, f.toContinuousLinearMap = g.toContinuousLinearMap ↔ f = g
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.greatestFib_sub_fib_greatestFib_le_greatestFib : ∀ {n : ℕ}, n ≠ 0 → (n - Nat.fib n.greatestFib).greatestFib ≤ n.greatestFib - 2
-- Mathlib.GroupTheory.PGroup
/-- If `p ∤ n`, then the `n`th power map is a bijection.  -/
IsPGroup.powEquiv' : {p : ℕ} → {G : Type u_1} → [inst : Group G] → IsPGroup p G → [hp : Fact (Nat.Prime p)] → {n : ℕ} → ¬p ∣ n → G ≃ G
-- Mathlib.Topology.Algebra.Star.LinearMap
ContinuousLinearMap.IntrinsicStar.isSelfAdjoint_toLinearMap_iff : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : InvolutiveStar R]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : StarAddMonoid E] [inst_5 : StarModule R E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module R F] [inst_8 : StarAddMonoid F] [inst_9 : StarModule R F]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : ContinuousStar E]
  [inst_13 : ContinuousStar F] (f : WithConv (E →L[R] F)), IsSelfAdjoint (WithConv.toConv ↑f.ofConv) ↔ IsSelfAdjoint f
-- Mathlib.NumberTheory.LSeries.ZMod
/-- If `Φ` is a periodic function, then the L-series of `Φ` converges for `1 < re s`.  -/
ZMod.LSeriesSummable_of_one_lt_re : ∀ {N : ℕ} [NeZero N] (Φ : ZMod N → ℂ) {s : ℂ}, 1 < s.re → LSeriesSummable (fun x => Φ ↑x) s
-- Mathlib.Topology.MetricSpace.Closeds
/-- The Hausdorff pseudo emetric on the powerset of a pseudo emetric space.
See note [reducible non-instances].  -/
PseudoEMetricSpace.hausdorff : {α : Type u_1} → [PseudoEMetricSpace α] → PseudoEMetricSpace (Set α)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_lt_rpow_iff : ∀ {x y z : ℝ}, 0 ≤ x → 0 ≤ y → 0 < z → (x ^ z < y ^ z ↔ x < y)
-- Mathlib.Tactic.NormNum.Pow
/-- Main part of `evalPow`.  -/
Mathlib.Meta.NormNum.evalPow.core : {u : Lean.Level} →
  {α : Q(Type u)} →
    (e : Q(«$α»)) →
      Q(«$α» → ℕ → «$α») →
        (a : Q(«$α»)) →
          (b nb : Q(ℕ)) →
            Q(Mathlib.Meta.NormNum.IsNat «$b» «$nb») →
              Q(Semiring «$α») → Mathlib.Meta.NormNum.Result a → OptionT Lean.CoreM (Mathlib.Meta.NormNum.Result e)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_X : ∀ {R : Type u} [inst : Semiring R], Polynomial.derivative Polynomial.X = 1
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.mk.injEq : ∀ {B : Type u₁} (as as_1 : B), ({ as := as } = { as := as_1 }) = (as = as_1)
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.instLE : {α : Type u_2} → [inst : Preorder α] → LE (OmegaCompletePartialOrder.Chain α)
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.mk.inj : ∀ {R : Type u} {S : Type v} {inst : CommSemiring R} {inst_1 : Semiring S} {inst_2 : Algebra R S} {f : Polynomial R}
  {map : Polynomial R →ₐ[R] S} {map_surjective : Function.Surjective ⇑map} {ker_map : RingHom.ker map = Ideal.span {f}}
  {map_1 : Polynomial R →ₐ[R] S} {map_surjective_1 : Function.Surjective ⇑map_1}
  {ker_map_1 : RingHom.ker map_1 = Ideal.span {f}},
  { map := map, map_surjective := map_surjective, ker_map := ker_map } =
      { map := map_1, map_surjective := map_surjective_1, ker_map := ker_map_1 } →
    map = map_1
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.iAlls.congr_simp : ∀ {L : FirstOrder.Language} {α : Type u'} (β : Type v') [inst : Finite β] (φ φ_1 : L.Formula (α ⊕ β)),
  φ = φ_1 → FirstOrder.Language.Formula.iAlls β φ = FirstOrder.Language.Formula.iAlls β φ_1
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.ofSubmodule_le_ofSubmodule : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] {S T : Submodule R E}, ↑S ≤ ↑T ↔ S ≤ T
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.LetRecClosure.localDecls : Lean.Elab.Term.MutualClosure.LetRecClosure → Array Lean.LocalDecl
-- Mathlib.Algebra.Category.Grp.CartesianMonoidal
AddCommGrpCat.μ_forget_apply : ∀ {G H : AddCommGrpCat} (p : ↑G) (q : ↑H),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.forget AddCommGrpCat) G H))
      (p, q) =
    (p, q)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rco_append_toArray_rco : ∀ {l m n : ℕ}, l ≤ m → m ≤ n → (l...m).toArray ++ (m...n).toArray = (l...n).toArray
-- Mathlib.RingTheory.PowerSeries.CoeffMulMem
PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal : ∀ {A : Type u_1} [inst : Semiring A] {I : Ideal A} {f g : PowerSeries A} (n : ℕ) [I.IsTwoSided],
  (∀ i ≤ n, (PowerSeries.coeff i) f ∈ I) → ∀ i ≤ n, (PowerSeries.coeff i) (f * g) ∈ I
-- Mathlib.Algebra.DirectSum.Internal
DirectSum.coe_mul_apply_eq_dfinsuppSum : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : SetLike σ R]
  [inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : AddMonoid ι] [inst_5 : SetLike.GradedMonoid A]
  [inst_6 : (i : ι) → (x : ↥(A i)) → Decidable (x ≠ 0)] (r r' : DirectSum ι fun i => ↥(A i)) (n : ι),
  ↑((r * r') n) = DFinsupp.sum r fun i ri => DFinsupp.sum r' fun j rj => if i + j = n then ↑ri * ↑rj else 0
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.equiv_symm_zero : ∀ {A : Type u_3} {E : Type u_4} [inst : AddCommGroup E], (WithCStarModule.equiv A E).symm 0 = 0
-- Mathlib.Data.Matrix.DMatrix
/-- `M.map f` is the DMatrix obtained by applying `f` to each entry of the matrix `M`.  -/
DMatrix.map : {m : Type u_1} →
  {n : Type u_2} →
    {α : m → n → Type v} → DMatrix m n α → {β : m → n → Type w} → (⦃i : m⦄ → ⦃j : n⦄ → α i j → β i j) → DMatrix m n β
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Finset.inf'_eq_csInf_image : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLattice α] (s : Finset ι) (H : s.Nonempty) (f : ι → α),
  s.inf' H f = sInf (f '' ↑s)