mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- Auxiliary lemma to express bilinearity of `QuadraticMap.polar` without subtraction.  -/
QuadraticMap.polar_add_left_iff : ∀ {M : Type u_4} {N : Type u_5} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {f : M → N} {x x' y : M},
  QuadraticMap.polar f (x + x') y = QuadraticMap.polar f x y + QuadraticMap.polar f x' y ↔
    f (x + x' + y) + (f x + f x' + f y) = f (x + x') + f (x' + y) + f (y + x)
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.findKeyDAux : {α : Type u_1} → {β : Type u_2} → [BEq α] → Lean.PersistentHashMap.Node α β → USize → α → α → α
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.coe_mk : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] (f : A → B) (h₁ : f 1 = 1)
  (h₂ :
    ∀ (x y : A),
      { toFun := f, map_one' := h₁ }.toFun (x * y) =
        { toFun := f, map_one' := h₁ }.toFun x * { toFun := f, map_one' := h₁ }.toFun y)
  (h₃ : (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0)
  (h₄ :
    ∀ (x y : A),
      (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun (x + y) =
        (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun x +
          (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun y)
  (h₅ :
    ∀ (r : R),
      (↑↑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ }).toFun ((algebraMap R A) r) =
        (algebraMap R B) r)
  (h₆ :
    ∀ (x : A),
      (↑↑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄,
                    commutes' := h₅ }.toRingHom).toFun
          (star x) =
        star
          ((↑↑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄,
                      commutes' := h₅ }.toRingHom).toFun
            x)),
  ⇑{ toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅, map_star' := h₆ } = f
-- Mathlib.Topology.NhdsWithin
Filter.EventuallyEq.mem_interior : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {s t : Set α}, s =ᶠ[nhds x] t → x ∈ interior s → x ∈ interior t
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateBoxImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.LetValue pu → Lean.Expr → Lean.FVarId → Lean.Compiler.LCNF.LetValue pu
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_mapM_mapM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Monad m]
  [LawfulMonad m] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [inst_7 : MonadAttach o] [LawfulMonad o] [WeaklyLawfulMonadAttach o] [inst_10 : MonadLiftT m n]
  [inst_11 : MonadLiftT n o] [LawfulMonadLiftT m n] [LawfulMonadLiftT n o] [inst : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → n γ} {g : γ → o δ} {it : Std.IterM m β},
  (Std.IterM.mapM g (Std.IterM.mapM f it)).toList =
    (Std.IterM.mapM
        (fun b => do
          let __do_lift ← liftM (f b)
          g __do_lift)
        it).toList
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.sat_of_insertRat : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ratUnits = #[] ∧ f.AssignmentsInvariant →
    ∀ (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool),
      Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p f →
        (f.insertRatUnits c.negate).2 = true → Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
/-- A function is `C^(n + 1)` on a domain with unique derivatives if and only if it is
differentiable there, and its derivative (formulated with `derivWithin`) is `C^n`.  -/
contDiffOn_succ_iff_derivWithin : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : 𝕜 → F} {s : Set 𝕜},
  UniqueDiffOn 𝕜 s →
    (ContDiffOn 𝕜 (n + 1) f s ↔
      DifferentiableOn 𝕜 f s ∧ (n = ⊤ → AnalyticOn 𝕜 f s) ∧ ContDiffOn 𝕜 n (derivWithin f s) s)
-- Mathlib.LinearAlgebra.InvariantBasisNumber
card_le_of_surjective : ∀ (R : Type u) [inst : Semiring R] [RankCondition R] {α : Type u_1} {β : Type u_2} [inst_2 : Fintype α]
  [inst_3 : Fintype β] (f : (α → R) →ₗ[R] β → R), Function.Surjective ⇑f → Fintype.card β ≤ Fintype.card α
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.yonedaMap.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v₁, u_1} D] (F : CategoryTheory.Functor C D) (X : C),
  CategoryTheory.yonedaMap F X = { app := fun x => TypeCat.ofHom fun f => F.map f, naturality := ⋯ }
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.map_specializes : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : C(α, β)) {x y : α},
  x ⤳ y → f x ⤳ f y
-- Mathlib.Algebra.CharP.Algebra
/-- If the algebra map `R →+* A` is injective then `A` has the same characteristic as `R`.  -/
charP_of_injective_algebraMap : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  Function.Injective ⇑(algebraMap R A) → ∀ (p : ℕ) [CharP R p], CharP A p
-- Mathlib.Data.Num.Bitwise
PosNum.lxor_eq_xor : ∀ (p q : PosNum), p.lxor q = p ^^^ q
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.isPlot_iInf_iff : ∀ {X : Type u_1} {ι : Type u_2} {D : ι → DiffeologicalSpace X} {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X},
  Diffeology.IsPlot p ↔ ∀ (i : ι), Diffeology.IsPlot p
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.delabPSigma : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- `zeta n A B` is a primitive `n`-th root of unity.  -/
IsCyclotomicExtension.zeta_spec : ∀ (n : ℕ) [inst : NeZero n] (A : Type w) (B : Type z) [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : Algebra A B]
  [inst_4 : IsCyclotomicExtension {n} A B], IsPrimitiveRoot (IsCyclotomicExtension.zeta n A B) n
-- Mathlib.AlgebraicGeometry.Birational.Dominant
/-- Restricting a dominant partial map to a dense open yields a dominant partial map.  -/
AlgebraicGeometry.Scheme.PartialMap.isDominant_restrict_hom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y) [AlgebraicGeometry.IsDominant f.hom] (U : X.Opens)
  (hU : Dense ↑U) (hU' : U ≤ f.domain), AlgebraicGeometry.IsDominant (f.restrict U hU hU').hom
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_eq_X_mul_U_add_T : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.U R (n + 1) = Polynomial.X * Polynomial.Chebyshev.U R n + Polynomial.Chebyshev.T R (n + 1)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piConst_obj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] (X : C)
  {X_1 Y : Type wᵒᵖ} (f : X_1 ⟶ Y),
  (CategoryTheory.Limits.piConst.obj X).map f =
    CategoryTheory.Limits.Pi.map' ⇑(CategoryTheory.ConcreteCategory.hom f.unop) fun x =>
      CategoryTheory.CategoryStruct.id X
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.append.match_1.eq_6 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α)
  (b l : RBTree.RBNode α) (v : α) (r : 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)),
  (match RBTree.RBNode.node RBTree.RBColor.red a x b, RBTree.RBNode.node RBTree.RBColor.black l v r 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_6 a x b (RBTree.RBNode.node RBTree.RBColor.black l v r) l v r ⋯
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.pderiv_one_equivMvPolynomial : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial (Polynomial R)),
  (MvPolynomial.pderiv 1) ((Polynomial.Bivariate.equivMvPolynomial R) p) =
    (Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.derivative p)
