mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- Given two distinct paths, `p` and `q`, with same endpoints, we can extract a cycle whose support
is a sublist of `p.support ++ q.support.reverse.tail`.
 -/
SimpleGraph.Walk.IsPath.exists_isCycle_sublist_of_ne : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p q : G.Walk u v},
  p.IsPath →
    q.IsPath →
      p ≠ q → ∃ w ∈ p.support, w ∈ q.support ∧ ∃ c, c.IsCycle ∧ c.support.Sublist (p.support ++ q.support.reverse.tail)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.WorkspaceEditClientCapabilities.mk.injEq : ∀ (documentChanges? : Option Bool) (changeAnnotationSupport? : Option Lean.Lsp.ChangeAnnotationSupport)
  (resourceOperations? : Option (Array String)) (documentChanges?_1 : Option Bool)
  (changeAnnotationSupport?_1 : Option Lean.Lsp.ChangeAnnotationSupport)
  (resourceOperations?_1 : Option (Array String)),
  ({ documentChanges? := documentChanges?, changeAnnotationSupport? := changeAnnotationSupport?,
        resourceOperations? := resourceOperations? } =
      { documentChanges? := documentChanges?_1, changeAnnotationSupport? := changeAnnotationSupport?_1,
        resourceOperations? := resourceOperations?_1 }) =
    (documentChanges? = documentChanges?_1 ∧
      changeAnnotationSupport? = changeAnnotationSupport?_1 ∧ resourceOperations? = resourceOperations?_1)
-- Mathlib.Topology.Constructions
IsClosed.inter_preimage_val_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsClosed s → (IsClosed (Subtype.val ⁻¹' t) ↔ IsClosed (s ∩ t))
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.MapFactorizationData.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} {X Y : C}
  {f : X ⟶ Y} [inst_1 : SizeOf C] [inst_2 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (W₁ x)]
  [inst_3 : ⦃X Y : C⦄ → (x : X ⟶ Y) → SizeOf (W₂ x)] (Z : C) (i : X ⟶ Z) (p : Z ⟶ Y)
  (fac :
    autoParam (CategoryTheory.CategoryStruct.comp i p = f)
      CategoryTheory.MorphismProperty.MapFactorizationData.fac._autoParam)
  (hi : W₁ i) (hp : W₂ p),
  sizeOf { Z := Z, i := i, p := p, fac := fac, hi := hi, hp := hp } =
    1 + sizeOf Z + sizeOf i + sizeOf p + sizeOf fac + sizeOf hi + sizeOf hp
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.hasProductsOfShape_of_hasProducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasProducts C] (J : Type w),
  CategoryTheory.Limits.HasProductsOfShape J C
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_lt_iff : ∀ {a b c : ENNReal}, b ≠ 0 ∨ c ≠ 0 → b ≠ ⊤ ∨ c ≠ ⊤ → (c / b < a ↔ c < a * b)
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.SmallHom.equiv_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) [inst_2 : L.IsLocalization W]
  {X Y Z : C} [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y]
  [inst_4 : CategoryTheory.Localization.HasSmallLocalizedHom W Y Z]
  [inst_5 : CategoryTheory.Localization.HasSmallLocalizedHom W X Z] (α : CategoryTheory.Localization.SmallHom W X Y)
  (β : CategoryTheory.Localization.SmallHom W Y Z),
  (CategoryTheory.Localization.SmallHom.equiv W L) (α.comp β) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.SmallHom.equiv W L) α)
      ((CategoryTheory.Localization.SmallHom.equiv W L) β)
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Equivalences of types induce isomorphisms of complete graphs on those types.  -/
SimpleGraph.Iso.completeGraph : {α : Type u_5} → {β : Type u_6} → α ≃ β → SimpleGraph.completeGraph α ≃g SimpleGraph.completeGraph β
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.MorphismProperty.comap_precoverage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (P : CategoryTheory.MorphismProperty D)
  (F : CategoryTheory.Functor C D), CategoryTheory.Precoverage.comap F P.precoverage = (P.inverseImage F).precoverage
