mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Tree.Data
/-- Get a `DeclNameGenerator` for auxiliary declarations that can be used by
children of this rapp. Successive calls to this function return
`DeclNameGenerators` that are guaranteed to generate distinct names.  -/
Aesop.RappRef.getChildAuxDeclNameGenerator : Aesop.RappRef → BaseIO Lean.DeclNameGenerator
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- If one affine subspace is less than or equal to another, the same applies to their
directions.  -/
AffineSubspace.direction_le : ∀ {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] {s₁ s₂ : AffineSubspace k P}, s₁ ≤ s₂ → s₁.direction ≤ s₂.direction
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.pow_subset_pow : ∀ {α : Type u_2} [inst : Monoid α] {s t : Set α} {m n : ℕ}, s ⊆ t → 1 ∈ t → m ≤ n → s ^ m ⊆ t ^ n
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
AlgebraicGeometry.Scheme.Hom.singleton_mem_fpqcPrecoverage : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Flat f] [AlgebraicGeometry.Surjective f]
  [AlgebraicGeometry.QuasiCompact f],
  CategoryTheory.Presieve.singleton f ∈ AlgebraicGeometry.Scheme.fpqcPrecoverage.coverings Y
-- Mathlib.Topology.Algebra.Order.LiminfLimsup
le_liminf_mul : ∀ {ι : Type u_1} {f : Filter ι} {u v : ι → ℝ} [f.NeBot],
  0 ≤ᶠ[f] u →
    Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u →
      0 ≤ᶠ[f] v →
        Filter.IsCoboundedUnder (fun x1 x2 => x1 ≥ x2) f v →
          Filter.liminf u f * Filter.liminf v f ≤ Filter.liminf (u * v) f
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_neg : ∀ {a : ISize} (h : System.Platform.numBits = 32), (-a).toBitVec32 h = -a.toBitVec32 h
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.addCommSemigroup : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [AddCommSemigroup α] → AddCommSemigroup (Matrix m n α)
-- Lean.SubExpr
Lean.SubExpr.mkRoot : Lean.Expr → Lean.SubExpr
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_bot : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] {a : α}, Set.Ico ⊥ a = Set.Iio a
-- Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
/-- A colimit cokernel cofork for the map
`∐ fun (_ : α) ↦ R ⟶ ∐ fun (_ : β) ↦ R` induced by a map `f : α → β`.  -/
CategoryTheory.Limits.sigmaConstCokernelCofork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (R : C) →
        {α : Type u_1} →
          {β : Type u_2} →
            (f : α → β) →
              [inst_2 : CategoryTheory.Limits.HasCoproduct fun x => R] →
                [inst_3 : CategoryTheory.Limits.HasCoproduct fun x => R] →
                  [CategoryTheory.Limits.HasCoproduct fun x => R] →
                    CategoryTheory.Limits.CokernelCofork
                      (CategoryTheory.Limits.Sigma.map' f fun x => CategoryTheory.CategoryStruct.id R)
-- Init.Data.UInt.Lemmas
USize.sub_eq_iff_eq_add : ∀ {a b c : USize}, a - b = c ↔ a = c + b
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.norm_integral_sub_setIntegral_le : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {μ : MeasureTheory.Measure X} [MeasureTheory.IsFiniteMeasure μ] {C : ℝ},
  (∀ᵐ (x : X) ∂μ, ‖f x‖ ≤ C) →
    ∀ {s : Set X},
      MeasurableSet s → MeasureTheory.Integrable f μ → ‖∫ (x : X), f x ∂μ - ∫ (x : X) in s, f x ∂μ‖ ≤ μ.real sᶜ * C
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
DerivedCategory.triangleOfSES_obj₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (hS : S.ShortExact),
  (DerivedCategory.triangleOfSES hS).obj₂ = DerivedCategory.Q.obj S.X₂
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalCStarAlgebra.toNonUnitalNormedRing : {A : Type u_1} → [self : NonUnitalCStarAlgebra A] → NonUnitalNormedRing A
-- Mathlib.Analysis.InnerProductSpace.Symmetric
/-- **Alias** of the reverse direction of `LinearMap.IsSymmetricProjection.ext_iff`.

---

Symmetric projections are equal iff their range are.  -/
LinearMap.IsSymmetricProjection.ext : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {S T : E →ₗ[𝕜] E}, S.IsSymmetricProjection → T.IsSymmetricProjection → S.range = T.range → S = T
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.integral_sub_average : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : α → E),
  ∫ (x : α), f x - ⨍ (a : α), f a ∂μ ∂μ = 0
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- `AddGroupExtension`s are equivalent iff there is an isomorphism making a commuting diagram.
Use `AddGroupExtension.Equiv.ofMonoidHom` in `Mathlib/GroupTheory/GroupExtension/Basic.lean` to
construct an equivalence without providing the inverse map.  -/
AddGroupExtension.Equiv : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] →
        [inst_1 : AddGroup E] →
          [inst_2 : AddGroup G] →
            AddGroupExtension N E G →
              {E' : Type u_4} → [inst_3 : AddGroup E'] → AddGroupExtension N E' G → Type (max u_2 u_4)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.insertMany_empty_list_cons : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {k : α} {v : β k} {tl : List ((a : α) × β a)},
  ↑(Std.DTreeMap.Internal.Impl.empty.insertMany (⟨k, v⟩ :: tl) ⋯) =
    ↑((Std.DTreeMap.Internal.Impl.insert k v Std.DTreeMap.Internal.Impl.empty ⋯).impl.insertMany tl ⋯)
