mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.DirectSum.Module
DirectSum.ker_lmap : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {N : ι → Type u_1} [inst_3 : (i : ι) → AddCommMonoid (N i)]
  [inst_4 : (i : ι) → Module R (N i)] (f : (i : ι) → M i →ₗ[R] N i),
  (DirectSum.lmap f).ker = Submodule.comap (DirectSum.coeFnLinearMap R) (Submodule.pi Set.univ fun i => (f i).ker)
-- Mathlib.Order.InitialSeg
InitialSeg.antisymm_symm : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r]
  [inst_1 : IsWellOrder β s] (f : InitialSeg r s) (g : InitialSeg s r), (f.antisymm g).symm = g.antisymm f
-- Mathlib.Algebra.Lie.CartanExists
/-- Let `L` be a Lie algebra of dimension `n` over a field `K` with at least `n` elements.
Given a Lie subalgebra `U` of `L`, and an element `x ∈ U` such that `U ≤ engel K x`.
Suppose that `engel K x` is minimal amongst the Engel subalgebras `engel K y` for `y ∈ U`.
Then `engel K x ≤ engel K y` for all `y ∈ U`.

Lemma 2 in [barnes1967].  -/
LieAlgebra.engel_isBot_of_isMin : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : LieRing L] [inst_2 : LieAlgebra K L] [Module.Finite K L],
  ↑(Module.finrank K L) ≤ Cardinal.mk K →
    ∀ (U : LieSubalgebra K L) (E : ↑{x | ∃ x_1 ∈ U, LieSubalgebra.engel K x_1 = x}), U ≤ ↑E → IsMin E → IsBot E
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.pow_card_mul_prod : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] {f : ι → M} {b : M},
  b ^ s.card * ∏ a ∈ s, f a = ∏ a ∈ s, b * f a
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
AlgebraicGeometry.Scheme.Hom.normalization.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} (f f_1 : X ⟶ Y) (e_f : f = f_1) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f],
  AlgebraicGeometry.Scheme.Hom.normalization f = AlgebraicGeometry.Scheme.Hom.normalization f_1
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.go : Lean.Expr → Bool → Bool → Lean.Meta.Grind.NormalizePattern.M✝ Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
CFC.log_exp : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A),
  autoParam (IsSelfAdjoint a) CFC.log_exp._auto_1 → CFC.log (NormedSpace.exp a) = a