-- Mathlib.Algebra.Quandle
Rack.self_act_invAct_eq : ∀ {R : Type u_1} [inst : Rack R] {x y : R}, Rack.invAct (Shelf.act x x) y = Rack.invAct x y
-- Init.SimpLemmas
and_self_right : ∀ {a b : Prop}, (a ∧ b) ∧ b ↔ a ∧ b
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerMap_map_right : ∀ {α : Type u_3} {β : Type u_5} {β' : Type u_6} {γ : Type u_7} {l : Type u_9} {m : Type u_10} {n : Type u_11}
  {p : Type u_12} (f : α → β' → γ) (g : β → β') (A : Matrix l m α) (B : Matrix n p β),
  Matrix.kroneckerMap f A (B.map g) = Matrix.kroneckerMap (fun a b => f a (g b)) A B
-- Lean.Meta.ArgsPacker
Lean.Meta.ArgsPacker.pack : Lean.Meta.ArgsPacker → Lean.Expr → ℕ → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Sites.PrecoverageToGrothendieck
/-- An auxiliary definition used to define the Grothendieck topology associated to a precoverage.
See `Precoverage.toGrothendieck`.
 -/
CategoryTheory.Precoverage.Saturate : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] → CategoryTheory.Precoverage C → (X : C) → CategoryTheory.Sieve X → Prop
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.nontrivial_iff_nontrivial : ∀ (R : Type u_8) (S : Type u_9) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [h : IsFractionRing R S], Nontrivial R ↔ Nontrivial S
-- Mathlib.Data.Num.Bitwise
Num.shiftr_eq_shiftRight : ∀ (p : Num) (n : ℕ), p.shiftr n = p >>> n
-- Mathlib.Data.Num.Bitwise
/-- Add a bit at the end of a `NzsNum`.  -/
NzsNum.bit : Bool → NzsNum → NzsNum
-- Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs
SimpleGraph.binomialRandom.eq_1 : ∀ (V : Type u_1) (p : ↑unitInterval),
  SimpleGraph.binomialRandom V p =
    MeasureTheory.Measure.comap SimpleGraph.edgeSet (ProbabilityTheory.setBernoulli Sym2.diagSetᶜ p)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.isNone_getElem?_toArray_roo_eq : ∀ {m n : ℤ} {i : ℕ}, ((m<...n).toArray[i]?.isNone = true) = ((n - (m + 1)).toNat ≤ i)
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup of a group inherits a natural power  -/
Subgroup.npow : {G : Type u_1} → [inst : Group G] → (H : Subgroup G) → Pow ↥H ℕ
-- Mathlib.Analysis.Calculus.Deriv.Add
HasDerivWithinAt.const_sub : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜} (c : F),
  HasDerivWithinAt f f' s x → HasDerivWithinAt (fun x => c - f x) (-f') s x
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_inter_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, Set.Ioc a b ∩ Set.Ioi c = Set.Ioc (max a c) b
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.alter.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (l' : Std.DTreeMap.Internal.Impl α β) →
      (motive : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β (l'.size - 1) (l'.size + 1) → Sort u_3) →
        (x : Std.DTreeMap.Internal.Impl.SizedBalancedTree α β (l'.size - 1) (l'.size + 1)) →
          ((d : Std.DTreeMap.Internal.Impl α β) →
              (hd : d.Balanced) →
                (hd'₁ : l'.size - 1 ≤ d.size) →
                  (hd'₂ : d.size ≤ l'.size + 1) →
                    motive { impl := d, balanced_impl := hd, lb_le_size_impl := hd'₁, size_impl_le_ub := hd'₂ }) →
            motive x
-- Lean.MetavarContext
Lean.MetavarContext.collectForwardDeps : Array Lean.Expr → Bool → optParam Bool true → Lean.MetavarContext.MkBindingM (Array Lean.Expr)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
/-- This is the subgroup of `nxn` matrices with entries over a
linear ordered ring and positive determinant.  -/
Matrix.GLPos : (n : Type u) →
  (R : Type v) →
    [inst : DecidableEq n] →
      [inst_1 : Fintype n] →
        [inst_2 : CommRing R] → [inst_3 : LinearOrder R] → [IsStrictOrderedRing R] → Subgroup (GL n R)
-- Mathlib.Algebra.CharP.Defs
CharP.exists : ∀ (R : Type u_1) [inst : NonAssocSemiring R], ∃ p, CharP R p
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.isFirstPatternInaccessible : Lean.Meta.Match.Alt → Bool
-- Init.Data.Vector.Perm
Vector.perm_comm : ∀ {α : Type u_1} {n : ℕ} {xs ys : Vector α n}, xs.Perm ys ↔ ys.Perm xs
-- Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
CategoryTheory.MonoidalClosed.ihomCurry_ihomUncurry : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y z : C)
  [inst_2 : CategoryTheory.Closed x] [inst_3 : CategoryTheory.Closed y]
  [inst_4 : CategoryTheory.Closed (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.ihomCurry x y z)
      (CategoryTheory.MonoidalClosed.ihomUncurry x y z) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj x y ⟹ z)
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.quasiIso_of_epi_of_isIso_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂)
  [CategoryTheory.Epi φ.τ₁] [CategoryTheory.IsIso φ.τ₂] [CategoryTheory.Mono φ.τ₃],
  CategoryTheory.ShortComplex.QuasiIso φ