-- Init.WF
Prod.lex_def : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} {s : β → β → Prop} {p q : α × β},
  Prod.Lex r s p q ↔ r p.1 q.1 ∨ p.1 = q.1 ∧ s p.2 q.2
-- Mathlib.Order.Preorder.Finite
Finset.exists_minimal : ∀ {α : Type u_2} [inst : LE α] [IsTrans α fun a a_1 => a_1 ≤ a] {s : Finset α},
  s.Nonempty → ∃ i, Minimal (fun x => x ∈ s) i
-- Mathlib.CategoryTheory.Triangulated.Adjunction
CategoryTheory.Adjunction.IsTriangulated.mk : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.Limits.HasZeroObject D] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : CategoryTheory.Preadditive D] [inst_6 : CategoryTheory.HasShift C ℤ] [inst_7 : CategoryTheory.HasShift D ℤ]
  [inst_8 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_10 : CategoryTheory.Pretriangulated C]
  [inst_11 : CategoryTheory.Pretriangulated D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {adj : F ⊣ G} [inst_12 : F.CommShift ℤ] [inst_13 : G.CommShift ℤ],
  autoParam (adj.CommShift ℤ) CategoryTheory.Adjunction.IsTriangulated.commShift._autoParam →
    autoParam F.IsTriangulated CategoryTheory.Adjunction.IsTriangulated.leftAdjoint_isTriangulated._autoParam →
      autoParam G.IsTriangulated CategoryTheory.Adjunction.IsTriangulated.rightAdjoint_isTriangulated._autoParam →
        adj.IsTriangulated
-- Mathlib.Condensed.Discrete.LocallyConstant
/-- `CompHausLike.LocallyConstant.functorToPresheaves` lands in sheaves.  -/
CompHausLike.LocallyConstant.functor : (P : TopCat → Prop) →
  [inst : CompHausLike.HasExplicitFiniteCoproducts P] →
    [inst_1 : CompHausLike.HasExplicitPullbacks P] →
      (hs :
          ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
            CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)) →
        CategoryTheory.Functor (Type (max u w))
          (CategoryTheory.Sheaf (CategoryTheory.coherentTopology (CompHausLike P)) (Type (max u w)))
