mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Std
LinearOrder.OfStdArgs.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (toPartialOrderArgs : PartialOrder.OfStdArgs α)
  (isLinearOrder :
    autoParam
      (let this := toPartialOrderArgs.le;
      Std.IsLinearOrder α)
      LinearOrder.OfStdArgs.isLinearOrder._autoParam)
  (decidableLE : autoParam (DecidableLE α) LinearOrder.OfStdArgs.decidableLE._autoParam)
  (decidableEq :
    autoParam
      (let this := toPartialOrderArgs;
      let this := decidableLE;
      DecidableEq α)
      LinearOrder.OfStdArgs.decidableEq._autoParam)
  (decidableLT :
    autoParam
      (let this := toPartialOrderArgs.toPreorderArgs;
      let this := decidableLE;
      DecidableLT α)
      LinearOrder.OfStdArgs.decidableLT._autoParam)
  (min :
    autoParam
      (let this := toPartialOrderArgs.le;
      let this := decidableLE;
      Min α)
      LinearOrder.OfStdArgs.min._autoParam)
  (max :
    autoParam
      (let this := toPartialOrderArgs.le;
      let this := decidableLE;
      Max α)
      LinearOrder.OfStdArgs.max._autoParam)
  (lawfulOrderLeftLeaningMin :
    autoParam (Std.LawfulOrderLeftLeaningMin α) LinearOrder.OfStdArgs.lawfulOrderLeftLeaningMin._autoParam)
  (lawfulOrderLeftLeaningMax :
    autoParam (Std.LawfulOrderLeftLeaningMax α) LinearOrder.OfStdArgs.lawfulOrderLeftLeaningMax._autoParam)
  (ord :
    autoParam
      (let this := toPartialOrderArgs.lt;
      let this := decidableEq;
      let this := decidableLT;
      Ord α)
      LinearOrder.OfStdArgs.ord._autoParam)
  (lawfulOrderOrd :
    autoParam
      (let this := toPartialOrderArgs.le;
      let this_1 := toPartialOrderArgs.lt;
      let this_2 := ⋯;
      let this_3 := isLinearOrder;
      let this_4 := decidableEq;
      let this_5 := decidableLT;
      Std.LawfulOrderOrd α)
      LinearOrder.OfStdArgs.lawfulOrderOrd._autoParam),
  sizeOf
      { toPartialOrderArgs := toPartialOrderArgs, isLinearOrder := isLinearOrder, decidableLE := decidableLE,
        decidableEq := decidableEq, decidableLT := decidableLT, min := min, max := max,
        lawfulOrderLeftLeaningMin := lawfulOrderLeftLeaningMin, lawfulOrderLeftLeaningMax := lawfulOrderLeftLeaningMax,
        ord := ord, lawfulOrderOrd := lawfulOrderOrd } =
    1 + sizeOf toPartialOrderArgs + sizeOf isLinearOrder + sizeOf min + sizeOf max + sizeOf lawfulOrderLeftLeaningMin +
          sizeOf lawfulOrderLeftLeaningMax +
        sizeOf ord +
      sizeOf lawfulOrderOrd
