mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.IsNilpotent.nilpotent_int : ∀ {L : Type v} {M : Type w} {inst : LieRing L} {inst_1 : AddCommGroup M} {inst_2 : LieRingModule L M}
  [self : LieModule.IsNilpotent L M], ∃ k, LieModule.lowerCentralSeries ℤ L M k = ⊥
-- Mathlib.Order.Filter.Pointwise
Filter.sub.instNeBot : ∀ {α : Type u_2} [inst : Sub α] {f g : Filter α} [f.NeBot] [g.NeBot], (f - g).NeBot
-- Init.Data.Array.Lemmas
Array.foldlM_start_stop : ∀ {α : Type u_1} {β : Type u_2} {m : Type u_2 → Type u_3} [inst : Monad m] {xs : Array α} {f : β → α → m β} {b : β}
  {start stop : ℕ}, Array.foldlM f b xs start stop = Array.foldlM f b (xs.extract start stop)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_map_of_getKey?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [EquivBEq α] [LawfulHashable α] {f : α → β → γ} {k k' : α},
  (↑m).WF →
    m.getKey? k = some k' →
      Std.DHashMap.Internal.Raw₀.Const.get? (Std.DHashMap.Internal.Raw₀.map f m) k =
        Option.map (f k') (Std.DHashMap.Internal.Raw₀.Const.get? m k)
-- Mathlib.Algebra.Star.Basic
IsLeftRegular.star : ∀ {R : Type u} [inst : Mul R] [inst_1 : StarMul R] {x : R}, IsLeftRegular x → IsRightRegular (star x)
-- Init.Data.BitVec.Lemmas
BitVec.neg_mul_not_eq_add_mul : ∀ {w : ℕ} {x y : BitVec w}, -(x * ~~~y) = x + x * y
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
LinearMap.IsPerfectCompl.flip_iff : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {p : M →ₗ[R] N →ₗ[R] R} [inst_5 : p.IsPerfPair] {U : Submodule R M}
  {V : Submodule R N}, p.flip.IsPerfectCompl V U ↔ p.IsPerfectCompl U V
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.inc.congr_simp : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId fvarId_1 : Lean.FVarId),
  fvarId = fvarId_1 →
    ∀ (n n_1 : ℕ),
      n = n_1 →
        ∀ (check check_1 : Bool),
          check = check_1 →
            ∀ (persistent persistent_1 : Bool),
              persistent = persistent_1 →
                ∀ (k k_1 : Lean.Compiler.LCNF.Code pu),
                  k = k_1 →
                    ∀ (h : pu = Lean.Compiler.LCNF.Purity.impure),
                      Lean.Compiler.LCNF.Code.inc fvarId n check persistent k h =
                        Lean.Compiler.LCNF.Code.inc fvarId_1 n_1 check_1 persistent_1 k_1 h
-- Init.Data.SInt.Lemmas
Int8.toInt32_ne_minValue : ∀ (a : Int8), a.toInt32 ≠ Int32.minValue
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Normal
CategoryTheory.IsMonHom.Normal.isMonHom : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {G H : C} {inst_2 : CategoryTheory.GrpObj G} {inst_3 : CategoryTheory.GrpObj H} {φ : H ⟶ G}
  [self : CategoryTheory.IsMonHom.Normal φ], CategoryTheory.IsMonHom φ
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.truncFinset_one : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s : Finset (σ →₀ ℕ)},
  0 ∈ s → (MvPowerSeries.truncFinset R s) 1 = 1
-- Lean.Meta.SynthInstance
/-- Assign a precomputed answer to `mvar`.
If it succeeds, the result is a new updated metavariable context and a new list of subgoals.  -/
Lean.Meta.SynthInstance.tryAnswer : Lean.MetavarContext →
  Lean.Expr → Lean.Meta.SynthInstance.Answer → Lean.Meta.SynthInstance.SynthM (Option Lean.MetavarContext)
