mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.PEquivOn.mk.inj : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {inst : LinearOrder ι} {f : ⦃i j : ι⦄ → i ≤ j → F j → F i}
  {inst_1 : SuccOrder ι} {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} {s : Set ι}
  {equiv : (i : ↑s) → F ↑i ≃ InverseSystem.piLT X ↑i} {nat : InverseSystem.IsNatEquiv f equiv}
  {compat :
    ∀ {i : ι} (hsi : Order.succ i ∈ s) (hi : ¬IsMax i) (x : F ↑⟨Order.succ i, hsi⟩),
      (equiv ⟨Order.succ i, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2}
  {equiv_1 : (i : ↑s) → F ↑i ≃ InverseSystem.piLT X ↑i} {nat_1 : InverseSystem.IsNatEquiv f equiv_1}
  {compat_1 :
    ∀ {i : ι} (hsi : Order.succ i ∈ s) (hi : ¬IsMax i) (x : F ↑⟨Order.succ i, hsi⟩),
      (equiv_1 ⟨Order.succ i, hsi⟩) x ⟨i, ⋯⟩ = ((equivSucc hi) x).2},
  { equiv := equiv, nat := nat, compat := compat } = { equiv := equiv_1, nat := nat_1, compat := compat_1 } →
    equiv = equiv_1
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.wideCoequalizer.desc.congr_simp : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  [inst_1 : CategoryTheory.Limits.HasWideCoequalizer f] [inst_2 : Nonempty J] {W : C} (k k_1 : Y ⟶ W) (e_k : k = k_1)
  (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp (f j₁) k = CategoryTheory.CategoryStruct.comp (f j₂) k),
  CategoryTheory.Limits.wideCoequalizer.desc k h = CategoryTheory.Limits.wideCoequalizer.desc k_1 ⋯
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Context.ematchDiag : Lean.Meta.Grind.Context → Bool
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.prodLeftIsoPullback_hom_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (Y Z : CategoryTheory.Over X)
  [inst_1 : CategoryTheory.Limits.HasPullback Y.hom Z.hom] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z],
  CategoryTheory.CategoryStruct.comp (Y.prodLeftIsoPullback Z).hom (CategoryTheory.Limits.pullback.fst Y.hom Z.hom) =
    CategoryTheory.Over.Hom.left CategoryTheory.Limits.prod.fst
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k fallback : α},
  (List.map Prod.fst l).contains k = false →
    (Std.ExtDTreeMap.Const.insertMany t l).getKeyD k fallback = t.getKeyD k fallback
