mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.SmoothSeries
/-- Consider a series of functions `∑' n, f n x` on a preconnected open set. If the series converges
at a point, and all functions in the series are differentiable with a summable bound on the
derivatives, then the series converges everywhere on the set.  -/
summable_of_summable_hasDerivAt_of_isPreconnected : ∀ {α : Type u_1} {𝕜 : Type u_3} {F : Type u_5} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [CompleteSpace F] {u : α → ℝ} [inst_4 : NormedSpace 𝕜 F] {g g' : α → 𝕜 → F}
  {t : Set 𝕜} {y₀ y : 𝕜},
  Summable u →
    IsOpen t →
      IsPreconnected t →
        (∀ (n : α), ∀ y ∈ t, HasDerivAt (g n) (g' n y) y) →
          (∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n) → y₀ ∈ t → (Summable fun x => g x y₀) → y ∈ t → Summable fun n => g n y
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- Eta-expanded form of `MeasureTheory.StronglyMeasurable.sub` -/
MeasureTheory.StronglyMeasurable.fun_sub : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Sub β]
  [ContinuousSub β],
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun i => f i - g i
-- Init.Data.Int.DivMod.Lemmas
Int.tmod_tmod_of_dvd : ∀ (n : ℤ) {m k : ℤ}, m ∣ k → (n.tmod k).tmod m = n.tmod m
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_univ_two' : ∀ {ι : Type u_1} {M : Type u_2} [inst : CommMonoid M] (f : ι → M) (a b : ι), ∏ i, f (![a, b] i) = f a * f b
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.vanishingIdeal_range_comap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S),
  PrimeSpectrum.vanishingIdeal (Set.range (PrimeSpectrum.comap f)) = (RingHom.ker f).radical
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.NatTrans.hcomp_eq_whiskerRight_comp_whiskerLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G : CategoryTheory.Functor C D}
  {H K : CategoryTheory.Functor D E} (α : G ⟶ F) (β : K ⟶ H),
  α ◫ β = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α K) (F.whiskerLeft β)
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.endRingEquiv_symm_apply_hom : ∀ {R : Type u} [inst : Ring R] (M : ModuleCat R) (f : ↑M →ₗ[R] ↑M), ModuleCat.Hom.hom (M.endRingEquiv.symm f) = f
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instReprTheoremForm : Repr Mathlib.Meta.FunProp.TheoremForm
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_eq_limsup_sum_nat : ∀ {f : ℕ → ENNReal}, ∑' (i : ℕ), f i = Filter.limsup (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop
-- Std.Data.DHashMap.DecidableEquiv
Std.DHashMap.instDecidableEquivOfLawfulBEq : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [LawfulBEq α] →
        [inst_2 : Hashable α] →
          [inst_3 : (k : α) → BEq (β k)] →
            [∀ (k : α), LawfulBEq (β k)] → (m₁ m₂ : Std.DHashMap α β) → Decidable (m₁.Equiv m₂)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMap_smul : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (c : ℝ) (x : NumberField.mixedEmbedding.realSpace K),
  ↑NumberField.mixedEmbedding.fundamentalCone.expMap (c • x) = ↑NumberField.mixedEmbedding.fundamentalCone.expMap x ^ c
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.AbsolutelyContinuous.zero : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α), MeasureTheory.Measure.AbsolutelyContinuous 0 μ
-- Init.Data.SInt.Lemmas
instLawfulOrderLTInt64 : Std.LawfulOrderLT Int64
-- Init.MetaTypes
Lean.Meta.Occurrences.pos.injEq : ∀ (idxs idxs_1 : List ℕ), (Lean.Meta.Occurrences.pos idxs = Lean.Meta.Occurrences.pos idxs_1) = (idxs = idxs_1)
-- Mathlib.Order.Filter.Extr
IsMaxOn.bddAbove : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α}, IsMaxOn f s a → BddAbove (f '' s)
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.biproduct_ι_comp_leftDistributor_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (X : C) (f : J → C) (j : J)
  {Z : C} (h : (⨁ fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.ι f j))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j) h
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncLTι_comp_truncGEπ_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.truncLTι n).app X) ((t.truncGEπ n).app X) = 0
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.toFun_eq_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M →ₙ* N), f.toFun = ⇑f
-- Mathlib.MeasureTheory.Measure.MeasuredSets
/-- Given a semiring of sets `C` covering the space modulo `0` and generating the measurable space
structure, any measurable set can be approximated by finite unions of elements of `C`.  -/
MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetSemiring : ∀ {α : Type u_1} [mα : MeasurableSpace α] {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  {C : Set (Set α)},
  MeasureTheory.IsSetSemiring C →
    (∃ D, D.Countable ∧ D ⊆ C ∧ μ (⋃₀ D)ᶜ = 0) →
      mα = MeasurableSpace.generateFrom C →
        ∀ {s : Set α}, MeasurableSet s → ∀ {ε : ENNReal}, 0 < ε → ∃ t ∈ supClosure C, μ (symmDiff t s) < ε
-- Mathlib.Order.Interval.Basic
NonemptyInterval.coe_top : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : BoundedOrder α], ↑⊤ = Set.univ
-- Mathlib.Algebra.Group.End
/-- The permutation of a type is equivalent to the units group of the endomorphisms monoid of this
type.  -/
Equiv.Perm.equivUnitsEnd : {α : Type u_4} → Equiv.Perm α ≃* (Function.End α)ˣ
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exradius.congr_simp : ∀ {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 : ℕ} [inst_4 : NeZero n] (s s_1 : Affine.Simplex ℝ P n),
  s = s_1 → ∀ (signs signs_1 : Finset (Fin (n + 1))), signs = signs_1 → s.exradius signs = s_1.exradius signs_1