-- Mathlib.Order.Closure
ClosureOperator.closure_sup_closure_le : ∀ {α : Type u_1} [inst : SemilatticeSup α] (c : ClosureOperator α) (x y : α), c x ⊔ c y ≤ c (x ⊔ y)
-- Mathlib.Order.Category.BddLat
BddLat.forget_lat_partOrd_eq_forget_bddOrd_partOrd : (CategoryTheory.forget₂ BddLat Lat).comp (CategoryTheory.forget₂ Lat PartOrd) =
  (CategoryTheory.forget₂ BddLat BddOrd).comp (CategoryTheory.forget₂ BddOrd PartOrd)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} {z₁ z₂ : CochainComplex.HomComplex.Cochain F G n},
  z₁ = z₂ ↔ ∀ (p q : ℤ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instSMulCommClass : ∀ {α : Type u_1} {R : Type u_3} [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal] {R' : Type u_4}
  [inst_2 : SMul R' ENNReal] [inst_3 : IsScalarTower R' ENNReal ENNReal] [SMulCommClass R R' ENNReal],
  SMulCommClass R R' (MeasureTheory.OuterMeasure α)
-- Mathlib.GroupTheory.OrderOfElement
orderOf_snd_dvd_orderOf : ∀ {α : Type u_4} {β : Type u_5} [inst : Monoid α] [inst_1 : Monoid β] {x : α × β}, orderOf x.2 ∣ orderOf x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_insertManyIfNewUnit_list_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] {l : List α},
  (t.insertManyIfNewUnit l).size ≤ t.size + l.length
-- Mathlib.Order.BoundedOrder.Basic
/-- **Alias** of `lt_top_of_lt`. -/
LT.lt.lt_top : ∀ {α : Type u} [inst : Preorder α] [inst_1 : OrderTop α] {a b : α}, a < b → a < ⊤
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.spanSingleton_inv : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K] (x : K),
  (FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x)⁻¹ = FractionalIdeal.spanSingleton (nonZeroDivisors R₁) x⁻¹
-- Mathlib.Data.Num.Basic
instZeroNum : Zero Num
-- Mathlib.Order.Interval.Set.Pi
Set.image_mulSingle_Icc_left : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → One (α i)] (i : ι) (a : α i), Pi.mulSingle i '' Set.Icc a 1 = Set.Icc (Pi.mulSingle i a) 1
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.closure_eq_of_le : ∀ {M : Type u_1} [inst : Add M] {s : Set M} {S : AddSubsemigroup M},
  s ⊆ ↑S → S ≤ AddSubsemigroup.closure s → AddSubsemigroup.closure s = S
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.adjunctionOfEquivLeft_counit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {G : CategoryTheory.Functor D C} {F_obj : C → D} (e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y))
  (he :
    ∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
      (e X Y') (CategoryTheory.CategoryStruct.comp h g) = CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g))
  (Y : D),
  (CategoryTheory.Adjunction.adjunctionOfEquivLeft e he).counit.app Y =
    (e (G.obj Y) Y).symm (CategoryTheory.CategoryStruct.id (G.obj Y))
-- Mathlib.Data.Finset.Max
Finset.max_eq_top : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : OrderTop α] {s : Finset α}, s.max = ⊤ ↔ ⊤ ∈ s
-- Mathlib.Data.List.Basic
List.map_filter : ∀ {α : Type u} {β : Type v} (p : α → Bool) {f : α → β},
  Function.Injective f →
    ∀ (l : List α) [inst : DecidablePred fun b => ∃ a, p a = true ∧ f a = b],
      List.map f (List.filter p l) = List.filter (fun b => decide (∃ a, p a = true ∧ f a = b)) (List.map f l)
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
/-- **Alias** of `LinearMap.BilinForm.mul_toMatrix`. -/
BilinForm.mul_toMatrix : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁)
  (B : LinearMap.BilinForm R₁ M₁) (M : Matrix n n R₁),
  M * (LinearMap.BilinForm.toMatrix b) B =
    (LinearMap.BilinForm.toMatrix b) (B.compLeft ((Matrix.toLin b b) M.transpose))
-- Init.Data.List.Basic
/-- Removes the first occurrence of `a` from `l`. If `a` does not occur in `l`, the list is returned
unmodified.

`O(|l|)`.

Examples:
* `[1, 5, 3, 2, 5].erase 5 = [1, 3, 2, 5]`
* `[1, 5, 3, 2, 5].erase 6 = [1, 5, 3, 2, 5]`
 -/
List.erase : {α : Type u_1} → [BEq α] → List α → α → List α
-- Mathlib.Data.Finset.Card
Finset.card_erase_lt_of_mem : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], a ∈ s → (s.erase a).card < s.card
-- Mathlib.Combinatorics.SimpleGraph.Walk.Counting
SimpleGraph.set_walk_length_toFinset_eq : ∀ {V : Type u} (G : SimpleGraph V) [inst : DecidableEq V] [inst_1 : G.LocallyFinite] (n : ℕ) (u v : V),
  {p | p.length = n}.toFinset = G.finsetWalkLength n u v
-- Std.Http.Internal.String
_private.Std.Http.Internal.String.0.Std.Http.Internal.UnquoteState.invalid : Std.Http.Internal.UnquoteState✝
-- Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
/-- Trivial corollary of
`circleAverage_log_norm_sub_const_eq_log_radius_add_posLog`: If `u : ℂ` lies within the closed ball
with center `c` and radius `R`, then the circle average
`circleAverage (log ‖· - u‖) c R` equals `log R`.
 -/
circleAverage_log_norm_sub_const_of_mem_closedBall : ∀ {a c : ℂ} {R : ℝ}, a ∈ Metric.closedBall c |R| → Real.circleAverage (fun x => Real.log ‖x - a‖) c R = Real.log R
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- **Fundamental theorem of calculus-2**, on the whole real line
When a function has a limit `m` at `-∞` and `n` at `+∞`, and its derivative is integrable, then the
integral of the derivative is `n - m`.