-- Lean.Elab.MutualInductive
Lean.Elab.Command.instInhabitedInductiveElabStep2 : Inhabited Lean.Elab.Command.InductiveElabStep2
-- Mathlib.Tactic.ToExpr
Mathlib.instToExprLevel_mathlib : Lean.ToExpr Lean.Level
-- Init.Data.Slice.Array.Lemmas
Array.array_mkSlice_roi : ∀ {α : Type u_1} {xs : Array α} {lo : ℕ}, (Std.Roi.Sliceable.mkSlice xs lo<...*).array = xs
-- Mathlib.Analysis.BoxIntegral.Partition.Measure
/-- If `μ` is a locally finite measure on `ℝⁿ`, then `fun J ↦ μ.real J` is a box-additive
function.  -/
MeasureTheory.Measure.toBoxAdditive : {ι : Type u_1} →
  [Finite ι] →
    (μ : MeasureTheory.Measure (ι → ℝ)) → [MeasureTheory.IsLocallyFiniteMeasure μ] → BoxIntegral.BoxAdditiveMap ι ℝ ⊤
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey_eq_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [Std.LawfulEqOrd α],
  t.WF → ∀ {he : t.isEmpty = false} {km : α}, t.maxKey he = km ↔ km ∈ t ∧ ∀ k ∈ t, (compare k km).isLE = true
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.ne_zero_iff_exists : ∀ {α : Type u} {x : WithZero α}, x ≠ 0 ↔ ∃ a, ↑a = x
-- Mathlib.GroupTheory.Perm.Sign
/-- Every finite symmetric group is generated by transpositions of adjacent elements.  -/
Equiv.Perm.mclosure_swap_castSucc_succ : ∀ (n : ℕ), Submonoid.closure (Set.range fun i => Equiv.swap i.castSucc i.succ) = ⊤
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
PartialDiffeomorph.trans_toPartialEquiv : ∀ {𝕜 : 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] {F' : Type u_4}
  [inst_5 : NormedAddCommGroup F'] [inst_6 : NormedSpace 𝕜 F'] {H₁ : Type u_5} [inst_7 : TopologicalSpace H₁]
  {H₂ : Type u_6} [inst_8 : TopologicalSpace H₂] {H₃ : Type u_7} [inst_9 : TopologicalSpace H₃]
  {I : ModelWithCorners 𝕜 E H₁} {J : ModelWithCorners 𝕜 F H₂} {K : ModelWithCorners 𝕜 F' H₃} {M : Type u_8}
  [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H₁ M] {N : Type u_9} [inst_12 : TopologicalSpace N]
  [inst_13 : ChartedSpace H₂ N] {P : Type u_10} [inst_14 : TopologicalSpace P] [inst_15 : ChartedSpace H₃ P]
  {n : WithTop ℕ∞} (Φ : PartialDiffeomorph I J M N n) (Ψ : PartialDiffeomorph J K N P n),
  (Φ.trans Ψ).toPartialEquiv = (Φ.toOpenPartialHomeomorph.trans Ψ.toOpenPartialHomeomorph).toPartialEquiv
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.instReprIndGroupInfo : Repr Lean.Elab.Structural.IndGroupInfo
-- Aesop.Tree.Data
Aesop.RappUnsafe.brecOn.go : {motive_1 : Aesop.GoalUnsafe → Sort u} →
  {motive_2 : Aesop.MVarClusterUnsafe → Sort u} →
    {motive_3 : Aesop.RappUnsafe → Sort u} →
      {motive_4 : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe → Sort u} →
        {motive_5 : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe → Sort u} →
          {motive_6 : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe → Sort u} →
            {motive_7 : Array (IO.Ref Aesop.RappUnsafe) → Sort u} →
              {motive_8 : Option (IO.Ref Aesop.RappUnsafe) → Sort u} →
                {motive_9 : Array (IO.Ref Aesop.GoalUnsafe) → Sort u} →
                  {motive_10 : Array (IO.Ref Aesop.MVarClusterUnsafe) → Sort u} →
                    {motive_11 : List (IO.Ref Aesop.RappUnsafe) → Sort u} →
                      {motive_12 : List (IO.Ref Aesop.GoalUnsafe) → Sort u} →
                        {motive_13 : List (IO.Ref Aesop.MVarClusterUnsafe) → Sort u} →
                          (t : Aesop.RappUnsafe) →
                            ((t : Aesop.GoalUnsafe) → t.below → motive_1 t) →
                              ((t : Aesop.MVarClusterUnsafe) → t.below → motive_2 t) →
                                ((t : Aesop.RappUnsafe) → t.below → motive_3 t) →
                                  ((t : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe) →
                                      Aesop.GoalUnsafe.below_1 t → motive_4 t) →
                                    ((t : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe) →
                                        Aesop.GoalUnsafe.below_2 t → motive_5 t) →
                                      ((t : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe) →
                                          Aesop.GoalUnsafe.below_3 t → motive_6 t) →
                                        ((t : Array (IO.Ref Aesop.RappUnsafe)) →
                                            Aesop.GoalUnsafe.below_4 t → motive_7 t) →
                                          ((t : Option (IO.Ref Aesop.RappUnsafe)) →
                                              Aesop.GoalUnsafe.below_5 t → motive_8 t) →
                                            ((t : Array (IO.Ref Aesop.GoalUnsafe)) →
                                                Aesop.GoalUnsafe.below_6 t → motive_9 t) →
                                              ((t : Array (IO.Ref Aesop.MVarClusterUnsafe)) →
                                                  Aesop.GoalUnsafe.below_7 t → motive_10 t) →
                                                ((t : List (IO.Ref Aesop.RappUnsafe)) →
                                                    Aesop.GoalUnsafe.below_8 t → motive_11 t) →
                                                  ((t : List (IO.Ref Aesop.GoalUnsafe)) →
                                                      Aesop.GoalUnsafe.below_9 t → motive_12 t) →
                                                    ((t : List (IO.Ref Aesop.MVarClusterUnsafe)) →
                                                        Aesop.GoalUnsafe.below_10 t → motive_13 t) →
                                                      motive_3 t ×' t.below
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
mul_inv_le_mul_inv_iff' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LE α] [MulLeftMono α] {a b c d : α}, a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b
-- Init.Data.String.Lemmas.Order
String.Pos.ofSlice_lt_iff : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos},
  String.Pos.ofSlice p < q ↔ ∀ (h₁ : q ≤ p₁), ∃ (h₀ : p₀ ≤ q), p < q.slice p₀ p₁ h₀ h₁
-- Init.Data.String.Lemmas.FindPos
String.Slice.pos_eq_posLE : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : String.Pos.Raw.IsValidForSlice s p}, s.pos p h = s.posLE p
-- Mathlib.Data.List.Destutter
_private.Mathlib.Data.List.Destutter.0.List.destutter'.match_1.splitter : {α : Type u_1} →
  (motive : α → List α → Sort u_2) →
    (x : α) → (x_1 : List α) → ((a : α) → motive a []) → ((a h : α) → (l : List α) → motive a (h :: l)) → motive x x_1