-- Mathlib.Logic.Unique
eq_const_of_unique : ∀ {α : Sort u_1} {β : Sort u_2} [inst : Unique α] (f : α → β), f = Function.const α (f default)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.atIdxD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {i : ℕ} {fallback : α},
  t₁.Equiv t₂ → t₁.atIdxD i fallback = t₂.atIdxD i fallback
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- Binary entropy is strictly decreasing in interval [1/2, 1].  -/
Real.binEntropy_strictAntiOn : StrictAntiOn Real.binEntropy (Set.Icc 2⁻¹ 1)
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.algEquivOfAlgEquiv_eq_map : ∀ {A : Type u_4} [inst : CommSemiring A] {R : Type u_5} [inst_1 : CommSemiring R] [inst_2 : Algebra A R]
  {M : Submonoid R} {S : Type u_6} [inst_3 : CommSemiring S] [inst_4 : Algebra A S] [inst_5 : Algebra R S]
  [inst_6 : IsScalarTower A R S] [inst_7 : IsLocalization M S] {P : Type u_7} [inst_8 : CommSemiring P]
  [inst_9 : Algebra A P] {T : Submonoid P} {Q : Type u_8} [inst_10 : CommSemiring Q] [inst_11 : Algebra A Q]
  [inst_12 : Algebra P Q] [inst_13 : IsScalarTower A P Q] [inst_14 : IsLocalization T Q] {h : R ≃ₐ[A] P}
  (H : Submonoid.map h M = T), ↑(IsLocalization.algEquivOfAlgEquiv S Q h H) = IsLocalization.map Q ↑h ⋯
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg.not_FirstNonzeroIsPos : ∀ {li : Tactic.ComputeAsymptotics.UnitMonomial}, li.FirstNonzeroIsNeg → ¬li.FirstNonzeroIsPos
-- Init.Data.SInt.Lemmas
Int16.toInt8_ofIntTruncate : ∀ {n : ℤ}, -2 ^ 15 ≤ n → n < 2 ^ 15 → (Int16.ofIntClamp n).toInt8 = Int8.ofInt n
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_of_isEmpty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m).WF → ∀ {a : α}, (↑m).isEmpty = true → Std.DHashMap.Internal.Raw₀.Const.get! m a = default
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintInfo.textEdits : Lean.Elab.InlayHintInfo → Array Lean.Elab.InlayHintTextEdit
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.instFullProdUncurry₃ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E], CategoryTheory.Functor.uncurry₃.Full
-- Mathlib.Logic.Basic
BAll.imp_left : ∀ {α : Sort u_1} {r p q : α → Prop}, (∀ (x : α), p x → q x) → (∀ (x : α), q x → r x) → ∀ (x : α), p x → r x
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.kahler_rightAngleRotation_right : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), (o.kahler x) (o.rightAngleRotation y) = Complex.I * (o.kahler x) y
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- A space is locally path-connected iff all path components of open subsets are neighbourhoods.  -/
locallyPathConnectedSpace_iff_pathComponentIn_mem_nhds : ∀ {X : Type u_4} [inst : TopologicalSpace X],
  LocallyPathConnectedSpace X ↔ ∀ (x : X) (u : Set X), IsOpen u → x ∈ u → pathComponentIn u x ∈ nhds x
