mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.nsmul_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] (a : α) (n : ℕ), n • {a} = {n • a}
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_insertManyIfNewUnit_list_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List α}, (t.insertManyIfNewUnit l).size ≤ t.size + l.length
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticFinishedSnapshot.mk : Lean.Language.Snapshot →
  Option Lean.Elab.Tactic.SavedState →
    Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Lean.Elab.Tactic.TacticFinishedSnapshot
-- Lean.Data.JsonRpc
_private.Lean.Data.JsonRpc.0.Lean.JsonRpc.messageMetaDataParser.parseStr : Std.Internal.Parsec.String.Parser String
-- Mathlib.Data.Nat.Factorization.Root
Nat.dvd_ceilRoot_pow : ∀ {a n : ℕ}, n ≠ 0 → a ∣ n.ceilRoot a ^ n
-- Init.Data.String.Lemmas.Order
String.Pos.lt_ofSliceFrom_iff : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos},
  q < String.Pos.ofSliceFrom p ↔ ∀ (h : p₀ ≤ q), p₀.sliceFrom q h < p
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftExtension.whiskerHom_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  {s t : CategoryTheory.Bicategory.LeftExtension f g} (i : s ⟶ t) {x : B} (h : c ⟶ x),
  (CategoryTheory.Bicategory.LeftExtension.whiskerHom i h).right =
    CategoryTheory.Bicategory.whiskerRight (CategoryTheory.StructuredArrow.Hom.right i) h
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.restrictScalars : ∀ {R : Type u_1} [inst : Ring R] (S : Type u_2) [inst_1 : Ring S] {M : Type u_4} [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : Module S M] {U : Submodule R M} {x y : M} [inst_5 : SMul S R]
  [inst_6 : IsScalarTower S R M], x ≡ y [SMOD Submodule.restrictScalars S U] ↔ x ≡ y [SMOD U]
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.take_zero : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.take 0 = SimpleGraph.Walk.nil.copy ⋯ ⋯
-- Mathlib.Data.Finset.Sum
Finset.toRight_cons_inl : ∀ {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)} {a : α} (ha : Sum.inl a ∉ u),
  (Finset.cons (Sum.inl a) u ha).toRight = u.toRight
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.zero_toGerm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [inst_2 : Zero β], MeasureTheory.AEEqFun.toGerm 0 = 0
-- Mathlib.MeasureTheory.Measure.Complex
MeasureTheory.SignedMeasure.toComplexMeasure_apply : ∀ {α : Type u_1} {m : MeasurableSpace α} {s t : MeasureTheory.SignedMeasure α} {i : Set α},
  (s.toComplexMeasure t) i = { re := s i, im := t i }
-- Init.Data.SInt.Lemmas
ISize.ofBitVec_int32ToBitVec : ∀ (x : Int32), ISize.ofBitVec (BitVec.signExtend System.Platform.numBits x.toBitVec) = x.toISize
-- Mathlib.Algebra.Lie.Abelian
TrivialLieModule.instLieModule : ∀ (R : Type u_1) (L : Type u_2) (M : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M], LieModule R L (TrivialLieModule R L M)
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.IsVonNBounded.add : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : AddZeroClass E] [inst_2 : TopologicalSpace E]
  [ContinuousAdd E] [inst_4 : DistribSMul 𝕜 E] {s t : Set E},
  Bornology.IsVonNBounded 𝕜 s → Bornology.IsVonNBounded 𝕜 t → Bornology.IsVonNBounded 𝕜 (s + t)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singletonZeroHom.eq_1 : ∀ {α : Type u_2} [inst : Zero α], Finset.singletonZeroHom = { toFun := singleton, map_zero' := ⋯ }
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
Measurable.piecewise : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f g : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β}
  {x : DecidablePred fun x => x ∈ s}, MeasurableSet s → Measurable f → Measurable g → Measurable (s.piecewise f g)
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- An affine combination over `s.subtype pred` equals one over `{x ∈ s | pred x}`.  -/
Finset.affineCombination_subtype_eq_filter : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P) (pred : ι → Prop)
  [inst_3 : DecidablePred pred],
  ((Finset.affineCombination k (Finset.subtype pred s) fun i => p ↑i) fun i => w ↑i) =
    (Finset.affineCombination k ({x ∈ s | pred x}) p) w
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The program.  -/
Turing.TM0to1.tr : {Γ : Type u_1} →
  {Λ : Type u_2} →
    [inst : Inhabited Λ] → Turing.TM0.Machine Γ Λ → Turing.TM0to1.Λ' Γ Λ → Turing.TM1.Stmt Γ (Turing.TM0to1.Λ' Γ Λ) Unit
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedActionMonoidal_η_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (X : D),
  (CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.MonoidalCategory.MonoidalRightAction.curriedAction C D)).app
      X =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso X).hom