-- Mathlib.Algebra.Lie.OfAssociative
LinearEquiv.lieConj_apply : ∀ {R : Type u} {M₁ : Type v} {M₂ : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂] (e : M₁ ≃ₗ[R] M₂) (f : Module.End R M₁), e.lieConj f = e.conj f
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.instInhabited : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [Inhabited C] → (U : CategoryTheory.Comonad C) → Inhabited (CategoryTheory.Cokleisli U)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- The second period in a `PeriodPair`.  -/
PeriodPair.ω₂ : PeriodPair → ℂ
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_neg_ofNat : ∀ (x : ℝ) (n : ℕ) [inst : n.AtLeastTwo], x ^ (-OfNat.ofNat n) = x ^ (-OfNat.ofNat n)
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
LinearMap.BilinForm.IsometryEquiv.instEquivLike : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₁] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                {B₁ : LinearMap.BilinForm R M₁} →
                  {B₂ : LinearMap.BilinForm R M₂} → EquivLike (B₁.IsometryEquiv B₂) M₁ M₂
-- Mathlib.Data.Finset.Interval
/-- Cardinality of an `Iic` of finsets.  -/
Finset.card_Iic_finset : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α}, (Finset.Iic s).card = 2 ^ s.card
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.of_add_left : ∀ {α : Type u_2} [inst : Add α] {s t : Set α}, (s + t).Nonempty → s.Nonempty
-- Mathlib.CategoryTheory.Countable
CategoryTheory.instCountableCategoryOfFinCategory : ∀ (α : Type u_1) [inst : CategoryTheory.SmallCategory α] [CategoryTheory.FinCategory α],
  CategoryTheory.CountableCategory α
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.GrothendieckTopology C}
  {fiber : CategoryTheory.Functor C (Type w)}
  {isCofiltered :
    autoParam (CategoryTheory.IsCofiltered fiber.Elements)
      CategoryTheory.GrothendieckTopology.Point.isCofiltered._autoParam}
  {initiallySmall :
    autoParam (CategoryTheory.InitiallySmall fiber.Elements)
      CategoryTheory.GrothendieckTopology.Point.initiallySmall._autoParam}
  {jointly_surjective :
    ∀ {X : C},
      ∀ R ∈ J X,
        ∀ (x : fiber.obj X), ∃ Y f, ∃ (_ : R.arrows f), ∃ y, (CategoryTheory.ConcreteCategory.hom (fiber.map f)) y = x}
  {fiber_1 : CategoryTheory.Functor C (Type w)}
  {isCofiltered_1 :
    autoParam (CategoryTheory.IsCofiltered fiber_1.Elements)
      CategoryTheory.GrothendieckTopology.Point.isCofiltered._autoParam}
  {initiallySmall_1 :
    autoParam (CategoryTheory.InitiallySmall fiber_1.Elements)
      CategoryTheory.GrothendieckTopology.Point.initiallySmall._autoParam}
  {jointly_surjective_1 :
    ∀ {X : C},
      ∀ R ∈ J X,
        ∀ (x : fiber_1.obj X),
          ∃ Y f, ∃ (_ : R.arrows f), ∃ y, (CategoryTheory.ConcreteCategory.hom (fiber_1.map f)) y = x},
  { fiber := fiber, isCofiltered := isCofiltered, initiallySmall := initiallySmall,
        jointly_surjective := jointly_surjective } =
      { fiber := fiber_1, isCofiltered := isCofiltered_1, initiallySmall := initiallySmall_1,
        jointly_surjective := jointly_surjective_1 } →
    fiber = fiber_1