-- Lean.Parser.Command
Lean.Parser.Command.openDecl.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Arrow.Hom.mk_hom : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] {P Q W : CategoryTheory.MorphismProperty T}
  [inst_1 : Q.IsMultiplicative] [inst_2 : W.IsMultiplicative] {A B : P.Arrow Q W}
  (f :
    (CategoryTheory.MorphismProperty.Arrow.forget P Q W).obj A ⟶
      (CategoryTheory.MorphismProperty.Arrow.forget P Q W).obj B)
  (hfl : Q (CategoryTheory.Arrow.Hom.left f)) (hfr : W (CategoryTheory.Arrow.Hom.right f)),
  CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.MorphismProperty.Arrow.Hom.mk f hfl hfr) = f
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.zero_apply : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R₁ M] [inst_5 : Module R₂ M₂]
  {σ₁₂ : R₁ →+* R₂} (x : M), 0 x = 0
-- Mathlib.Topology.Algebra.GroupCompletion
UniformSpace.Completion.instAddCommGroup : {α : Type u_3} →
  [inst : UniformSpace α] → [inst_1 : AddCommGroup α] → [IsUniformAddGroup α] → AddCommGroup (UniformSpace.Completion α)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.uniqueDiffOn_preimage_source : ∀ {𝕜 : 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) {β : Type u_4}
  [inst_4 : TopologicalSpace β] {e : OpenPartialHomeomorph H β}, UniqueDiffOn 𝕜 (↑I.symm ⁻¹' e.source ∩ Set.range ↑I)
-- Mathlib.Data.Nat.Factorization.Defs
Nat.factorization_le_iff_dvd : ∀ {d n : ℕ}, d ≠ 0 → n ≠ 0 → (d.factorization ≤ n.factorization ↔ d ∣ n)
-- Init.Data.Slice.List.Basic
instSliceableListSliceNat_5 : {α : Type u} → Std.Roi.Sliceable (ListSlice α) ℕ (ListSlice α)
-- Init.Data.String.Lemmas.Basic
String.Pos.nextn_eq_nextn_toSlice : ∀ {n : ℕ} {s : String} {p : s.Pos}, p.nextn n = String.Pos.ofToSlice (p.toSlice.nextn n)
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_unsat : ∀ (ctx : Int.Internal.Linear.Context) (k : ℤ) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.isUnsatDvd k p = true → k ∣ Int.Internal.Linear.Poly.denote' ctx p → False
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
_private.Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula.0.ModularForm.eq_zero_of_pow_eq_smul : ∀ {p p4 p6 : PowerSeries ℂ} {c4 c6 : ℂ},
  (PowerSeries.coeff 0) p4 = 1 →
    (PowerSeries.coeff 0) p6 = 1 →
      (PowerSeries.coeff 1) p4 = 240 → (PowerSeries.coeff 1) p6 = -504 → c4 • p4 = p ^ 2 → c6 • p6 = p ^ 3 → p = 0
-- Mathlib.Order.WellFoundedSet
Set.IsPWO.insert : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α}, s.IsPWO → ∀ (a : α), (insert a s).IsPWO
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.FibrantObject.instIsFibrantObjι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] (X : HomotopicalAlgebra.FibrantObject C),
  HomotopicalAlgebra.IsFibrant (HomotopicalAlgebra.FibrantObject.ι.obj X)
