mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Nilpotent
/-- Note that the below inequality can be strict. For example the ideal of strictly-upper-triangular
2x2 matrices inside the Lie algebra of upper-triangular 2x2 matrices with `k = 1`.  -/
LieModule.coe_lowerCentralSeries_ideal_le : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I : LieIdeal R L}
  (k : ℕ), ↑(LieModule.lowerCentralSeries R (↥I) (↥I) k) ≤ ↑(LieModule.lowerCentralSeries R L (↥I) k)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightIso_inverse_map_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) {Y X : CategoryTheory.Comma L R₂} (f : Y ⟶ X),
  ((CategoryTheory.Comma.mapRightIso L i).inverse.map f).right = f.right
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.tensorHom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X₁ Y₁ X₂ Y₂ : CategoryTheory.Grp C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom =
    CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom
-- Lean.Data.Position
/-- The positions of newline characters.
The first entry is always `0` and the last always the index of the last character.
In particular, if the last character is a newline, that index will appear twice.  -/
Lean.FileMap.positions : Lean.FileMap → Array String.Pos.Raw
-- Mathlib.RingTheory.WittVector.Defs
WittVector.hasNatScalar : {p : ℕ} → {R : Type u_1} → [hp : Fact (Nat.Prime p)] → [CommRing R] → SMul ℕ (WittVector p R)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycleOn.pow_card_apply : ∀ {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α}, f.IsCycleOn ↑s → a ∈ s → (f ^ s.card) a = a
-- Mathlib.Algebra.Group.Action.Defs
SMulCommClass.op_right : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} [inst : SMul M α] [inst_1 : SMul N α] [inst_2 : SMul Nᵐᵒᵖ α]
  [IsCentralScalar N α] [SMulCommClass M N α], SMulCommClass M Nᵐᵒᵖ α
