mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Real.Spectrum
SpectrumRestricts.nnreal_lt_iff : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] {a : A},
  SpectrumRestricts a ⇑ContinuousMap.realToNNReal →
    ∀ {r : NNReal}, (∀ x ∈ spectrum NNReal a, r < x) ↔ ∀ x ∈ spectrum ℝ a, ↑r < x
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- Universal property of the free product of algebras, property:
for every `R`-algebra `B`, every family of maps `maps : (i : I) → (A i →ₐ[R] B)` lifts
to a unique arrow `π` from `FreeProduct R A` such that  `π ∘ ι i = maps i`.  -/
LinearAlgebra.FreeProduct.lift_comp_ι : ∀ {I : Type u} [inst : DecidableEq I] {i : I} (R : Type v) [inst_1 : CommSemiring R] (A : I → Type w)
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)] {B : Type w'} [inst_4 : Semiring B]
  [inst_5 : Algebra R B] (maps : {i : I} → A i →ₐ[R] B),
  ((LinearAlgebra.FreeProduct.lift R A) fun {i} => maps).comp (LinearAlgebra.FreeProduct.ι R A i) = maps
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_trans_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.natTransTruncLTOfLE a b hab).app X) ((t.natTransTruncLTOfLE b c hbc).app X) =
    (t.natTransTruncLTOfLE a c ⋯).app X
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.isUnitSubmonoid_eq_of_mulOpposite : ∀ (R : Type u_1) [inst : Ring R] [IsArtinianRing Rᵐᵒᵖ], IsUnit.submonoid R = nonZeroDivisors R
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.ext : ∀ {x y : SimplexCategory}, x.len = y.len → x = y
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_add_right : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y Z : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp X 2 μ →
    MeasureTheory.MemLp Y 2 μ →
      MeasureTheory.MemLp Z 2 μ →
        ProbabilityTheory.covariance X (Y + Z) μ =
          ProbabilityTheory.covariance X Y μ + ProbabilityTheory.covariance X Z μ
-- Aesop.Rule.Name
_private.Aesop.Rule.Name.0.Aesop.RuleName.Json.name : Aesop.RuleName.Json✝ → Lean.Name
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.tendsto_iff_forall_toWeakDualBCNN_tendsto : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {γ : Type u_3} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω},
  Filter.Tendsto μs F (nhds μ) ↔
    ∀ (f : BoundedContinuousFunction Ω NNReal),
      Filter.Tendsto (fun i => (μs i).toWeakDualBCNN f) F (nhds (μ.toWeakDualBCNN f))
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.lid_symm_apply : ∀ {R : Type u_1} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring B] [inst_2 : Bialgebra R B] (a : B),
  (Bialgebra.TensorProduct.lid R B).symm a = 1 ⊗ₜ[R] a
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum_single_index : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid γ] {i : ι} {b : β i}
  {h : (i : ι) → β i → γ}, h i 0 = 0 → (fun₀ | i => b).sum h = h i b
-- Init.Core
/-- A total relation satisfies `r a b` or `r b a`.  -/
Std.Total.total : ∀ {α : Sort u} {r : α → α → Prop} [self : Std.Total r] (a b : α), r a b ∨ r b a
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] {f : X → Y},
  IsLocallyConstant f → ∀ (g : Y → Z), IsLocallyConstant (g ∘ f)
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.findMin.eq_1 : ∀ {α : Type u_1} (le : α → α → Bool) (k : Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α)
  (x : Batteries.BinomialHeap.Imp.FindMin α),
  Batteries.BinomialHeap.Imp.Heap.findMin le k Batteries.BinomialHeap.Imp.Heap.nil x = x
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_xor : ∀ {v i : ℕ} {x y : BitVec v}, (x ^^^ y).getLsbD i = (x.getLsbD i ^^ y.getLsbD i)
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
aeSeq.aeSeq_eq_mk_ae : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : ι → α → β}
  {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} [Countable ι] (hf : ∀ (i : ι), AEMeasurable (f i) μ),
  (∀ᵐ (x : α) ∂μ, p x fun n => f n x) → ∀ᵐ (a : α) ∂μ, ∀ (i : ι), aeSeq hf p i a = AEMeasurable.mk (f i) ⋯ a
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuous_ofMul : ∀ {α : Type ua} [inst : UniformSpace α], UniformContinuous ⇑Additive.ofMul
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Given a limit cone for the pair `f g : X ⟶ Y`, for any `Z`, morphisms from `Z` to its point are in
bijection with morphisms `h : Z ⟶ X` such that `h ≫ f = h ≫ g`.
Further, this bijection is natural in `Z`: see `Fork.IsLimit.homIso_natural`.
This is a special case of `IsLimit.homIso'`, often useful to construct adjunctions.
 -/