-- Mathlib.Data.WSeq.Basic
/-- drop the first `n` elements from `s`.  -/
Stream'.WSeq.drop : {α : Type u} → Stream'.WSeq α → ℕ → Stream'.WSeq α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_eq_some_get! : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {a : α}, a ∈ t → Std.ExtDTreeMap.Const.get? t a = some (Std.ExtDTreeMap.Const.get! t a)
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_toArray : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m.toArray.isEmpty = m.isEmpty
-- Init.Data.UInt.Lemmas
USize.add_right_inj : ∀ {a b : USize} (c : USize), c + a = c + b ↔ a = b
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.inclusion_inj : ∀ {M : Type u_1} [inst : MulOneClass M] {S T : Submonoid M} (h : S ≤ T) {x y : ↥S},
  (Submonoid.inclusion h) x = (Submonoid.inclusion h) y ↔ x = y
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.operation_attachLift : ∀ {m : Type w → Type w'} [Monad m] [inst : MonadAttach m] {α : Type w} {x : m α},
  (Std.Iterators.PostconditionT.attachLift x).operation = MonadAttach.attach x
-- Mathlib.Algebra.Lie.BaseChange
LieAlgebra.ExtendScalars.instBracketTensorProduct : (R : Type u_1) →
  (A : Type u_2) →
    (L : Type u_3) →
      (M : Type u_4) →
        [inst : CommRing R] →
          [inst_1 : CommRing A] →
            [inst_2 : Algebra R A] →
              [inst_3 : LieRing L] →
                [inst_4 : LieAlgebra R L] →
                  [inst_5 : AddCommGroup M] →
                    [inst_6 : Module R M] →
                      [inst_7 : LieRingModule L M] →
                        [LieModule R L M] → Bracket (TensorProduct R A L) (TensorProduct R A M)
-- Mathlib.Algebra.Homology.HomotopyFiber
/-- The inclusion `K ⟶ K.pathObject`.  -/
HomologicalComplex.pathObject.ι : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {α : Type u_2} →
        {c : ComplexShape α} →
          (K : HomologicalComplex C c) →
            [inst_2 : DecidableRel c.Rel] →
              [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [inst_4 : K.HasPathObject] → K ⟶ K.pathObject
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.mk_pow : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (x : ℕ × K) (n : ℕ),
  PerfectClosure.mk K p x ^ n = PerfectClosure.mk K p (x.1, x.2 ^ n)
-- Init.GrindInstances.ToInt
Lean.Grind.instToIntNatCiOfNatInt : Lean.Grind.ToInt ℕ (Lean.Grind.IntInterval.ci 0)
-- Mathlib.Data.Finset.Fold
Finset.le_fold_min : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {b : β} {s : Finset α} [inst : LinearOrder β] (c : β),
  c ≤ Finset.fold min b f s ↔ c ≤ b ∧ ∀ x ∈ s, c ≤ f x
-- Mathlib.LinearAlgebra.Matrix.IsDiag
Matrix.IsDiag.transpose : ∀ {α : Type u_1} {n : Type u_4} [inst : Zero α] {A : Matrix n n α}, A.IsDiag → A.transpose.IsDiag
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.eventually_le_atBot : ∀ {α : Type u_3} [inst : Preorder α] (a : α), ∀ᶠ (x : α) in Filter.atBot, x ≤ a
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.num.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (I : FractionalIdeal S P), I.num = Submodule.comap (Algebra.linearMap R P) (I.den • ↑I)
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.gate.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (a : Std.Tactic.BVDecide.Gate) (a_1 a_2 : Std.Tactic.BVDecide.BoolExpr α),
  sizeOf (Std.Tactic.BVDecide.BoolExpr.gate a a_1 a_2) = 1 + sizeOf a + sizeOf a_1 + sizeOf a_2
-- Mathlib.Order.RelClasses
/-- Set notation form of `Eq.le` -/
Eq.subset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a = b → a ⊆ b
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toList_rcc_ne_zero_iff : ∀ {m n : ℤ} {i : ℕ}, (m...=n).toList[i]! ≠ 0 ↔ i < (n + 1 - m).toNat ∧ m + ↑i ≠ 0
-- Mathlib.RingTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx_eq`. -/
Ideal.ramificationIdx'_eq : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  (q : Ideal S) [q.LiesOver p] [inst_4 : q.IsPrime],
  q.ramificationIdx R =
    (Module.length (Localization.AtPrime q)
        (Localization.AtPrime q ⧸ Ideal.map (algebraMap R (Localization.AtPrime q)) p)).toNat
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- If `F ≤ E` are two intermediate fields of `L / K`, then `F` is also an intermediate field of
`E / K`. It is an inverse of `IntermediateField.lift`, and can be viewed as a dual to
`IntermediateField.extendScalars`.
 -/
IntermediateField.restrict : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] → [inst_2 : Algebra K L] → {F E : IntermediateField K L} → F ≤ E → IntermediateField K ↥E
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
/-- The Tate complex defined by connecting inhomogeneous chains and cochains with the Tate norm.  -/
tateComplex : {R G : Type u} →
  [inst : CommRing R] → [inst_1 : Group G] → [Fintype G] → Rep.{u, u, u} R G → CochainComplex (ModuleCat R) ℤ
-- Mathlib.CategoryTheory.NatTrans
CategoryTheory.NatTrans.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F G : CategoryTheory.Functor C D} {x y : CategoryTheory.NatTrans F G}, x = y ↔ x.app = y.app
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.natCast_toNat`.

---

**Alias** of the reverse direction of `ENat.natCast_toNat_eq_self`. -/
ENat.coe_toNat : ∀ {n : ℕ∞}, n ≠ ⊤ → ↑n.toNat = n
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.Const.eq_of_beq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [inst_2 : BEq β]
  [LawfulBEq β] (m₁ m₂ : Std.ExtDTreeMap α (fun x => β) cmp), Std.ExtDTreeMap.Const.beq m₁ m₂ = true → m₁ = m₂
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.addEquivBiprod_apply_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y₁ Y₂ : C} {n : ℕ} (e : CategoryTheory.Abelian.Ext X (Y₁ ⊞ Y₂) n),
  (CategoryTheory.Abelian.Ext.addEquivBiprod e).2 =
    e.comp (CategoryTheory.Abelian.Ext.mk₀ CategoryTheory.Limits.biprod.snd) ⋯
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxi.Iterator.instIteratorLoop.loop.wf.eq_def : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  {n : Type u → Type w} [inst_2 : Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop)
  (wf : Std.IteratorLoop.WellFounded (Std.Rxi.Iterator α) Id Pl) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) (acc : γ) (next : α)
  (h : LargeEnough next) (f : (out : α) → LargeEnough out → (c : γ) → n { s // Pl out c s }),
  Std.Rxi.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl acc next h f = do
    let __do_lift ← f next h acc
    match __do_lift with
      | ⟨ForInStep.yield acc', property⟩ =>
        match hs : Std.PRange.succ? next with
        | some next' => Std.Rxi.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl acc' next' ⋯ f
        | none => pure acc'
      | ⟨ForInStep.done acc', property⟩ => pure acc'
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.induction_on : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s), (∀ (z : α), C ↑z) → C x
-- Init.Data.Vector.Erase
Vector.getElem_eraseIdx_of_ge : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (w : i < n) {j : ℕ} (h : j < n - 1),
  i ≤ j → (xs.eraseIdx i w)[j] = xs[j + 1]
-- Mathlib.Order.Bounds.Image
image2_upperBounds_lowerBounds_subset_upperBounds_image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β},
  (∀ (b : β), Monotone (Function.swap f b)) →
    (∀ (a : α), Antitone (f a)) → Set.image2 f (upperBounds s) (lowerBounds t) ⊆ upperBounds (Set.image2 f s t)