-- Mathlib.LinearAlgebra.RootSystem.Basic
RootPairing.equiv_of_mapsTo_symm_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (p : M →ₗ[R] N →ₗ[R] R) (root : ι ↪ M)
  (coroot : ι ↪ N) (i : ι)
  (h : ∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root))
  (hp : ∀ (i : ι), (p (root i)) (coroot i) = 2) (j : ι),
  (RootPairing.equiv_of_mapsTo p root coroot i h hp).symm j = ⋯.choose
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.mul_inv_cancel : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {p : RatFunc K}, p ≠ 0 → p * p⁻¹ = 1
-- Mathlib.Analysis.SpecialFunctions.Exp
Complex.exp_sub_sum_range_succ_isLittleO_pow : ∀ (n : ℕ), (fun x => Complex.exp x - ∑ i ∈ Finset.range (n + 1), x ^ i / ↑i.factorial) =o[nhds 0] fun x => x ^ n
-- Mathlib.Tactic.Ring.Common
/-- A sum `a + b` is a polynomial if `a` is a monomial and `b` is another polynomial.  -/
Mathlib.Tactic.Ring.Common.ExSum.add : {u : Lean.Level} →
  {α : Q(Type u)} →
    {BaseType : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        {a b : Q(«$α»)} →
          Mathlib.Tactic.Ring.Common.ExProd BaseType sα a →
            Mathlib.Tactic.Ring.Common.ExSum BaseType sα b → Mathlib.Tactic.Ring.Common.ExSum BaseType sα q(«$a» + «$b»)
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso_inv_τ₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  {T T' : CategoryTheory.Pretriangulated.Triangle C} (e : T ≅ T')
  (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  (CategoryTheory.Pretriangulated.shortComplexOfDistTriangleIsoOfIso e hT).inv.τ₁ = e.inv.hom₁
-- Mathlib.Order.KrullDimension
Order.height_orderIso : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) (x : α),
  Order.height (f x) = Order.height x
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.coe_tsum : ∀ {α : Type u_1} {f : α → NNReal}, Summable f → ↑(tsum f) = ∑' (a : α), ↑(f a)
-- Lean.Parser.Command
Lean.Parser.Command.exit : Lean.Parser.Parser
-- Lean.Meta.Tactic.Grind.Core
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.addEqStep.go : Lean.Expr →
  Bool →
    Lean.Expr →
      Lean.Expr →
        Lean.Meta.Grind.ENode →
          Lean.Meta.Grind.ENode → Lean.Meta.Grind.ENode → Lean.Meta.Grind.ENode → Bool → Lean.Meta.Grind.GoalM Unit
-- Mathlib.GroupTheory.SchurZassenhaus
Subgroup.eq_one_of_smul_eq_one : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} [inst_1 : IsMulCommutative ↥H] [inst_2 : H.FiniteIndex]
  [inst_3 : H.Normal], (Nat.card ↥H).Coprime H.index → ∀ (α : H.QuotientDiff) (h : ↥H), h • α = α → h = 1
-- Mathlib.Order.Interval.Finset.Basic
Finset.sup'_Iic : ∀ {α : Type u_2} [inst : SemilatticeSup α] [inst_1 : LocallyFiniteOrderBot α] (a : α), (Finset.Iic a).sup' ⋯ id = a
-- Lean.Parser.Do
/-- *experimental*

`idbg e` enables live inspection of program state from the editor. When placed in a `do` block,
it captures all local variables in scope and the expression `e`, then:

- **In the language server**: starts a TCP server on localhost waiting for the running program to
  connect; the editor will mark this part of the program as "in progress" during this wait but that
  will not block `lake build` of the project.
- **In the compiled program**: on first execution of the `idbg` call site, connects to the server,
  receives the expression, compiles and evaluates it using the program's actual runtime values, and
  sends the `repr` result back.

The result is displayed as an info diagnostic on the `idbg` keyword. The expression `e` can be
edited while the program is running - each edit triggers re-elaboration of `e`, a new TCP exchange,
and an updated result. This makes `idbg` a live REPL for inspecting and experimenting with
program state at a specific point in execution. Only when `idbg` is inserted, moved, or removed does
the program need to be recompiled and restarted.

# Known Limitations

* The program will poll the server for up to 10 minutes and needs to be killed manually
  otherwise.
* Use of multiple `idbg` at once untested, likely too much overhead from overlapping imports without
  further changes.
* `LEAN_PATH` must be properly set up so the compiled program can import its origin module.
* Untested on Windows and macOS.
 -/