Note that such a function always has a limit at `-∞` and `+∞`,
see `tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic` and
`tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi`.  -/
MeasureTheory.integral_of_hasDerivAt_of_tendsto : ∀ {E : Type u_1} {f f' : ℝ → E} {m n : E} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E],
  (∀ (x : ℝ), HasDerivAt f (f' x) x) →
    MeasureTheory.Integrable f' MeasureTheory.volume →
      Filter.Tendsto f Filter.atBot (nhds m) → Filter.Tendsto f Filter.atTop (nhds n) → ∫ (x : ℝ), f' x = n - m
-- Mathlib.Algebra.Polynomial.Eval.SMul
Polynomial.smul_comp : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : SMulZeroClass S R] [IsScalarTower S R R] (s : S)
  (p q : Polynomial R), (s • p).comp q = s • p.comp q
-- Mathlib.NumberTheory.LSeries.Nonvanishing
/-- If `χ` is a bad character, then `F` is an entire function.  -/
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.BadChar.F_differentiable : ∀ {N : ℕ} [inst : NeZero N] (B : DirichletCharacter.BadChar✝ N), Differentiable ℂ (DirichletCharacter.BadChar.F✝ B)
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.one_le_rpow : ∀ {x : NNReal} {z : ℝ}, 1 ≤ x → 0 ≤ z → 1 ≤ x ^ z
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.subset_add_self : ∀ {G : Type u} [inst : AddGroup G] (B : AddGroupFilterBasis G) {U : Set G}, U ∈ B → U ⊆ U + U
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min!_empty : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α], ∅.min! = default
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ofList_eq_foldl : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List (α × β)},
  Std.ExtTreeMap.ofList l cmp = List.foldl (fun acc p => acc.insert p.1 p.2) ∅ l
-- Mathlib.Topology.Instances.ENat
ENat.instOrderTopology : OrderTopology ℕ∞
-- Aesop.Tree.Data
Aesop.NormalizationState.provenByNormalization.inj : ∀ {postState : Lean.Meta.SavedState} {script : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))}
  {postState_1 : Lean.Meta.SavedState}
  {script_1 : Array (Aesop.DisplayRuleName × Option (Array Aesop.Script.LazyStep))},
  Aesop.NormalizationState.provenByNormalization postState script =
      Aesop.NormalizationState.provenByNormalization postState_1 script_1 →
    postState = postState_1 ∧ script = script_1
-- Init.Data.Array.Erase
Array.erase_eq_empty_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : Array α} {a : α}, xs.erase a = #[] ↔ xs = #[] ∨ xs = #[a]
-- Std.Data.HashMap.Lemmas
Std.HashMap.any_eq_false_iff_forall_mem_getElem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α] {p : α → β → Bool},
  m.any p = false ↔ ∀ (a : α) (h : a ∈ m), p a m[a] = false