-- Mathlib.Algebra.Homology.CochainComplexOpposite
ComplexShape.instIsRelIffIntEmbeddingUpIntDownInt : ComplexShape.embeddingUpIntDownInt.IsRelIff
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.resCoindHomEquiv.eq_1 : ∀ {k : Type u} {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  (B : Rep.{max w t, u, w} k H) (A : Rep.{max w t, u, v} k G),
  Rep.resCoindHomEquiv.{t, u, v, w} φ B A =
    { toFun := fun f => Rep.resCoindToHom φ B A f, map_add' := ⋯, map_smul' := ⋯,
      invFun := fun f =>
        Rep.ofHom
          { toLinearMap := LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Rep.Hom.hom f).toLinearMap,
            isIntertwining' := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
/-- The naturality of `HomotopyCategory.BinaryProduct.inverse`
with respect to the second variable.  -/
SSet.Truncated.HomotopyCategory.BinaryProduct.idProdMapHomotopyCategoryCompInverseIso : (X : SSet.Truncated 2) →
  {Y Y' : SSet.Truncated 2} →
    (g : Y ⟶ Y') →
      ((CategoryTheory.Functor.id X.HomotopyCategory).prod (SSet.Truncated.mapHomotopyCategory g)).comp
          (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y') ≅
        (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).comp
          (SSet.Truncated.mapHomotopyCategory (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g))
-- Mathlib.MeasureTheory.Group.Arithmetic
Finset.measurable_prod : ∀ {M : Type u_2} {ι : Type u_3} {α : Type u_4} [inst : CommMonoid M] [inst_1 : MeasurableSpace M] [MeasurableMul₂ M]
  {m : MeasurableSpace α} {f : ι → α → M} (s : Finset ι),
  (∀ i ∈ s, Measurable (f i)) → Measurable fun a => ∏ i ∈ s, f i a
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.IsCollisionNode : {α : Type u_1} → {β : Type u_2} → Lean.PersistentHashMap.Node α β → Prop
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.mk.inj : ∀ {X : Type u_5} {inst : TopologicalSpace X} {toSetoid : Setoid X}
  {isOpen_setOfPred_rel : ∀ (x : X), IsOpen (Set.ofPred (toSetoid x))} {toSetoid_1 : Setoid X}
  {isOpen_setOfPred_rel_1 : ∀ (x : X), IsOpen (Set.ofPred (toSetoid_1 x))},
  { toSetoid := toSetoid, isOpen_setOfPred_rel := isOpen_setOfPred_rel } =
      { toSetoid := toSetoid_1, isOpen_setOfPred_rel := isOpen_setOfPred_rel_1 } →
    toSetoid = toSetoid_1
-- Mathlib.LinearAlgebra.AffineSpace.Slope
slope_neg : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E] (f : k → E) (x y : k),
  slope (fun t => -f t) x y = -slope f x y
-- Init.Data.List.Lemmas
List.foldl_eq_foldr_reverse : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : β → α → β} {b : β},
  List.foldl f b l = List.foldr (fun x y => f y x) b l.reverse
-- Mathlib.Analysis.Convex.Uniform
UniformConvexSpace.uniform_convex : ∀ {E : Type u_1} {inst : SeminormedAddCommGroup E} [self : UniformConvexSpace E] ⦃ε : ℝ⦄,
  0 < ε → ∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.fintypeMultiples.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} [inst_1 : Fintype M],
  AddSubmonoid.fintypeMultiples =
    {
      elems :=
        { val := Multiset.pmap Subtype.mk (Finset.filter (Membership.mem (AddSubmonoid.multiples a)) Finset.univ).val ⋯,
          nodup := ⋯ },
      complete := ⋯ }
-- Mathlib.Probability.Distributions.Uniform
PMF.uniformOfFinset_apply_of_mem : ∀ {α : Type u_1} {s : Finset α} (hs : s.Nonempty) {a : α}, a ∈ s → (PMF.uniformOfFinset s hs) a = (↑s.card)⁻¹
-- Lean.Environment
Lean.instBEqAsyncBranch : BEq Lean.AsyncBranch
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.isSeparated_packingRadius : ∀ {X : Type u_3} [inst : MetricSpace X] (self : Delone.DeloneSet X),
  Metric.IsSeparated (↑self.packingRadius) self.carrier
-- Mathlib.FieldTheory.Normal.Closure
IntermediateField.normalClosureOperator_isClosed : ∀ (F : Type u_1) (L : Type u_3) [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L] [inst_3 : Normal F L]
  (x : IntermediateField F L),
  (IntermediateField.normalClosureOperator F L).IsClosed x = ((fun K => IntermediateField.normalClosure F (↥K) L) x = x)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SyntheticMVarKind.postponed.injEq : ∀ (ctx ctx_1 : Lean.Elab.Term.SavedContext),
  (Lean.Elab.Term.SyntheticMVarKind.postponed ctx = Lean.Elab.Term.SyntheticMVarKind.postponed ctx_1) = (ctx = ctx_1)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivAt.fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} [ContinuousAdd E] [ContinuousSMul 𝕜 E]
  [ContinuousAdd F] [ContinuousSMul 𝕜 F] [T2Space F], HasFDerivAt f f' x → fderiv 𝕜 f x = f'
-- Mathlib.Order.MinMax
min_lt_of_left_lt : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, b < a → min b c < a
-- Mathlib.Algebra.AffineMonoid.Basic
/-- An affine monoid is a finitely generated cancellative torsion-free commutative monoid.  -/
IsAffineMonoid : (M : Type u_1) → [CommMonoid M] → Prop
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.insertMany_list_singleton : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} {k : α} {v : β},
  Std.DTreeMap.Const.insertMany t [(k, v)] = t.insert k v
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.comap_sup_eq_of_le_range : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) {H K : AddSubgroup N},
  H ≤ f.range → K ≤ f.range → AddSubgroup.comap f H ⊔ AddSubgroup.comap f K = AddSubgroup.comap f (H ⊔ K)
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.combine'.match_3.splitter : (motive : ℕ → Sort u_1) → (fuel : ℕ) → (Unit → motive 0) → ((fuel : ℕ) → motive fuel.succ) → motive fuel
-- Mathlib.CategoryTheory.MorphismProperty.Concrete
/-- In the category of types, any map can be functorially factored as a surjective
map followed by an injective map.  -/
CategoryTheory.functorialSurjectiveInjectiveFactorizationData : CategoryTheory.ConcreteCategory.FunctorialSurjectiveInjectiveFactorizationData (Type u)
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.mul_le_mul_right : ∀ {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R}, N ≤ P → M * N ≤ M * P
-- Lean.Elab.Tactic.Induction
/-- Construct the an eliminator/recursor application. `targets` contains the explicit and implicit
targets for the eliminator, not yet generalized.
For example, the indices of builtin recursors are considered implicit targets.
Remark: the method `addImplicitTargets` may be used to compute the sequence of implicit and
explicit targets from the explicit ones.
 -/