-- Init.Data.List.Lemmas
List.getD_eq_getElem?_getD : ∀ {α : Type u_1} {l : List α} {i : ℕ} {a : α}, l.getD i a = l[i]?.getD a
-- Mathlib.Util.PrintSorries
Mathlib.PrintSorries.State.mk.injEq : ∀ (visited : Lean.NameSet) (sorries : Std.HashSet Lean.Expr) (sorryMsgs : Array Lean.MessageData)
  (visited_1 : Lean.NameSet) (sorries_1 : Std.HashSet Lean.Expr) (sorryMsgs_1 : Array Lean.MessageData),
  ({ visited := visited, sorries := sorries, sorryMsgs := sorryMsgs } =
      { visited := visited_1, sorries := sorries_1, sorryMsgs := sorryMsgs_1 }) =
    (visited = visited_1 ∧ sorries = sorries_1 ∧ sorryMsgs = sorryMsgs_1)
-- Mathlib.AlgebraicGeometry.Sites.Representability
/-- Suppose
* F is a `Type u`-valued sheaf on `Sch` with respect to the Zariski topology
* X : ι → Sch is a family of schemes
* f : Π i, yoneda.obj (X i) ⟶ F is a family of relatively representable open immersions
* f is jointly surjective

Then `F` is representable, and the representing object is glued from the `X i`s
 -/
AlgebraicGeometry.Scheme.LocalRepresentability.representableBy : {F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type u)} →
  {ι : Type u} →
    {X : ι → AlgebraicGeometry.Scheme} →
      {f : (i : ι) → CategoryTheory.yoneda.obj (X i) ⟶ F.obj} →
        (hf : ∀ (i : ι), AlgebraicGeometry.IsOpenImmersion.presheaf (f i)) →
          [CategoryTheory.Presheaf.IsLocallySurjective AlgebraicGeometry.Scheme.zariskiTopology
                (CategoryTheory.Limits.Sigma.desc f)] →
            F.obj.RepresentableBy (AlgebraicGeometry.Scheme.LocalRepresentability.glueData hf).glued
-- Init.Data.Vector.Range
Vector.mk_add_mem_zipIdx_iff_getElem? : ∀ {α : Type u_1} {n k i : ℕ} {x : α} {xs : Vector α n}, (x, k + i) ∈ xs.zipIdx k ↔ xs[i]? = some x
-- Mathlib.Algebra.Algebra.Operations
/-- Exactness of the sequence `1 → Rˣ → Aˣ → (Submodule R A)ˣ → Pic R → Pic A` at `Aˣ`.
See Exercise I.3.7(iv) in [Weibel2013] or Theorem 2.4 in [RobertsSingh1993].  -/
Submodule.ker_unitsMap_spanSingleton : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A],
  (Units.map ↑(Submodule.spanSingleton R)).ker = (Units.map ↑(algebraMap R A)).range
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.IsPositive.inner_nonneg_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E}, T.IsPositive → ∀ (x : E), 0 ≤ inner 𝕜 (T x) x
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.image_inter_image_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (U V : Set α),
  Quotient.mk' '' U ∩ Quotient.mk' '' V = ∅ ↔ ∀ x ∈ U, ∀ (g : G), g +ᵥ x ∉ V
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
ChevalleyThm.MvPolynomialC.numBound.eq_1 : ∀ (k : ℕ) (D : ℕ → ℕ), ChevalleyThm.MvPolynomialC.numBound k D 0 = k
-- Init.Data.Int.DivMod.Lemmas
Int.eq_one_of_mul_eq_one_right : ∀ {a b : ℤ}, 0 ≤ a → a * b = 1 → a = 1
-- Mathlib.GroupTheory.Perm.Subgroup
Equiv.Perm.sigmaCongrRightHom.card_range : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Fintype ↥(Equiv.Perm.sigmaCongrRightHom β).range]
  [inst_1 : Fintype ((a : α) → Equiv.Perm (β a))],
  Fintype.card ↥(Equiv.Perm.sigmaCongrRightHom β).range = Fintype.card ((a : α) → Equiv.Perm (β a))
-- Init.Data.Array.Erase
Array.eraseIdx_eq_empty_iff : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {h : i < xs.size}, xs.eraseIdx i h = #[] ↔ xs.size = 1 ∧ i = 0
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of a right invariant measure under a left additive action is right
invariant, assuming that the action preserves addition.  -/
MeasureTheory.isAddRightInvariant_map_vadd : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddSemigroup G] [MeasurableAdd G] {μ : MeasureTheory.Measure G}
  {α : Type u_3} [inst_3 : VAdd α G] [VAddCommClass α Gᵃᵒᵖ G] [MeasurableConstVAdd α G] [μ.IsAddRightInvariant] (a : α),
  (MeasureTheory.Measure.map (fun x => a +ᵥ x) μ).IsAddRightInvariant
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
ModelWithCorners.mdifferentiableAt : ∀ {𝕜 : 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) {x : H},
  MDiffAt ↑I x