-- Mathlib.Algebra.GroupWithZero.Pi
Pi.commMonoidWithZero : {ι : Type u_1} → {α : ι → Type u_2} → [(i : ι) → CommMonoidWithZero (α i)] → CommMonoidWithZero ((i : ι) → α i)
-- Aesop.Options.Public
Aesop.Options.mk : Aesop.Strategy →
  ℕ →
    ℕ →
      ℕ →
        ℕ →
          ℕ →
            Lean.Meta.TransparencyMode →
              Lean.Meta.TransparencyMode →
                Lean.Meta.TransparencyMode →
                  Option Lean.Meta.TransparencyMode → Bool → Bool → Bool → Bool → Bool → Bool → Bool → Aesop.Options
-- Lean.Elab.MutualInductive
Lean.Elab.Command.instInhabitedInductiveView.default : Lean.Elab.Command.InductiveView
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.surjective : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N), Function.Surjective ⇑e
-- Mathlib.Topology.Separation.Regular
Homeomorph.t4Space : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [T4Space X] (h : X ≃ₜ Y),
  T4Space Y
-- Mathlib.NumberTheory.FrobeniusNumber
Nat.setGcd_dvd_of_mem : ∀ {s : Set ℕ} {n : ℕ}, n ∈ s → Nat.setGcd s ∣ n
-- Mathlib.Algebra.Ring.Opposite
NonUnitalRingHom.toOpposite_apply : ∀ {R : Type u_2} {S : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (f : R →ₙ+* S) (hf : ∀ (x y : R), Commute (f x) (f y)), ⇑(f.toOpposite hf) = MulOpposite.op ∘ ⇑f
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.instField : {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) → Field (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
-- Lean.Server.References
/-- URI of the module that is imported.  -/
Lean.Server.ModuleImport.uri : Lean.Server.ModuleImport → Lean.Lsp.DocumentUri
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
upperHemicontinuous_iff_preimage_Iic : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} [inst_1 : TopologicalSpace β],
  UpperHemicontinuous f ↔ ∀ (x : α), ∀ u ∈ nhdsSet (f x), f ⁻¹' Set.Iic u ∈ nhds x
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.relMap_sumInl : ∀ {L₁ : FirstOrder.Language} {L₂ : FirstOrder.Language} {S : Type u_3} [inst : L₁.Structure S] [inst_1 : L₂.Structure S]
  {n : ℕ} (R : L₁.Relations n),
  FirstOrder.Language.Structure.RelMap (Sum.inl R) = FirstOrder.Language.Structure.RelMap R
-- Lean.Elab.PreDefinition.FixedParams
/-- The dependency structure of the function parameter.
If `paramIdx₂ ∈ revDeps[funIdx][paraIdx₁]`, then the type of `paramIdx₂` depends on `paramIdx₁`
 -/
Lean.Elab.FixedParams.Info.revDeps : Lean.Elab.FixedParams.Info → Array (Array (Array ℕ))
-- Mathlib.Topology.LocalAtTarget
IsOpenQuotientMap.restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  IsOpenQuotientMap f → ∀ (s : Set β), IsOpenQuotientMap (s.restrictPreimage f)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.RefVec.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ}
  (refs : Vector Std.Sat.AIG.Fanin w) (hrefs : ∀ {i : ℕ} (h : i < w), refs[i].gate < aig.decls.size)
  (refs_1 : Vector Std.Sat.AIG.Fanin w) (hrefs_1 : ∀ {i : ℕ} (h : i < w), refs_1[i].gate < aig.decls.size),
  ({ refs := refs, hrefs := hrefs } = { refs := refs_1, hrefs := hrefs_1 }) = (refs = refs_1)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.le_inf_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} {f : β → α} {a : α},
  a ≤ s.inf f ↔ ∀ b ∈ s, a ≤ f b