-- Lean.Parser.Term
Lean.Parser.Term.funStrictImplicitBinder.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_exists : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (obj : Fin (n + 1) → C)
  (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ),
  ∃ F e,
    ∀ (i : ℕ) (hi : i < n),
      mapSucc ⟨i, hi⟩ =
        CategoryTheory.CategoryStruct.comp (e ⟨i, ⋯⟩).inv
          (CategoryTheory.CategoryStruct.comp (F.map' i (i + 1) ⋯ hi) (e ⟨i + 1, ⋯⟩).hom)
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.atBot_eq_generate_of_forall_exists_le : ∀ {α : Type u_3} [inst : Preorder α] {s : Set α},
  (∀ (x : α), ∃ y ∈ s, y ≤ x) → Filter.atBot = Filter.generate (Set.Iic '' s)
-- Mathlib.Order.Heyting.Basic
Prod.instHImp : {α : Type u_2} → {β : Type u_3} → [HImp α] → [HImp β] → HImp (α × β)
-- Mathlib.LinearAlgebra.Prod
LinearMap.map_coprod_prod : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) (p : Submodule R M) (q : Submodule R M₂),
  Submodule.map (f.coprod g) (p.prod q) = Submodule.map f p ⊔ Submodule.map g q
-- Mathlib.CategoryTheory.Functor.Flat
CategoryTheory.flat_iff_lan_flat : ∀ {C D : Type u₁} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.SmallCategory D]
  [CategoryTheory.Limits.HasFiniteLimits C] (F : CategoryTheory.Functor C D),
  CategoryTheory.RepresentablyFlat F ↔ CategoryTheory.RepresentablyFlat F.op.lan
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.commAlgEquiv_C_X : ∀ {R : Type u_2} {S₁ : Type u_3} {S₂ : Type u_4} [inst : CommSemiring R] (i : S₂),
  (MvPolynomial.commAlgEquiv R S₁ S₂) (MvPolynomial.C (MvPolynomial.X i)) = MvPolynomial.X i
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.swap_bijective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  Function.Bijective ⇑(AddMonoid.Coprod.swap M N)
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
AlgebraicGeometry.Scheme.Hom.genericPoint_mem_smoothLocus_of_perfectField : ∀ {X : AlgebraicGeometry.Scheme} {K : Type u} [inst : Field K] [PerfectField K]
  [inst_2 : AlgebraicGeometry.IsIntegral X] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K))
  [inst_3 : AlgebraicGeometry.LocallyOfFinitePresentation f],
  genericPoint ↥X ∈ AlgebraicGeometry.Scheme.Hom.smoothLocus f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula.0.WeierstrassCurve.Projective.toAffine_negAddY_of_ne : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  P 2 ≠ 0 →
    Q 2 ≠ 0 →
      ∀ {n d : F},
        d ≠ 0 →
          W.toAffine.negAddY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (n / d) =
            (n *
                    (n ^ 2 * P 2 * Q 2 + W.a₁ * n * P 2 * Q 2 * d - W.a₂ * P 2 * Q 2 * d ^ 2 - P 0 * Q 2 * d ^ 2 -
                        Q 0 * P 2 * d ^ 2 -
                      P 0 * Q 2 * d ^ 2) +
                  P 1 * Q 2 * d ^ 3) /
                (P 2 * Q 2) ^ 2 /
              (d ^ 3 / (P 2 * Q 2))
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.norm_compL_le : ∀ (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_7) (Gₗ : Type u_9) [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup Fₗ] [inst_2 : SeminormedAddCommGroup Gₗ] [inst_3 : NontriviallyNormedField 𝕜]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 Fₗ] [inst_6 : NormedSpace 𝕜 Gₗ],
  ‖ContinuousLinearMap.compL 𝕜 E Fₗ Gₗ‖ ≤ 1
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.all_zero_of_le_zero_le_of_sum_eq_zero : ∀ {α : Type u_4} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {s : Multiset α},
  (∀ x ∈ s, 0 ≤ x) → s.sum = 0 → ∀ x ∈ s, x = 0
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.emptyAt.sizeOf_spec : ∀ {s : String.Slice} (pos : s.Pos) (h : pos ≠ s.endPos),
  sizeOf (String.Slice.Pattern.ForwardSliceSearcher.emptyAt pos h) = 1 + sizeOf pos
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_ε_η : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {C' : Type u₁'}
  [inst_4 : CategoryTheory.Category.{v₁', u₁'} C'] (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal]
  (G : CategoryTheory.Functor D C'),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.LaxMonoidal.ε F))
      (G.map (CategoryTheory.Functor.OplaxMonoidal.η F)) =
    CategoryTheory.CategoryStruct.id (G.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdxD.eq_1 : ∀ {α : Type u} {β : α → Type v} (x : ℕ) (x_1 : (a : α) × β a), Std.DTreeMap.Internal.Impl.leaf.entryAtIdxD x x_1 = x_1
-- Mathlib.NumberTheory.ModularForms.Basic
ModularForm.add : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → Add (ModularForm Γ k)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_hom_inv_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) {Z_1 : C} (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj Z V ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g f.hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom h f.inv) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.CategoryStruct.id V))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom h (CategoryTheory.CategoryStruct.id V)) h_1)
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.restr_apply : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} (h : e.IsImage s t) (hs : IsOpen (e.source ∩ s)),
  ↑(h.restr hs) = ↑e
