mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_mem_multiset : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (m : Multiset ι)
  (f : { x // x ∈ m } → M) (g : ι → M), (∀ (x : { x // x ∈ m }), f x = g ↑x) → ∑ x, f x = ∑ x ∈ m.toFinset, g x
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainBotCoeff_of_not_linearIndependent : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  ¬LinearIndependent R ![P.root i, P.root j] → RootPairing.chainBotCoeff i j = 0
-- Mathlib.Analysis.Convex.StrictConvexBetween
Sbtw.dist_lt_max_dist : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [StrictConvexSpace ℝ V]
  [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (p : P) {p₁ p₂ p₃ : P},
  Sbtw ℝ p₁ p₂ p₃ → dist p₂ p < max (dist p₁ p) (dist p₃ p)
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.hasForgetToAddCommMonoid : (R : Type u) → [inst : Semiring R] → CategoryTheory.HasForget₂ (SemimoduleCat R) AddCommMonCat
-- Mathlib.Algebra.Order.Module.Defs
instSMulPosMonoNatOfIsOrderedAddMonoid : ∀ {M : Type u_3} [inst : PartialOrder M] [inst_1 : AddCommMonoid M] [IsOrderedAddMonoid M], SMulPosMono ℕ M
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.contDiffAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞}, ContDiffWithinAt 𝕜 n f s x → s ∈ nhds x → ContDiffAt 𝕜 n f x
-- Mathlib.Order.LiminfLimsup
GaloisConnection.l_limsup_le : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice β]
  [inst_1 : ConditionallyCompleteLattice γ] {f : Filter α} {v : α → β} {l : β → γ} {u : γ → β},
  GaloisConnection l u →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f fun x => l (v x)) GaloisConnection.l_limsup_le._auto_1 →
      autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f v) GaloisConnection.l_limsup_le._auto_3 →
        l (Filter.limsup v f) ≤ Filter.limsup (fun x => l (v x)) f