Lean.Elab.Tactic.ElimApp.mkElimApp : Lean.Meta.ElimInfo → Array Lean.Expr → Lean.Name → Lean.Elab.TermElabM Lean.Elab.Tactic.ElimApp.Result
-- Mathlib.CategoryTheory.CommSq
/-- The square commutes.  -/
CategoryTheory.CommSq.w : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z},
  CategoryTheory.CommSq f g h i → CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g i
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.op_sSup : ∀ {G : Type u_2} [inst : AddGroup G] (S : Set (AddSubgroup G)), (sSup S).op = sSup (AddSubgroup.unop ⁻¹' S)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.coe_map : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S) (s : Subsemiring R),
  ↑(Subsemiring.map f s) = ⇑f '' ↑s
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The image of a `0`-hypercover under a functor.  -/
CategoryTheory.Precoverage.ZeroHypercover.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      {S : C} →
        {D : Type u_1} →
          [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
            {K : CategoryTheory.Precoverage D} →
              (F : CategoryTheory.Functor C D) →
                J.ZeroHypercover S → J ≤ CategoryTheory.Precoverage.comap F K → K.ZeroHypercover (F.obj S)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRank_loopyOn : ∀ {α : Type u_1} (X : Set α), (Matroid.loopyOn X).eRank = 0
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.OmissionReason.string : String → Lean.PrettyPrinter.Delaborator.OmissionReason
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.denote_insert : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α) (k : ℤ)
  (v : Lean.Grind.Linarith.Var) (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.Poly.denote ctx (Lean.Grind.Linarith.Poly.insert k v p) =
    Lean.Grind.Linarith.Poly.denote ctx p + k • Lean.Grind.Linarith.Var.denote ctx v
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β},
  k ∉ t → (f (Std.ExtDTreeMap.Const.get? t k)).isNone = true → (Std.ExtDTreeMap.Const.alter t k f).size = t.size
-- Mathlib.GroupTheory.Nilpotent
/-- If `N` is a normal additive subgroup of `G`, then the set
`{x : G | ∀ y : G, x + y -x - y ∈ N}` is an additive subgroup of `G`
(because it is the preimage in `G` of the centre of the additive quotient group `G/N`.)  -/
AddSubgroup.upperCentralSeriesStep : {G : Type u_1} → [inst : AddGroup G] → (N : AddSubgroup G) → [N.Normal] → AddSubgroup G
-- Init.Data.String.Basic
/-- Given a slice and two valid positions within the slice, obtain a new slice on the same underlying
string formed by the new bounds, or `none` if the given end is strictly less than the given start.  -/
String.Slice.slice? : (s : String.Slice) → s.Pos → s.Pos → Option String.Slice
-- Mathlib.Algebra.Order.Group.Int.Sum
/-- Sharp upper bound for the sum of a finset of integers that is bounded above, `range` version.  -/
Finset.sum_le_sum_range : ∀ {s : Finset ℤ} {c : ℤ}, (∀ x ∈ s, x ≤ c) → ∑ x ∈ s, x ≤ ∑ n ∈ Finset.range s.card, (c - ↑n)
-- Mathlib.Analysis.Analytic.Binomial
Complex.ofReal_choose : ∀ (a : ℝ) (n : ℕ), ↑(Ring.choose a n) = Ring.choose (↑a) n
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the forward direction of `lipschitzOnWith_iff_norm_inv_mul_le`. -/
LipschitzOnWith.norm_inv_mul_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F] {s : Set E} {f : E → F}
  {C : NNReal}, LipschitzOnWith C f s → ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖(f x)⁻¹ * f y‖ ≤ ↑C * ‖x⁻¹ * y‖