-- Init.Data.UInt.Bitwise
USize.zero_shiftLeft : ∀ {a : USize}, 0 <<< a = 0
-- Std.Internal.Do.PredTrans
/-- Unfolding `pure` through `apply`.  -/
Std.Internal.Do.PredTrans.apply_pure : ∀ {α : Type u_1} {Pred : Type u} {EPred : Type v} (a : α) (post : α → Pred) (epost : EPred),
  (pure a).apply post epost = post a
-- Mathlib.Topology.Order.Lattice
Filter.Tendsto.finset_sup'_nhds_apply : ∀ {L : Type u_1} [inst : TopologicalSpace L] {ι : Type u_3} {α : Type u_4} {s : Finset ι} {f : ι → α → L} {l : Filter α}
  {g : ι → L} [inst_1 : SemilatticeSup L] [ContinuousSup L] (hne : s.Nonempty),
  (∀ i ∈ s, Filter.Tendsto (f i) l (nhds (g i))) →
    Filter.Tendsto (fun a => s.sup' hne fun x => f x a) l (nhds (s.sup' hne g))
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.instDecidableRelSameCycleInv : {α : Type u_2} → (f : Equiv.Perm α) → [DecidableRel f.SameCycle] → DecidableRel f⁻¹.SameCycle
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.BicartesianSq.toIsPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z}, CategoryTheory.BicartesianSq f g h i → CategoryTheory.IsPullback f g h i
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_prod_of_regular : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {ι : Type u_3} {P : ι → MvPolynomial σ R}
  {s : Finset ι}, (∀ i ∈ s, IsRegular (m.leadingCoeff (P i))) → m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)
-- Mathlib.Algebra.SkewMonoidAlgebra.Single
SkewMonoidAlgebra.single_add_erase : ∀ {M : Type u_4} {α : Type u_5} [inst : AddCommMonoid M] (a : α) (f : SkewMonoidAlgebra M α),
  SkewMonoidAlgebra.single a (f.coeff a) + (SkewMonoidAlgebra.erase a) f = f