-- Mathlib.RingTheory.AdicCompletion.RingHom
IsAdicComplete.mk_liftAlgHom : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (I : Ideal S) [inst_3 : IsAdicComplete I S] [inst_4 : CommRing A] [inst_5 : Algebra R A]
  (f : (n : ℕ) → A →ₐ[R] S ⧸ I ^ n) (hf : ∀ {m n : ℕ} (hle : m ≤ n), (Ideal.Quotient.factorₐ R ⋯).comp (f n) = f m)
  (n : ℕ) (x : A), (Ideal.Quotient.mk (I ^ n)) ((IsAdicComplete.liftAlgHom I f ⋯) x) = (f n) x
-- Mathlib.Order.PrimeIdeal
Order.Ideal.PrimePair.I_isProper : ∀ {P : Type u_1} [inst : Preorder P] (IF : Order.Ideal.PrimePair P), IF.I.IsProper
-- Mathlib.GroupTheory.Perm.DomMulAct
/-- The cardinality of the type of permutations preserving a function  -/
DomMulAct.stabilizer_card : ∀ {α : Type u_1} {ι : Type u_2} (f : α → ι) [inst : Fintype α] [inst_1 : DecidableEq α] [inst_2 : DecidableEq ι]
  [inst_3 : Fintype ι], Fintype.card { g // f ∘ ⇑g = f } = ∏ i, (Fintype.card { a // f a = i }).factorial
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.transvection.of_right_eq_zero : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] (f : Module.Dual R V)
  (hf : optParam (f 0 = 0) ⋯), LinearEquiv.transvection hf = LinearEquiv.refl R V
-- Mathlib.Topology.Algebra.Group.Basic
IsOpen.inv : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [ContinuousInv G] {s : Set G},
  IsOpen s → IsOpen s⁻¹
-- Mathlib.Order.Hom.WithTopBot
WithBot.subtypeOrderIso_apply_coe : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] [inst_2 : DecidablePred fun x => x = ⊥]
  (a : { a // a ≠ ⊥ }), WithBot.subtypeOrderIso ↑a = ↑a
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.instIsSFiniteKernelBoolBoolKernelOfSFinite : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SFinite μ]
  [MeasureTheory.SFinite ν], ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.boolKernel μ ν)