CategoryTheory.Limits.Fork.IsLimit.homIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f g : X ⟶ Y} →
        {t : CategoryTheory.Limits.Fork f g} →
          CategoryTheory.Limits.IsLimit t →
            (Z : C) →
              (Z ⟶ t.pt) ≃ { h // CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g }
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.snd_map_prodMk₀ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {X : α → β} {Y : α → γ} {μ : MeasureTheory.Measure α},
  AEMeasurable X μ → (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ).snd = MeasureTheory.Measure.map Y μ
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.forget_preservesLimitsOfRight : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z),
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan g f) (AlgebraicGeometry.PresheafedSpace.forget C)
-- Init.Data.Iterators.Combinators.FlatMap
/-- Let `it` be an iterator and `f` a function mapping `it`'s outputs to iterators.
Then `it.flatMap f` is an iterator that goes over `it` and for each output, it applies `f` and
iterates over the resulting iterator. `it.flatMap f` emits all values obtained from the inner
iterators -- first, all of the first inner iterator, then all of the second one, and so on.

**Marble diagram:**

```text
it                 ---a      --b      c    --d -⊥
f a                    a1-a2⊥
f b                             b1-b2⊥
f c                                    c1-c2⊥
f d                                           ⊥
it.flatMap         ----a1-a2----b1-b2--c1-c2----⊥
```

**Termination properties:**

* `Finite` instance: only if `it` and the inner iterators are finite
* `Productive` instance: only if `it` is finite and the inner iterators are productive

For certain functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided out of the box. For example, if the outer
iterator is productive and the inner
iterators are productive *and provably never empty*, then the resulting iterator is also productive.

**Performance:**

This combinator incurs an additional O(1) cost with each output of `it` or an internal iterator.

For each value emitted by the outer iterator `it`, this combinator calls `f`.
 -/
Std.Iter.flatMap : {α β α₂ γ : Type w} → [Std.Iterator α Id β] → [Std.Iterator α₂ Id γ] → (f : β → Std.Iter γ) → Std.Iter β → Std.Iter γ
-- Init.Data.SInt.Bitwise
Int32.ofBitVec_xor : ∀ (a b : BitVec 32), Int32.ofBitVec (a ^^^ b) = Int32.ofBitVec a ^^^ Int32.ofBitVec b
-- Mathlib.FieldTheory.Isaacs
Field.nonempty_algHom_of_exists_root : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K] [alg : Algebra.IsAlgebraic F E],
  (∀ (x : E), ∃ y, (Polynomial.aeval y) (minpoly F x) = 0) → Nonempty (E →ₐ[F] K)
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- The 2-morphism filling the triangle diagram.  -/
CategoryTheory.Bicategory.LeftLift.unit : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} → (t : CategoryTheory.Bicategory.LeftLift f g) → g ⟶ CategoryTheory.CategoryStruct.comp t.lift f
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.ext : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] {S T : StarSubalgebra R A},
  (∀ (x : A), x ∈ S ↔ x ∈ T) → S = T
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N →ₗ[R] P), LinearMap.rTensor M f = TensorProduct.map f LinearMap.id
-- Mathlib.RingTheory.Flat.EquationalCriterion
/-- **Equational criterion for flatness**:
a module $M$ is flat if and only if every relation $\sum_i f_i x_i = 0$ in $M$ is trivial.  -/
Module.Flat.iff_forall_isTrivialRelation : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.Flat R M ↔ ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → Module.IsTrivialRelation f x
-- Mathlib.Analysis.Asymptotics.ExpGrowth
Monotone.expGrowthInf_nonneg : ∀ {u : ℕ → ENNReal}, Monotone u → u ≠ 0 → 0 ≤ ExpGrowth.expGrowthInf u
-- Mathlib.Data.Set.Lattice.Image
Set.iInter.eq_1 : ∀ {α : Type u} {ι : Sort v} (s : ι → Set α), Set.iInter s = iInf s
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
/-- the map to the successor  -/
CategoryTheory.SmallObject.SuccStruct.toSucc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (self : CategoryTheory.SmallObject.SuccStruct C) → (X : C) → X ⟶ self.succ X
-- Mathlib.Topology.Homeomorph.Lemmas
IsHomeomorph.isOpenEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f → Topology.IsOpenEmbedding f
-- Mathlib.Analysis.Meromorphic.Order
/-- **Alias** of `MeromorphicOn.codiscrete_setOfPred_meromorphicOrderAt_eq_zero_or_top`.