-- Mathlib.MeasureTheory.Group.Prod
/-- Any two nonzero left-invariant measures are absolutely continuous w.r.t. each other.  -/
MeasureTheory.absolutelyContinuous_of_isAddLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableNeg G] [μ.IsAddLeftInvariant] [ν.IsAddLeftInvariant],
  ν ≠ 0 → μ.AbsolutelyContinuous ν
-- Mathlib.SetTheory.Lists
Lists'.ofList.eq_2 : ∀ {α : Type u_1} (a : Lists α) (l : List (Lists α)), Lists'.ofList (a :: l) = Lists'.cons a (Lists'.ofList l)
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithTop.decidableLE.match_1.splitter : {α : Type u_1} →
  (motive : WithTop α → WithTop α → Sort u_2) →
    (x x_1 : WithTop α) →
      ((x : WithTop α) → motive none x) →
        ((a : α) → motive (some a) none) → ((a b : α) → motive (some a) (some b)) → motive x x_1
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The identity functor is also the identity on additive group objects.  -/
CategoryTheory.Functor.mapAddGrpIdIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (CategoryTheory.Functor.id C).mapAddGrp ≅ CategoryTheory.Functor.id (CategoryTheory.AddGrp C)
-- Mathlib.Algebra.Group.EvenFunction
/-- The zero function is even.  -/
Function.Even.zero : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg α] [inst_1 : Zero β], Function.Even fun x => 0
-- Mathlib.Data.Fintype.OfMap
/-- If `f : α ≃ β` and `α` is a fintype, then `β` is also a fintype.  -/
Fintype.ofEquiv : {β : Type u_2} → (α : Type u_4) → [Fintype α] → α ≃ β → Fintype β
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.withDensity.instIsFiniteMeasure : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.IsFiniteMeasure (ν.withDensity (μ.rnDeriv ν))
-- Mathlib.Topology.MetricSpace.Equicontinuity
/-- For a family of functions between (pseudo) metric spaces, a convenient way to prove
equicontinuity is to show that all of the functions share a common *global* continuity modulus.  -/
Metric.equicontinuous_of_continuity_modulus : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] {ι : Type u_4} [inst_1 : PseudoMetricSpace β] (b : ℝ → ℝ),
  Filter.Tendsto b (nhds 0) (nhds 0) →
    ∀ (F : ι → β → α), (∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)) → Equicontinuous F
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instInhabited : {E : Type u_3} → [inst : AddGroup E] → Inhabited (AddGroupSeminorm E)
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The circumradius of a simplex with at least two points is
positive.  -/
Affine.Simplex.circumradius_pos : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 1)), 0 < s.circumradius
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.Hom.map_snd : ∀ {X Y : Bipointed} (self : X.Hom Y), self.toFun X.toProd.2 = Y.toProd.2
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
/-- Choice of continuous right inverse for `f : F →L[R] E`, given that such an inverse exists.  -/
ContinuousLinearMap.HasRightInverse.rightInverse : {R : Type u_1} →
  [inst : Semiring R] →
    {E : Type u_2} →
      {F : Type u_4} →
        [inst_1 : TopologicalSpace E] →
          [inst_2 : AddCommMonoid E] →
            [inst_3 : Module R E] →
              [inst_4 : TopologicalSpace F] →
                [inst_5 : AddCommMonoid F] → [inst_6 : Module R F] → {f : E →L[R] F} → f.HasRightInverse → F →L[R] E
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.AtPrime.instIsScalarTowerOfIsLiesOverAlgebra_1 : ∀ {A : Type u_4} {B : Type u_5} {C : Type u_6} [inst : CommSemiring A] [inst_1 : CommSemiring B] [inst_2 : Algebra A B]
  [inst_3 : CommSemiring C] [inst_4 : Algebra A C] [inst_5 : Algebra B C] [IsScalarTower A B C] (p : Ideal A)
  [inst_7 : p.IsPrime] (P : Ideal B) [inst_8 : P.IsPrime] [inst_9 : P.LiesOver p] (Q : Ideal C) [inst_10 : Q.IsPrime]
  [inst_11 : Q.LiesOver P] [inst_12 : Q.LiesOver p]
  [inst_13 : Algebra (Localization.AtPrime p) (Localization.AtPrime P)] [Localization.AtPrime.IsLiesOverAlgebra p P]
  [inst_15 : Algebra (Localization.AtPrime P) (Localization.AtPrime Q)] [Localization.AtPrime.IsLiesOverAlgebra P Q]
  [inst_17 : Algebra (Localization.AtPrime p) (Localization.AtPrime Q)] [Localization.AtPrime.IsLiesOverAlgebra p Q],
  IsScalarTower (Localization.AtPrime p) (Localization.AtPrime P) (Localization.AtPrime Q)