-- Mathlib.GroupTheory.Torsion
/-- The additive `p`-primary component is the submonoid of elements `g` such that
`p ^ k • g = 0` for some `k`. For prime `p`, these are exactly the elements of additive
`p`-power order.  -/
AddCommMonoid.primaryComponent : (G : Type u_1) → [inst : AddCommMonoid G] → ℕ → AddSubmonoid G
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.beq_congr : ∀ {w : ℕ} (lhs rhs lhs' rhs' : BitVec w), lhs' = lhs → rhs' = rhs → (lhs' == rhs') = (lhs == rhs)
-- Init.Data.List.BasicAux
List.append_cancel_right : ∀ {α : Type u_1} {as bs cs : List α}, as ++ bs = cs ++ bs → as = cs
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.instForInProdOfMonad : {α : Type u} → {β : Type v} → {m : Type w → Type w'} → [Monad m] → ForIn m (Std.HashMap.Raw α β) (α × β)
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.pushforwardIso_f : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.RespectsIso] [inst_1 : P.ContainsIdentities]
  [inst_2 : P.IsStableUnderComposition] {X Y : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (f : X ⟶ Y)
  [inst_3 : CategoryTheory.IsIso f] (x : 𝒰.I₀), (𝒰.pushforwardIso f).f x = CategoryTheory.CategoryStruct.comp (𝒰.f x) f
-- Init.Data.Int.Pow
Int.two_pow_pred_sub_two_pow : ∀ {w : ℕ}, 0 < w → ↑(2 ^ (w - 1)) - ↑(2 ^ w) = -↑(2 ^ (w - 1))
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
/-- Any morphism in `SimplexCategoryGenRel` can be decomposed as a `P_σ` followed by a `P_δ`.  -/
SimplexCategoryGenRel.exists_P_σ_P_δ_factorization : ∀ {x y : SimplexCategoryGenRel} (f : x ⟶ y),
  ∃ z e m,
    ∃ (_ : SimplexCategoryGenRel.P_σ e) (_ : SimplexCategoryGenRel.P_δ m), f = CategoryTheory.CategoryStruct.comp e m
-- Mathlib.Analysis.Normed.Group.ZeroAtInfty
zero_at_infty_of_norm_le : ∀ {E : Type u_1} {F : Type u_2} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddCommGroup F] [ProperSpace E]
  (f : E → F), (∀ (ε : ℝ), 0 < ε → ∃ r, ∀ (x : E), r < ‖x‖ → ‖f x‖ < ε) → Filter.Tendsto f (Filter.cocompact E) (nhds 0)
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.addSubgroupOfEquivOfLe.eq_1 : ∀ {G : Type u_7} [inst : AddGroup G] {H K : AddSubgroup G} (h : H ≤ K),
  AddSubgroup.addSubgroupOfEquivOfLe h =
    { toFun := fun g => ⟨↑↑g, ⋯⟩, invFun := fun g => ⟨⟨↑g, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- A cover of `X` in the coverage `K` is a `0`-hypercover for `K`.  -/
AlgebraicGeometry.Scheme.Cover : CategoryTheory.Precoverage AlgebraicGeometry.Scheme → AlgebraicGeometry.Scheme → Type (max (u + 1) (v + 1))
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- **Alias** of the forward direction of `SimpleGraph.isContained_iff_exists_iso_subgraph`.

---

`B` contains `A` if and only if `B` has a subgraph `B'` and `B'` is isomorphic to `A`.  -/
SimpleGraph.IsContained.exists_iso_subgraph : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β}, A.IsContained B → ∃ B', Nonempty (A ≃g B'.coe)
-- Mathlib.Order.Birkhoff
OrderEmbedding.birkhoffSet.eq_1 : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : Fintype α] [inst_2 : DecidablePred SupIrred],
  OrderEmbedding.birkhoffSet =
    if h : IsEmpty α then OrderEmbedding.ofIsEmpty
    else
      have this := Fintype.toOrderBot α;
      RelEmbedding.trans OrderIso.lowerSetSupIrred.toOrderEmbedding
        { toFun := SetLike.coe, inj' := ⋯, map_rel_iff' := ⋯ }
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context.mk.injEq : ∀ (f fType : Lean.Expr) (args mvars : Array Lean.Expr) (bInfos : Array Lean.BinderInfo) (forceRegularApp : Bool)
  (f_1 fType_1 : Lean.Expr) (args_1 mvars_1 : Array Lean.Expr) (bInfos_1 : Array Lean.BinderInfo)
  (forceRegularApp_1 : Bool),
  ({ f := f, fType := fType, args := args, mvars := mvars, bInfos := bInfos, forceRegularApp := forceRegularApp } =
      { f := f_1, fType := fType_1, args := args_1, mvars := mvars_1, bInfos := bInfos_1,
        forceRegularApp := forceRegularApp_1 }) =
    (f = f_1 ∧
      fType = fType_1 ∧ args = args_1 ∧ mvars = mvars_1 ∧ bInfos = bInfos_1 ∧ forceRegularApp = forceRegularApp_1)
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.instDecidableRelAdjMulCayleyOfDecidableEqOfDecidablePredMemSet.eq_1 : ∀ {M : Type u_1} (s : Set M) [inst : Group M] [inst_1 : DecidableEq M] [inst_2 : DecidablePred fun x => x ∈ s]
  (u v : M),
  SimpleGraph.instDecidableRelAdjMulCayleyOfDecidableEqOfDecidablePredMemSet s u v =
    decidable_of_iff (u ≠ v ∧ (u⁻¹ * v ∈ s ∨ v⁻¹ * u ∈ s)) ⋯
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.instPreorder : Preorder DyckWord
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_of_mem_insertMany_list : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α},
  k ∈ m.insertMany l → (List.map Prod.fst l).contains k = false → k ∈ m
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.sum_mem : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  {ι : Type w} {t : Finset ι} {f : ι → A}, (∀ x ∈ t, f x ∈ S) → ∑ x ∈ t, f x ∈ S
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.edge_other_incident_set : ∀ {V : Type u} (G : SimpleGraph V) [inst : DecidableEq V] {v : V} {e : Sym2 V} (h : e ∈ G.incidenceSet v),
  e ∈ G.incidenceSet (G.otherVertexOfIncident h)