-- Mathlib.RingTheory.RingHom.StandardSmooth
/-- Helper lemma for the `algebraize` tactic  -/
RingHom.IsStandardSmoothOfRelativeDimension.toAlgebra : ∀ (n : ℕ) {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  RingHom.IsStandardSmoothOfRelativeDimension n f → Algebra.IsStandardSmoothOfRelativeDimension n R S
-- Lean.Elab.Tactic.Omega.Frontend
/-- Pending disjunctions, which we will case split one at a time if we can't get a contradiction.
 -/
Lean.Elab.Tactic.Omega.MetaProblem.disjunctions : Lean.Elab.Tactic.Omega.MetaProblem → List Lean.Expr
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Real.borel_eq_generateFrom_Ioi_rat : borel ℝ = MeasurableSpace.generateFrom (⋃ a, {Set.Ioi ↑a})
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_eq_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : LawfulBEq α]
  {a : α} {h : a ∈ m}, Std.ExtDHashMap.Const.get m a h = m.get a h
-- Mathlib.Combinatorics.Additive.ETransform
/-- This statement is meant to be combined with `le_or_lt_of_add_le_add` and similar lemmas.  -/
Finset.MulETransform.card : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Group α] (e : α) (x : Finset α × Finset α),
  (Finset.mulETransformLeft e x).1.card + (Finset.mulETransformLeft e x).2.card +
      ((Finset.mulETransformRight e x).1.card + (Finset.mulETransformRight e x).2.card) =
    x.1.card + x.2.card + (x.1.card + x.2.card)
-- Mathlib.Order.Partition.Basic
Partition.mem_inf_iff : ∀ {α : Type u_2} [inst : Order.Frame α] {s a : α} {P Q : Partition s}, a ∈ P ⊓ Q ↔ a ≠ ⊥ ∧ ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instMonoid.eq_1 : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S],
  OreLocalization.instMonoid =
    { toMul := OreLocalization.instMul, mul_assoc := ⋯, toOne := OreLocalization.instOne, one_mul := ⋯, mul_one := ⋯,
      npow := OreLocalization.npow, npow_zero := ⋯, npow_succ := ⋯ }
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int32.reduceToNatClampNeg : Lean.Meta.Simp.DSimproc
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- Given three points not equal to `p`, the angle between the first and the second at `p` plus
the angle between the second and the third equals the angle between the first and the third.  -/
EuclideanGeometry.oangle_add : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p p₁ p₂ p₃ : P},
  p₁ ≠ p →
    p₂ ≠ p →
      p₃ ≠ p → EuclideanGeometry.oangle p₁ p p₂ + EuclideanGeometry.oangle p₂ p p₃ = EuclideanGeometry.oangle p₁ p p₃
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Measurable.cos : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ}, Measurable f → Measurable fun x => Real.cos (f x)
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_closure_singleton_self : ∀ {G : Type u_1} [inst : Group G] (x : G), x ∈ Subgroup.closure {x}
-- Mathlib.Data.Rat.Cast.Order
Rat.preimage_cast_Ioo : ∀ {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] (p q : ℚ),
  Rat.cast ⁻¹' Set.Ioo ↑p ↑q = Set.Ioo p q
