mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Matrix.Mul
Matrix.smul_one_eq_diagonal : ∀ {m : Type u_2} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : DecidableEq m] (a : α),
  a • 1 = Matrix.diagonal fun x => a
-- Mathlib.Order.Interval.Set.Disjoint
Set.biUnion_Ioc_eq_Ioi_self_iff : ∀ {ι : Sort u} {α : Type v} [inst : LinearOrder α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α},
  ⋃ i, ⋃ (hi : p i), Set.Ioc a (f i hi) = Set.Ioi a ↔ ∀ (x : α), a < x → ∃ i, ∃ (hi : p i), x ≤ f i hi
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.Const.aux_size_modify : ∀ {α : Type u} {β : Type v} [inst : Ord α] {k : α} {f : β → β} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  (Std.DTreeMap.Internal.Impl.Const.modify k f t).size = t.size
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Justification.brecOn.eq : ∀
  {motive :
    (a : Lean.Omega.Constraint) → (a_1 : Lean.Omega.Coeffs) → Lean.Elab.Tactic.Omega.Justification a a_1 → Sort u}
  {a : Lean.Omega.Constraint} {a_1 : Lean.Omega.Coeffs} (t : Lean.Elab.Tactic.Omega.Justification a a_1)
  (F_1 :
    (a : Lean.Omega.Constraint) →
      (a_2 : Lean.Omega.Coeffs) →
        (t : Lean.Elab.Tactic.Omega.Justification a a_2) →
          Lean.Elab.Tactic.Omega.Justification.below t → motive a a_2 t),
  Lean.Elab.Tactic.Omega.Justification.brecOn t F_1 =
    F_1 a a_1 t (Lean.Elab.Tactic.Omega.Justification.brecOn.go t F_1).2
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.instIsTriangulatedOppositeOpOpEquivalence : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C],
  (CategoryTheory.opOpEquivalence C).IsTriangulated
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (not_mem : k ∉ m₁) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).getKey k h' = m₂.getKey k ⋯
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.map_mk₁ : ∀ {Γ : Type u_1} {Γ' : Type u_2} [inst : Inhabited Γ] [inst_1 : Inhabited Γ'] (f : Turing.PointedMap Γ Γ') (l : List Γ),
  Turing.Tape.map f (Turing.Tape.mk₁ l) = Turing.Tape.mk₁ (List.map f.f l)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.measureUnivNNReal_pos : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ],
  μ ≠ 0 → 0 < MeasureTheory.measureUnivNNReal μ
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.HasLeftKanExtension.hasInitial : ∀ {B : Type u} {inst : CategoryTheory.Bicategory B} {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  [self : CategoryTheory.Bicategory.HasLeftKanExtension f g],
  CategoryTheory.Limits.HasInitial (CategoryTheory.Bicategory.LeftExtension f g)
-- Mathlib.Data.Int.GCD
/-- Euclid's lemma: if `a ∣ b * c` and `gcd a b = 1` then `a ∣ c`.
Compare with `IsCoprime.dvd_of_dvd_mul_right` and
`UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors`  -/
Int.dvd_of_dvd_mul_right_of_gcd_one : ∀ {a b c : ℤ}, a ∣ b * c → a.gcd b = 1 → a ∣ c
-- Lean.Meta.Sym.Arith.Types
/-- `CommSemiring` instance for `type`  -/
Lean.Meta.Sym.Arith.CommRing.commSemiringInst : Lean.Meta.Sym.Arith.CommRing → Lean.Expr
-- Mathlib.RingTheory.Valuation.Discrete.Basic
/-- An element `π : A` is a uniformizer if `v π` is a generator of the value group that is `< 1`.  -/
Valuation.IsUniformizer : {Γ : Type u_1} →
  [inst : LinearOrderedCommGroupWithZero Γ] →
    {A : Type u_2} → [inst_1 : Ring A] → (v : Valuation A Γ) → [hv : v.IsRankOneDiscrete] → A → Prop
-- Lean.Parser.Term.Basic
Lean.Parser.Tactic.tacticSeqIndentGt.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.toAddMonoidHom'_apply : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R₁ M] [inst_5 : Module R₂ M₂]
  {σ₁₂ : R₁ →+* R₂} (f : M →ₛₗ[σ₁₂] M₂), LinearMap.toAddMonoidHom' f = f.toAddMonoidHom
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- Estimate for `log⁺` of a product. See `Real.posLog_prod` for a variant involving
multiple factors.  -/
Real.posLog_mul : ∀ {x y : ℝ}, (x * y).posLog ≤ x.posLog + y.posLog
-- Mathlib.Algebra.Module.CharacterModule
AddCon.liftOn.congr_simp : ∀ {M : Type u_1} [inst : Add M] {β : Sort u_4} {c : AddCon M} (q q_1 : c.Quotient),
  q = q_1 →
    ∀ (f f_1 : M → β) (e_f : f = f_1) (h : ∀ (a b : M), c a b → f a = f b),
      AddCon.liftOn q f h = AddCon.liftOn q_1 f_1 ⋯
-- Mathlib.Tactic.Sat.FromLRAT
/-- Append a literal to a clause.  -/
Sat.Clause.cons : Sat.Literal → Sat.Clause → Sat.Clause
-- Batteries.Data.Array.Match
_private.Batteries.Data.Array.Match.0.Array.Matcher.finitenessRelation : {n : Type u_1 → Type u_2} →
  {α σ : Type u_1} →
    [inst : Monad n] →
      [inst_1 : BEq α] →
        (m : Array.Matcher α) →
          [inst_2 : Std.Iterator σ n α] →
            [Std.Iterators.Finite σ n] → Std.Iterators.FinitenessRelation (Array.Matcher.Iterator σ n α m) n
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddMonCat.FilteredColimits.colimitZero.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J AddMonCat)
  [inst_1 : CategoryTheory.IsFiltered J],
  AddMonCat.FilteredColimits.colimitZero F = { zero := AddMonCat.FilteredColimits.M.mk F ⟨⋯.some, 0⟩ }