-- Mathlib.Condensed.Discrete.Colimit
Condensed.isoLocallyConstantOfIsColimit_inv : ∀ (X : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [inst : CategoryTheory.Limits.PreservesFiniteProducts X]
  (hX : (S : Profinite) → CategoryTheory.Limits.IsColimit (X.mapCocone S.asLimitCone.op)),
  (Condensed.isoLocallyConstantOfIsColimit X hX).inv = CompHausLike.LocallyConstant.counitApp X
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- **Alias** of `MvPowerSeries.le_order_mul`.

---

The order of the product of two formal power series
is at least the sum of their orders.  -/
MvPowerSeries.order_mul_ge : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f g : MvPowerSeries σ R}, f.order + g.order ≤ (f * g).order
-- Mathlib.Algebra.Lie.Cochain
LieModule.Cohomology.d₁₂_apply_apply : ∀ (R : Type u_1) [inst : CommRing R] (L : Type u_2) [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (f : LieModule.Cohomology.oneCochain R L M) (x y : L),
  (((LieModule.Cohomology.d₁₂ R L M) f) x) y = ⁅x, f y⁆ - ⁅y, f x⁆ - f ⁅x, y⁆
-- Mathlib.Algebra.Group.Nat.Defs
Nat.instIsMulTorsionFree : IsMulTorsionFree ℕ
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
/-- The special-value formula `Γ(k + 1 + 1/2) = (2 * k + 1)‼ * √π / (2 ^ (k + 1))` for half-integer
values of the gamma function in terms of `Nat.doubleFactorial`.  -/
Real.Gamma_nat_add_one_add_half : ∀ (k : ℕ), Real.Gamma (↑k + 1 + 1 / 2) = ↑(2 * k + 1).doubleFactorial * √Real.pi / 2 ^ (k + 1)
-- Lean.Meta.Tactic.Simp.Simproc
/-- Builtin simproc declaration extension state.

It contains:
- The discrimination tree keys for each simproc (including symbolic evaluation procedures) name.
- The actual procedure associated with a name.
 -/
Lean.Meta.Simp.BuiltinSimprocs : Type
-- Mathlib.CategoryTheory.Category.ULift
/-- One half of the equivalence between `C` and `AsSmall C`.  -/
CategoryTheory.AsSmall.down : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor (CategoryTheory.AsSmall C) C
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
_private.Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors.0.«term_~ᵤ_» : Lean.TrailingParserDescr
-- Aesop.Script.Step
Aesop.Script.Step.instToMessageData : Lean.ToMessageData Aesop.Script.Step
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.addCommGroup : {R : Type u_1} →
  [inst : Ring R] →
    {R₂ : Type u_2} →
      [inst_1 : Ring R₂] →
        {M : Type u_4} →
          [inst_2 : TopologicalSpace M] →
            [inst_3 : AddCommGroup M] →
              {M₂ : Type u_5} →
                [inst_4 : TopologicalSpace M₂] →
                  [inst_5 : AddCommGroup M₂] →
                    [inst_6 : Module R M] →
                      [inst_7 : Module R₂ M₂] →
                        {σ₁₂ : R →+* R₂} → [IsTopologicalAddGroup M₂] → AddCommGroup (M →SL[σ₁₂] M₂)
-- Mathlib.Algebra.Group.TypeTags.Basic
Pi.single_additiveOfMul_eq : ∀ {ι : Type u_1} [inst : DecidableEq ι] {M : ι → Type u_2} [inst_1 : (i : ι) → Monoid (M i)] (i : ι) (a : M i) (j : ι),
  Pi.single i (Additive.ofMul a) j = Additive.ofMul (Pi.mulSingle i a j)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_bot' : ∀ {α : Type u_1} {E : Type u_3} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [hμ : NeZero μ] (f : α → E),
  μ[f | ⊥] = fun x => (μ.real Set.univ)⁻¹ • ∫ (x : α), f x ∂μ
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
/-- This holds true for all `x : ℝ` because of the junk values `0 / 0 = 0` and `log 0 = 0`.  -/
Real.log_div_self : ∀ (x : ℝ), Real.log (x / x) = 0
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalCommCStarAlgebra.mk : {A : Type u_1} →
  [toNonUnitalNormedCommRing : NonUnitalNormedCommRing A] →
    [toStarRing : StarRing A] →
      [toCompleteSpace : CompleteSpace A] →
        [toCStarRing : CStarRing A] →
          [toNormedSpace : NormedSpace ℂ A] →
            [toIsScalarTower : IsScalarTower ℂ A A] →
              [toSMulCommClass : SMulCommClass ℂ A A] → [toStarModule : StarModule ℂ A] → NonUnitalCommCStarAlgebra A
-- Mathlib.Combinatorics.Additive.Convolution
Finset.convolution.congr_simp : ∀ {G : Type u_1} [inst : Group G] {inst_1 : DecidableEq G} [inst_2 : DecidableEq G] (A A_1 : Finset G),
  A = A_1 → ∀ (B B_1 : Finset G), B = B_1 → ∀ (a a_1 : G), a = a_1 → A.convolution B a = A_1.convolution B_1 a_1
-- Mathlib.Tactic.Simps.Basic
Simps.Config.mk : Bool →
  Array Lean.Elab.Attribute →
    Bool →
      Bool →
        Lean.Meta.TransparencyMode →
          Lean.Meta.TransparencyMode → Bool → List Lean.Name → Bool → Option String → Simps.Config
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_insertManyIfNewUnit_list_le : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF → ∀ {l : List α}, (↑↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).size ≤ (↑m).size + l.length
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsFiltered.coeq.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {j j' : C}
  (f f_1 : j ⟶ j'),
  f = f_1 →
    ∀ (f' f'_1 : j ⟶ j'), f' = f'_1 → CategoryTheory.IsFiltered.coeq f f' = CategoryTheory.IsFiltered.coeq f_1 f'_1
-- Mathlib.GroupTheory.Congruence.Defs
Con.one.eq_1 : ∀ {M : Type u_1} [inst : Mul M] [inst_1 : One M] (c : Con M), c.one = { one := Quotient.mk'' 1 }
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.instIsMonHomTensorHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y Z W : C} [inst_3 : CategoryTheory.MonObj X]
  [inst_4 : CategoryTheory.MonObj Y] [inst_5 : CategoryTheory.MonObj Z] [inst_6 : CategoryTheory.MonObj W] {f : X ⟶ Y}
  {g : Z ⟶ W} [CategoryTheory.IsMonHom f] [CategoryTheory.IsMonHom g],
  CategoryTheory.IsMonHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)
-- Init.Data.Vector.Lemmas
Vector.allM_eq_not_anyM_not : ∀ {m : Type → Type u_1} {α : Type u_2} {n : ℕ} [inst : Monad m] [LawfulMonad m] {p : α → m Bool} {xs : Vector α n},
  Vector.allM p xs = (fun x => !x) <$> Vector.anyM (fun x => (fun x => !x) <$> p x) xs
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.Term.instCountableOfSigmaNatFunctions : ∀ {L : FirstOrder.Language} {α : Type u'} [h1 : Countable α] [h2 : Countable ((l : ℕ) × L.Functions l)],
  Countable (L.Term α)
-- Mathlib.Tactic.NormNum.DivMod
Mathlib.Meta.NormNum.isInt_ediv_neg : ∀ {a b q q' : ℤ}, Mathlib.Meta.NormNum.IsInt (a / -b) q → -q = q' → Mathlib.Meta.NormNum.IsInt (a / b) q'
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.hom_ext_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Type u_3}
  [inst_3 : Semiring A] [inst_4 : Algebra R A] {f g : TensorAlgebra R M →ₐ[R] A},
  f = g ↔ f.toLinearMap ∘ₗ TensorAlgebra.ι R = g.toLinearMap ∘ₗ TensorAlgebra.ι R
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfLEArgs.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (toLinearPreorderOfLEArgs : Std.Packages.LinearPreorderOfLEArgs α)
  (le_antisymm :
    autoParam
      (let this := toLinearPreorderOfLEArgs.le;
      ∀ (a b : α), a ≤ b → b ≤ a → a = b)
      Std.Packages.PartialOrderOfLEArgs.le_antisymm._autoParam)
  (min :
    autoParam
      (let this := toLinearPreorderOfLEArgs.le;
      let this := toLinearPreorderOfLEArgs.decidableLE;
      Min α)
      Std.Packages.LinearOrderOfLEArgs.min._autoParam)
  (max :
    autoParam
      (let this := toLinearPreorderOfLEArgs.le;
      let this := toLinearPreorderOfLEArgs.decidableLE;
      Max α)
      Std.Packages.LinearOrderOfLEArgs.max._autoParam)
  (min_eq :
    autoParam
      (let this := toLinearPreorderOfLEArgs.le;
      let this_1 := toLinearPreorderOfLEArgs.decidableLE;
      let this_2 := min;
      ∀ (a b : α), a ⊓ b = if a ≤ b then a else b)
      Std.Packages.LinearOrderOfLEArgs.min_eq._autoParam)
  (max_eq :
    autoParam
      (let this := toLinearPreorderOfLEArgs.le;
      let this_1 := toLinearPreorderOfLEArgs.decidableLE;
      let this_2 := max;
      ∀ (a b : α), a ⊔ b = if b ≤ a then a else b)
      Std.Packages.LinearOrderOfLEArgs.max_eq._autoParam),
  sizeOf
      { toLinearPreorderOfLEArgs := toLinearPreorderOfLEArgs, le_antisymm := le_antisymm, min := min, max := max,
        min_eq := min_eq, max_eq := max_eq } =
    1 + sizeOf toLinearPreorderOfLEArgs + sizeOf min + sizeOf max
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
Polynomial.isRoot_of_unity_of_root_cyclotomic : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} {ζ : R} {i : ℕ},
  i ∈ n.divisors → (Polynomial.cyclotomic i R).IsRoot ζ → ζ ^ n = 1
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffSection.instNeg : {𝕜 : 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} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {n : WithTop ℕ∞} →
                              {V : M → Type u_6} →
                                [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                  [inst_9 : (x : M) → TopologicalSpace (V x)] →
                                    [inst_10 : FiberBundle F V] →
                                      [inst_11 : (x : M) → AddCommGroup (V x)] →
                                        [inst_12 : (x : M) → Module 𝕜 (V x)] →
                                          [VectorBundle 𝕜 F V] → Neg (ContMDiffSection I F n V)
-- Mathlib.LinearAlgebra.Matrix.Block
/-- The inverse of a block-triangular matrix is block-triangular.  -/
Matrix.blockTriangular_inv_of_blockTriangular : ∀ {α : Type u_1} {m : Type u_3} {R : Type v} {M : Matrix m m R} {b : m → α} [inst : CommRing R] [inst_1 : DecidableEq m]
  [inst_2 : Fintype m] [inst_3 : LinearOrder α] [Invertible M], M.BlockTriangular b → M⁻¹.BlockTriangular b
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.coe_inj : ∀ {R : Type u_1} [inst : Semiring R] {φ ψ : Polynomial R}, ↑φ = ↑ψ ↔ φ = ψ
-- Init.Data.String.Substring
/-- Returns the position that's the specified number of characters forward from the given position in a
substring. If the end position of the substring is reached, it is returned.

Both the input position and the returned position are interpreted relative to the substring's start
position, not the underlying string.
 -/
Substring.Raw.nextn : Substring.Raw → ℕ → String.Pos.Raw → String.Pos.Raw
-- Std.Internal.Do.Order.Heyting
Lean.Order.instPreservesSupForallMeet : ∀ {σ : Type v} {β : σ → Type u} [inst : (s : σ) → Lean.Order.CompleteLattice (β s)]
  [∀ (s : σ) (c : β s), Lean.Order.PreservesSup (Lean.Order.meet c)] (a : (s : σ) → β s),
  Lean.Order.PreservesSup (Lean.Order.meet a)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernel.map_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasKernel f] (q : Y ⟶ Y)
  (w :
    CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id X) f),
  CategoryTheory.Limits.kernel.map f f (CategoryTheory.CategoryStruct.id X) q w =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.kernel f)
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_subset : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s t : Set M} {x : M} {V W : (x : M) → TangentSpace I x}
  [inst_6 : IsManifold I 2 M] [CompleteSpace E],
  s ⊆ t →
    UniqueMDiffAt[s] x →
      MDiffAt[t] (T% V) x →
        MDiffAt[t] (T% W) x → VectorField.mlieBracketWithin I V W s x = VectorField.mlieBracketWithin I V W t x