-- Mathlib.RingTheory.LaurentSeries
/-- Given a Cauchy filter `ℱ` in the Laurent Series and a bound `D`, for almost all series in the
filter the coefficients below `D` coincide with `Cauchy.coeff hℱ`.  -/
LaurentSeries.Cauchy.coeff_eventually_equal : ∀ {K : Type u_2} [inst : Field K] {ℱ : Filter (LaurentSeries K)} (hℱ : Cauchy ℱ) {D : ℤ},
  ∀ᶠ (f : LaurentSeries K) in ℱ, ∀ d < D, LaurentSeries.Cauchy.coeff hℱ d = f.coeff d
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- Composing with a surjective linear map is injective.  -/
AlternatingMap.compLinearMap_injective : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {M₂ : Type u_10} [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] (f : M₂ →ₗ[R] M), Function.Surjective ⇑f → Function.Injective fun g => g.compLinearMap f
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.condExpIndSMul_nonneg : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {hm : m ≤ m0} {E : Type u_10}
  [inst : NormedAddCommGroup E] [inst_1 : PartialOrder E] [inst_2 : NormedSpace ℝ E] [IsOrderedModule ℝ E]
  [MeasureTheory.SigmaFinite (μ.trim hm)] (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : E),
  0 ≤ x → 0 ≤ᵐ[μ] ↑↑(MeasureTheory.condExpIndSMul hm hs hμs x)
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfpFamily_eq_self : ∀ {ι : Type u_1} {f : ι → Ordinal.{u} → Ordinal.{u}} [Small.{u, u_1} ι] {a : Ordinal.{u}},
  (∀ (i : ι), f i a = a) → Ordinal.nfpFamily f a = a
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
/-- For a based functor `F : 𝒳 ⟶ 𝒴`, then whenever an arrow `φ` in `𝒳` lifts some `f` in `𝒮`,
then `F(φ)` also lifts `f`.  -/
CategoryTheory.BasedFunctor.preserves_isHomLift : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴) {R S : 𝒮} {a b : 𝒳.obj} (f : R ⟶ S)
  (φ : a ⟶ b) [𝒳.p.IsHomLift f φ], 𝒴.p.IsHomLift f (F.map φ)
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- When `M` is a `B`-additive module in `D` and `f : A ⟶ B` is a morphism of internal
additive monoid objects, `M` inherits an `A`-additive module structure via
"restriction of scalars", i.e `δ[A, M] = f ⊵ₗ M ≫ δ[B, M]`.  -/
CategoryTheory.AddMod.scalarRestriction : {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.MonoidalLeftAction C D] →
            {A B : C} →
              [inst_4 : CategoryTheory.AddMonObj A] →
                [inst_5 : CategoryTheory.AddMonObj B] →
                  (f : A ⟶ B) →
                    [CategoryTheory.IsAddMonHom f] →
                      (M : D) → [CategoryTheory.AddModObj B M] → CategoryTheory.AddModObj A M
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.equivLim_coherence : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E]
  {i : WithTop (Module.rank F E).ord.ToType} (hi : Order.IsSuccPrelimit i)
  (x : ↥(Field.Emb.Cardinal.filtration i) →ₐ[F] AlgebraicClosure E) (l : ↑(Set.Iio i)),
  ↑((Field.Emb.Cardinal.equivLim hi) x) l = Field.Emb.Cardinal.embFunctor F E ⋯ x
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.ofSlice_lt_iff : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos},
  String.Slice.Pos.ofSlice p < q ↔ ∀ (h₁ : q ≤ p₁), ∃ (h₀ : p₀ ≤ q), p < q.slice p₀ p₁ h₀ h₁
-- Init.Grind.Ring.Basic
/-- The canonical map from the integers is consistent with the canonical map from the natural numbers.  -/
Lean.Grind.Ring.intCast_ofNat : ∀ {α : Type u} [self : Lean.Grind.Ring α] (n : ℕ), ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.ordCompare_minKey!_modify_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.TreeMap.Raw α β compare} [inst_2 : Inhabited α],
  t.WF → ∀ {k : α} {f : β → β}, compare (t.modify k f).minKey! t.minKey! = Ordering.eq