-- Mathlib.CategoryTheory.GuitartExact.VerticalComposition
CategoryTheory.TwoSquare.GuitartExact.vComp'_iff_of_equivalences : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {H₁ : CategoryTheory.Functor C₁ D₁} {L₁ : CategoryTheory.Functor C₁ C₂} {R₁ : CategoryTheory.Functor D₁ D₂}
  {H₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂) {H₃ : CategoryTheory.Functor C₃ D₃}
  (E : C₂ ≌ C₃) (E' : D₂ ≌ D₃) (w' : H₂.comp E'.functor ≅ E.functor.comp H₃) {L₁₂ : CategoryTheory.Functor C₁ C₃}
  {R₁₂ : CategoryTheory.Functor D₁ D₃} (eL : L₁.comp E.functor ≅ L₁₂) (eR : R₁.comp E'.functor ≅ R₁₂),
  (w.vComp' w'.hom eL eR).GuitartExact ↔ w.GuitartExact
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.eq_zero_of_frequently : ∀ {f : UpperHalfPlane → ℂ},
  MDiff f → ∀ {τ : UpperHalfPlane}, (∃ᶠ (z : UpperHalfPlane) in nhdsWithin τ {τ}ᶜ, f z = 0) → f = 0
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roo_eq_cons : ∀ {m n : ℤ}, m + 1 < n → (m<...n).toList = (m + 1) :: ((m + 1)<...n).toList
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.coe_coe_fst : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (e' : Bundle.Pretrivialization F Bundle.TotalSpace.proj) {b : B} {y : E b}, b ∈ e'.baseSet → (↑e' ⟨b, y⟩).1 = b
-- Mathlib.Order.WithBot
WithBot.unbotD_eq_unbotD_iff : ∀ {α : Type u_1} {d : α} {x y : WithBot α},
  WithBot.unbotD d x = WithBot.unbotD d y ↔ x = y ∨ x = ↑d ∧ y = ⊥ ∨ x = ⊥ ∧ y = ↑d
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instDivisionAddCommMonoid : {α : Type u_1} → [SubtractionCommMonoid α] → SubtractionCommMonoid (Colex α)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic
CFC.exp_eq_normedSpace_exp : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] {p : A → Prop} [inst_1 : NormedRing A] [inst_2 : StarRing A]
  [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : ContinuousFunctionalCalculus 𝕜 A p] {a : A},
  autoParam (p a) CFC.exp_eq_normedSpace_exp._auto_1 → cfc NormedSpace.exp a = NormedSpace.exp a
-- Mathlib.Tactic.GRewrite.Core
/-- The result returned by `Lean.MVarId.grewrite`.  -/
Mathlib.Tactic.GRewrite.GRewriteResult : Type
-- Mathlib.Analysis.Calculus.TangentCone.Basic
/-- Tangent cone of `s` at `x` depends only on `𝓝[s] x`.  -/
tangentConeAt_congr : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : SMul 𝕜 E] [inst_2 : TopologicalSpace E] {s t : Set E}
  {x : E} [ContinuousAdd E], nhdsWithin x s = nhdsWithin x t → tangentConeAt 𝕜 s x = tangentConeAt 𝕜 t x
-- Mathlib.RingTheory.Derivation.Basic
/-- We can push forward derivations using linear maps, i.e., the composition of a derivation with a
linear map is a derivation. Furthermore, this operation is linear on the spaces of derivations.  -/
LinearMap.compDer : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module A M] →
                [inst_5 : Module R M] →
                  {N : Type u_5} →
                    [inst_6 : AddCommMonoid N] →
                      [inst_7 : Module A N] →
                        [inst_8 : Module R N] →
                          [inst_9 : IsScalarTower R A M] →
                            [inst_10 : IsScalarTower R A N] → (M →ₗ[A] N) → Derivation R A M →ₗ[A] Derivation R A N
-- Mathlib.CategoryTheory.Sites.Point.Category
CategoryTheory.GrothendieckTopology.Point.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C} {Φ₁ Φ₂ : J.Point}
  {hom hom_1 : Φ₂.fiber ⟶ Φ₁.fiber}, { hom := hom } = { hom := hom_1 } → hom = hom_1
