mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
rTensor.inverse_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [inst_7 : AddCommGroup Q] [inst_8 : Module R Q]
  (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) (y : TensorProduct R N Q),
  (rTensor.inverse Q hfg hg) ((LinearMap.rTensor Q g) y) = Submodule.Quotient.mk y
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.range_sin : Set.range Complex.sin = Set.univ
-- Init.Data.Order.MinMaxOn
instAssociativeMinOnOfIsLinearPreorder : ∀ {β : Type u_1} {α : Sort u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β},
  Std.Associative (minOn f)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.instPartialOrder : {α : Type u_1} → [inst : TopologicalSpace α] → PartialOrder (TopologicalSpace.NonemptyCompacts α)
-- Lean.Expr
Lean.Expr.fvar.inj : ∀ {fvarId fvarId_1 : Lean.FVarId}, Lean.Expr.fvar fvarId = Lean.Expr.fvar fvarId_1 → fvarId = fvarId_1
-- Mathlib.Algebra.Opposites
AddOpposite.instDecidableEq : {α : Type u_1} → [DecidableEq α] → DecidableEq αᵃᵒᵖ
-- Init.Grind.AC
Lean.Grind.AC.Context.vars : {α : Sort u} → Lean.Grind.AC.Context α → Lean.RArray (PLift α)
-- Mathlib.Topology.ClusterPt
Filter.EventuallyEq.mapClusterPt_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {F : Filter α} {u : α → X} {x : X} {v : α → X},
  u =ᶠ[F] v → (MapClusterPt x F u ↔ MapClusterPt x F v)
-- Mathlib.Analysis.Convex.Between
sbtw_const_vsub_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P} (p : P), Sbtw R (p -ᵥ x) (p -ᵥ y) (p -ᵥ z) ↔ Sbtw R x y z
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.comp.eq_2 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x : CategoryTheory.WithTerminal C) (_X : C),
  CategoryTheory.WithTerminal.comp =
    match (motive := (x x_1 x_2 : CategoryTheory.WithTerminal C) → x.Hom x_1 → x_1.Hom x_2 → x.Hom x_2)
      CategoryTheory.WithTerminal.of _X, x, CategoryTheory.WithTerminal.star with
    | CategoryTheory.WithTerminal.of _X, CategoryTheory.WithTerminal.of _Y, CategoryTheory.WithTerminal.of _Z =>
      fun f g => CategoryTheory.CategoryStruct.comp f g
    | CategoryTheory.WithTerminal.of _X, x, CategoryTheory.WithTerminal.star => fun _f _g => PUnit.unit
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of _X, x => fun f _g => PEmpty.elim f
    | x, CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.of _Y => fun _f g => PEmpty.elim g
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star =>
      fun x x_1 => PUnit.unit
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inrCompInrCompInverseAssociator_hom_app_down : ∀ (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] (X : E),
  ((CategoryTheory.sum.inrCompInrCompInverseAssociator C D E).hom.app X).down =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (Sum.inr X)).down
      (CategoryTheory.CategoryStruct.id (Sum.inr X)).down
-- Init.Grind.Interactive
/-- `finish?` tries to close the current goal using `grind`'s default strategy and suggests a tactic script.  -/
Lean.Parser.Tactic.Grind.finishTrace : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- Given
```
Y₃ - i₃ -> X₃
|          |
g₂         f₂
∨          ∨
Y₂ - i₂ -> X₂
|          |
g₁         f₁
∨          ∨
Y₁ - i₁ -> X₁
```
The big square is a pushout if both the small squares are.
 -/
CategoryTheory.Limits.pasteVertIsPushout : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {Y₃ Y₂ Y₁ X₃ : C} →
      {g₂ : Y₃ ⟶ Y₂} →
        {g₁ : Y₂ ⟶ Y₁} →
          {i₃ : Y₃ ⟶ X₃} →
            {t₁ : CategoryTheory.Limits.PushoutCocone g₂ i₃} →
              {i₂ : Y₂ ⟶ t₁.pt} →
                {t₂ : CategoryTheory.Limits.PushoutCocone g₁ i₂} →
                  (hi₂ : i₂ = t₁.inl) →
                    CategoryTheory.Limits.IsColimit t₁ →
                      CategoryTheory.Limits.IsColimit t₂ → CategoryTheory.Limits.IsColimit (t₁.pasteVert t₂ hi₂)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Sections