Lean.Parser.Term.doIdbg : Lean.Parser.Parser
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.id.match_1.eq_1 : ∀ {C : Type u_1} (motive : CategoryTheory.WithInitial C → Sort u_2) (a : C)
  (h_1 : (a : C) → motive (CategoryTheory.WithInitial.of a)) (h_2 : Unit → motive CategoryTheory.WithInitial.star),
  (match CategoryTheory.WithInitial.of a with
    | CategoryTheory.WithInitial.of a => h_1 a
    | CategoryTheory.WithInitial.star => h_2 ()) =
    h_1 a
-- Init.Data.Array.Lemmas
Array.map_pop : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α}, Array.map f xs.pop = (Array.map f xs).pop
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The inverse in a group object  -/
CategoryTheory.GrpObj.inv : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {inst_1 : CategoryTheory.CartesianMonoidalCategory C} → {X : C} → [self : CategoryTheory.GrpObj X] → X ⟶ X
-- Mathlib.RingTheory.WittVector.Compare
WittVector.zmodEquivTrunc_compat : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂),
  (TruncatedWittVector.truncate hk).comp
      ((TruncatedWittVector.zmodEquivTrunc p k₂).toRingHom.comp (PadicInt.toZModPow k₂)) =
    (TruncatedWittVector.zmodEquivTrunc p k₁).toRingHom.comp (PadicInt.toZModPow k₁)
-- Init.Data.List.Scan.Lemmas
List.getElem_scanl_zero : ∀ {β : Type u_1} {α : Type u_2} {b : β} {l : List α} {f : β → α → β}, (List.scanl f b l)[0] = b
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.ae_measure_preimage_add_right_lt_top : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd₂ G] {s : Set G} [MeasurableNeg G]
  (μ' ν' : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ'] [MeasureTheory.SigmaFinite ν']
  [μ'.IsAddLeftInvariant] [ν'.IsAddLeftInvariant], μ' s ≠ ⊤ → ∀ᵐ (x : G) ∂μ', ν' ((fun x_1 => x_1 + x) ⁻¹' s) < ⊤
-- Mathlib.Algebra.Pointwise.Stabilizer
MulAction.mem_stabilizer_finset : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] {a : G} [inst_2 : DecidableEq α]
  {s : Finset α}, a ∈ MulAction.stabilizer G s ↔ ∀ (b : α), a • b ∈ s ↔ b ∈ s
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.getD : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Std.LawfulEqCmp cmp] → Std.DTreeMap α β cmp → (a : α) → β a → β a
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.InjectiveSeminorm
PiTensorProduct.toDualContinuousMultilinearMap.eq_1 : ∀ {ι : Type uι} [inst : Fintype ι] {𝕜 : Type u𝕜} [inst_1 : NontriviallyNormedField 𝕜] {E : ι → Type uE}
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (F : Type u_1)
  [inst_4 : SeminormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F],
  PiTensorProduct.toDualContinuousMultilinearMap F =
    {
      toFun := fun x =>
        ((↑PiTensorProduct.lift).flip x ∘ₗ ContinuousMultilinearMap.toMultilinearMapLinear).mkContinuous ‖x‖ ⋯,
      map_add' := ⋯, map_smul' := ⋯ }
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.ConsumerNode.mk.inj : ∀ {mvar key : Lean.Expr} {mctx : Lean.MetavarContext} {subgoals : List Lean.Expr} {size : ℕ} {mvar_1 key_1 : Lean.Expr}
  {mctx_1 : Lean.MetavarContext} {subgoals_1 : List Lean.Expr} {size_1 : ℕ},
  { mvar := mvar, key := key, mctx := mctx, subgoals := subgoals, size := size } =
      { mvar := mvar_1, key := key_1, mctx := mctx_1, subgoals := subgoals_1, size := size_1 } →
    mvar = mvar_1 ∧ key = key_1 ∧ mctx = mctx_1 ∧ subgoals = subgoals_1 ∧ size = size_1