-- Mathlib.Topology.Algebra.UniformConvergence
instGroupUniformOnFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Group β],
  instGroupUniformOnFun =
    { toMonoid := instMonoidUniformOnFun, toInv := instInvUniformOnFun, toDiv := instDivUniformOnFun,
      toZPow := ZPow.ofPow, div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯ }
-- Mathlib.Order.Monotone.Monovary
MonotoneOn.antivaryOn : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι} [inst_2 : LinearOrder ι], MonotoneOn f s → AntitoneOn g s → AntivaryOn f g s
-- Mathlib.CategoryTheory.HomCongr
CategoryTheory.Iso.homCongr_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ Y₁ X₂ Y₂ : C} (α : X₁ ≅ X₂) (β : Y₁ ≅ Y₂),
  (α.homCongr β).symm = α.symm.homCongr β.symm
-- Mathlib.Algebra.Homology.Localization
HomologicalComplexUpToQuasiIso.Qh_inverts_quasiIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.CategoryWithHomology C]
  [inst_3 : (HomologicalComplex.quasiIso C c).HasLocalization] [inst_4 : c.QFactorsThroughHomotopy C],
  (HomotopyCategory.quasiIso C c).IsInvertedBy HomologicalComplexUpToQuasiIso.Qh
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.measurableSet_toMeasurable : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α),
  MeasurableSet (MeasureTheory.toMeasurable μ s)
-- Mathlib.MeasureTheory.VectorMeasure.AddContent
/-- Consider an additive content on a dense ring of sets. Assume that it is dominated by a finite
positive measure. Then it extends to a countably additive vector measure.  -/
MeasureTheory.VectorMeasure.exists_extension_of_isSetRing_of_le_measure_of_dense : ∀ {α : Type u_1} {hα : MeasurableSpace α} {E : Type u_2} [inst : NormedAddCommGroup E] [CompleteSpace E]
  {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {C : Set (Set α)} {m : MeasureTheory.AddContent E C},
  MeasureTheory.IsSetRing C →
    (∀ s ∈ C, MeasurableSet s) →
      (∀ s ∈ C, ‖m s‖ₑ ≤ μ s) →
        (∀ (t : Set α) (ε : ENNReal), MeasurableSet t → 0 < ε → ∃ s ∈ C, μ (symmDiff s t) < ε) →
          ∃ m', (∀ s ∈ C, m' s = m s) ∧ ∀ (s : Set α), ‖m' s‖ₑ ≤ μ s
-- Mathlib.RingTheory.Ideal.Maps
Ideal.exists_of_comap_eq_ker_sup : ∀ {A : Type u_1} {B : Type u_2} [inst : Ring A] [inst_1 : Ring B] (f : A →+* B),
  Function.Surjective ⇑f →
    ∀ {I : Ideal B} {J : Ideal A}, Ideal.comap f I = RingHom.ker f ⊔ J → ∀ {x : B}, x ∈ I → ∃ y ∈ J, f y = x