-- Mathlib.Topology.SmallInductiveDimension
smallInductiveDimension_lt_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {n : ℕ}, smallInductiveDimension X < ↑n ↔ HasSmallInductiveDimensionLT X n
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.forIn_eq_forIn_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ},
  (forIn t init fun a d => f a.fst d) = forIn t.keys init f
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_diff_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ \ t₂).get? k = t₁.get? k
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.placesOver.eq_1 : ∀ {K : Type u_4} (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K), NumberField.InfinitePlace.placesOver L v = {w | w.LiesOver v}
-- Init.Data.List.Perm
List.isPerm.eq_2 : ∀ {α : Type u} [inst : BEq α] (x : List α) (a : α) (l : List α),
  (a :: l).isPerm x = (x.contains a && l.isPerm (x.erase a))
-- Mathlib.Algebra.Order.Monoid.Defs
add_self_nonpos_iff : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {a : α}, a + a ≤ 0 ↔ a ≤ 0
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.modulus_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
  (f : C(α, β)) {ε : ℝ} {h : 0 < ε}, 0 < f.modulus ε h
-- Mathlib.Tactic.Translate.Core
/-- Get the translation for the given name,
falling back to translating a prefix of the name if the full name can't be translated.
This allows translating automatically generated declarations such as `IsRegular.casesOn`.
We make sure that the new constant is realized.  -/
Mathlib.Tactic.Translate.findPrefixTranslation? : Lean.Name → Mathlib.Tactic.Translate.TranslateData → Lean.CoreM (Option Mathlib.Tactic.Translate.TranslationInfo)
-- Init.Data.Slice.List.Lemmas
List.mkSlice_rio_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : List α} {hi : ℕ}, (Std.Rio.Sliceable.mkSlice xs *...hi) = Std.Rco.Sliceable.mkSlice xs 0...hi
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.smul_sup : ∀ {R : Type u_1} {E : Type u_3} [inst : AddGroup E] [inst_1 : SMul R ℝ] [inst_2 : SMul R NNReal]
  [inst_3 : IsScalarTower R NNReal ℝ] (r : R) (p q : NonarchAddGroupSeminorm E), r • (p ⊔ q) = r • p ⊔ r • q
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.ae_iff_measure_eq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  {p : α → Prop}, MeasureTheory.NullMeasurableSet {a | p a} μ → ((∀ᵐ (a : α) ∂μ, p a) ↔ μ {a | p a} = μ Set.univ)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_iSup_add_one : ∀ {γ : Type u} [inst : LinearOrder γ] {f : γ → Ordinal.{u}}, StrictMono f → (⨆ i, f i + 1).cof = Order.cof γ
-- Lean.Meta.ExprLens
/-- Given a constructor index for Expr, runs `g` on the value of that subexpression and replaces it.
If the subexpression is under a binder it will instantiate and abstract the binder body correctly.
Mdata is ignored. An index of 3 is interpreted as the type of the expression. An index of 3 will throw since we can't replace types.

See also `Lean.Meta.transform`, `Lean.Meta.traverseChildren`.  -/
_private.Lean.Meta.ExprLens.0.Lean.Meta.lensCoord : {M : Type → Type} →
  [Monad M] →
    [MonadLiftT Lean.MetaM M] →
      [MonadControlT Lean.MetaM M] → [Lean.MonadError M] → (Lean.Expr → M Lean.Expr) → ℕ → Lean.Expr → M Lean.Expr
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_le_set_union : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t s' t' : Set α}, s ≤ᵐ[μ] t → s' ≤ᵐ[μ] t' → s ∪ s' ≤ᵐ[μ] t ∪ t'
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
ModuleCat.MonoidalCategory.tensorμ_eq_tensorTensorTensorComm : ∀ {R : Type u} [inst : CommRing R] {A B C D : ModuleCat R},
  CategoryTheory.MonoidalCategory.tensorμ A B C D =
    ModuleCat.ofHom ↑(TensorProduct.tensorTensorTensorComm R ↑A ↑B ↑C ↑D)
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.mk : {α : Type u_8} →
  {β : Type u_9} →
    [inst : InfSet α] →
      [inst_1 : InfSet β] → (toFun : α → β) → (∀ (s : Set α), toFun (sInf s) = sInf (toFun '' s)) → sInfHom α β
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.instOfNonempty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) [Nonempty D],
  CategoryTheory.IsCofiltered (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate F)