-- Mathlib.CategoryTheory.Sums.Basic
/-- Precomposing `swap` with the right inclusion gives the left inclusion.  -/
CategoryTheory.Sum.swapCompInr : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (CategoryTheory.Sum.inr_ C D).comp (CategoryTheory.Sum.swap C D) ≅ CategoryTheory.Sum.inl_ D C
-- Mathlib.Data.Finset.Defs
Finset.subset_def : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t ↔ s.val ⊆ t.val
-- Mathlib.Probability.Moments.Basic
ContinuousLinearMap.integral_id_map : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace ℝ E] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : NormedSpace ℝ F] [CompleteSpace E] [CompleteSpace F] [inst_9 : MeasurableSpace E]
  {μ : MeasureTheory.Measure E} [OpensMeasurableSpace E] [inst_11 : MeasurableSpace F] [BorelSpace F]
  [SecondCountableTopology F],
  MeasureTheory.Integrable id μ →
    ∀ (L : E →L[𝕜] F), ∫ (x : F), x ∂MeasureTheory.Measure.map (⇑L) μ = L (∫ (x : E), x ∂μ)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.CommRing.mk : Lean.Meta.Grind.Arith.CommRing.Ring →
  Option Lean.Expr →
    Option ℕ →
      Lean.Expr →
        Lean.Expr →
          Option Lean.Expr →
            Option Lean.Expr →
              Option (Lean.Expr × Lean.Expr × ℕ) →
                Lean.PArray (Lean.Expr × Lean.Meta.Grind.Arith.CommRing.RingExpr) →
                  ℕ →
                    ℕ →
                      Lean.Meta.Grind.Arith.CommRing.Queue →
                        List Lean.Meta.Grind.Arith.CommRing.EqCnstr →
                          Lean.PArray Lean.Meta.Grind.Arith.CommRing.DiseqCnstr →
                            Bool →
                              Lean.PHashSet Lean.Expr →
                                ℕ →
                                  Option Lean.Meta.Grind.Arith.CommRing.EqCnstr →
                                    Bool → Lean.Meta.Grind.Arith.CommRing.CommRing
-- Mathlib.Algebra.Category.BoolRing
/-- Typecheck a `RingHom` as a morphism in `BoolRing`.  -/
BoolRing.ofHom : {R S : Type u} →
  [inst : BooleanRing R] →
    [inst_1 : BooleanRing S] →
      (R →+* S) → ({ carrier := R, booleanRing := inst } ⟶ { carrier := S, booleanRing := inst_1 })
-- Mathlib.Order.Filter.CardinalInter
/-- `cardinalGenerate g hc` is the greatest `CardinalInterFilter c` containing `g`.  -/
Filter.cardinalGenerate_isGreatest : ∀ {α : Type u} {c : Cardinal.{u}} {g : Set (Set α)} (hc : 2 < c),
  IsGreatest {f | CardinalInterFilter f c ∧ g ⊆ f.sets} (Filter.cardinalGenerate g hc)
-- Init.Internal.Order.Basic
/-- The least upper bound of chains exists.
 -/
Lean.Order.CCPO.has_csup : ∀ {α : Sort u} [self : Lean.Order.CCPO α] {c : α → Prop}, Lean.Order.chain c → Exists (Lean.Order.is_sup c)
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.postcomposing₂_map_as_app_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : B) {X Y : a ⟶ b} (η : X ⟶ Y) (x : Bᵒᵖ)
  (x_1 : Opposite.unop x ⟶ a),
  (((CategoryTheory.Bicategory.postcomposing₂ a b).map η).as.app x).toNatTrans.app x_1 =
    CategoryTheory.Bicategory.whiskerLeft x_1 η
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_neg : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Neg G] [ContinuousNeg G] (a : G),
  Filter.Tendsto Neg.neg (nhds a) (nhds (-a))
-- Mathlib.Order.Basic
Prod.lt_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {x y : α × β},
  x < y ↔ x.1 < y.1 ∧ x.2 ≤ y.2 ∨ x.1 ≤ y.1 ∧ x.2 < y.2
-- Batteries.Util.ProofWanted
/-- `proof_wanted` is a synonym for `theorem_wanted`; see its documentation. (It is expected to be
deprecated in favour of `theorem_wanted` eventually.)  -/
proof_wanted : Lean.Parser.Parser
-- Mathlib.Computability.RegularExpressions
RegularExpression.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), RegularExpression.map f RegularExpression.zero = 0
-- Init.Data.List.Monadic
List.forIn'_loop_congr : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {xs : List α} [inst : Monad m] {as bs : List α}
  {f : (a' : α) → a' ∈ as → β → m (ForInStep β)} {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)} {b : β}
  (ha : ∃ ys, ys ++ xs = as) (hb : ∃ ys, ys ++ xs = bs),
  (∀ (a : α) (m_1 : a ∈ as) (m' : a ∈ bs) (b : β), f a m_1 b = g a m' b) →
    List.forIn'.loop as f xs b ha = List.forIn'.loop bs g xs b hb
-- Mathlib.Analysis.SpecialFunctions.Exp
ContinuousOn.rexp : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ} {s : Set α},
  ContinuousOn f s → ContinuousOn (fun y => Real.exp (f y)) s
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.right : {J : CategoryTheory.Limits.MultispanShape} → J.R → CategoryTheory.Limits.WalkingMultispan J
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited γ] {f : α → β → γ} {k k' : α},
  t.WF → t.getKey? k = some k' → (Std.TreeMap.Raw.map f t)[k]! = (Option.map (f k') t[k]?).get!