-- Mathlib.CategoryTheory.Filtered.FinallySmall
/-- If `C` is a locally small filtered finally small category,
this is a small filtered category, equipped with a final functor to `C`
(see `fromFilteredFinalModel`).  -/
CategoryTheory.FinallySmall.FilteredFinalModel : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsFiltered C] → [CategoryTheory.LocallySmall.{w, v, u} C] → [CategoryTheory.FinallySmall C] → Type w
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_norm : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ : Int.Internal.Linear.Poly),
  p₁.norm.beq' p₂ = true → Int.Internal.Linear.Poly.denote' ctx p₁ = 0 → Int.Internal.Linear.Poly.denote' ctx p₂ = 0
-- Mathlib.Data.Set.Restrict
Set.codRestrict_range_surjective : ∀ {α : Type u_1} {ι : Sort u_5} (f : ι → α), Function.Surjective (Set.codRestrict f (Set.range f) ⋯)
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_sdiff_add_inter : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet t →
    autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_sdiff_add_inter._auto_1 → μ.real (s \ t) + μ.real (s ∩ t) = μ.real s
-- Batteries.Recycling.RBTree.Basic
_private.Batteries.Recycling.RBTree.Basic.0.RBTree.RBNode.append.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → RBTree.RBNode α → Sort u_2) (x : RBTree.RBNode α)
  (h_1 : (x : RBTree.RBNode α) → motive RBTree.RBNode.nil x) (h_2 : (x : RBTree.RBNode α) → motive x RBTree.RBNode.nil)
  (h_3 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.red c y d))
  (h_4 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c : RBTree.RBNode α) →
          (y : α) →
            (d : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.black a x b) (RBTree.RBNode.node RBTree.RBColor.black c y d))
  (h_5 :
    (a l : RBTree.RBNode α) →
      (v : α) →
        (r : RBTree.RBNode α) →
          a = RBTree.RBNode.node RBTree.RBColor.black l v r →
            (b : RBTree.RBNode α) →
              (x : α) →
                (c : RBTree.RBNode α) →
                  motive (RBTree.RBNode.node RBTree.RBColor.black l v r) (RBTree.RBNode.node RBTree.RBColor.red b x c))
  (h_6 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b c l : RBTree.RBNode α) →
          (v : α) →
            (r : RBTree.RBNode α) →
              c = RBTree.RBNode.node RBTree.RBColor.black l v r →
                motive (RBTree.RBNode.node RBTree.RBColor.red a x b) (RBTree.RBNode.node RBTree.RBColor.black l v r)),
  (x = RBTree.RBNode.nil → False) →
    (match x, RBTree.RBNode.nil with
      | RBTree.RBNode.nil, x => h_1 x
      | x, RBTree.RBNode.nil => h_2 x
      | RBTree.RBNode.node RBTree.RBColor.red a x b, RBTree.RBNode.node RBTree.RBColor.red c y d => h_3 a x b c y d
      | RBTree.RBNode.node RBTree.RBColor.black a x b, RBTree.RBNode.node RBTree.RBColor.black c y d => h_4 a x b c y d
      | a@h:(RBTree.RBNode.node RBTree.RBColor.black l v r), RBTree.RBNode.node RBTree.RBColor.red b x c =>
        h_5 a l v r h b x c
      | RBTree.RBNode.node RBTree.RBColor.red a x b, c@h:(RBTree.RBNode.node RBTree.RBColor.black l v r) =>
        h_6 a x b c l v r h) =
      h_2 x
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
AddCommMonCat.FilteredColimits.colimitAddCommMonoid.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddCommMonCat),
  AddCommMonCat.FilteredColimits.colimitAddCommMonoid F =
    { toAddMonoid := (AddCommMonCat.FilteredColimits.M F).str, add_comm := ⋯ }