-- Mathlib.Algebra.Star.StarRingHom
/-- By definition, a ⋆-ring equivalence preserves the `star` operation.  -/
StarRingEquiv.map_star' : ∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B] (self : A ≃⋆+* B) (a : A), self.toFun (star a) = star (self.toFun a)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {he : t ≠ ∅}, t.get! (t.min he) = t.min he
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A functor reflecting larger colimits also reflects smaller colimits.  -/
CategoryTheory.Limits.reflectsColimitsOfSize_of_univLE : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [UnivLE.{w, w'}] [UnivLE.{w₂, w₂'}]
  [CategoryTheory.Limits.ReflectsColimitsOfSize.{w', w₂', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
-- Mathlib.Algebra.MvPolynomial.Comap
MvPolynomial.comap.eq_1 : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] (f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R)
  (x : τ → R) (i : σ), MvPolynomial.comap f x i = (MvPolynomial.aeval x) (f (MvPolynomial.X i))
-- Mathlib.Combinatorics.Colex
/-- If `s ≤ t` in colex, and all elements in `t` are small, then all elements in `s` are small.  -/
Finset.Colex.forall_le_mono : ∀ {α : Type u_1} [inst : PartialOrder α] {s t : Finset α} {a : α},
  toColex s ≤ toColex t → (∀ b ∈ t, b ≤ a) → ∀ b ∈ s, b ≤ a
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.hasLeftResolutions_iff_iso_of_essSurj_of_full : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [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} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {W₁' : CategoryTheory.MorphismProperty D₁}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [R.functor.EssSurj] [R.functor.Full] [R.IsInduced] [L.functor.EssSurj]
  [W₂'.RespectsIso] (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor),
  T.HasLeftResolutions ↔ B.HasLeftResolutions
-- Mathlib.Algebra.Group.TypeTags.Finite
Multiplicative.fintype : {α : Type u} → [Fintype α] → Fintype (Multiplicative α)
-- Mathlib.Dynamics.Ergodic.MeasurePreserving
MeasureTheory.MeasurableEquiv.measurePreserving_symm : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (μ : MeasureTheory.Measure α)
  (e : α ≃ᵐ β), MeasureTheory.MeasurePreserving (⇑e.symm) (MeasureTheory.Measure.map (⇑e) μ) μ
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.getConst.eq_2 : ∀ (k : ℤ) (v : Int.Internal.Linear.Var) (p_1 : Int.Internal.Linear.Poly),
  (Int.Internal.Linear.Poly.add k v p_1).getConst = p_1.getConst
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.strictWidthInfty_SL2Z : (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictWidthInfty = 1
-- Lean.Elab.Do.Basic
/-- Register the given name as that of a `mut` variable.  -/
Lean.Elab.Do.declareMutVar : {α : Type} → Lean.Ident → Lean.Elab.Do.DoElabM α → Lean.Elab.Do.DoElabM α
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- The canonical map to the left cosets.  -/
MulActionHom.toQuotient : {G : Type u} → [inst : Group G] → (H : Subgroup G) → G →ₑ[id] G ⧸ H
-- Init.Data.Vector.Lemmas
Vector.sum_empty : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α], #v[].sum = 0
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
/-- Helper lemma for `integral_log`: case where `a = 0` and `b` is positive.  -/
integral_log_from_zero_of_pos : ∀ {b : ℝ}, 0 < b → ∫ (s : ℝ) in 0..b, Real.log s = b * Real.log b - b
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- A set of points in a two-dimensional space is coplanar.  -/
coplanar_of_finrank_eq_two : ∀ {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] (s : Set P), Module.finrank k V = 2 → Coplanar k s
-- Mathlib.Geometry.Euclidean.MongePoint
Affine.Simplex.mongePlane.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2)) (i₁ i₂ : Fin (n + 3)),
  s.mongePlane i₁ i₂ =
    AffineSubspace.mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓
      affineSpan ℝ (Set.range s.points)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_insertList_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α},
      (k == k') = true →
        List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert →
          k ∈ List.map Sigma.fst toInsert →
            ∀ {h : Std.Internal.List.containsKey k' (Std.Internal.List.insertList l toInsert) = true},
              Std.Internal.List.getKey k' (Std.Internal.List.insertList l toInsert) h = k
-- Std.Do.Triple.SpecLemmas
Std.Do.Iter.foldM_filter : ∀ {ps : Std.Do.PostShape} {α β δ : Type w} {n : Type w → Type w''} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [LawfulMonad n] [inst_4 : Std.Do.WPMonad n ps]
  [inst_5 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {f : β → Bool} {g : δ → β → n δ} {init : δ}
  {it : Std.Iter β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄ Std.Iter.foldM (fun d b => if f b = true then g d b else pure d) init it ⦃Q⦄ →
    ⦃P⦄ Std.Iter.foldM g init (Std.Iter.filter f it) ⦃Q⦄
-- Mathlib.MeasureTheory.Integral.TorusIntegral
TorusIntegrable.eq_1 : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] (f : (Fin n → ℂ) → E) (c : Fin n → ℂ) (R : Fin n → ℝ),
  TorusIntegrable f c R =
    MeasureTheory.IntegrableOn (fun θ => f (torusMap c R θ)) (Set.Icc 0 fun x => 2 * Real.pi) MeasureTheory.volume
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.arsinh_zero : Real.arsinh 0 = 0
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_set_union : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {t₁ t₂ : Set β} {a : α}, a +ᵥ t₁ ∪ t₂ = (a +ᵥ t₁) ∪ (a +ᵥ t₂)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_mapM_eq_toListRev_mapWithPostcondition : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → n γ} {it : Std.IterM m β},
  (Std.IterM.mapM f it).toListRev =
    (Std.IterM.mapWithPostcondition (fun b => Std.Iterators.PostconditionT.attachLift (f b)) it).toListRev
-- Mathlib.Control.ULiftable
/-- Given a universe polymorphic type family `M.{u} : Type u₁ → Type
u₂`, this class convert between instantiations, from
`M.{u} : Type u₁ → Type u₂` to `M.{v} : Type v₁ → Type v₂` and back.

`f` is an outParam, because `g` can almost always be inferred from the current monad.
At any rate, the lift should be unique, as the intent is to only lift the same constants with
different universe parameters.  -/
ULiftable : outParam (Type u₀ → Type u₁) → (Type v₀ → Type v₁) → Type (max (max (max (u₀ + 1) u₁) (v₀ + 1)) v₁)
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsOrdinal.mem_trans : ∀ {x y z : ZFSet.{u}}, z.IsOrdinal → x ∈ y → y ∈ z → x ∈ z
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_dvd_iff_dvd_mul : ∀ {a b c : ℤ}, b ∣ a → b ≠ 0 → (a / b ∣ c ↔ a ∣ b * c)
-- Init.Data.UInt.Bitwise
UInt8.ofFin_rev : ∀ (a : Fin UInt8.size), UInt8.ofFin a.rev = ~~~UInt8.ofFin a
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.instMinAbs : {α : Type u_1} → [inst : Field α] → [inst_1 : LinearOrder α] → [inst_2 : IsStrictOrderedRing α] → Min (CauSeq α abs)
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
Matrix.Nonsingular.linearIndependent_row : ∀ {R : Type u_1} {n : Type u_3} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n R}
  [IsCancelAdd R], A.Nonsingular → LinearIndependent R A.row
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.isConj_iff : ∀ {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] {σ τ : Equiv.Perm α},
  σ.IsCycle → τ.IsCycle → (IsConj σ τ ↔ σ.support.card = τ.support.card)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Pred.0.Std.Tactic.BVDecide.BVPred.bitblast.match_9.eq_1 : ∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
  (motive : Std.Tactic.BVDecide.BVExpr.WithCache Std.Tactic.BVDecide.BVPred aig → Sort u_1)
  (pred : Std.Tactic.BVDecide.BVPred) (cache : Std.Tactic.BVDecide.BVExpr.Cache aig)
  (h_1 :
    (pred : Std.Tactic.BVDecide.BVPred) →
      (cache : Std.Tactic.BVDecide.BVExpr.Cache aig) → motive { val := pred, cache := cache }),
  (match { val := pred, cache := cache } with
    | { val := pred, cache := cache } => h_1 pred cache) =
    h_1 pred cache
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.comap.congr_simp : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f f_1 : F),
  f = f_1 →
    ∀ (s s_1 : NonUnitalSubsemiring S), s = s_1 → NonUnitalSubsemiring.comap f s = NonUnitalSubsemiring.comap f_1 s_1
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
_private.Mathlib.AlgebraicGeometry.Morphisms.Flat.0.AlgebraicGeometry.isIso_pushoutSection_of_iSup_eq.match_1_6.eq_1 : ∀ {ι : Type u_1} (motive : CategoryTheory.Pairwise ι → Sort u_2) (i : ι)
  (h_1 : (i : ι) → motive (CategoryTheory.Pairwise.single i))
  (h_2 : (i j : ι) → motive (CategoryTheory.Pairwise.pair i j)),
  (match CategoryTheory.Pairwise.single i with
    | CategoryTheory.Pairwise.single i => h_1 i
    | CategoryTheory.Pairwise.pair i j => h_2 i j) =
    h_1 i