---

The set where a meromorphic function has zero or infinite
order is codiscrete within its domain of meromorphicity.  -/
MeromorphicOn.codiscrete_setOf_meromorphicOrderAt_eq_zero_or_top : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜},
  MeromorphicOn f U → {u | meromorphicOrderAt f ↑u = 0 ∨ meromorphicOrderAt f ↑u = ⊤} ∈ Filter.codiscrete ↑U
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprod_inl_fst_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] (i : ι),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) (CategoryTheory.Limits.biprod.fst.f i) =
    CategoryTheory.CategoryStruct.id (K.X i)
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.monic_restriction : ∀ {R : Type u} [inst : Ring R] {p : Polynomial R}, p.restriction.Monic ↔ p.Monic
-- Init.Data.Iterators.Lemmas.Combinators.Attach
Std.Iter.toArray_attachWith : ∀ {α β : Type u_1} {P : β → Prop} [inst : Std.Iterator α Id β] {it : Std.Iter β}
  {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [inst_1 : Std.Iterators.Finite α Id],
  (it.attachWith P hP).toArray = it.toArray.attachWith P ⋯
-- Mathlib.Topology.UniformSpace.UniformConvergence
UniformCauchySeqOnFilter.mono_left : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {p : Filter ι} {p' : Filter α}
  {p'' : Filter ι}, UniformCauchySeqOnFilter F p p' → p'' ≤ p → UniformCauchySeqOnFilter F p'' p'
-- Mathlib.Data.Finset.Image
Finset.disjoint_map : ∀ {α : Type u_1} {β : Type u_2} {s t : Finset α} (f : α ↪ β), Disjoint (Finset.map f s) (Finset.map f t) ↔ Disjoint s t
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {fallback : α}, t.getKey! (t.maxKeyD fallback) = t.maxKeyD fallback
-- Std.Data.DHashMap.Lemmas
/-- Variant of `get!_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.DHashMap.Const.get!_map' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.DHashMap α fun x => β}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] [inst_2 : Inhabited γ] {f : α → β → γ} {k : α},
  Std.DHashMap.Const.get! (Std.DHashMap.map f m) k =
    (Option.pmap (fun v h => f (m.getKey k h) v) (Std.DHashMap.Const.get? m k) ⋯).get!
-- Init.Data.Vector.Basic
/-- Get an element of a vector using a `USize` index and a proof that the index is within bounds.  -/
Vector.uget : {α : Type u_1} → {n : ℕ} → Vector α n → (i : USize) → i.toNat < n → α
-- Init.Data.BitVec.Basic
/-- Theorem for normalizing the bitvector literal representation.  -/
BitVec.ofNat_eq_ofNat : ∀ {n i : ℕ}, OfNat.ofNat i = BitVec.ofNat n i
-- Mathlib.Order.PartialSups
exists_partialSups_eq : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : LocallyFiniteOrderBot ι] [inst_2 : LinearOrder α]
  (f : ι → α) (i : ι), ∃ j ≤ i, (partialSups f) i = f j
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.d_map_fourδ₄Toδ₃_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₃₄ : i₂ ⟶ i₄)
  (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.d_map_fourδ₄Toδ₃._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.d_map_fourδ₄Toδ₃._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.d_map_fourδ₄Toδ₃._auto_5) {Z : C}
  (h : X.E f₁ f₂ f₃₄ n₁ n₂ n₃ hn₂ hn₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃)
      (CategoryTheory.CategoryStruct.comp
        (X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (CategoryTheory.ComposableArrows.fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ hn₂ hn₃)
        h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instAddMonoidWithOne : {k : Type u_1} → {G : Type u_2} → [One G] → [inst : AddMonoidWithOne k] → AddMonoidWithOne (SkewMonoidAlgebra k G)
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.isoApp_associator : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {X Y Z : (i : I) → C i} {i : I},
  CategoryTheory.Pi.isoApp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z) i =
    CategoryTheory.MonoidalCategoryStruct.associator (X i) (Y i) (Z i)
-- Init.Data.SInt.Lemmas
Int64.toISize_neg : ∀ (x : Int64), (-x).toISize = -x.toISize
-- Mathlib.Data.Finset.Sups
Finset.diffs_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : GeneralizedBooleanAlgebra α] {s : Finset α} {b : α},
  s.diffs {b} = Finset.image (fun x => x \ b) s
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.symmEquiv.eq_1 : ∀ (P : Type u_9) (Q : Type u_10) [inst : Mul P] [inst_1 : Mul Q],
  MulEquiv.symmEquiv P Q = { toFun := MulEquiv.symm, invFun := MulEquiv.symm, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.vadd_set_iInter₂_subset : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : VAdd α β] (a : α) (t : (i : ι) → κ i → Set β),
  a +ᵥ ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, a +ᵥ t i j
-- Mathlib.Algebra.Lie.OfAssociative
LieSubmodule.coe_toEnd_pow : ∀ (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] [inst_6 : LieModule R L M]
  (N : LieSubmodule R L M) (x : L) (y : ↥N) (n : ℕ),
  ↑(((LieModule.toEnd R L ↥N) x ^ n) y) = ((LieModule.toEnd R L M) x ^ n) ↑y
-- Mathlib.Order.Atoms
IsSimpleOrder.eq_bot_of_lt : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : BoundedOrder α] [IsSimpleOrder α] {a b : α}, a < b → a = ⊥
-- Aesop.Builder.Basic
Aesop.CoreRuleBuilderOutput.tac : Aesop.CoreRuleBuilderOutput → Aesop.RuleTacDescr
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
ContDiffWithinAt.rpow_const_of_ne : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E} {p : ℝ}
  {n : WithTop ℕ∞}, ContDiffWithinAt ℝ n f s x → f x ≠ 0 → ContDiffWithinAt ℝ n (fun x => f x ^ p) s x
-- Mathlib.Algebra.Module.ZLattice.Covolume
ZLattice.covolume_ne_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [inst_5 : DiscreteTopology ↥L] [IsZLattice ℝ L]
  (μ : autoParam (MeasureTheory.Measure E) _auto_22✝) [μ.IsAddHaarMeasure], ZLattice.covolume L μ ≠ 0
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.Hom.comm : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  {X X' : CategoryTheory.Abelian.SpectralObject C ι} (self : X.Hom X') (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i j k : ι}
  (f : i ⟶ j) (g : j ⟶ k),
  CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) ((self.hom n₁).app (CategoryTheory.ComposableArrows.mk₁ f)) =
    CategoryTheory.CategoryStruct.comp ((self.hom n₀).app (CategoryTheory.ComposableArrows.mk₁ g)) (X'.δ f g n₀ n₁ hn₁)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_erase_le_maxKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty = false →
    (compare (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.maxKey! t.maxKey!).isLE = true
-- Mathlib.MeasureTheory.Measure.Restrict
MeasurableEquiv.comap_apply : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} (e : α ≃ᵐ β)
  (μ : MeasureTheory.Measure β) (s : Set α), (MeasureTheory.Measure.comap (⇑e) μ) s = μ (⇑e.symm ⁻¹' s)
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Broadcast.Receiver.mk.inj : ∀ {α : Type} {inner inner_1 : Std.Bounded.Receiver✝ α}, { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.median_reindex : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {m n : ℕ} [inst_4 : NeZero m] [inst_5 : NeZero n] (s : Affine.Simplex k P n)
  (e : Fin (n + 1) ≃ Fin (m + 1)), (s.reindex e).median = s.median ∘ ⇑e.symm
-- Init.Data.UInt.Bitwise
UInt8.toUInt32_shiftLeft : ∀ (a b : UInt8), (a <<< b).toUInt32 = a.toUInt32 <<< (b % 8).toUInt32 % 256
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.symm_comp_self_toEmbedding : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Equiv M N), f.symm.toEmbedding.comp f.toEmbedding = FirstOrder.Language.Embedding.refl L M
-- Mathlib.Algebra.Group.Opposite
MulOpposite.isDedekindFiniteMonoid_iff : ∀ {α : Type u_1} [inst : MulOne α], IsDedekindFiniteMonoid αᵐᵒᵖ ↔ IsDedekindFiniteMonoid α
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isCycle_def : ∀ {V : Type u} {G : SimpleGraph V} {u : V} (p : G.Walk u u),
  p.IsCycle ↔ p.IsTrail ∧ p ≠ SimpleGraph.Walk.nil ∧ p.support.tail.Nodup
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : Inhabited α] {a : α} {c : ℕ},
  (Std.DHashMap.emptyWithCapacity c).getKey! a = default
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.forIn'_eq_match_step.match_1.splitter : {γ : Type u_1} →
  (motive : ForInStep γ → Sort u_2) →
    (__do_lift : ForInStep γ) →
      ((c : γ) → motive (ForInStep.yield c)) → ((c : γ) → motive (ForInStep.done c)) → motive __do_lift
-- Mathlib.Data.Finset.Lattice.Lemmas
/-- To prove a relation on pairs of `Finset X`, it suffices to show that it is
* symmetric,
* it holds when one of the `Finset`s is empty,
* it holds for pairs of singletons,
* if it holds for `[a, c]` and for `[b, c]`, then it holds for `[a ∪ b, c]`.
 -/
Finset.induction_on_union : ∀ {α : Type u_1} [inst : DecidableEq α] (P : Finset α → Finset α → Prop),
  (∀ {a b : Finset α}, P a b → P b a) →
    (∀ {a : Finset α}, P a ∅) →
      (∀ {a b : α}, P {a} {b}) → (∀ {a b c : Finset α}, P a c → P b c → P (a ∪ b) c) → ∀ (a b : Finset α), P a b
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsUpperSet.isClosed_iff_isLower : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpperSet α] {s : Set α},
  IsClosed s ↔ IsLowerSet s
-- Mathlib.Algebra.Symmetrized
SymAlg.instZero.eq_1 : ∀ {α : Type u_1} [inst : Zero α], SymAlg.instZero = { zero := SymAlg.sym 0 }
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_insertMany_emptyWithCapacity_list : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k : α},
  (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).contains k = (List.map Sigma.fst l).contains k
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.all_filterMap : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [inst_3 : Std.IteratorLoop α m m] [LawfulMonad m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β}
  {f : β → Option β'} {p : β' → Bool},
  Std.IterM.all p (Std.IterM.filterMap f it) =
    Std.IterM.all
      (fun x =>
        match f x with
        | some fx => p fx
        | none => true)
      it
-- Mathlib.RingTheory.Localization.Away.Basic
Localization.awayMap_bijective_of_dvd : ∀ {S : Type u_2} [inst : CommSemiring S] {R : Type u_4} [inst_1 : CommRing R] (f : R →+* S) {a b : R},
  a ∣ b → Function.Bijective ⇑(Localization.awayMap f a) → Function.Bijective ⇑(Localization.awayMap f b)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.Proj.add_apply : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {V : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ}
  (s t : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj V)) (x : ↥(Opposite.unop V)),
  ↑(s + t) x = ↑s x + ↑t x
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleExpr.toRuleConfigs : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadError m] → Aesop.Frontend.RuleExpr → Aesop.Frontend.RuleConfig → m (Array Aesop.Frontend.RuleConfig)
-- Mathlib.Order.Filter.Bases.Basic
Filter.inf_neBot_iff_frequently_right : ∀ {α : Type u_1} {f g : Filter α}, (f ⊓ g).NeBot ↔ ∀ {p : α → Prop}, (∀ᶠ (x : α) in g, p x) → ∃ᶠ (x : α) in f, p x