-- Mathlib.Algebra.Group.Subsemigroup.Membership
Subsemigroup.mem_biSup_of_directedOn : ∀ {M : Type u_2} [inst : Mul M] {ι : Type u_3} {p : ι → Prop} {S : ι → Subsemigroup M},
  DirectedOn (Function.onFun (fun x1 x2 => x1 ≤ x2) S) {i | p i} →
    ∀ {x : M}, x ∈ ⨆ i, ⨆ (_ : p i), S i ↔ ∃ i, p i ∧ x ∈ S i
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_insert_le : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k : α} {v : β k}, (m.insert k v).size ≤ m.size + 1
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.IsReduced.linearIndependent_iff : ∀ {ι : 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 : RootPairing ι R M N) {i j : ι}
  [Nontrivial R] [P.IsReduced], LinearIndependent R ![P.root i, P.root j] ↔ i ≠ j ∧ P.root i ≠ -P.root j
-- Mathlib.Topology.Algebra.UniformConvergence
instCommMonoidUniformFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid β],
  instCommMonoidUniformFun = { toMonoid := instMonoidUniformFun, mul_comm := ⋯ }
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartRing.lie_smul_eq_mul : ∀ {A₁ : Type u_2} {L₁ : Type u_3} [inst : CommRing A₁] [inst_1 : LieRing L₁] [inst_2 : Module A₁ L₁]
  [inst_3 : LieRingModule L₁ A₁] [LieRinehartRing A₁ L₁] (a b : A₁) (x : L₁), ⁅a • x, b⁆ = a * ⁅x, b⁆