-- Mathlib.Algebra.DirectSum.Ring
/-- `of A 0` is a `RingHom`, using the `DirectSum.GradeZero.semiring` structure.  -/
DirectSum.ofZeroRingHom : {ι : Type u_1} →
  [inst : DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst_1 : (i : ι) → AddCommMonoid (A i)] →
        [inst_2 : AddMonoid ι] → [inst_3 : DirectSum.GSemiring A] → A 0 →+* DirectSum ι fun i => A i
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Group.covconv_swap : ∀ {N : Type u_2} {r : N → N → Prop} [inst : Group N] [CovariantClass N N (Function.swap fun x1 x2 => x1 * x2) r],
  ContravariantClass N N (Function.swap fun x1 x2 => x1 * x2) r
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- `∑ x ∈ s, f x` is the sum of `f x` as `x` ranges over the elements
of the finite set `s`.

When the index type is a `Fintype`, the notation `∑ x, f x`, is a shorthand for
`∑ x ∈ Finset.univ, f x`.  -/
Finset.sum : {ι : Type u_1} → {M : Type u_3} → [AddCommMonoid M] → Finset ι → (ι → M) → M
-- Mathlib.Data.Set.Basic
Set.sep_subset : ∀ {α : Type u} (s : Set α) (p : α → Prop), {x | x ∈ s ∧ p x} ⊆ s
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.π₃_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y),
  CategoryTheory.Pretriangulated.Triangle.π₃.map f = f.hom₃