-- Mathlib.Algebra.Group.Units.Defs
Units.copy_eq : ∀ {α : Type u} [inst : Monoid α] (u : αˣ) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑u⁻¹),
  u.copy val hv inv hi = u
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_sub_one : ∀ {x : ℝ}, x ≠ 0 → ∀ (y : ℝ), x ^ (y - 1) = x ^ y / x
-- Mathlib.Order.Interval.Set.Infinite
Set.Iic_infinite : ∀ {α : Type u_1} [inst : Preorder α] [NoMinOrder α] (a : α), (Set.Iic a).Infinite
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.Hom.match_1.splitter : {C : Type u_1} →
  (motive : CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → Sort u_2) →
    (x x_1 : CategoryTheory.WithInitial C) →
      ((X Y : C) → motive (CategoryTheory.WithInitial.of X) (CategoryTheory.WithInitial.of Y)) →
        ((a : C) →
            (x : CategoryTheory.WithInitial C) →
              (∀ (Y : C), x = CategoryTheory.WithInitial.of Y → False) → motive (CategoryTheory.WithInitial.of a) x) →
          ((x : CategoryTheory.WithInitial C) → motive CategoryTheory.WithInitial.star x) → motive x x_1
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.norm.inj : ∀ {c₁ : Lean.Meta.Grind.Arith.Linear.IneqCnstr} {k : ℕ} {c₁_1 : Lean.Meta.Grind.Arith.Linear.IneqCnstr} {k_1 : ℕ},
  Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.norm c₁ k = Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.norm c₁_1 k_1 →
    c₁ = c₁_1 ∧ k = k_1
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.mem_vadd_set_neg : ∀ {α : Type u_2} [inst : AddGroup α] {a b : α} {s : Set α}, a ∈ b +ᵥ -s ↔ b ∈ a +ᵥ s
-- Mathlib.NumberTheory.Padics.MahlerBasis
/-- The value of a Mahler series at a natural number `n` is given by the finite sum of the first `m`
terms, for any `n ≤ m`.
 -/