-- Mathlib.Analysis.Fourier.RiemannLebesgueLemma
/-- Riemann-Lebesgue lemma for functions on a finite-dimensional inner-product space, formulated
via dual space. **Do not use** -- it is only a stepping stone to
`tendsto_integral_exp_smul_cocompact` where the inner-product-space structure isn't required.  -/
tendsto_integral_exp_smul_cocompact_of_inner_product : ∀ {E : Type u_1} {V : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : V → E)
  [inst_2 : NormedAddCommGroup V] [inst_3 : MeasurableSpace V] [BorelSpace V] [inst_5 : InnerProductSpace ℝ V]
  [FiniteDimensional ℝ V] (μ : MeasureTheory.Measure V) [μ.IsAddHaarMeasure],
  Filter.Tendsto (fun w => ∫ (v : V), Real.fourierChar (-w v) • f v ∂μ) (Filter.cocompact (StrongDual ℝ V)) (nhds 0)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_filterMapWithPostcondition.match_3.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α m β] →
      {it : Std.IterM m β} →
        (motive : it.Step → Sort u_3) →
          (x : it.Step) →
            ((it' : Std.IterM m β) →
                (out : β) →
                  (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
              ((it' : Std.IterM m β) →
                  (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
                ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.CategoryTheory.Localization.Predicate
/-- The equivalence of categories `(D ⥤ E) ≌ (W.FunctorsInverting E)` induced by
the composition with a localization functor `L : C ⥤ D` with respect to
`W : MorphismProperty C`.  -/
CategoryTheory.Localization.functorEquivalence : {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] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            (E : Type u_3) →
              [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
                [L.IsLocalization W] → CategoryTheory.Functor D E ≌ W.FunctorsInverting E
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.IsReflection.pow_two : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} {cs : CoxeterSystem M W} {t : W},
  cs.IsReflection t → t ^ 2 = 1
-- Mathlib.Data.Finset.Slice
Set.Sized.empty_mem_iff : ∀ {α : Type u_1} {A : Set (Finset α)} {r : ℕ}, Set.Sized r A → (∅ ∈ A ↔ A = {∅})
-- Mathlib.NumberTheory.Niven
/-- `sin(q * π)` for `q : ℚ` is algebraic over `ℤ`, using the real `sin` function.  -/
Real.isAlgebraic_sin_rat_mul_pi : ∀ (q : ℚ), IsAlgebraic ℤ (Real.sin (↑q * Real.pi))
-- Lean.Elab.Tactic.Monotonicity
/-- Finds tagged monotonicity theorems of the form `monotone (fun x => e)`.
 -/
Lean.Meta.Monotonicity.findMonoThms : Lean.Expr → Lean.MetaM (Array Lean.Name)
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.mk : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : Group N] →
        [inst_1 : Group E] →
          [inst_2 : Group G] →
            {S : GroupExtension N E G} →
              {E' : Type u_4} →
                [inst_3 : Group E'] →
                  {S' : GroupExtension N E' G} →
                    (toMulEquiv : E ≃* E') →
                      ⇑toMulEquiv ∘ ⇑S.inl = ⇑S'.inl → ⇑S'.rightHom ∘ ⇑toMulEquiv = ⇑S.rightHom → S.Equiv S'
-- Mathlib.Analysis.Normed.Ring.InfiniteSum
Summable.mul_norm : ∀ {R : Type u_1} {ι : Type u_2} {ι' : Type u_3} [inst : NormedRing R] {f : ι → R} {g : ι' → R},
  (Summable fun x => ‖f x‖) → (Summable fun x => ‖g x‖) → Summable fun x => ‖f x.1 * g x.2‖
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.mvarName : Lean.Expr → Lean.MetaM Lean.Name
-- Mathlib.Data.List.AList
AList.insert_union : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {s₁ s₂ : AList β},
  AList.insert a b (s₁ ∪ s₂) = AList.insert a b s₁ ∪ s₂
-- Mathlib.MeasureTheory.Measure.PreVariation
MeasureTheory.ennrealPreVariation_zero : ∀ {X : Type u_1} [inst : MeasurableSpace X], MeasureTheory.ennrealPreVariation 0 ⋯ ⋯ = 0
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.degree_quadratic_le : ∀ {R : Type u} {a b c : R} [inst : Semiring R],
  (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c).degree ≤ 2
-- Mathlib.Algebra.Category.MonCat.Limits
/-- The forgetful functor from commutative additive monoids to types preserves all limits.  -/
AddCommMonCat.forget_createsLimitsOfSize : CategoryTheory.CreatesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddMonCat)
-- Mathlib.Algebra.Order.Ring.Abs
sq_lt_sq : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α}, a ^ 2 < b ^ 2 ↔ |a| < |b|
-- Mathlib.GroupTheory.Sylow
Sylow.instCoeOutSubgroup : {p : ℕ} → {G : Type u_1} → [inst : Group G] → CoeOut (Sylow p G) (Subgroup G)
-- Mathlib.Analysis.Meromorphic.Basic
/-- If `f` is meromorphic, if `g` agrees with `f` on a codiscrete set, then `g` is also meromorphic.
 -/
Meromorphic.congr_codiscrete : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E}, Meromorphic f → f =ᶠ[Filter.codiscrete 𝕜] g → Meromorphic g
-- Mathlib.CategoryTheory.Limits.FintypeCat
CategoryTheory.Limits.FintypeCat.instHasColimitsOfShapeFintypeCatOfFinCategory : ∀ {J : Type} [inst : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J],
  CategoryTheory.Limits.HasColimitsOfShape J FintypeCat
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.keys_eq_keys_toListModel : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β},
  m.keys = Std.Internal.List.keys (Std.DHashMap.Internal.toListModel m.buckets)
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.comap_inf : ∀ {K : Type u} {L : Type v} [inst : DivisionRing K] [inst_1 : DivisionRing L] (s t : Subfield L) (f : K →+* L),
  Subfield.comap f (s ⊓ t) = Subfield.comap f s ⊓ Subfield.comap f t
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- The adjunction between the forgetful functor and the indiscrete topology functor.  -/
TopModuleCat.indiscreteAdj : (R : Type u) →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] → CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R) ⊣ TopModuleCat.indiscrete R
-- Mathlib.LinearAlgebra.Determinant
/-- In a finite-dimensional vector space, the zero map has determinant `1` in dimension `0`,
and `0` otherwise. We give a formula that also works in infinite dimension, where we define
the determinant to be `1`.  -/
LinearMap.det_zero : ∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M] [Module.Free A M],
  LinearMap.det 0 = 0 ^ Module.finrank A M
-- Aesop.Forward.State
Aesop.ClusterState.instToMessageData : Lean.ToMessageData Aesop.ClusterState
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkSpecializes_stalkPushforward_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  (f : X ⟶ Y) (F : TopCat.Presheaf C X) {x y : ↑X} (h : x ⤳ y) {F_1 : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F_1 X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory C F_1]
  (x_1 : carrier (((TopCat.Presheaf.pushforward C f).obj F).stalk ((TopCat.Hom.hom f) y))),
  (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.stalkPushforward C f F x))
      ((CategoryTheory.ConcreteCategory.hom (((TopCat.Presheaf.pushforward C f).obj F).stalkSpecializes ⋯)) x_1) =
    (CategoryTheory.ConcreteCategory.hom (F.stalkSpecializes h))
      ((CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.stalkPushforward C f F y)) x_1)