-- Mathlib.Analysis.Convex.Strong
/-- **Alias** of the reverse direction of `uniformConcaveOn_zero`. -/
ConcaveOn.uniformConcaveOn_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E} {f : E → ℝ},
  ConcaveOn ℝ s f → UniformConcaveOn s 0 f
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.lift_of : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} {H : Type u_2} [inst_1 : Group H] (f : G →* H)
  (x : H) (hx : ∀ (a : ↥A), x * f ↑a = f ↑(φ a) * x) (g : G), (HNNExtension.lift f x hx) (HNNExtension.of g) = f g
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
HurwitzKernelBounds.f_nat.eq_1 : ∀ (k : ℕ) (a t : ℝ) (n : ℕ), HurwitzKernelBounds.f_nat k a t n = (↑n + a) ^ k * Real.exp (-Real.pi * (↑n + a) ^ 2 * t)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
/-- The portion of `SzemerediRegularity.increment` which partitions `U`.  -/
SzemerediRegularity.chunk : {α : Type u_1} →
  [inst : Fintype α] →
    [inst_1 : DecidableEq α] →
      {P : Finpartition Finset.univ} →
        P.IsEquipartition →
          (G : SimpleGraph α) → [DecidableRel G.Adj] → ℝ → {U : Finset α} → U ∈ P.parts → Finpartition U
-- Mathlib.GroupTheory.Index
Subgroup.index_map_dvd : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (H : Subgroup G) {f : G →* G'},
  Function.Surjective ⇑f → (Subgroup.map f H).index ∣ H.index
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.indiscreteTopology : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X] [IndiscreteTopology Y]
  {f : X → Y}, Topology.IsInducing f → IndiscreteTopology X
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
Finset.Nonempty.smul_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : Zero β] [inst_2 : SMulZeroClass α β] {s : Finset α},
  s.Nonempty → s • 0 = 0
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- The sine of an angle in a right-angled triangle as a ratio of sides, version subtracting
vectors.  -/
InnerProductGeometry.sin_angle_sub_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → x ≠ 0 ∨ y ≠ 0 → Real.sin (InnerProductGeometry.angle x (x - y)) = ‖y‖ / ‖x - y‖
-- Mathlib.Analysis.Normed.Group.Quotient
/-- An isometric version of `QuotientGroup.quotientQuotientEquivQuotient`.  -/
QuotientGroup.quotientQuotientIsometryEquivQuotient : {M : Type u_1} →
  [inst : SeminormedCommGroup M] → {S T : Subgroup M} → S ≤ T → (M ⧸ S) ⧸ Subgroup.map (QuotientGroup.mk' S) T ≃ᵢ M ⧸ T
-- Init.System.IO
/-- The child process's standard output handle, if it was configured as `IO.Process.Stdio.piped`, or
`()` otherwise.
 -/
IO.Process.Child.stdout : {cfg : IO.Process.StdioConfig} → IO.Process.Child cfg → cfg.stdout.toHandleType
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Basic
two_mul_natCast_pentagonal : ∀ (k : ℤ), 2 * ↑(pentagonal k) = k * (3 * k - 1)
-- Mathlib.Algebra.Ring.BooleanRing
instBooleanRingPUnit : BooleanRing PUnit.{u_4 + 1}
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- `leftSection` composed with `f` is `pi` composed with `rightSection`  -/
CategoryTheory.IsSplitCoequalizer.leftSection_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z}
  (self : CategoryTheory.IsSplitCoequalizer f g π),
  CategoryTheory.CategoryStruct.comp self.leftSection f = CategoryTheory.CategoryStruct.comp π self.rightSection
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.ae_nonneg_restrict_of_forall_setIntegral_nonneg : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ) →
    (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → 0 ≤ ∫ (x : α) in s, f x ∂μ) →
      ∀ {t : Set α}, MeasurableSet t → μ t ≠ ⊤ → 0 ≤ᵐ[μ.restrict t] f