-- Mathlib.LinearAlgebra.FreeModule.Basic
/-- **Alias** of `Module.Free.shrink`. -/
Module.Free.Module.free_shrink : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [inst_4 : Small.{w, v} M], Module.Free R (Shrink.{w, v} M)
-- Lean.Meta.Tactic.Grind.CastLike
/-- Returns `true` if `f` is a cast-like operation.  -/
Lean.Meta.Grind.isCastLikeFn : Lean.Expr → Bool
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_embedding_le_arrow : ∀ (α : Type u) (β' : Type v), Cardinal.mk (α ↪ β') ≤ Cardinal.mk (α → β')
-- Mathlib.CategoryTheory.Subobject.Basic
/-- Any functor `MonoOver X ⥤ MonoOver Y` descends to a functor
`Subobject X ⥤ Subobject Y`, because `MonoOver Y` is thin.  -/
CategoryTheory.Subobject.lower : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          {Y : D} →
            CategoryTheory.Functor (CategoryTheory.MonoOver X) (CategoryTheory.MonoOver Y) →
              CategoryTheory.Functor (CategoryTheory.Subobject X) (CategoryTheory.Subobject Y)
-- Lean.Elab.Tactic.Ext
/-- Given an 'ext' theorem, ensures that there is an iff version of the theorem (if possible),
without validating any pre-existing theorems.
Returns the name of the 'ext_iff' theorem.
 -/
_private.Lean.Elab.Tactic.Ext.0.Lean.Elab.Tactic.Ext.realizeExtIffTheorem : Lean.Name → Lean.Elab.TermElabM Lean.Name
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.of_toQuadraticForm' : ∀ {n : Type u_2} [inst : Fintype n] {R : Type u_5} [inst_1 : CommRing R] [inst_2 : PartialOrder R] [inst_3 : StarRing R]
  [TrivialStar R] [inst_5 : DecidableEq n] {M : Matrix n n R},
  M.IsSymm → QuadraticMap.PosDef M.toQuadraticForm' → M.PosDef
-- Mathlib.Algebra.Group.Ideal
SemigroupIdeal.subset_closure : ∀ {M : Type u_1} [inst : Mul M] {s : Set M}, s ⊆ ↑(SemigroupIdeal.closure s)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_insert_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, t.isEmpty = true → (t.insert k v).minKey ⋯ = k
-- Mathlib.Algebra.Group.Invertible.Basic
/-- If a function `f : R → S` has a left-inverse that is a monoid hom,
then `r : R` is invertible if `f r` is.

The inverse is computed as `g (⅟(f r))`  -/
Invertible.ofLeftInverse : {R : Type u_1} →
  {S : Type u_2} →
    {G : Type u_3} →
      [inst : MulOneClass R] →
        [inst_1 : MulOneClass S] →
          [inst_2 : FunLike G S R] →
            [MonoidHomClass G S R] →
              (f : R → S) → (g : G) → (r : R) → Function.LeftInverse (⇑g) f → [Invertible (f r)] → Invertible r
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
ExteriorAlgebra.instGradedMonoidNatSubmoduleExteriorPower : ∀ (R : Type u_1) (M : Type u_2) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  SetLike.GradedMonoid fun i => ⋀[R]^i M
-- Mathlib.AlgebraicGeometry.PointsPi
AlgebraicGeometry.pointsPi.eq_1 : ∀ {ι : Type u} (R : ι → CommRingCat) (X : AlgebraicGeometry.Scheme)
  (f : AlgebraicGeometry.Spec (CommRingCat.of ((i : ι) → ↑(R i))) ⟶ X) (i : ι),
  AlgebraicGeometry.pointsPi R X f i =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Pi.evalRingHom (fun x => ↑(R x)) i))) f
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeExtension.vle_iff_vle : ∀ {A : Type u_1} {B : Type u_2} {inst : CommSemiring A} {inst_1 : Semiring B} {inst_2 : ValuativeRel A}
  {inst_3 : ValuativeRel B} {inst_4 : Algebra A B} [self : ValuativeExtension A B] (a b : A),
  (algebraMap A B) a ≤ᵥ (algebraMap A B) b ↔ a ≤ᵥ b
-- Mathlib.GroupTheory.PGroup
isPGroup_iff_pow_pow_eq_one : ∀ {p : ℕ} {G : Type u_1} [inst : Group G], IsPGroup p G ↔ ∀ (g : G), ∃ k, g ^ p ^ k = 1
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- An analogue of `Filter.HasBasis.tendsto_right_iff` for `TendstoUniformlyOn`.  -/
Filter.HasBasis.tendstoUniformlyOn_iff_of_uniformity : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {X : Type u_5} {ιβ : Type u_8} {F : X → α → β} {f : α → β}
  {l : Filter X} {s : Set α} {pβ : ιβ → Prop} {sβ : ιβ → Set (β × β)},
  (uniformity β).HasBasis pβ sβ →
    (TendstoUniformlyOn F f l s ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ x ∈ s, (f x, F n x) ∈ sβ i)
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- If `g` is surjective, then the kernel of `(id A) ⊗ g` is generated by the kernel of `g`  -/
Algebra.TensorProduct.lTensor_ker : ∀ {R : Type u_4} [inst : CommRing R] {A : Type u_6} {C : Type u_8} {D : Type u_9} [inst_1 : Ring A] [inst_2 : Ring C]
  [inst_3 : Ring D] [inst_4 : Algebra R A] [inst_5 : Algebra R C] [inst_6 : Algebra R D] (g : C →ₐ[R] D),
  Function.Surjective ⇑g →
    RingHom.ker (Algebra.TensorProduct.map (AlgHom.id R A) g) =
      Ideal.map Algebra.TensorProduct.includeRight (RingHom.ker g)
