mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Nilpotent.Lemmas
Module.End.IsNilpotent.mapQ : ∀ {R : Type u_1} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {p : Submodule R M} (hp : p ≤ Submodule.comap f p), IsNilpotent f → IsNilpotent (p.mapQ p f hp)
-- Std.Data.DHashMap.Raw
/-- Creates a hash map from a list of keys, associating the value `()` with each key.

This is mainly useful to implement `HashSet.ofList`, so if you are considering using this,
`HashSet` or `HashSet.Raw` might be a better fit for you.  -/
Std.DHashMap.Raw.Const.unitOfList : {α : Type u} → [BEq α] → [Hashable α] → List α → Std.DHashMap.Raw α fun x => Unit
-- Init.Omega.IntList
Lean.Omega.IntList.gcd_dvd_dot_left : ∀ (xs ys : Lean.Omega.IntList), ↑xs.gcd ∣ xs.dot ys
-- Mathlib.Algebra.Polynomial.Reverse
/-- If `i ≤ N`, then `revAt N i` returns `N - i`, otherwise it returns `i`.
Essentially, this embedding is only used for `i ≤ N`.
The advantage of `revAt N i` over `N - i` is that `revAt` is an involution.
 -/
Polynomial.revAt : ℕ → ℕ ↪ ℕ
-- Mathlib.Topology.WithTopology
WithTopology.instSemilatticeInf.eq_1 : ∀ {X : Type u_1} (t : TopologicalSpace X) [inst : SemilatticeInf X],
  WithTopology.instSemilatticeInf t = Function.Injective.semilatticeInf WithTopology.ofTopology ⋯ ⋯ ⋯ ⋯
-- Mathlib.Data.PNat.Defs
PNat.mk_one : ∀ {h : 0 < 1}, ⟨1, h⟩ = 1
-- Init.Data.List.Nat.Range
List.zipIdx_map : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {k : ℕ} {f : α → β},
  (List.map f l).zipIdx k = List.map (Prod.map f id) (l.zipIdx k)
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.coconeEquiv_inverse_obj_pt_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)}
  (t : CategoryTheory.Limits.Cocone (CategoryTheory.WithInitial.liftFromUnder.obj K)),
  (CategoryTheory.WithInitial.coconeEquiv.inverse.obj t).pt.hom = t.ι.app CategoryTheory.WithInitial.star
-- Mathlib.Logic.Function.Basic
Function.IsPartialInv.eq : ∀ {α : Type u_4} {β : Sort u_5} {f : α → β} {g : β → Option α}, Function.IsPartialInv f g → ∀ (x : α), g (f x) = some x
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.mk.injEq : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] {B : Type u_5} [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B]
  (toMulActionHom : A →ₑ[⇑φ] B) (map_one' : toMulActionHom.toFun 1 = 1)
  (map_mul' : ∀ (x y : A), toMulActionHom.toFun (x * y) = toMulActionHom.toFun x * toMulActionHom.toFun y)
  (toMulActionHom_1 : A →ₑ[⇑φ] B) (map_one'_1 : toMulActionHom_1.toFun 1 = 1)
  (map_mul'_1 : ∀ (x y : A), toMulActionHom_1.toFun (x * y) = toMulActionHom_1.toFun x * toMulActionHom_1.toFun y),
  ({ toMulActionHom := toMulActionHom, map_one' := map_one', map_mul' := map_mul' } =
      { toMulActionHom := toMulActionHom_1, map_one' := map_one'_1, map_mul' := map_mul'_1 }) =
    (toMulActionHom = toMulActionHom_1)
-- Mathlib.Geometry.Euclidean.Projection
Affine.Simplex.orthogonalProjectionSpan_restrict : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {n : ℕ}
  (s : Affine.Simplex 𝕜 P n) (S : AffineSubspace 𝕜 P) (hS : affineSpan 𝕜 (Set.range s.points) ≤ S) (p : ↥S),
  ↑↑((s.restrict S hS).orthogonalProjectionSpan p) = ↑(s.orthogonalProjectionSpan ↑p)
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.copy.congr_simp : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} (f f_1 : ↑(GenLoop N X x)) (e_f : f = f_1)
  (g g_1 : (N → ↑unitInterval) → X) (e_g : g = g_1) (h : g = ⇑f), GenLoop.copy f g h = GenLoop.copy f_1 g_1 ⋯
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.map_mem_nthRootsFinset_one : ∀ {R : Type u} {n : ℕ} [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_1} {F : Type u_2} [inst_2 : CommRing S]
  [inst_3 : IsDomain S] [inst_4 : FunLike F R S] [RingHomClass F R S] {x : R},
  x ∈ Polynomial.nthRootsFinset n 1 → ∀ (f : F), f x ∈ Polynomial.nthRootsFinset n 1
-- Std.Sat.CNF.RelabelFin
/-- Obtain the literal with the largest identifier in `f`.
 -/
Std.Sat.CNF.maxLiteral : Std.Sat.CNF ℕ → Option ℕ
-- Mathlib.Data.Set.Image
Set.preimage_comp_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ},
  Set.preimage (g ∘ f) = Set.preimage f ∘ Set.preimage g
-- Mathlib.AlgebraicTopology.DoldKan.NReflectsIso
AlgebraicTopology.DoldKan.instReflectsIsomorphismsSimplicialObjectKaroubiChainComplexNatN₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C],
  AlgebraicTopology.DoldKan.N₁.ReflectsIsomorphisms
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.toList_eq_if_roo : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α],
  r.toList =
    have init := Std.PRange.UpwardEnumerable.least;
    if init < r.upper then init :: (init<...r.upper).toList else []