-- Init.SimpLemmas
implies_true : ∀ (α : Sort u), (∀ (a : α), True) = True
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Increment
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Increment.0.termM : Lean.ParserDescr
-- Mathlib.Logic.Relation
Relation.reflTransGen_le_of_equivalence_of_le : ∀ {α : Type u_1} {r r' : α → α → Prop}, Equivalence r → r' ≤ r → Relation.ReflTransGen r' ≤ r
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.isIso_actionHom : ∀ {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.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {x y : C} {x' y' : D} (f : x ⟶ y) (g : x' ⟶ y')
  [CategoryTheory.IsIso f] [CategoryTheory.IsIso g],
  CategoryTheory.IsIso (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f g)
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.piFinTwo_apply : ∀ (X : Fin 2 → Type u) [inst : (i : Fin 2) → TopologicalSpace (X i)], ⇑(Homeomorph.piFinTwo X) = fun f => (f 0, f 1)
-- Init.Data.String.Lemmas.Order
String.Pos.ne_startPos_of_slice_ne_startPos : ∀ {s : String} {p p₀ p₁ : s.Pos} {h₁ : p₀ ≤ p} {h₂ : p ≤ p₁},
  p.slice p₀ p₁ h₁ h₂ ≠ (s.slice p₀ p₁ ⋯).startPos → p ≠ s.startPos
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The range of a surjective ring homomorphism is the whole of the codomain.  -/
RingHom.range_eq_top_of_surjective : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R →+* S),
  Function.Surjective ⇑f → f.range = ⊤
-- Mathlib.FieldTheory.PolynomialGaloisGroup
Polynomial.Gal.restrictDvd_surjective : ∀ {F : Type u_1} [inst : Field F] {p q : Polynomial F} (hpq : p ∣ q),
  q ≠ 0 → Function.Surjective ⇑(Polynomial.Gal.restrictDvd hpq)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instDivisionMonoid.eq_1 : ∀ {α : Type u_1} [inst : DivisionMonoid α],
  Colex.instDivisionMonoid =
    { toDivInvMonoid := Colex.instDivInvMonoid, inv_inv := ⋯, mul_inv_rev := ⋯, inv_eq_of_mul := ⋯ }
-- Lean.Meta.Tactic.LibrarySearch
/-- A discharger that tries `try?` on the goal.
The proof is wrapped in `Try.Marker` so that suggestions display `(by try?)`
instead of the complex proof term.
Returns `some []` if try? succeeds, `none` otherwise (leaving the goal as a subgoal).
 -/
Lean.Meta.LibrarySearch.tryDischarger : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))
-- Mathlib.Order.GameAdd
Prod.GameAdd.to_sym2 : ∀ {α : Type u_1} {rα : α → α → Prop} {a₁ a₂ b₁ b₂ : α},
  Prod.GameAdd rα rα (a₁, b₁) (a₂, b₂) → Sym2.GameAdd rα s(a₁, b₁) s(a₂, b₂)
-- Init.Data.List.Sublist
List.prefix_iff_getElem : ∀ {α : Type u_1} {l₁ l₂ : List α},
  l₁ <+: l₂ ↔ ∃ (h : l₁.length ≤ l₂.length), ∀ (i : ℕ) (hx : i < l₁.length), l₁[i] = l₂[i]
-- Mathlib.RingTheory.TensorProduct.Maps
/-- If the R- and S-actions on A and B satisfy `CompatibleSMul` both ways,
then `A ⊗[S] B` is canonically isomorphic to `A ⊗[R] B`.  -/
Algebra.TensorProduct.equivOfCompatibleSMul : (R : Type u_3) →
  (S : Type u_4) →
    (T : Type u_5) →
      (A : Type u_6) →
        (B : Type u_7) →
          [inst : CommSemiring R] →
            [inst_1 : CommSemiring S] →
              [inst_2 : CommSemiring T] →
                [inst_3 : Semiring A] →
                  [inst_4 : Semiring B] →
                    [inst_5 : Algebra R A] →
                      [inst_6 : Algebra R B] →
                        [inst_7 : Algebra S A] →
                          [inst_8 : Algebra S B] →
                            [inst_9 : Algebra T A] →
                              [inst_10 : SMulCommClass R T A] →
                                [inst_11 : SMulCommClass S T A] →
                                  [SMulCommClass R S A] →
                                    [TensorProduct.CompatibleSMul R S A B] →
                                      [TensorProduct.CompatibleSMul S R A B] →
                                        TensorProduct S A B ≃ₐ[T] TensorProduct R A B
-- Mathlib.CategoryTheory.IsoCat
CategoryTheory.IsoCat.symm_inverse : ∀ {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] (e : CategoryTheory.IsoCat C D), e.symm.inverse = e.functor
-- Mathlib.Order.Ideal
/-- The ideal is downward closed.  -/
Order.IsIdeal.IsLowerSet : ∀ {P : Type u_2} [inst : LE P] {I : Set P}, Order.IsIdeal I → IsLowerSet I
-- Mathlib.Data.Sum.Order
WithTop.orderIsoSumLexPUnit_symm_inl : ∀ {α : Type u_1} [inst : LE α] (a : α), WithTop.orderIsoSumLexPUnit.symm (toLex (Sum.inl a)) = ↑a