-- Mathlib.Algebra.Group.Hom.Instances
MonoidHom.compr₂_apply : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [inst : MulOneClass M] [inst_1 : MulOneClass N]
  [inst_2 : CommMonoid P] [inst_3 : CommMonoid Q] (f : M →* N →* P) (g : P →* Q) (m : M) (n : N),
  ((f.compr₂ g) m) n = g ((f m) n)
-- Mathlib.GroupTheory.Index
Subgroup.index_bot : ∀ {G : Type u_1} [inst : Group G], ⊥.index = Nat.card G
-- Mathlib.Data.DFinsupp.Multiset
DFinsupp.toMultiset_le_toMultiset : ∀ {α : Type u_1} [inst : DecidableEq α] {f g : Π₀ (_a : α), ℕ}, DFinsupp.toMultiset f ≤ DFinsupp.toMultiset g ↔ f ≤ g
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_union : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset α} {t₁ t₂ : Finset β},
  s • (t₁ ∪ t₂) = s • t₁ ∪ s • t₂
-- Mathlib.Tactic.Sat.FromLRAT
/-- Construct a literal. Positive numbers are translated to positive literals,
and negative numbers become negative literals. The input is assumed to be nonzero.  -/
Sat.Literal.ofInt : ℤ → Sat.Literal
-- Mathlib.AlgebraicTopology.DoldKan.PInfty
AlgebraicTopology.DoldKan.map_PInfty_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.Preadditive D]
  (G : CategoryTheory.Functor C D) [G.Additive] (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  AlgebraicTopology.DoldKan.PInfty.f n = G.map (AlgebraicTopology.DoldKan.PInfty.f n)
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
/-- Auxiliary definition for `reflection`: the reflection as a linear equivalence.  -/
Submodule.reflectionLinearEquiv : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] → (K : Submodule 𝕜 E) → [K.HasOrthogonalProjection] → E ≃ₗ[𝕜] E
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.IsRefl.ker_flip : ∀ {R : Type u_1} {R₁ : Type u_2} {M : Type u_5} {M₁ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : CommSemiring R₁] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R₁ M₁]
  {I₁ I₂ : R₁ →+* R} {B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M}, B.IsRefl → B.flip.ker = B.ker