-- Mathlib.Logic.Basic
forall_eq_apply_imp_iff' : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} {p : β → Prop}, (∀ (a : α) (b : β), b = f a → p b) ↔ ∀ (a : α), p (f a)
-- Mathlib.Algebra.Group.Basic
eq_add_of_sub_eq' : ∀ {G : Type u_3} [inst : AddCommGroup G] {a b c : G}, a - b = c → a = b + c
-- Std.Data.TreeSet.Slice
Std.TreeSet.toList_ric : ∀ {α : Type u} (cmp : autoParam (α → α → Ordering) Std.TreeSet.toList_ric._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeSet α cmp} {bound : α},
  Std.Slice.toList (Std.Ric.Sliceable.mkSlice t *...=bound) = List.filter (fun e => (cmp e bound).isLE) t.toList
-- Mathlib.Data.Finset.Basic
/-- The disjoint union of finsets is a sum  -/
Equiv.Finset.union : {α : Type u_1} → [inst : DecidableEq α] → (s t : Finset α) → Disjoint s t → ↥s ⊕ ↥t ≃ ↥(s ∪ t)
-- Mathlib.Data.Multiset.Dedup
Multiset.Subset.dedup_add_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s ⊆ t → (s + t).dedup = t.dedup
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.zero_sub_eq_eval : ∀ {R : Type u_2} {M : Type u_3} [inst : AddCommGroup M] [inst_1 : Ring R] [inst_2 : Module R M]
  (l : Mathlib.Tactic.Module.NF R M), 0 - l.eval = (-l).eval
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- The functor equipping a module with the indiscrete topology.
This is right adjoint to the forgetful functor.  -/
TopModuleCat.indiscrete : (R : Type u) → [inst : Ring R] → [inst_1 : TopologicalSpace R] → CategoryTheory.Functor (ModuleCat R) (TopModuleCat R)
-- Mathlib.NumberTheory.FLT.Three
/-- Given `S : Solution`, we let `S.u₂` and `S.Y` be any elements such that
`S.Y ^ 3 * S.u₂ = S.y`  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.Y : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} →
      {hζ : IsPrimitiveRoot ζ 3} →
        FermatLastTheoremForThreeGen.Solution✝ hζ →
          [inst_1 : NumberField K] → [IsCyclotomicExtension {3} ℚ K] → NumberField.RingOfIntegers K
-- Mathlib.Analysis.Normed.Operator.Prod
ContinuousLinearMap.prodMapL_apply : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {M₁ : Type u_5} {M₂ : Type u_6} {M₃ : Type u_7} {M₄ : Type u_8}
  [inst_1 : SeminormedAddCommGroup M₁] [inst_2 : NormedSpace 𝕜 M₁] [inst_3 : SeminormedAddCommGroup M₂]
  [inst_4 : NormedSpace 𝕜 M₂] [inst_5 : SeminormedAddCommGroup M₃] [inst_6 : NormedSpace 𝕜 M₃]
  [inst_7 : SeminormedAddCommGroup M₄] [inst_8 : NormedSpace 𝕜 M₄] (p : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)),
  (ContinuousLinearMap.prodMapL 𝕜 M₁ M₂ M₃ M₄) p = p.1.prodMap p.2