-- Init.Data.Dyadic.Basic
Int.shiftRight_trailingZeros_mod_two : ∀ {i : ℤ}, i ≠ 0 → i >>> i.trailingZeros % 2 = 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.isEmpty_insertMany_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF → ∀ {l : List (α × β)}, (Std.DHashMap.Raw.Const.insertMany m l).isEmpty = (m.isEmpty && l.isEmpty)
-- Aesop.Rule
Aesop.RegularRule.instToFormat : Std.ToFormat Aesop.RegularRule
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.inclusion.eq_1 : ∀ {M : Type u_1} [inst : Mul M] {S T : Subsemigroup M} (h : S ≤ T),
  Subsemigroup.inclusion h = (MulMemClass.subtype S).codRestrict T ⋯
-- Mathlib.Algebra.Ring.Periodic
/-- If a function is `antiperiodic` with antiperiod `c`, then it is also `Periodic` with period
`2 * c`.  -/
Function.Antiperiodic.periodic_two_mul : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : NonAssocSemiring α] [inst_1 : InvolutiveNeg β],
  Function.Antiperiodic f c → Function.Periodic f (2 * c)
-- Mathlib.Data.Fintype.BigOperators
/-- If a product of a `Finset` of a subsingleton type has a given
value, so do the terms in that product.  -/
Fintype.eq_of_subsingleton_of_prod_eq : ∀ {M : Type u_4} [inst : CommMonoid M] {ι : Type u_5} [Subsingleton ι] {s : Finset ι} {f : ι → M} {b : M},
  ∏ i ∈ s, f i = b → ∀ i ∈ s, f i = b
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.exists_disjoint_cylinder : ∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)]
  {s : Set ((n : ℕ) → E n)}, IsClosed s → ∀ {x : (n : ℕ) → E n}, x ∉ s → ∃ n, Disjoint s (PiNat.cylinder x n)
-- Mathlib.Topology.Algebra.WithZeroTopology
WithZeroTopology.isClosed_iff : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {s : Set Γ₀},
  IsClosed s ↔ 0 ∈ s ∨ ∃ γ, γ ≠ 0 ∧ s ⊆ Set.Ici γ
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- If every `x ∈ s` has a neighbourhood within `s` on which `b ↦ ∏' i, f i b` converges uniformly
to `g`, then the product converges locally uniformly on `s` to `g`. Note that this is not a
tautology, and the converse is only true if the domain is locally compact.  -/
hasProdLocallyUniformlyOn_of_of_forall_exists_nhds : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  (∀ x ∈ s, ∃ t ∈ nhdsWithin x s, HasProdUniformlyOn f g t) → HasProdLocallyUniformlyOn f g s
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.mapM'.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive []) (h_2 : (a : α) → (l : List α) → motive (a :: l)),
  (match [] with
    | [] => h_1 ()
    | a :: l => h_2 a l) =
    h_1 ()
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.edgeSet_copy : ∀ {V : Type u} {G : SimpleGraph V} {u v u' v' : V} (p : G.Walk u v) (hu : u = u') (hv : v = v'),
  (p.copy hu hv).edgeSet = p.edgeSet