CategoryTheory.MonoidalClosed.curry.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X Y : C}
  [inst_2 : CategoryTheory.Closed A],
  CategoryTheory.MonoidalClosed.curry = ⇑((CategoryTheory.ihom.adjunction A).homEquiv Y X)
-- Lean.Elab.Tactic.Try
/-- Given a set of declaration names, returns `grind` parameters of the form `= <declName>`  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkGrindEqnParams : Array Lean.Name → Lean.MetaM (Array (Lean.TSyntax `Lean.Parser.Tactic.grindParam))
-- Mathlib.Data.Subtype
Subtype.restrict_def : ∀ {α : Sort u_4} {β : Type u_5} (f : α → β) (p : α → Prop), Subtype.restrict p f = f ∘ fun a => ↑a
-- Init.Data.String.Basic
String.Pos.ofToSlice_comp_toSlice : ∀ {s : String}, String.Pos.ofToSlice ∘ String.Pos.toSlice = id
-- Init.Data.Vector.Zip
Vector.zip_replicate : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} {n : ℕ},
  (Vector.replicate n a).zip (Vector.replicate n b) = Vector.replicate n (a, b)
-- Mathlib.Algebra.Order.Group.End
RelEmbedding.mul_apply : ∀ {α : Type u_1} {r : α → α → Prop} (e₁ e₂ : r ↪r r) (x : α), (e₁ * e₂) x = e₁ (e₂ x)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopicRel.equivalence : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {S : Set X},
  Equivalence fun f g => f.HomotopicRel g S
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q),
  (CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation f).I = CategoryTheory.Abelian.coimage f
-- Mathlib.Combinatorics.SimpleGraph.Matching
/-- The subgraph `M` of `G` is a matching if every vertex of `M` is incident to exactly one edge in `M`.
We say that the vertices in `M.support` are *matched* or *saturated*.
 -/
SimpleGraph.Subgraph.IsMatching : {V : Type u_1} → {G : SimpleGraph V} → G.Subgraph → Prop
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.one_le_prod' : ∀ {ι : Type u_1} {N : Type u_5} [inst : CommMonoid N] [inst_1 : Preorder N] {f : ι → N} {s : Finset ι} [MulLeftMono N],
  (∀ i ∈ s, 1 ≤ f i) → 1 ≤ ∏ i ∈ s, f i
-- Mathlib.Order.Partition.Basic
Partition.Rel.trans : ∀ {α : Type u_1} {x y z : α} {u : Set α} {P : Partition u}, P.Rel x y → P.Rel y z → P.Rel x z
-- Std.Time.DateTime.WallTime
/-- Adds a `Second.Offset` to the given `WallTime`.
 -/
Std.Time.WallTime.addSeconds : Std.Time.WallTime → Std.Time.Second.Offset → Std.Time.WallTime
-- Init.Grind.Ordered.Ring
Lean.Grind.OrderedRing.mul_le_mul_of_nonneg_left : ∀ {R : Type u} [inst : Lean.Grind.Ring R] [inst_1 : LE R] [inst_2 : LT R] [inst_3 : Std.IsPartialOrder R]
  [Lean.Grind.OrderedRing R] [Std.LawfulOrderLT R] {a b c : R}, a ≤ b → 0 ≤ c → c * a ≤ c * b
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.le_truncatedSup : ∀ {α : Type u_1} [inst : SemilatticeSup α] {s : Finset α} {a : α} [inst_1 : DecidableLE α] [inst_2 : OrderTop α],
  a ≤ s.truncatedSup a
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffOn_of_analyticOn_of_fderivWithin : ∀ {𝕜 : 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} {n : WithTop ℕ∞}, AnalyticOn 𝕜 f s → ContDiffOn 𝕜 ⊤ (fun y => fderivWithin 𝕜 f s y) s → ContDiffOn 𝕜 n f s
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.mk.injEq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι₂ : Type u_5} {M₂ : Type u_6} {N₂ : Type u_7}
  [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂] [inst_7 : AddCommGroup N₂] [inst_8 : Module R N₂]
  {P : RootPairing ι R M N} {Q : RootPairing ι₂ R M₂ N₂} (weightMap : M →ₗ[R] M₂) (coweightMap : N₂ →ₗ[R] N)
  (indexEquiv : ι ≃ ι₂)
  (weight_coweight_transpose : weightMap.dualMap ∘ₗ ↑Q.flip.toPerfPair = ↑P.flip.toPerfPair ∘ₗ coweightMap)
  (root_weightMap : ⇑weightMap ∘ ⇑P.root = ⇑Q.root ∘ ⇑indexEquiv)
  (coroot_coweightMap : ⇑coweightMap ∘ ⇑Q.coroot = ⇑P.coroot ∘ ⇑indexEquiv.symm) (weightMap_1 : M →ₗ[R] M₂)
  (coweightMap_1 : N₂ →ₗ[R] N) (indexEquiv_1 : ι ≃ ι₂)
  (weight_coweight_transpose_1 : weightMap_1.dualMap ∘ₗ ↑Q.flip.toPerfPair = ↑P.flip.toPerfPair ∘ₗ coweightMap_1)
  (root_weightMap_1 : ⇑weightMap_1 ∘ ⇑P.root = ⇑Q.root ∘ ⇑indexEquiv_1)
  (coroot_coweightMap_1 : ⇑coweightMap_1 ∘ ⇑Q.coroot = ⇑P.coroot ∘ ⇑indexEquiv_1.symm),
  ({ weightMap := weightMap, coweightMap := coweightMap, indexEquiv := indexEquiv,
        weight_coweight_transpose := weight_coweight_transpose, root_weightMap := root_weightMap,
        coroot_coweightMap := coroot_coweightMap } =
      { weightMap := weightMap_1, coweightMap := coweightMap_1, indexEquiv := indexEquiv_1,
        weight_coweight_transpose := weight_coweight_transpose_1, root_weightMap := root_weightMap_1,
        coroot_coweightMap := coroot_coweightMap_1 }) =
    (weightMap = weightMap_1 ∧ coweightMap = coweightMap_1 ∧ indexEquiv = indexEquiv_1)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.coboundaries.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n : ℤ),
  CochainComplex.HomComplex.coboundaries K L n =
    { carrier := {α | ∃ m, ∃ (_ : m + 1 = n), ∃ β, CochainComplex.HomComplex.δ m n β = ↑α}, add_mem' := ⋯,
      zero_mem' := ⋯, neg_mem' := ⋯ }
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.reduceCyclically.reduce_flatten_replicate_succ : ∀ {α : Type u} {L : List (α × Bool)} [inst : DecidableEq α],
  FreeAddGroup.IsReduced L →
    ∀ (n : ℕ),
      FreeAddGroup.reduce (List.replicate (n + 1) L).flatten =
        FreeAddGroup.reduceCyclically.conjugator L ++
            (List.replicate (n + 1) (FreeAddGroup.reduceCyclically L)).flatten ++
          FreeAddGroup.negRev (FreeAddGroup.reduceCyclically.conjugator L)
-- Mathlib.Algebra.Algebra.Operations
SubMulAction.algebraMap_mem : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R),
  (algebraMap R A) r ∈ 1
-- Mathlib.Algebra.Order.CauSeq.Basic
/-- A sequence is Cauchy if the distance between its entries tends to zero.  -/
IsCauSeq : {α : Type u_3} →
  [inst : Field α] →
    [inst_1 : LinearOrder α] → [IsStrictOrderedRing α] → {β : Type u_4} → [Ring β] → (β → α) → (ℕ → β) → Prop
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
contDiffPointwiseHolderAt_iff : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (k : ℕ) (α : ↑unitInterval) (f : E → F) (a : E),
  ContDiffPointwiseHolderAt k α f a ↔
    ContDiffAt ℝ (↑k) f a ∧ (fun x => iteratedFDeriv ℝ k f x - iteratedFDeriv ℝ k f a) =O[nhds a] fun x => ‖x - a‖ ^ ↑α
-- Mathlib.Data.Set.Insert
Set.singleton_union : ∀ {α : Type u_1} {s : Set α} {a : α}, {a} ∪ s = insert a s
-- Mathlib.Data.Quot
Trunc.nonempty : ∀ {α : Sort u_1} (q : Trunc α), Nonempty α
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
fderivWithin_csinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E},
  DifferentiableWithinAt ℂ f s x →
    UniqueDiffWithinAt ℂ s x →
      fderivWithin ℂ (fun x => Complex.sinh (f x)) s x = Complex.cosh (f x) • fderivWithin ℂ f s x
-- Mathlib.Data.Finsupp.Defs
/-- Given `Finite α`, `equivFunOnFinite` is the `Equiv` between `α →₀ β` and `α → β`.
(All functions on a finite type are finitely supported.)  -/
Finsupp.equivFunOnFinite : {α : Type u_1} → {M : Type u_4} → [inst : Zero M] → [Finite α] → (α →₀ M) ≃ (α → M)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.map_mk : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} (φ : G →g G') (v : V),
  SimpleGraph.ConnectedComponent.map φ (G.connectedComponentMk v) = G'.connectedComponentMk (φ v)
-- Mathlib.Order.Bounded
Set.bounded_le_inter_lt : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
  Set.Bounded (fun x1 x2 => x1 ≤ x2) (s ∩ {b | a < b}) ↔ Set.Bounded (fun x1 x2 => x1 ≤ x2) s
-- Mathlib.Tactic.Linter.FlexibleLinter
/-- MetavarContext before the tactic  -/
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.TacticData.mctxBefore : Mathlib.Linter.Flexible.TacticData✝ → Lean.MetavarContext
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInf_iInf : ∀ {ι : Type u_1} [Finite ι] (u : ι → ℕ → EReal),
  LinearGrowth.linearGrowthInf (⨅ i, u i) = ⨅ i, LinearGrowth.linearGrowthInf (u i)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal.0.AugmentedSimplexCategory.tensorObj.match_1.eq_2 : ∀ (motive : AugmentedSimplexCategory → AugmentedSimplexCategory → Sort u_1) (x : AugmentedSimplexCategory)
  (h_1 : (m n : SimplexCategory) → motive (CategoryTheory.WithInitial.of m) (CategoryTheory.WithInitial.of n))
  (h_2 : (x : AugmentedSimplexCategory) → motive CategoryTheory.WithInitial.star x)
  (h_3 : (x : AugmentedSimplexCategory) → motive x CategoryTheory.WithInitial.star),
  (match CategoryTheory.WithInitial.star, x with
    | CategoryTheory.WithInitial.of m, CategoryTheory.WithInitial.of n => h_1 m n
    | CategoryTheory.WithInitial.star, x => h_2 x
    | x, CategoryTheory.WithInitial.star => h_3 x) =
    h_2 x
-- Init.Data.Order.Ord
Array.instOrientedOrd : ∀ {α : Type u_1} [inst : Ord α] [Std.OrientedOrd α], Std.OrientedOrd (Array α)
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_le_length_insertListConst : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)},
  l.length ≤ (Std.Internal.List.insertListConst l toInsert).length
-- Mathlib.Topology.Path
/-- The end point of a `Path`.  -/
Path.target' : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} (self : Path x y), self.toFun 1 = y
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrixRight'_id : ∀ {R : Type u_1} [inst : Semiring R] {m : Type u_3} [inst_1 : Fintype m] [inst_2 : DecidableEq m],
  LinearMap.toMatrixRight' LinearMap.id = 1
-- Mathlib.Algebra.Order.Ring.Basic
Even.pow_nonneg : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsOrderedRing R] [ExistsAddOfLE R] {n : ℕ},
  Even n → ∀ (a : R), 0 ≤ a ^ n
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableAt_of_isInvertible_fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E}, (fderiv 𝕜 f x).IsInvertible → DifferentiableAt 𝕜 f x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.equiv_iff_toList_perm_toList : ∀ {α : Type u} {β : α → Type v} (m₁ m₂ : Std.DHashMap.Raw α β), m₁.Equiv m₂ ↔ m₁.toList.Perm m₂.toList
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.MonicDegreeEq.degree : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] [Nontrivial R] (p : Polynomial.MonicDegreeEq R n), (↑p).degree = ↑n
-- Init.Data.Array.Count
Array.count_eq_zero_of_not_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {xs : Array α}, a ∉ xs → Array.count a xs = 0
-- Mathlib.Data.Nat.Factorization.Root
Nat.ceilRoot_eq_zero : ∀ {a n : ℕ}, n.ceilRoot a = 0 ↔ n = 0 ∨ a = 0
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.subtype_injective : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} (H : S) [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G],
  Function.Injective ⇑↑H
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.Ioo_sub_one_left_eq_Ioc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Sub α] [PredSubOrder α] [NoMinOrder α] (a b : α),
  Set.Ioo (a - 1) b = Set.Ico a b
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.nontrivial_lowerCentralSeriesLast : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [LieModule R L M] [Nontrivial M]
  [LieModule.IsNilpotent L M], Nontrivial ↥(LieModule.lowerCentralSeriesLast R L M)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.map_coeIdeal : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {P' : Type u_3} [inst_3 : CommRing P'] [inst_4 : Algebra R P'] (g : P →ₐ[R] P') (I : Ideal R),
  FractionalIdeal.map g ↑I = ↑I
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.get!ₘ_eq_getValueCast! : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} [inst_3 : Inhabited (β a)],
      m.get!ₘ a = Std.Internal.List.getValueCast! a (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {km : α},
  t.max? = some km → t.get? km = some km
-- Init.Data.Array.Find
_private.Init.Data.Array.Find.0.Array.of_findIdx?_eq_some.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.ε_η : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.Monoidal],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F)
      (CategoryTheory.Functor.OplaxMonoidal.η F) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.toSentence.eq_9 : FirstOrder.Field.FieldAxiom.existsPairNE.toSentence =
  (((FirstOrder.Language.var ∘ Sum.inr) 0).bdEqual ((FirstOrder.Language.var ∘ Sum.inr) 1)).not.ex.ex
-- Mathlib.Topology.Separation.Hausdorff
SeparationQuotient.t2Space_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X], T2Space (SeparationQuotient X) ↔ R1Space X
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_ofBool : ∀ (b : Bool) (i : ℕ), (BitVec.ofBool b).getLsbD i = (decide (i = 0) && b)
-- Mathlib.Algebra.Algebra.Operations
Submodule.span_singleton_mul : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] {x : A}
  {p : Submodule R A}, (R ∙ x) * p = x • p
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.toList_eq_match_rco : ∀ {α : Type u} {r : Std.Roo α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α],
  r.toList =
    match Std.PRange.succ? r.lower with
    | none => []
    | some next => (next...r.upper).toList
-- Init.Data.BitVec.Lemmas
/-- If a bitvector interpreted as a natural number is strictly smaller than `2 ^ (k + 1)` and greater than or
equal to 2 ^ k, then the bit at position `k` must be `true`  -/
BitVec.getElem_eq_true_of_lt_of_le : ∀ {w k : ℕ} {x : BitVec w} (hk' : k < w), x.toNat < 2 ^ (k + 1) → 2 ^ k ≤ x.toNat → x[k] = true
-- Mathlib.Data.Complex.Basic
Complex.instCoeReal : Coe ℝ ℂ
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
Std.Iterators.Types.FilterMap.mk.inj : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {lift : ⦃α : Type w⦄ → m α → n α}
  {f : β → Std.Iterators.PostconditionT n (Option γ)} {inner inner_1 : Std.IterM m β},
  { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.instSubringClass : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A],
  SubringClass (Subalgebra R A) A
-- Mathlib.LinearAlgebra.DFinsupp
iSupIndep.linearEquiv_symm_apply : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : DecidableEq ι] [inst_1 : Ring R] [inst_2 : AddCommGroup N]
  [inst_3 : Module R N] {p : ι → Submodule R N} (ind : iSupIndep p) (iSup_top : ⨆ i, p i = ⊤) {i : ι} {x : N}
  (h : x ∈ p i), (ind.linearEquiv iSup_top).symm x = fun₀ | i => ⟨x, h⟩
-- Mathlib.Topology.EMetricSpace.Diam
Metric.ediam_image_le_iff : ∀ {α : Type u_1} {X : Type u_2} [inst : PseudoEMetricSpace X] {d : ENNReal} {f : α → X} {s : Set α},
  Metric.ediam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d
-- Mathlib.Topology.Order.IsLUB
Dense.exists_seq_strictAnti_tendsto_of_lt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [FirstCountableTopology α] {s : Set α},
  Dense s →
    ∀ {x y : α}, x < y → ∃ u, StrictAnti u ∧ (∀ (n : ℕ), u n ∈ Set.Ioo x y ∩ s) ∧ Filter.Tendsto u Filter.atTop (nhds x)
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.instAddCommGroup : {Γ : Type u_1} →
  {R : Type u_3} →
    {α : Type u_5} →
      [inst : PartialOrder Γ] → [inst_1 : AddCommGroup R] → AddCommGroup (HahnSeries.SummableFamily Γ R α)
-- Mathlib.Analysis.Complex.Exponential
Real.one_le_exp : ∀ {x : ℝ}, 0 ≤ x → 1 ≤ Real.exp x
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
withSeminorms_iInf : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {κ : ι → Type u_11} {p : (i : ι) → SeminormFamily 𝕜 E (κ i)} {t : ι → TopologicalSpace E},
  (∀ (i : ι), WithSeminorms (p i)) → WithSeminorms (SeminormFamily.sigma p)
-- Mathlib.Analysis.LocallyConvex.AbsConvexOpen
/-- The topology of a locally convex space is induced by the gauge seminorm family.  -/
with_gaugeSeminormFamily : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : Module ℝ E] [inst_5 : IsScalarTower ℝ 𝕜 E] [inst_6 : ContinuousSMul ℝ E]
  [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [LocallyConvexSpace 𝕜 E], WithSeminorms (gaugeSeminormFamily 𝕜 E)
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
ergodic_mul_left_of_denseRange_zpow : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [inst_3 : MeasurableSpace G]
  [SecondCountableTopology G] [BorelSpace G] {g : G},
  (DenseRange fun x => g ^ x) →
    ∀ (μ : MeasureTheory.Measure G) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [μ.IsMulLeftInvariant],
      Ergodic (fun x => g * x) μ
-- Mathlib.Computability.Language
/-- Maps the alphabet of a language.  -/
Language.map : {α : Type u_1} → {β : Type u_2} → (α → β) → Language α →+* Language β
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_mul : ∀ {R : Type u} [inst : Semiring R] {n : ℕ} (p q : Polynomial R),
  (⇑Polynomial.derivative)^[n] (p * q) =
    ∑ k ∈ Finset.range n.succ, n.choose k • ((⇑Polynomial.derivative)^[n - k] p * (⇑Polynomial.derivative)^[k] q)
-- Mathlib.Data.List.Rotate
List.cyclicPermutations_of_ne_nil : ∀ {α : Type u} (l : List α),
  l ≠ [] → l.cyclicPermutations = (List.zipWith (fun x1 x2 => x1 ++ x2) l.tails l.inits).dropLast
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.isRelPrime : ∀ {R : Type u} [inst : CommSemiring R] {a b : R}, IsCoprime a b → IsRelPrime a b
-- Init.Data.List.Lemmas
List.mem_reverse : ∀ {α : Type u_1} {x : α} {as : List α}, x ∈ as.reverse ↔ x ∈ as