-- Mathlib.CategoryTheory.Sites.Subcanonical
/-- If the coproduct inclusions form a covering of `J` and coproducts are disjoint,
the yoneda embedding to `J`-sheaves preserves coproducts.  -/
CategoryTheory.GrothendieckTopology.preservesColimitsOfShape_yoneda_of_ofArrows_inj_mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {ι : Type u_1} [CategoryTheory.Limits.CoproductsOfShapeDisjoint C ι]
  [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasStrictInitialObjects C],
  (∀ {X : ι → C} {c : CategoryTheory.Limits.Cofan X} (x : CategoryTheory.Limits.IsColimit c),
      CategoryTheory.Sieve.ofArrows X c.inj ∈ J c.pt) →
    (∀ (Y : C) (a : CategoryTheory.Limits.IsInitial Y), ⊥ ∈ J Y) →
      CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ι) J.yoneda
-- Mathlib.Algebra.Order.AddGroupWithTop
WithTop.LinearOrderedAddCommGroup.neg_top : ∀ {G : Type u_1} [inst : AddCommGroup G], -⊤ = ⊤
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_cfc_nnreal_le_iff : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A] [inst_3 : PartialOrder A]
  [inst_4 : StarOrderedRing A] [inst_5 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_6 : NonnegSpectrumClass ℝ A] (f : NNReal → NNReal) (a : A) (c : NNReal),
  autoParam (ContinuousOn f (spectrum NNReal a)) nnnorm_cfc_nnreal_le_iff._auto_1 →
    autoParam (0 ≤ a) nnnorm_cfc_nnreal_le_iff._auto_3 → (‖cfc f a‖₊ ≤ c ↔ ∀ x ∈ spectrum NNReal a, f x ≤ c)
-- Init.Data.SInt.Lemmas
Int8.toInt_bmod_65536 : ∀ (x : Int8), x.toInt.bmod 65536 = x.toInt
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.LiftStruct.opEquiv_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} (sq : CategoryTheory.CommSq f i p g) (l : sq.LiftStruct),
  (CategoryTheory.CommSq.LiftStruct.opEquiv sq) l = l.op