-- Lean.Meta.Tactic.Simp.Rewrite
_private.Lean.Meta.Tactic.Simp.Rewrite.0.Lean.Meta.Simp.dischargeUsingAssumption? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)
-- Mathlib.RingTheory.Congruence.Basic
RingCon.instDistribMulActionQuotientOfIsScalarTower : {α : Type u_1} →
  {R : Type u_3} →
    [inst : Monoid α] →
      [inst_1 : NonAssocSemiring R] →
        [inst_2 : DistribMulAction α R] → [IsScalarTower α R R] → (c : RingCon R) → DistribMulAction α c.Quotient
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
FreeSimplexQuiver.Hom.δ.sizeOf_spec : ∀ {n : ℕ} (i : Fin (n + 2)), sizeOf (FreeSimplexQuiver.Hom.δ i) = 1 + sizeOf n + sizeOf i
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsAddMonHom.zero_hom_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {M' N' : C}
  {inst_2 : CategoryTheory.AddMonObj M'} {inst_3 : CategoryTheory.AddMonObj N'} (f : M' ⟶ N')
  [self : CategoryTheory.IsAddMonHom f] {Z : C} (h : N' ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero h
-- Std.Internal.Do.Triple.Basic
/-- A program whose `match`/`if`/`do` elaboration postpones on a metavariable expected type and so
needs the monadic-application hint `(_ : _ → _) _` to recover its monad by first-order unification.  -/
_private.Std.Internal.Do.Triple.Basic.0.Std.Internal.Do.isSplitProgram : Lean.Syntax → Bool
-- Mathlib.Analysis.InnerProductSpace.OfNorm
/-- Auxiliary definition for the `add_left` property.  -/
_private.Mathlib.Analysis.InnerProductSpace.OfNorm.0.InnerProductSpaceable.innerProp' : {𝕜 : Type u_1} → [inst : RCLike 𝕜] → (E : Type u_2) → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → 𝕜 → Prop
-- Init.Tactics
/-- The `norm_cast` family of tactics is used to normalize certain coercions (*casts*) in expressions.
- `norm_cast` normalizes casts in the target.
- `norm_cast at h` normalizes casts in hypothesis `h`.

The tactic is basically a version of `simp` with a specific set of lemmas to move casts
upwards in the expression.
Therefore even in situations where non-terminal `simp` calls are discouraged (because of fragility),
`norm_cast` is considered to be safe.
It also has special handling of numerals.

For instance, given an assumption
```lean
a b : ℤ
h : ↑a + ↑b < (10 : ℚ)
```
writing `norm_cast at h` will turn `h` into
```lean
h : a + b < 10
```

There are also variants of basic tactics that use `norm_cast` to normalize expressions during
their operation, to make them more flexible about the expressions they accept
(we say that it is a tactic *modulo* the effects of `norm_cast`):
- `exact_mod_cast` for `exact` and `apply_mod_cast` for `apply`.
  Writing `exact_mod_cast h` and `apply_mod_cast h` will normalize casts
  in the goal and `h` before using `exact h` or `apply h`.
- `rw_mod_cast` for `rw`. It applies `norm_cast` between rewrites.
- `assumption_mod_cast` for `assumption`.
  This is effectively `norm_cast at *; assumption`, but more efficient.
  It normalizes casts in the goal and, for every hypothesis `h` in the context,
  it will try to normalize casts in `h` and use `exact h`.

See also `push_cast`, which moves casts inwards rather than lifting them outwards.
 -/
Lean.Parser.Tactic.tacticNorm_cast__ : Lean.ParserDescr
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.nnnorm_def : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)), ‖f‖₊ = (MeasureTheory.eLpNorm (↑↑f) p μ).toNNReal
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet.isEmpty : {α : Type u_1} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashSet α → Bool
-- ProofWidgets.Data.Html
ProofWidgets.LayoutKind.block : ProofWidgets.LayoutKind
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.map_directSumDecompose : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] [inst_4 : DecidableEq ι] [inst_5 : AddMonoid ι]
  [inst_6 : AddSubmonoidClass σ A] [inst_7 : AddSubmonoidClass τ B] (𝒜 : ι → σ) (ℬ : ι → τ) [inst_8 : GradedRing 𝒜]
  [inst_9 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ) {x : A} {i : ι},
  f ↑(((DirectSum.decompose 𝒜) x) i) = ↑(((DirectSum.decompose ℬ) (f x)) i)
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
HasFPowerSeriesOnBall.fderiv_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {f : E → F} {x : E} [CompleteSpace F],
  HasFPowerSeriesOnBall f p x r →
    ∀ {y : E}, ↑‖y‖₊ < r → fderiv 𝕜 f (x + y) = (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin y 1)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_sup_comap_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F},
  Function.Surjective ⇑f →
    ∀ (S T : AddSubmonoid N), AddSubmonoid.map f (AddSubmonoid.comap f S ⊔ AddSubmonoid.comap f T) = S ⊔ T
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey_eq_get_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.maxKey he = t.maxKey?.get ⋯
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.uniformContinuous_coe : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β], UniformContinuous DFunLike.coe
-- Lean.Meta.CtorIdxHInj
Lean.Meta.mkCtorIdxHInjTheoremNameFor : Lean.Name → Lean.Name
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getEntryLED_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : (a : α) × β a}, t₁.Equiv t₂ → t₁.getEntryLED k fallback = t₂.getEntryLED k fallback
-- Mathlib.Probability.HasLaw
ProbabilityTheory.iIndepFun_iff_hasLaw_pi_pi : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
  {ι : Type u_3} [inst : Fintype ι] {𝓧 : ι → Type u_4} {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)}
  {μ : (i : ι) → MeasureTheory.Measure (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i},
  (∀ (i : ι), ProbabilityTheory.HasLaw (X i) (μ i) P) →
    (ProbabilityTheory.iIndepFun X P ↔ ProbabilityTheory.HasLaw (fun ω i => X i ω) (MeasureTheory.Measure.pi μ) P)
-- Mathlib.Topology.Bornology.Absorbs
Absorbs.eq_1 : ∀ (M : Type u_1) {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] (s t : Set α),
  Absorbs M s t = ∀ᶠ (a : M) in Bornology.cobounded M, t ⊆ a • s
-- Lean.Elab.Do.Basic
/-- Call `caller` with a duplicable proxy of `dec`.
When the proxy is elaborated more than once, a join point is introduced so that `dec` is only
elaborated once to fill in the RHS of this join point.

This is useful for control-flow constructs like `if` and `match`, where multiple tail-called
branches share the continuation.
 -/
Lean.Elab.Do.DoElemCont.withDuplicableCont : Lean.Elab.Do.DoElemCont →
  Lean.Elab.Do.ControlInfo → (Lean.Elab.Do.DoElemCont → Lean.Elab.Do.DoElabM Lean.Expr) → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.RingTheory.Ideal.GoingUp
/-- **Alias** of `Ideal.IsIntegral.isMaximal_of_isMaximal_comap`. -/
Ideal.IntegralClosure.isMaximal_of_isMaximal_comap : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_3} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.IsIntegral R A] (I : Ideal A) [I.IsPrime], (Ideal.comap (algebraMap R A) I).IsMaximal → I.IsMaximal
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_le_iff_forall_finset_subset_card_le : ∀ {α : Type u} {n : ℕ} {t : Set α}, Cardinal.mk ↑t ≤ ↑n ↔ ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.bound' : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]},
  ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 →
    Filter.Tendsto (fun n => ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * T_gen✝ p F a ^ 2 ^ n) Filter.atTop
      (nhds 0)
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndepOn.extend.congr_simp : ∀ {ι : Type u'} {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {v v_1 : ι → V} (e_v : v = v_1) {s s_1 : Set ι} (e_s : s = s_1) {t t_1 : Set ι} (e_t : t = t_1)
  (hs : LinearIndepOn K v s) (hst : s ⊆ t) (a a_1 : ι), a = a_1 → hs.extend hst a = ⋯.extend ⋯ a_1
-- Std.Data.DTreeMap.Internal.Operations
/-- The tree is balanced.  -/
Std.DTreeMap.Internal.Impl.SizedBalancedTree.balanced_impl : ∀ {α : Type u} {β : α → Type v} {lb ub : ℕ} (self : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β lb ub),
  self.impl.Balanced
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_rco_eq_none : ∀ {m n i : ℕ}, n ≤ i + m → (m...n).toList[i]? = none
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.tendsto_integral_Ioi_zero : ∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [l.IsCountablyGenerated]
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {b : ι → ℝ} {f : ℝ → E},
  Filter.Tendsto b l Filter.atTop → Filter.Tendsto (fun i => ∫ (x : ℝ) in Set.Ioi (b i), f x ∂μ) l (nhds 0)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.mem_toSubmodule : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L)
  {x : L}, x ∈ L'.toSubmodule ↔ x ∈ L'
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.tr.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} (enc : Γ → List.Vector Bool n) (dec : List.Vector Bool n → Γ)
  (M : Λ → Turing.TM1.Stmt Γ Λ σ) (a : Γ) (q : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1to1.tr enc dec M (Turing.TM1to1.Λ'.write a q) =
    Turing.TM1to1.write (enc a).toList (Turing.TM1to1.move n Turing.Dir.left (Turing.TM1to1.trNormal dec q))
-- Mathlib.Data.Sigma.Lex
PSigma.Lex.mono_right : ∀ {ι : Sort u_1} {α : ι → Sort u_2} {r : ι → ι → Prop} {s₁ s₂ : (i : ι) → α i → α i → Prop},
  (∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b) → ∀ {a b : (i : ι) ×' α i}, PSigma.Lex r s₁ a b → PSigma.Lex r s₂ a b
-- Mathlib.Order.Hom.Lattice
InfHom.instBoundedOrder : {α : Type u_2} →
  {β : Type u_3} → [inst : Min α] → [inst_1 : SemilatticeInf β] → [BoundedOrder β] → BoundedOrder (InfHom α β)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Prod.braiding_counitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  (CategoryTheory.Prod.braiding C D).counitIso =
    CategoryTheory.Iso.refl ((CategoryTheory.Prod.swap D C).comp (CategoryTheory.Prod.swap C D))
-- Mathlib.Data.Finset.NAry
Finset.image₂_insert_right : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s : Finset α} {t : Finset β}
  {b : β} [inst_1 : DecidableEq β],
  Finset.image₂ f s (insert b t) = Finset.image (fun a => f a b) s ∪ Finset.image₂ f s t
-- Init.Data.SInt.Lemmas
ISize.toInt8_toInt16 : ∀ (n : ISize), n.toInt16.toInt8 = n.toInt8
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey?_insertManyIfNewUnit_emptyWithCapacity_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  l.contains k = false →
    (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)).getKey? k =
      none
-- Mathlib.Logic.IsEmpty.Basic
rightTotal_iff_isEmpty_right : ∀ {α : Type u_4} {β : Type u_5} (R : α → β → Prop) [IsEmpty α], Relator.RightTotal R ↔ IsEmpty β
-- Lean.Data.Lsp.Basic
Lean.Lsp.ChangeAnnotation.mk.inj : ∀ {label : String} {needsConfirmation : Bool} {description? : Option String} {label_1 : String}
  {needsConfirmation_1 : Bool} {description?_1 : Option String},
  { label := label, needsConfirmation := needsConfirmation, description? := description? } =
      { label := label_1, needsConfirmation := needsConfirmation_1, description? := description?_1 } →
    label = label_1 ∧ needsConfirmation = needsConfirmation_1 ∧ description? = description?_1
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.le_himp_of_meet_le_comm : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R : l}
  [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.PartialOrder.rel (Lean.Order.meet Q P) R → Lean.Order.PartialOrder.rel P (Lean.Order.himp Q R)
-- Mathlib.RepresentationTheory.Rep.Iso
/-- Auxiliary definition for `toModuleMonoidAlgebra`.  -/
Rep.toModuleMonoidAlgebraMap : {k : Type u} →
  {G : Type v} →
    [inst : CommRing k] →
      [inst_1 : Monoid G] →
        {V W : Rep.{w, u, v} k G} →
          (V ⟶ W) → (ModuleCat.of (MonoidAlgebra k G) V.ρ.asModule ⟶ ModuleCat.of (MonoidAlgebra k G) W.ρ.asModule)
-- Mathlib.Logic.Function.Iterate
/-- If a function `g` is invariant under composition with a function `f` (i.e., `g ∘ f = g`), then
`g` is invariant under composition with any iterate of `f`.  -/
Function.iterate_invariant : ∀ {α : Type u} {β : Type v} {f : α → α} {g : α → β}, g ∘ f = g → ∀ (n : ℕ), g ∘ f^[n] = g
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.endSection.inj : ∀ {stx : Lean.Syntax} {id? : Option Lean.Name} {danglingDot : Bool} {scopeNames : List String} {stx_1 : Lean.Syntax}
  {id?_1 : Option Lean.Name} {danglingDot_1 : Bool} {scopeNames_1 : List String},
  Lean.Elab.CompletionInfo.endSection stx id? danglingDot scopeNames =
      Lean.Elab.CompletionInfo.endSection stx_1 id?_1 danglingDot_1 scopeNames_1 →
    stx = stx_1 ∧ id? = id?_1 ∧ danglingDot = danglingDot_1 ∧ scopeNames = scopeNames_1