-- Mathlib.CategoryTheory.Sites.Adjunction
CategoryTheory.Sheaf.adjunction_unit_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {F : CategoryTheory.Functor D E} {G : CategoryTheory.Functor E D} [inst_3 : CategoryTheory.HasWeakSheafify J D]
  [inst_4 : J.HasSheafCompose F] (adj : G ⊣ F) (X : CategoryTheory.Sheaf J E),
  ((CategoryTheory.Sheaf.adjunction J adj).unit.app X).hom =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Adjunction.whiskerRight Cᵒᵖ adj).unit.app X.obj)
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J (X.obj.comp G)) F)
-- Lean.CoreM
/-- Next macro scope. We use macro scopes to avoid accidental name capture.  -/
Lean.Core.State.nextMacroScope : Lean.Core.State → Lean.MacroScope
-- Mathlib.Analysis.Convex.Between
sbtw_pointReflection_of_ne : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {x y : P},
  x ≠ y → Sbtw R y x ((AffineEquiv.pointReflection R x) y)
-- Mathlib.Algebra.Ring.CharZero
Nat.cast_pow_eq_one : ∀ {R : Type u_2} {n : ℕ} [inst : Semiring R] [CharZero R] {a : ℕ}, n ≠ 0 → (↑a ^ n = 1 ↔ a = 1)
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleFactorsFinset_eq_singleton_self_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {f : Equiv.Perm α}, f.cycleFactorsFinset = {f} ↔ f.IsCycle
-- Mathlib.Order.Filter.Ring
Filter.EventuallyLE.mul_le_mul : ∀ {α : Type u} {β : Type v} [inst : MulZeroClass β] [inst_1 : Preorder β] [PosMulMono β] [MulPosMono β] {l : Filter α}
  {f₁ f₂ g₁ g₂ : α → β}, f₁ ≤ᶠ[l] f₂ → g₁ ≤ᶠ[l] g₂ → 0 ≤ᶠ[l] g₁ → 0 ≤ᶠ[l] f₂ → f₁ * g₁ ≤ᶠ[l] f₂ * g₂
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_ofList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k : α}, l.contains k = false → (Std.ExtTreeSet.ofList l cmp).get? k = none
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `some n` if `e` has already been "internalized" into the
Otherwise, returns `none`s.
 -/
Lean.Meta.Grind.Goal.getENode? : Lean.Meta.Grind.Goal → Lean.Expr → Option Lean.Meta.Grind.ENode
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.primeFactors.eq_1 : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  (a : M), UniqueFactorizationMonoid.primeFactors a = (UniqueFactorizationMonoid.normalizedFactors a).toFinset
-- Mathlib.Order.Std
/-- `Ord` is compatible with ≤.  -/
LinearOrder.OfStdArgs.lawfulOrderOrd : ∀ {α : Type u_1} (self : LinearOrder.OfStdArgs α),
  let this := self.le;
  let this_1 := self.lt;
  let this_2 := ⋯;
  let this_3 := ⋯;
  let this_4 := self.decidableEq;
  let this_5 := self.decidableLT;
  Std.LawfulOrderOrd α
-- Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
Set.Nonempty.div_zero : ∀ {α : Type u_1} [inst : GroupWithZero α] {s : Set α}, s.Nonempty → s / 0 = 0
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- The injection into an additive pi group with the same values commutes.  -/
Pi.single_apply_addCommute : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → AddZeroClass (f i)] (x : (i : I) → f i)
  (i j : I), AddCommute (Pi.single i (x i)) (Pi.single j (x j))