-- Init.Data.Function
Function.uncurry_curry : ∀ {α : Type u_1} {β : Type u_2} {φ : Sort u_3} (f : α × β → φ), Function.uncurry (Function.curry f) = f
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.castLE.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} (x x_1 : ℕ) (x_2 : x ≤ x_1) (x_3 : L.BoundedFormula α x),
  FirstOrder.Language.BoundedFormula.castLE x_2 x_3 =
    match x, x_1, x_2, x_3 with
    | _m, _n, _h, FirstOrder.Language.BoundedFormula.falsum => FirstOrder.Language.BoundedFormula.falsum
    | _m, _n, h, FirstOrder.Language.BoundedFormula.equal t₁ t₂ =>
      FirstOrder.Language.BoundedFormula.equal (FirstOrder.Language.Term.relabel (Sum.map id (Fin.castLE h)) t₁)
        (FirstOrder.Language.Term.relabel (Sum.map id (Fin.castLE h)) t₂)
    | _m, _n, h, FirstOrder.Language.BoundedFormula.rel R ts =>
      FirstOrder.Language.BoundedFormula.rel R (FirstOrder.Language.Term.relabel (Sum.map id (Fin.castLE h)) ∘ ts)
    | _m, _n, h, f₁.imp f₂ =>
      (FirstOrder.Language.BoundedFormula.castLE h f₁).imp (FirstOrder.Language.BoundedFormula.castLE h f₂)
    | _m, _n, h, f.all => (FirstOrder.Language.BoundedFormula.castLE ⋯ f).all
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.valued_ofCompletion : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  (y : (IsDedekindDomain.HeightOneSpectrum.valuation K v).Completion), Valued.v { toCompletion := y } = Valued.v y
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.inLocalDecls : List Lean.LocalDecl → Lean.FVarId → Bool
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.count_of_coprime : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)] {a : Associates α},
  a ≠ 0 →
    ∀ {b : Associates α},
      b ≠ 0 →
        (∀ (d : Associates α), d ∣ a → d ∣ b → ¬Prime d) →
          ∀ {p : Associates α}, Irreducible p → p.count a.factors = 0 ∨ p.count b.factors = 0
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ToBackwardSearcher.DefaultBackwardSearcher.mk.inj : ∀ {ρ : Type} {pat : ρ} {s : String.Slice} {currPos currPos_1 : s.Pos},
  { currPos := currPos } = { currPos := currPos_1 } → currPos = currPos_1