-- Mathlib.Analysis.Calculus.FDeriv.Comp
fderivWithin_comp_of_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} (x : E) {s : Set E} {g : F → G} {t : Set F}
  {y : F},
  DifferentiableWithinAt 𝕜 g t y →
    DifferentiableWithinAt 𝕜 f s x →
      Set.MapsTo f s t →
        UniqueDiffWithinAt 𝕜 s x →
          f x = y → fderivWithin 𝕜 (g ∘ f) s x = fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x
-- Lean.Meta.LitValues
/-- Return `some n` if `e` is an `OfNat.ofNat`-application encoding the `UInt32` with value `n`.  -/
Lean.Meta.getUInt32Value? : Lean.Expr → Lean.MetaM (Option UInt32)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
/-- The polynomial `W(X, Y, Z) := Y² + a₁XYZ + a₃YZ³ - (X³ + a₂X²Z² + a₄XZ⁴ + a₆Z⁶)` associated to a
Weierstrass curve `W` over a ring `R` in Jacobian coordinates.

This is represented as a term of type `MvPolynomial (Fin 3) R`, where `X`, `Y`, and `Z`
represent `X`, `Y`, and `Z` respectively.  -/
WeierstrassCurve.Jacobian.polynomial : {R : Type r} → [inst : CommRing R] → WeierstrassCurve.Jacobian R → MvPolynomial (Fin 3) R
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.GoodProducts.smaller_factorization : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (o : Ordinal.{u}),
  (fun p => ↑p) ∘ (Profinite.NobelingProof.GoodProducts.range_equiv_smaller C o).toFun =
    ⇑(Profinite.NobelingProof.πs C o) ∘ fun p => ↑p