-- Mathlib.Data.List.Basic
List.filterMap_eq_map_iff_forall_eq_some : ∀ {α : Type u} {β : Type v} {f : α → Option β} {g : α → β} {l : List α},
  List.filterMap f l = List.map g l ↔ ∀ x ∈ l, f x = some (g x)
-- Mathlib.Algebra.Group.Invertible.Basic
Invertible.mulLeft_symm_apply : ∀ {α : Type u} [inst : Monoid α] {a : α} (x : Invertible a) (b : α) (x_1 : Invertible (a * b)),
  (x.mulLeft b).symm x_1 = invertibleOfInvertibleMul a b
-- Lean.Declaration
Lean.AxiomVal.mk : Lean.ConstantVal → Bool → Lean.AxiomVal
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.le_smul_caratheodory : ∀ {α : Type u_1} (a : ENNReal) (m : MeasureTheory.OuterMeasure α), m.caratheodory ≤ (a • m).caratheodory
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote.eq_1 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α),
  Lean.Grind.CommRing.Mon.denote ctx Lean.Grind.CommRing.Mon.unit = 1
-- Mathlib.Combinatorics.SimpleGraph.DegreeSum
SimpleGraph.two_mul_card_edgeFinset : ∀ {V : Type u} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj],
  2 * G.edgeFinset.card =
    {x |
        match x with
        | (x, y) => G.Adj x y}.card
-- Mathlib.Analysis.InnerProductSpace.PiL2
FiniteDimensional.range_orthonormalBasisSingleton : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : Unique ι] (h : Module.finrank 𝕜 E = 1) {v : E}
  (hv : ‖v‖ = 1), Set.range ⇑(FiniteDimensional.orthonormalBasisSingleton ι 𝕜 h v hv) = {v}
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Semiring.natCastFn? : Lean.Meta.Grind.Arith.CommRing.Semiring → Option Lean.Expr
-- Aesop.Tree.Data
Aesop.GoalOrigin.droppedMVar : Aesop.GoalOrigin
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- Given the relation for grewriting at the given position, figure out all of the
subrelations that could also be used.  -/
_private.Mathlib.Tactic.ClickSuggestions.GRewrite.0.Mathlib.Tactic.ClickSuggestions.gcongrBackward : Lean.Name → Lean.Expr → Bool → Lean.MetaM (Array Mathlib.Tactic.ClickSuggestions.GrwPos)
-- Mathlib.Algebra.Module.Injective
/-- Since we assumed `Q` being Baer, the linear map `x ↦ f' (x • y) : I ⟶ Q` extends to `R ⟶ Q`,
call this extended map `φ`  -/
Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo : {R : Type u} →
  [inst : Ring R] →
    {Q : Type v} →
      [inst_1 : AddCommGroup Q] →
        [inst_2 : Module R Q] →
          {M : Type u_1} →
            {N : Type u_2} →
              [inst_3 : AddCommGroup M] →
                [inst_4 : AddCommGroup N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module R N] →
                      (i : M →ₗ[R] N) → (M →ₗ[R] Q) → [Fact (Function.Injective ⇑i)] → Module.Baer R Q → N → R →ₗ[R] Q
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
/-- **Alias** of `Ideal.strongNormalizationMonoid`. -/
Ideal.normalizationMonoid : {A : Type u_2} → [inst : CommRing A] → StrongNormalizationMonoid (Ideal A)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.map_left : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MultispanShape}
  (d : CategoryTheory.Limits.MultispanIndex J C) (F : CategoryTheory.Functor C D) (i : J.L),
  (d.map F).left i = F.obj (d.left i)
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.adjunction_counit_app_self : ∀ {X : TopCat} (U : TopologicalSpace.Opens ↑X), ⋯.adjunction.counit.app U = CategoryTheory.eqToHom ⋯
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
RingOfIntegers.ZModXQuotSpanEquivQuotSpan.eq_1 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {θ : NumberField.RingOfIntegers K} {p : ℕ}
  [inst_2 : Fact (Nat.Prime p)] (hp : ¬p ∣ RingOfIntegers.exponent θ),
  RingOfIntegers.ZModXQuotSpanEquivQuotSpan hp =
    (Ideal.quotientEquivAlgOfEq ℤ ⋯).toRingEquiv.trans
      (((Ideal.span {Polynomial.map (Ideal.Quotient.mk (Ideal.span {↑p})) (minpoly ℤ θ)}).quotientEquiv
              (Ideal.map (↑(Polynomial.mapEquiv (Int.quotientSpanNatEquivZMod p)))
                (Ideal.span {Polynomial.map (Ideal.Quotient.mk (Ideal.span {↑p})) (minpoly ℤ θ)}))
              (Polynomial.mapEquiv (Int.quotientSpanNatEquivZMod p)) ⋯).symm.trans
        ((KummerDedekind.quotMapEquivQuotQuotMap ⋯ ⋯).symm.trans (Ideal.quotientEquivAlgOfEq ℤ ⋯).toRingEquiv))