-- Mathlib.Order.SuccPred.LinearLocallyFinite
LinearOrder.isPredArchimedean_of_isSuccArchimedean : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : PredOrder ι] [IsSuccArchimedean ι],
  IsPredArchimedean ι
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.Hom.zero_app : ∀ {X : AlgebraicGeometry.Scheme} {M N : X.Modules} {U : X.Opens}, AlgebraicGeometry.Scheme.Modules.Hom.app 0 U = 0
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuous_iff_isClosed_preimage : ∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrder γ] {f : α → γ},
  UpperSemicontinuous f ↔ ∀ (y : γ), IsClosed (f ⁻¹' Set.Ici y)
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsKleinFour.not_isCyclic : ∀ {G : Type u_1} [inst : Group G] [IsKleinFour G], ¬IsCyclic G
-- Std.Time.Date.Unit.Day
/-- Convert `Second.Offset` into `Day.Offset`.
 -/
Std.Time.Day.Offset.ofSeconds : Std.Time.Second.Offset → Std.Time.Day.Offset
-- Std.Internal.UV.System
Std.Internal.UV.System.CPUTimes.mk.injEq : ∀ (user nice sys idle irq user_1 nice_1 sys_1 idle_1 irq_1 : UInt64),
  ({ user := user, nice := nice, sys := sys, idle := idle, irq := irq } =
      { user := user_1, nice := nice_1, sys := sys_1, idle := idle_1, irq := irq_1 }) =
    (user = user_1 ∧ nice = nice_1 ∧ sys = sys_1 ∧ idle = idle_1 ∧ irq = irq_1)
-- Lean.Elab.Tactic.Try
/-- Returns the suggestions represented by `tac`.   -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.getSuggestionOfTactic : Lean.TSyntax `tactic → Array (Lean.TSyntax `tactic)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- **Alias** of `SkewMonoidAlgebra.ofCoeff_injective`. -/
SkewMonoidAlgebra.ofFinsupp_injective : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k], Function.Injective SkewMonoidAlgebra.ofCoeff
-- Mathlib.Data.Rat.Cast.CharZero
/-- [Stacks Tag 09FR](https://stacks.math.columbia.edu/tag/09FR) (Characteristic zero case.) -/
Rat.cast_injective : ∀ {α : Type u_3} [inst : DivisionRing α] [CharZero α], Function.Injective Rat.cast
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- If `X ⟶ Y` is an open immersion of PresheafedSpaces, and `Y` is a LocallyRingedSpace, we can
upgrade it into a morphism of LocallyRingedSpace.
 -/
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpaceHom : {X : AlgebraicGeometry.PresheafedSpace CommRingCat} →
  (Y : AlgebraicGeometry.LocallyRingedSpace) →
    (f : X ⟶ Y.toPresheafedSpace) →
      [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] →
        AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.toLocallyRingedSpace Y f ⟶ Y
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.coe_smul : ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [inst_2 : DecidableEq α] {n : ℕ} {g : G}
  {s : ↑(Set.powersetCard α n)}, ↑(g • s) = g • ↑s
-- Init.Grind.Module.Basic
Lean.Grind.instSubCoOfAddOfNeg : ∀ {α : Type u_1} {lo hi : ℤ} [inst : Lean.Grind.ToInt α (Lean.Grind.IntInterval.co lo hi)]
  [inst_1 : Lean.Grind.AddCommGroup α] [Lean.Grind.ToInt.Add α (Lean.Grind.IntInterval.co lo hi)]
  [Lean.Grind.ToInt.Neg α (Lean.Grind.IntInterval.co lo hi)], Lean.Grind.ToInt.Sub α (Lean.Grind.IntInterval.co lo hi)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.ext_iff : ∀ {R : Type u} {M : Type v} [inst : VAdd R M] {p q : SubAddAction R M}, p = q ↔ ∀ (x : M), x ∈ p ↔ x ∈ q
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of `Left.neg_nonpos_iff`.

---

Uses `left` co(ntra)variant.  -/
neg_nonpos : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] {a : α}, -a ≤ 0 ↔ 0 ≤ a
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.BiconeMorphism.mk.inj : ∀ {J : Type w} {C : Type uC} {inst : CategoryTheory.Category.{uC', uC} C}
  {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C} {F : J → C} {A B : CategoryTheory.Limits.Bicone F}
  {hom : A.pt ⟶ B.pt}
  {wπ :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp hom (B.π j) = A.π j)
      CategoryTheory.Limits.BiconeMorphism.wπ._autoParam}
  {wι :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (A.ι j) hom = B.ι j)
      CategoryTheory.Limits.BiconeMorphism.wι._autoParam}
  {hom_1 : A.pt ⟶ B.pt}
  {wπ_1 :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp hom_1 (B.π j) = A.π j)
      CategoryTheory.Limits.BiconeMorphism.wπ._autoParam}
  {wι_1 :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (A.ι j) hom_1 = B.ι j)
      CategoryTheory.Limits.BiconeMorphism.wι._autoParam},
  { hom := hom, wπ := wπ, wι := wι } = { hom := hom_1, wπ := wπ_1, wι := wι_1 } → hom = hom_1
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.inv_Ici : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a : α), (Set.Ici a)⁻¹ = Set.Iic a⁻¹
-- Mathlib.Data.Nat.BitIndices
Nat.bitIndices_one : Nat.bitIndices 1 = [0]
-- Mathlib.CategoryTheory.Subobject.ArtinianObject
CategoryTheory.isArtinianObject_of_isZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C},
  CategoryTheory.Limits.IsZero X → CategoryTheory.IsArtinianObject X
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.π_comp_eqToHom_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (f : J → C) [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  {j j' : J} (w : j = j') {Z : C} (h : f j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π f j') h
-- Mathlib.Order.Interval.Set.Defs
Set.Ico_def : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), {x | a ≤ x ∧ x < b} = Set.Ico a b
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.take_take : ∀ {A : Type u_1} {T : ↥(Descriptive.tree A)} (m n : ℕ) (x : ↥T),
  Descriptive.Tree.take m (Descriptive.Tree.take n x) = Descriptive.Tree.take (min m n) x
-- Mathlib.Algebra.Group.Action.Opposite
/-- With `open scoped RightActions`, an alternative symbol for left actions, `r +ᵥ m`.

In lemma names this is still called `vadd`.  -/
RightActions.«term_+ᵥ>_» : Lean.TrailingParserDescr
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_top : ∀ {a : ENNReal}, a ≠ 0 → a * ⊤ = ⊤
-- Mathlib.CategoryTheory.Category.PartialFun
partialFunToPointed_obj : ∀ (X : PartialFun), partialFunToPointed.obj X = { X := Option X, point := none }
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_le_iff_of_dvd_of_neg : ∀ {a b c : ℤ}, b < 0 → b ∣ a → (a / b ≤ c ↔ b * c ≤ a)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItem.data? : Lean.Lsp.CompletionItem → Option Lean.Json
-- Mathlib.Topology.Algebra.InfiniteSum.Order
le_hasSum : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : AddCommMonoid α] [inst_1 : Preorder α]
  [IsOrderedAddMonoid α] [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α} [L.NeBot]
  [L.LeAtTop], HasSum f a L → ∀ (i : ι), (∀ (j : ι), j ≠ i → 0 ≤ f j) → f i ≤ a
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Turn an element of a type `F` satisfying `AddActionSemiHomClass F φ X Y`
into an actual `AddActionHom`.
This is declared as the default coercion from `F` to `AddActionSemiHom φ X Y`.  -/
AddActionSemiHomClass.toAddActionHom : {M : Type u_2} →
  {N : Type u_3} →
    {φ : M → N} →
      {X : Type u_5} →
        [inst : VAdd M X] →
          {Y : Type u_6} →
            [inst_1 : VAdd N Y] →
              {F : Type u_8} → [inst_2 : FunLike F X Y] → [AddActionSemiHomClass F φ X Y] → F → X →ₑ[φ] Y
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.restrictFreeVar.eq_5 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] (x : ℕ) (φ : L.BoundedFormula α (x + 1))
  (f : ↥φ.all.freeVarFinset → β), φ.all.restrictFreeVar f = (φ.restrictFreeVar f).all