PadicInt.mahlerSeries_apply_nat : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : Module ℤ_[p] E]
  [inst_2 : IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] [CompleteSpace E] {a : ℕ → E},
  Filter.Tendsto a Filter.atTop (nhds 0) →
    ∀ {m n : ℕ}, m ≤ n → (PadicInt.mahlerSeries a) ↑m = ∑ i ∈ Finset.range (n + 1), m.choose i • a i
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.mk.congr_simp : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (pt : C) (π π_1 : (j : J) → pt ⟶ F j) (e_π : π = π_1)
  (ι ι_1 : (j : J) → F j ⟶ pt) (e_ι : ι = ι_1)
  (ι_π :
    ∀ (j j' : J), CategoryTheory.CategoryStruct.comp (ι j) (π j') = if h : j = j' then CategoryTheory.eqToHom ⋯ else 0),
  { pt := pt, π := π, ι := ι, ι_π := ι_π } = { pt := pt, π := π_1, ι := ι_1, ι_π := ⋯ }
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableVAdd₂.toMeasurableVAdd : ∀ {M : Type u_2} {X : Type u_3} [inst : MeasurableSpace X] [inst_1 : VAdd M X] [inst_2 : MeasurableSpace M]
  [MeasurableVAdd₂ M X], MeasurableVAdd M X
-- Mathlib.MeasureTheory.OuterMeasure.AE
/-- **Alias** of `MeasureTheory.measure_congr`.

---

If two sets are equal modulo a set of measure zero, then `μ s = μ t`.  -/
Filter.EventuallyEq.measure_eq : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, s =ᵐ[μ] t → μ s = μ t
-- Mathlib.GroupTheory.Coset.Basic
orbit_addSubgroup_eq_self_of_mem : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {a : α}, a ∈ s → AddAction.orbit (↥s) a = ↑s
-- Std.Data.DHashMap.Raw
/-- Creates a hash map from a list of mappings. If the same key appears multiple times, the last
occurrence takes precedence.  -/
Std.DHashMap.Raw.ofList : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable α] → List ((a : α) × β a) → Std.DHashMap.Raw α β
-- Mathlib.Analysis.Normed.Lp.MeasurableSpace
WithLp.measurableSpace : (p : ENNReal) → (X : Type u_1) → [MeasurableSpace X] → MeasurableSpace (WithLp p X)
-- Mathlib.ModelTheory.Definability
/-- The preimage of a definable set under a definable map is definable.  -/
Set.Definable.preimage_map : ∀ {M : Type u_1} {L : FirstOrder.Language} [inst : L.Structure M] {A : Set M} {α : Type u_4} {β : Type u_5} [Finite β]
  {F : (α → M) → β → M}, Set.DefinableMap L A F → ∀ {S : Set (β → M)}, A.Definable L S → A.Definable L (F ⁻¹' S)
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousLinearMap.cpolynomialAt_uncurry_of_multilinear : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {ι : Type u_5}
  {Em : ι → Type u_6} [inst_5 : (i : ι) → NormedAddCommGroup (Em i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_7 : Fintype ι] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F) {x : G × ((i : ι) → Em i)},
  CPolynomialAt 𝕜 (fun p => (f p.1) p.2) x
-- Mathlib.Analysis.Convex.Mul
ConcaveOn.smul' : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : CommRing E] [inst_4 : LinearOrder E] [IsStrictOrderedRing E]
  [inst_6 : AddCommGroup F] [inst_7 : LinearOrder F] [IsOrderedAddMonoid F] [inst_9 : AddCommGroup G]
  [inst_10 : Module 𝕜 G] [inst_11 : Module 𝕜 E] [inst_12 : Module 𝕜 F] [inst_13 : Module E F] [IsScalarTower 𝕜 E F]
  [SMulCommClass 𝕜 E F] [IsOrderedModule 𝕜 F] [IsStrictOrderedModule E F] {s : Set G} {f : G → E} {g : G → F}
  [IsOrderedModule 𝕜 E],
  ConcaveOn 𝕜 s f →
    ConcaveOn 𝕜 s g →
      (∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x) → (∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x) → AntivaryOn f g s → ConcaveOn 𝕜 s (f • g)
-- Mathlib.Data.Complex.Basic
Complex.instDivInvMonoid : DivInvMonoid ℂ
-- Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing
IsDiscreteValuationRing.exists_lift_of_le_one : ∀ {A : Type u_1} {K : Type u_2} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : IsDiscreteValuationRing A]
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] {x : K},
  (IsDedekindDomain.HeightOneSpectrum.valuation K (IsDiscreteValuationRing.maximalIdeal A)) x ≤ 1 →
    ∃ a, (algebraMap A K) a = x
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsUpperSet.toAlexandrovDiscrete : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpperSet α], AlexandrovDiscrete α
-- Mathlib.Geometry.Polygon.Basic
/-- The boundary of the polygon is the union of all its edges.  -/
Polygon.boundary : (R : Type u_1) →
  {V : Type u_2} →
    {P : Type u_3} →
      {n : ℕ} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup V] → [Module R V] → [AddTorsor V P] → [PartialOrder R] → Polygon P n → Set P
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- Evaluation of functions into an indexed collection of additive semigroups at a point is an
additive semigroup homomorphism. This is `Function.eval i` as an `AddHom`.  -/
Pi.evalAddHom : {I : Type u} → (f : I → Type v) → [inst : (i : I) → Add (f i)] → (i : I) → ((i : I) → f i) →ₙ+ f i
-- Init.Data.List.Zip
List.take_zipWith : ∀ {α : Type u_1} {α_1 : Type u_2} {α_2 : Type u_3} {f : α → α_1 → α_2} {l : List α} {l' : List α_1} {i : ℕ},
  List.take i (List.zipWith f l l') = List.zipWith f (List.take i l) (List.take i l')
-- Std.Data.DHashMap.Basic
/-- Checks if any element satisfies the predicate, short-circuiting if a predicate succeeds.  -/
Std.DHashMap.any : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → ((a : α) → β a → Bool) → Bool
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rii.toArray_iter : ∀ {α : Type u_1} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α] [inst_3 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rii α},
  r.iter.toArray = r.toArray
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.size_insert_le : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {v : β k}, (m.insert k v).size ≤ m.size + 1
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.con_addSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] (c : AddCon G), QuotientAddGroup.con c.addSubgroup = c
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.skeleton_monotone : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D],
  Monotone (Topology.RelCWComplex.skeleton C)