-- Init.Data.Range.Polymorphic.Lemmas
Std.toList_roi_eq_toList_rci_of_isSome_succ? : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α] {lo : α} (h : (Std.PRange.succ? lo).isSome = true),
  lo<...*.toList = ((Std.PRange.succ? lo).get h)...*.toList
-- Aesop.Forward.PremiseIndex
Aesop.instDecidableRelPremiseIndexLe : DecidableRel fun x1 x2 => x1 ≤ x2
-- Mathlib.Algebra.Group.Subsemigroup.Membership
AddSubsemigroup.mem_sSup_of_directed_on : ∀ {M : Type u_2} [inst : Add M] {S : Set (AddSubsemigroup M)},
  DirectedOn (fun x1 x2 => x1 ≤ x2) S → ∀ {x : M}, x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
-- Mathlib.LinearAlgebra.Matrix.Polynomial
Polynomial.coeff_det_X_add_C_zero : ∀ {n : Type u_1} {α : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A B : Matrix n n α),
  (Polynomial.X • A.map ⇑Polynomial.C + B.map ⇑Polynomial.C).det.coeff 0 = B.det
-- Batteries.Data.ByteArray
ByteArray.data_mkEmpty : ∀ (cap : ℕ), (ByteArray.emptyWithCapacity cap).data = #[]
-- Init.Data.String.Iterator
/-- Moves the iterator's position backward by one character, unconditionally.

The position is not changed if the iterator is at the beginning of the string.
 -/
String.Legacy.Iterator.prev : String.Legacy.Iterator → String.Legacy.Iterator
-- Std.Data.DTreeMap.Iterator
/-- Returns a finite iterator over the values of a tree map.
The iterator yields the values in order and then terminates.

The key and value types must live in the same universe.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Std.DTreeMap.valuesIter : {α β : Type u} → {cmp : α → α → Ordering} → Std.DTreeMap α (fun x => β) cmp → Std.Iter β
-- Mathlib.Algebra.ContinuedFractions.Translations
_private.Mathlib.Algebra.ContinuedFractions.Translations.0.GenContFract.contsAux.match_3.eq_3 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match n.succ.succ with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_3 n
-- Lean.Meta.Tactic.Apply
Lean.Meta.synthAppInstances : Lean.Name → Lean.MVarId → Array Lean.Expr → Array Lean.BinderInfo → Bool → Bool → Lean.MetaM Unit
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.opUnitIso.eq_1 : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V],
  HomologicalComplex.opUnitIso V c =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        (HomologicalComplex.Hom.isoOfComponents (fun x => CategoryTheory.Iso.refl ((Opposite.unop X).op.unopSymm.X x))
            ⋯).op)
      ⋯
-- ProofWidgets.Component.Basic
/-- Present pretty-printed code as interactive text.

The most common use case is to instantiate this component from a `Lean.Expr`. To do so, you must
eagerly pretty-print the `Expr` using `Widget.ppExprTagged`. See also `InteractiveExpr`.  -/
ProofWidgets.InteractiveCode : ProofWidgets.Component ProofWidgets.InteractiveCodeProps
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.setRed.eq_2 : ∀ {α : Type u_1}, RBTree.RBNode.nil.setRed = RBTree.RBNode.nil
-- Init.Data.UInt.Lemmas
USize.neg_inj : ∀ {a b : USize}, -a = -b ↔ a = b
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
le_ciInf_exists : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {p : ι → Prop} {f : Exists p → α},
  ⨅ i, ⨅ (h : p i), f ⋯ ≤ ⨅ (ih : Exists p), f ih