-- Mathlib.Data.List.InsertIdx
List.get_insertIdx_self : ∀ {α : Type u} (l : List α) (x : α) (n : ℕ) (hn : n ≤ l.length) (hn' : optParam (n < (l.insertIdx n x).length) ⋯),
  (l.insertIdx n x).get ⟨n, hn'⟩ = x
-- Mathlib.Topology.Algebra.UniformMulAction
uniformContinuous_mul_left' : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : UniformSpace R] [UniformContinuousConstSMul R R] (a : R),
  UniformContinuous fun b => a * b
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
/-- The next two statements say that `tateComplexFunctor` is an exact functor from `Rep R G` to
`CochainComplex (ModuleCat R) ℤ`.  -/
TateCohomology.preservesFiniteLimits_tateComplexFunctor : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G],
  CategoryTheory.Limits.PreservesFiniteLimits (tateComplexFunctor R G)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
/-- The predicate saying that a dependent function on an open `U` is realised as a fixed fraction
`r / s` of *same grading* in each of the stalks (which are localizations at various prime ideals).
 -/
AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.IsFraction : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          {𝒜 : ℕ → σ} →
            [inst_3 : GradedRing 𝒜] →
              {U : TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜)} →
                ((x : ↥U) → HomogeneousLocalization.AtPrime 𝒜 (↑x).asHomogeneousIdeal.toIdeal) → Prop
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
RootPairing.RootPositiveForm.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] (P P_1 : RootPairing ι R M N) (e_P : P = P_1)
  [inst_8 : P.IsValuedIn S], RootPairing.RootPositiveForm S P = RootPairing.RootPositiveForm S P_1
-- Mathlib.LinearAlgebra.Reflection
Module.injOn_dualMap_subtype_span_range_range : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_3}
  [IsAddTorsionFree M] {r : ι ↪ M} {c : ι → Module.Dual R M},
  (Set.range ⇑r).Finite →
    (∀ (i : ι), (c i) (r i) = 2) →
      (∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (r i) (c i))) (Set.range ⇑r) (Set.range ⇑r)) →
        Set.InjOn (⇑(Submodule.span R (Set.range ⇑r)).subtype.dualMap) (Set.range c)
-- Mathlib.Order.RelSeries
RelSeries.tail_toFun : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (len_pos : p.length ≠ 0) (a : Fin (p.length - 1 + 1)),
  (p.tail len_pos).toFun a = (Fin.tail p.toFun ∘ Fin.cast ⋯) a
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- The inclusion map from `E →[𝕜] F` to `E →WOT[𝕜] F`, bundled as a continuous linear map.  -/
ContinuousLinearMap.WOTofCLM : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        {σ : 𝕜₁ →+* 𝕜₂} →
          {E : Type u_3} →
            {F : Type u_4} →
              [inst_2 : AddCommGroup E] →
                [inst_3 : TopologicalSpace E] →
                  [inst_4 : Module 𝕜₁ E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : TopologicalSpace F] →
                        [inst_7 : Module 𝕜₂ F] →
                          [inst_8 : IsTopologicalAddGroup F] →
                            [inst_9 : ContinuousConstSMul 𝕜₂ F] →
                              [ContinuousSMul 𝕜₁ E] → (E →SL[σ] F) →L[𝕜₂] E →SWOT[σ] F
-- Mathlib.Tactic.ClickSuggestions.Apply
/-- The key that is used for sorting and deduplicating `apply` lemmas.  -/
Mathlib.Tactic.ClickSuggestions.ApplyKey : Type