-- Mathlib.Tactic.Linter.UnusedInstancesInType
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.Parameter.mk.injEq : ∀ (fvar? type? : Option Lean.Expr) (idx : ℕ) (appearsInTypeProof : Bool) (fvar?_1 type?_1 : Option Lean.Expr)
  (idx_1 : ℕ) (appearsInTypeProof_1 : Bool),
  ({ fvar? := fvar?, type? := type?, idx := idx, appearsInTypeProof := appearsInTypeProof } =
      { fvar? := fvar?_1, type? := type?_1, idx := idx_1, appearsInTypeProof := appearsInTypeProof_1 }) =
    (fvar? = fvar?_1 ∧ type? = type?_1 ∧ idx = idx_1 ∧ appearsInTypeProof = appearsInTypeProof_1)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- If a function is `C^n` on a set with `n ≥ 1`, then it is differentiable there.  -/
ContDiffOn.differentiableOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞}, ContDiffOn 𝕜 n f s → n ≠ 0 → DifferentiableOn 𝕜 f s
-- Mathlib.Order.PFilter
Order.PFilter.inf_mem_iff : ∀ {P : Type u_1} [inst : SemilatticeInf P] {x y : P} {F : Order.PFilter P}, x ⊓ y ∈ F ↔ x ∈ F ∧ y ∈ F
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback_hom_app_comp_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X : C} (g : Z ⟶ X)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] (T : CategoryTheory.Over X) {Z_1 : C} (h : T.left ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left ((CategoryTheory.ChosenPullbacksAlong.pullbackIsoOverPullback g).hom.app T))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst T.hom g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst T.hom g) h
-- Mathlib.Order.Grade
GradeOrder.mk : {𝕆 : Type u_5} →
  {α : Type u_6} →
    [inst : Preorder 𝕆] →
      [inst_1 : Preorder α] →
        (grade : α → 𝕆) → StrictMono grade → (∀ ⦃a b : α⦄, a ⋖ b → grade a ⋖ grade b) → GradeOrder 𝕆 α
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.ofAbs_one : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S), WithAbs.ofAbs 1 = 1
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.closure_preimage_eq_top : ∀ {G : Type u_1} [inst : Group G] (s : Set G), Subgroup.closure (⇑(Subgroup.closure s).subtype ⁻¹' s) = ⊤
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.instInhabitedOfDefault : {ι : Type u_1} → {A : ι → Type u_2} → [inst : Inhabited ι] → [Inhabited (A default)] → Inhabited (GradedMonoid A)
-- Mathlib.Data.Nat.Digits.Defs
/-- The addition of ofDigits of two lists is equal to ofDigits of digit-wise addition of them  -/
Nat.ofDigits_add_ofDigits_eq_ofDigits_zipWith_of_length_eq : ∀ {b : ℕ} {l1 l2 : List ℕ},
  l1.length = l2.length →
    Nat.ofDigits b l1 + Nat.ofDigits b l2 = Nat.ofDigits b (List.zipWith (fun x1 x2 => x1 + x2) l1 l2)
-- Mathlib.Topology.Separation.CompletelyRegular
instCompletelyRegularSpaceForall : ∀ {ι : Type u_1} {X : ι → Type u_2} [t : (i : ι) → TopologicalSpace (X i)]
  [ht : ∀ (i : ι), CompletelyRegularSpace (X i)], CompletelyRegularSpace ((i : ι) → X i)
-- Init.Data.List.Scan.Lemmas
_private.Init.Data.List.Scan.Lemmas.0.List.scanl.eq_1 : ∀ {β : Type u_1} {α : Type u_2} (f : β → α → β) (init : β) (as : List α),
  List.scanl f init as = (List.scanlM (fun x1 x2 => pure (f x1 x2)) init as).run
-- Mathlib.GroupTheory.Perm.Cycle.Factors
/-- Factors a permutation `f` into a `Finset` of disjoint cyclic permutations that multiply to `f`.
 -/
Equiv.Perm.cycleFactorsFinset : {α : Type u_2} → [DecidableEq α] → [Fintype α] → Equiv.Perm α → Finset (Equiv.Perm α)
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.isCoprime_y_z : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K],
  IsCoprime (FermatLastTheoremForThreeGen.Solution.y✝ S) (FermatLastTheoremForThreeGen.Solution.z✝ S)