-- Mathlib.RingTheory.MvPowerSeries.Basic
/-- Multivariate formal power series, where `σ` is the index set of the variables
and `R` is the coefficient ring.  -/
MvPowerSeries : Type u_1 → Type u_2 → Type (max (max u_2 0) u_1)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.subset_vadd_set_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {A B : Set β} {a : α},
  A ⊆ a +ᵥ B ↔ -a +ᵥ A ⊆ B
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.surjectiveOnStalks_residueField : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [inst_1 : I.IsPrime],
  (algebraMap R I.ResidueField).SurjectiveOnStalks
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.descCycles.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) {A : C} {n : ℤ}
  (x x_1 : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg) ⟶ A) (e_x : x = x_1)
  (hx : CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)) x = 0),
  X.descCycles f g fg h x hx = X.descCycles f g fg h x_1 ⋯
-- Batteries.Data.AssocList
List.toAssocList.eq_1 : ∀ {α : Type u_1} {β : Type u_2}, [].toAssocList = Batteries.AssocList.nil
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.copy_eq : ∀ {M : Type u_4} {N : Type u_5} {x : MulOne M} {x_1 : MulOne N} (f : M →* N) (f' : M → N) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Algebra.Group.Units.Basic
mul_eq_one : ∀ {α : Type u} [inst : CommMonoid α] [Subsingleton αˣ] {a b : α}, a * b = 1 ↔ a = 1 ∧ b = 1