-- Mathlib.FieldTheory.AbelRuffini
gal_C_isSolvable : ∀ {F : Type u_1} [inst : Field F] (x : F), Group.IsSolvable (Polynomial.C x).Gal
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.PullbackShift.natTrans.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) {D : Type u_4}
  [inst_4 : CategoryTheory.Category.{v_2, u_4} D] [inst_5 : CategoryTheory.HasShift D B]
  {F G : CategoryTheory.Functor C D} (τ : F ⟶ G), CategoryTheory.PullbackShift.natTrans φ τ = τ
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cocyclesMap_id_comp_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{u, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C) (n : ℕ)
  {Z : ModuleCat k} (h : groupCohomology.cocycles C n ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (groupCohomology.cocyclesMap (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) n) h =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesMap (MonoidHom.id G) φ n)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesMap (MonoidHom.id G) ψ n) h)
-- Mathlib.MeasureTheory.Function.Egorov
MeasureTheory.Egorov.iUnionNotConvergentSeq.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [inst : PseudoEMetricSpace β]
  {μ : MeasureTheory.Measure α} {s : Set α} {ε : ℝ} {f : ι → α → β} {g : α → β} [inst_1 : SemilatticeSup ι]
  [inst_2 : Nonempty ι] [inst_3 : Countable ι] (hε : 0 < ε) (hf : ∀ (n : ι), Measurable fun a => edist (f n a) (g a))
  (hsm : MeasurableSet s) (hs : μ s ≠ ⊤)
  (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))),
  MeasureTheory.Egorov.iUnionNotConvergentSeq hε hf hsm hs hfg =
    ⋃ n,
      s ∩ MeasureTheory.Egorov.notConvergentSeq f g n (MeasureTheory.Egorov.notConvergentSeqLTIndex ⋯ hf hsm hs hfg n)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.LeanClientCapabilities.mk.inj : ∀ {incrementalDiagnosticSupport? silentDiagnosticSupport? : Option Bool}
  {rpcWireFormat? : Option Lean.Lsp.RpcWireFormat}
  {incrementalDiagnosticSupport?_1 silentDiagnosticSupport?_1 : Option Bool}
  {rpcWireFormat?_1 : Option Lean.Lsp.RpcWireFormat},
  { incrementalDiagnosticSupport? := incrementalDiagnosticSupport?,
        silentDiagnosticSupport? := silentDiagnosticSupport?, rpcWireFormat? := rpcWireFormat? } =
      { incrementalDiagnosticSupport? := incrementalDiagnosticSupport?_1,
        silentDiagnosticSupport? := silentDiagnosticSupport?_1, rpcWireFormat? := rpcWireFormat?_1 } →
    incrementalDiagnosticSupport? = incrementalDiagnosticSupport?_1 ∧
      silentDiagnosticSupport? = silentDiagnosticSupport?_1 ∧ rpcWireFormat? = rpcWireFormat?_1
-- Lean.Elab.Do.InferControlInfo
Lean.Elab.Do.InferControlInfo.ofElem : Lean.DoElem → Lean.Elab.TermElabM Lean.Elab.Do.ControlInfo
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.continuousOn_smul : ∀ {𝕜 : Type u_2} {E : Type u_5} [inst : NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f : ℝ → 𝕜}
  {g : ℝ → E} [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 E] [IsBoundedSMul 𝕜 E],
  IntervalIntegrable g μ a b → ContinuousOn f (Set.uIcc a b) → IntervalIntegrable (fun x => f x • g x) μ a b
-- Mathlib.Data.Set.Sups
/-- The point-wise infimum `a ⊓ b` of `a, b : α`.  -/
«term_⊼_» : Lean.TrailingParserDescr
-- Mathlib.Data.Multiset.AddSub
Multiset.le_add_sub : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s ≤ t + (s - t)
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.convexOn_mul_log : ConvexOn ℝ (Set.Ici 0) fun x => x * Real.log x