-- Mathlib.NumberTheory.KummerDedekind
/-- The **Kummer-Dedekind Theorem**.  -/
KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S} {I : Ideal R}
  [inst_3 : IsDomain R] [inst_4 : IsIntegrallyClosed R] [inst_5 : IsDedekindDomain S]
  [inst_6 : Module.IsTorsionFree R S] (hI : I.IsMaximal) (hI' : I ≠ ⊥)
  (hx : Ideal.comap (algebraMap R S) (conductor R x) ⊔ I = ⊤) (hx' : IsIntegral R x),
  UniqueFactorizationMonoid.normalizedFactors (Ideal.map (algebraMap R S) I) =
    Multiset.map (fun f => ↑((KummerDedekind.normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx').symm f))
      (UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))).attach
-- Mathlib.GroupTheory.Complement
/-- Given two subgroups `H' ⊆ H`, there exists a right transversal to `H'` inside `H`.  -/
Subgroup.exists_right_transversal_of_le : ∀ {G : Type u_1} [inst : Group G] {H' H : Subgroup G},
  H' ≤ H → ∃ S, ↑H' * S = ↑H ∧ Nat.card ↥H' * Nat.card ↑S = Nat.card ↥H
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.instFaithfulSMulPolynomial : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R}, FaithfulSMul (Polynomial R) W'.CoordinateRing
-- Mathlib.RingTheory.Algebraic.Basic
Algebra.IsAlgebraic.nontrivial : ∀ (R : Type u) (A : Type v) [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  [alg : Algebra.IsAlgebraic R A], Nontrivial R