-- Lean.Server.CodeActions.Provider
/-- Find the syntax on which to trigger tactic code actions.
This is a pure syntax pass, without regard to elaboration information.

* `preferred : String.Pos → Bool`: used to select "preferred `tacticSeq`s" based on the cursor
  column, when the cursor selection would otherwise be ambiguous. For example, in:
  ```
  · foo
    · bar
      baz
    |
  ```
  where the cursor is at the `|`, we select the `tacticSeq` starting with `foo`, while if the
  cursor was indented to align with `baz` then we would select the `bar; baz` sequence instead.

* `range`: the cursor selection. We do not do much with range selections; if a range selection
  covers more than one tactic then we abort.

* `root`: the root syntax to process

The return value is either a selected tactic, or a selected point in a tactic sequence.
 -/
Lean.CodeAction.findTactic? : (String.Pos.Raw → Bool) → Lean.Syntax.Range → Lean.Syntax → Option Lean.CodeAction.FindTacticResult
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.mk_eq_mk_iff' : ∀ {α : Type u_1} [inst : AddCommMonoid α] [IsCancelAdd α] {s : AddSubmonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s},
  AddLocalization.mk a₁ a₂ = AddLocalization.mk b₁ b₂ ↔ ↑b₂ + a₁ = ↑a₂ + b₁
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.measurableSMul₂_iterateAddAct : ∀ {α : Type u_2} {x : MeasurableSpace α} {f : α → α}, Measurable f → MeasurableVAdd₂ (IterateAddAct f) α
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.rootSpaceProduct.congr_simp : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H] (χ₁ χ₂ χ₃ : ↥H → R) (hχ : χ₁ + χ₂ = χ₃),
  LieAlgebra.rootSpaceProduct R L H χ₁ χ₂ χ₃ hχ = LieAlgebra.rootSpaceProduct R L H χ₁ χ₂ χ₃ hχ