-- Mathlib.CategoryTheory.Presentable.ColimitPresentation
CategoryTheory.Limits.ColimitPresentation.id_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} {I : J → Type u_2}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] [inst_2 : (j : J) → CategoryTheory.Category.{u_3, u_2} (I j)]
  {D : CategoryTheory.Functor J C} {P : (j : J) → CategoryTheory.Limits.ColimitPresentation (I j) (D.obj j)}
  (x : CategoryTheory.Limits.ColimitPresentation.Total P),
  (CategoryTheory.CategoryStruct.id x).hom = CategoryTheory.CategoryStruct.id ((P x.fst).diag.obj x.snd)
-- Std.Data.Iterators.Lemmas.Equivalence.StepCongr
Std.IterM.Equiv.liftInner_stepAsHetT_pbind_congr : ∀ {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} {α₁ β α₂ : Type u_1} {γ : Type u_4} [inst : Monad m]
  [inst_1 : LawfulMonad m] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst_6 : Std.Iterator α₁ m β] [inst_7 : Std.Iterator α₂ m β] {ita : Std.IterM m β} {itb : Std.IterM m β}
  {f :
    (x : Std.IterStep (Std.IterM m β) β) →
      (Std.Iterators.HetT.liftInner n ita.stepAsHetT).Property x → Std.Iterators.HetT n γ}
  {g :
    (x : Std.IterStep (Std.IterM m β) β) →
      (Std.Iterators.HetT.liftInner n itb.stepAsHetT).Property x → Std.Iterators.HetT n γ},
  ita.Equiv itb →
    (∀ (sa : Std.IterStep (Std.IterM m β) β) (hsa : (Std.Iterators.HetT.liftInner n ita.stepAsHetT).Property sa)
        (sb : Std.IterStep (Std.IterM m β) β) (hsb : (Std.Iterators.HetT.liftInner n itb.stepAsHetT).Property sb),
        sa.bundledQuotient = sb.bundledQuotient → f sa hsa = g sb hsb) →
      (Std.Iterators.HetT.liftInner n ita.stepAsHetT).pbind f = (Std.Iterators.HetT.liftInner n itb.stepAsHetT).pbind g
-- Mathlib.Data.Nat.EvenOddRec
/-- Recursion principle on even and odd numbers: if we have `P 0`, and for all `i : ℕ` we can
extend from `P i` to both `P (2 * i)` and `P (2 * i + 1)`, then we have `P n` for all `n : ℕ`.
This is nothing more than a wrapper around `Nat.binaryRec`, to avoid having to switch to
dealing with `bit0` and `bit1`.  -/
Nat.evenOddRec : {P : ℕ → Sort u_1} → P 0 → ((n : ℕ) → P n → P (2 * n)) → ((n : ℕ) → P n → P (2 * n + 1)) → (n : ℕ) → P n
-- Lean.Data.Json.FromToJson.Extra
_private.Lean.Data.Json.FromToJson.Extra.0.Lean.TreeMap.fromJson? : {α : Type} →
  {cmp : String → String → Ordering} → [Lean.FromJson α] → Lean.Json → Except String (Std.TreeMap String α cmp)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_insertMany_list_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {l : List (α × β)}, (Std.DHashMap.Const.insertMany m l).size ≤ m.size + l.length
-- Std.Internal.Do.Order.Instances
Std.Internal.Do.CompleteLattice.instAssociativeJoin : ∀ {l : Type u_1} [inst : Lean.Order.CompleteLattice l], Std.Associative fun x1 x2 => Lean.Order.join x1 x2
-- Mathlib.NumberTheory.FLT.Basic
/-- Statement of Fermat's Last Theorem over the naturals for a given exponent.  -/
FermatLastTheoremFor : ℕ → Prop