-- Init.Data.Nat.Dvd
Nat.mul_dvd_mul : ∀ {a b c d : ℕ}, a ∣ b → c ∣ d → a * c ∣ b * d
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap.0.Std.IterM.step_flatMapAfterM.match_1.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] {it₁ : Std.IterM m β}
  (motive : it₁.Step → Sort u_3) (it₁' : Std.IterM m β) (b : β) (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' b))
  (h_1 :
    (it₁' : Std.IterM m β) →
      (b : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' b)) → motive ⟨Std.IterStep.yield it₁' b, h⟩)
  (h_2 :
    (it₁' : Std.IterM m β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.yield it₁' b, h⟩ with
    | ⟨Std.IterStep.yield it₁' b, h⟩ => h_1 it₁' b h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_1 it₁' b h
-- Mathlib.RepresentationTheory.Rep.Basic
_private.Mathlib.RepresentationTheory.Rep.Basic.0.Rep.Hom.mk.injEq : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G}
  (hom' hom'_1 : A.ρ.IntertwiningMap B.ρ), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.tensorObj_obj : ∀ (R : Type u) [inst : CommRing R] (M N : FGModuleCat R),
  (CategoryTheory.MonoidalCategoryStruct.tensorObj M N).obj =
    CategoryTheory.MonoidalCategoryStruct.tensorObj M.obj N.obj
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Two vectors are equal if and only if they have equal norms and zero angle between them.  -/
Orientation.eq_iff_norm_eq_and_oangle_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), x = y ↔ ‖x‖ = ‖y‖ ∧ o.oangle x y = 0
-- Mathlib.Algebra.Algebra.RestrictScalars
instInhabitedRestrictScalars : (R : Type u_1) → (S : Type u_2) → (M : Type u_3) → [I : Inhabited M] → Inhabited (RestrictScalars R S M)
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
/-- The **Ruzsa-Szemerédi number** of a fintype is the maximum number of edges a locally linear
graph on that type can have.

In other words, `ruzsaSzemerediNumber α` is the maximum number of edges a graph on `α` can have such
that each edge belongs to exactly one triangle.  -/
ruzsaSzemerediNumber : (α : Type u_1) → [DecidableEq α] → [Fintype α] → ℕ
-- Mathlib.RingTheory.LocalRing.Defs
IsLocalRing.toNontrivial : ∀ {R : Type u_1} {inst : Semiring R} [self : IsLocalRing R], Nontrivial R
-- Mathlib.Data.Finset.Slice
Finset.eq_of_mem_slice : ∀ {α : Type u_1} {𝒜 : Finset (Finset α)} {A : Finset α} {r₁ r₂ : ℕ}, A ∈ 𝒜.slice r₁ → A ∈ 𝒜.slice r₂ → r₁ = r₂
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
ContMDiff.clm_postcomp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_8} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_9} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_10} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {n : WithTop ℕ∞}
  {f : M → F₂ →L[𝕜] F₃},
  ContMDiff I (modelWithCornersSelf 𝕜 (F₂ →L[𝕜] F₃)) n f →
    ContMDiff I (modelWithCornersSelf 𝕜 ((F₁ →L[𝕜] F₂) →L[𝕜] F₁ →L[𝕜] F₃)) n fun y =>
      ContinuousLinearMap.postcomp F₁ (f y)
-- Mathlib.Data.Set.Function
Set.eqOn_union : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {f₁ f₂ : α → β},
  Set.EqOn f₁ f₂ (s₁ ∪ s₂) ↔ Set.EqOn f₁ f₂ s₁ ∧ Set.EqOn f₁ f₂ s₂
-- Mathlib.Data.Finsupp.Defs
Finsupp.coe_zero : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M], ⇑0 = 0
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.le_add_le : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] [inst_1 : LE α] [inst_2 : Std.IsPreorder α] [Lean.Grind.OrderedAdd α]
  {a b : α}, a ≤ 0 → b ≤ 0 → a + b ≤ 0
-- Mathlib.Analysis.Calculus.Deriv.AffineMap
AffineMap.hasStrictDerivAt_lineMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {a b : E} {x : 𝕜}, HasStrictDerivAt (⇑(AffineMap.lineMap a b)) (b - a) x