-- Mathlib.Data.Complex.Basic
Complex.normSq_mk : ∀ (x y : ℝ), Complex.normSq { re := x, im := y } = x * x + y * y
-- Std.Time.Internal.Bounded
/-- Creates a new `Bounded` integer that the relation is less-equal.
 -/
Std.Time.Internal.Bounded.LE.exact : (val : ℕ) → Std.Time.Internal.Bounded.LE ↑val ↑val
-- Mathlib.Data.Finset.Insert
Finset.mem_insert : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, a ∈ insert b s ↔ a = b ∨ a ∈ s
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
/-- Given a sequence of finite sets `s₀ ⊆ s₁ ⊆ s₂ ⋯`, the sum of `gᵢ` over `i ∈ sₙ` is
equal to `∑_{i ∈ s₀} gᵢ` + `∑_{j < n, i ∈ sⱼ₊₁ \ sⱼ} gᵢ`. -/
Finset.sum_eq_sum_range_sdiff : ∀ {α : Type u_3} {β : Type u_4} [inst : DecidableEq α] [inst_1 : AddCommMonoid β] (s : ℕ → Finset α),
  Monotone s → ∀ (g : α → β) (n : ℕ), ∑ i ∈ s n, g i = ∑ i ∈ s 0, g i + ∑ i ∈ Finset.range n, ∑ j ∈ s (i + 1) \ s i, g j
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_inter_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → Std.DTreeMap.Raw.Const.get! (m₁ ∩ m₂) k = Std.DTreeMap.Raw.Const.get! m₁ k
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_roc_add_add_eq_append : ∀ {m n k : ℕ}, (m<...=m + n + k).toArray = (m<...=m + n).toArray ++ ((m + n)<...=m + n + k).toArray
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_union : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m₁ →
    Std.DHashMap.Internal.Raw.WFImp ↑m₂ →
      (Std.DHashMap.Internal.toListModel (↑(m₁.union m₂)).buckets).Perm
        (Std.Internal.List.insertList (Std.DHashMap.Internal.toListModel (↑m₁).buckets)
          (Std.DHashMap.Internal.toListModel (↑m₂).buckets))