-- Mathlib.Topology.ShrinkingLemma
/-- Least upper bound of a nonempty chain of partial refinements.  -/
ShrinkingLemma.PartialRefinement.chainSup : {ι : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {u : ι → Set X} →
        {s : Set X} →
          {p : Set X → Prop} →
            (c : Set (ShrinkingLemma.PartialRefinement u s p)) →
              IsChain (fun x1 x2 => x1 ≤ x2) c →
                c.Nonempty → (∀ x ∈ s, {i | x ∈ u i}.Finite) → s ⊆ ⋃ i, u i → ShrinkingLemma.PartialRefinement u s p
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.Infinite.ne_real : ∀ {x : ℝ*}, x.Infinite → ∀ (r : ℝ), x ≠ ↑r
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.topEquiv_symm_apply_coe : ∀ {M : Type u_1} [inst : Add M] (x : M), ↑(AddSubsemigroup.topEquiv.symm x) = x
-- Init.Data.UInt.Basic
instMulUSize : Mul USize
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.diag.eq_1 : ∀ (A : Type u_2) [inst : AddMonoid A] [inst_1 : TopologicalSpace A],
  ContinuousAddMonoidHom.diag A = (ContinuousAddMonoidHom.id A).prod (ContinuousAddMonoidHom.id A)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The function field `R(W) := Frac(R[W])` of a Weierstrass curve `W`.  -/
WeierstrassCurve.Affine.FunctionField : {R : Type r} → [CommRing R] → WeierstrassCurve.Affine R → Type r
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsIsoMapTruncLTTruncGEAppTruncLTι : ∀ {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) [CategoryTheory.IsTriangulated C] (a b : ℤ) (X : C),
  CategoryTheory.IsIso ((t.truncLT b).map ((t.truncGE a).map ((t.truncLTι b).app X)))
-- Lean.Compiler.IR.Basic
Lean.IR.instBEqJoinPointId : BEq Lean.IR.JoinPointId