-- Init.Data.Array.Count
Array.count.eq_1 : ∀ {α : Type u} [inst : BEq α] (a : α) (as : Array α), Array.count a as = Array.countP (fun x => x == a) as
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus_eq_top_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.LocallyOfFiniteType f],
  AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus f = ⊤ ↔ AlgebraicGeometry.LocallyQuasiFinite f
-- Mathlib.Analysis.Convex.Topology
/-- If `x ∈ closure s` and `y ∈ interior s`, then the segment `(x, y]` is included in `interior s`.
 -/
Convex.add_smul_sub_mem_interior' : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E]
  [AddRightMono 𝕜] {s : Set E},
  Convex 𝕜 s → ∀ {x y : E}, x ∈ closure s → y ∈ interior s → ∀ {t : 𝕜}, t ∈ Set.Ioc 0 1 → x + t • (y - x) ∈ interior s
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Convert the tree to a list in ascending order.  -/
RBTree.RBNode.toList : {α : Type u_1} → RBTree.RBNode α → List α
-- Mathlib.Data.List.GetD
List.getD_surjective_iff : ∀ {α : Type u} {l : List α} {d : α}, (Function.Surjective fun x => l.getD x d) ↔ ∀ (x : α), x = d ∨ x ∈ l
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKeyD_insertMany_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k k' fallback : α},
      cmp k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
          k ∈ List.map Prod.fst l → (Std.DTreeMap.Raw.Const.insertMany t l).getKeyD k' fallback = k
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverExtension.mbtc : {σ : Type} → Lean.Meta.Grind.SolverExtension σ → Lean.Meta.Grind.GoalM Bool
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
isPrimitiveRoot_of_mem_primitiveRoots : ∀ {R : Type u_4} {k : ℕ} [inst : CommRing R] [inst_1 : IsDomain R] {ζ : R}, ζ ∈ primitiveRoots k R → IsPrimitiveRoot ζ k
-- Mathlib.Algebra.Lie.Subalgebra
LieHom.mem_range : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L₂ : Type w}
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) (x : L₂), x ∈ f.range ↔ ∃ y, f y = x
-- Mathlib.NumberTheory.KummerDedekind
quotAdjoinEquivQuotMap.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S} {I : Ideal R}
  (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (h_alg : Function.Injective ⇑(algebraMap (↥R[x]) S)),
  quotAdjoinEquivQuotMap hx h_alg = quotAdjoinEquivQuotMap hx h_alg
-- Mathlib.RingTheory.Localization.InvSubmonoid
IsLocalization.smul_toInvSubmonoid : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalization M S] (m : ↥M), m • ↑((IsLocalization.toInvSubmonoid M S) m) = 1
-- Mathlib.NumberTheory.Padics.PadicNumbers
Rat.padicValuation.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) [inst : Fact (Nat.Prime p)], Rat.padicValuation p = Rat.padicValuation p_1
-- Mathlib.Order.Partition.Finpartition
Finpartition.indiscrete_parts : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} (ha : a ≠ ⊥), (Finpartition.indiscrete ha).parts = {a}
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Functor.weightedLimObjMap_id : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (W : CategoryTheory.Functor J (Type w)) (F : CategoryTheory.Functor J C)
  [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F],
  W.weightedLimObjMap (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id (W.weightedLimObjObj F)