-- Mathlib.LinearAlgebra.AffineSpace.Basis
mem_fintypeAffineCoords_iff_sum : ∀ {ι : Type u_1} {k : Type u_2} [inst : Ring k] [inst_1 : Fintype ι] {w : ι → k},
  w ∈ fintypeAffineCoords ι k ↔ ∑ i, w i = 1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_insertIfNew : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k a : α} {v : β},
  Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl a =
    if compare k a = Ordering.eq ∧ k ∉ t then some v else Std.DTreeMap.Internal.Impl.Const.get? t a
-- Lean.Meta.Tactic.SolveByElim
Lean.Meta.SolveByElim.ApplyRulesConfig.mk.sizeOf_spec : ∀ (toBacktrackConfig : Lean.Meta.Tactic.Backtrack.BacktrackConfig) (toApplyConfig : Lean.Meta.ApplyConfig)
  (transparency : Lean.Meta.TransparencyMode) (symm exfalso : Bool),
  sizeOf
      { toBacktrackConfig := toBacktrackConfig, toApplyConfig := toApplyConfig, transparency := transparency,
        symm := symm, exfalso := exfalso } =
    1 + sizeOf toBacktrackConfig + sizeOf toApplyConfig + sizeOf transparency + sizeOf symm + sizeOf exfalso
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.OneTruncation₂.nerveHomEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {X Y : SSet.OneTruncation₂ ((SSet.truncation 2).obj (CategoryTheory.nerve C))} (f : X ⟶ Y),
  SSet.OneTruncation₂.nerveHomEquiv f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.hom f.edge) (CategoryTheory.eqToHom ⋯))
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- `Finset α` is a `MulOneClass` under pointwise operations if `α` is.  -/
Finset.mulOneClass : {α : Type u_2} → [DecidableEq α] → [MulOneClass α] → MulOneClass (Finset α)
-- Init.PropLemmas
decide_eq_decide : ∀ {p q : Prop} {x : Decidable p} {x_1 : Decidable q}, decide p = decide q ↔ (p ↔ q)
-- Mathlib.Order.SuccPred.Archimedean
/-- If `a ≤ b` then one can get to `b` from `a` by iterating `pred`  -/
IsPredArchimedean.exists_pred_iterate_of_le : ∀ {α : Type u_3} {inst : Preorder α} {inst_1 : PredOrder α} [self : IsPredArchimedean α] {a b : α},
  a ≤ b → ∃ n, Order.pred^[n] b = a
-- Mathlib.Data.Multiset.Replicate
Multiset.eq_replicate_card : ∀ {α : Type u_1} {a : α} {s : Multiset α}, s = Multiset.replicate s.card a ↔ ∀ b ∈ s, b = a
-- Mathlib.Topology.IsLocalHomeomorph
IsLocalHomeomorphOn.mono : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s t : Set X},
  IsLocalHomeomorphOn f t → s ⊆ t → IsLocalHomeomorphOn f s
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.subst.injEq : ∀ (x : Int.Internal.Linear.Var) (c₁ : Lean.Meta.Grind.Arith.Cutsat.EqCnstr) (c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr)
  (x_1 : Int.Internal.Linear.Var) (c₁_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr)
  (c₂_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.subst x c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.subst x_1 c₁_1 c₂_1) =
    (x = x_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)