mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Tree.Data
Aesop.GoalUnsafe.brecOn_5.eq : ∀ {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 : Option (IO.Ref Aesop.RappUnsafe))
  (F_1 : (t : Aesop.GoalUnsafe) → t.below → motive_1 t) (F_2 : (t : Aesop.MVarClusterUnsafe) → t.below → motive_2 t)
  (F_3 : (t : Aesop.RappUnsafe) → t.below → motive_3 t)
  (F_4 : (t : Aesop.GoalData Aesop.RappUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_1 t → motive_4 t)
  (F_5 : (t : Aesop.MVarClusterData Aesop.GoalUnsafe Aesop.RappUnsafe) → Aesop.GoalUnsafe.below_2 t → motive_5 t)
  (F_6 : (t : Aesop.RappData Aesop.GoalUnsafe Aesop.MVarClusterUnsafe) → Aesop.GoalUnsafe.below_3 t → motive_6 t)
  (F_7 : (t : Array (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_4 t → motive_7 t)
  (F_8 : (t : Option (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_5 t → motive_8 t)
  (F_9 : (t : Array (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_6 t → motive_9 t)
  (F_10 : (t : Array (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_7 t → motive_10 t)
  (F_11 : (t : List (IO.Ref Aesop.RappUnsafe)) → Aesop.GoalUnsafe.below_8 t → motive_11 t)
  (F_12 : (t : List (IO.Ref Aesop.GoalUnsafe)) → Aesop.GoalUnsafe.below_9 t → motive_12 t)
  (F_13 : (t : List (IO.Ref Aesop.MVarClusterUnsafe)) → Aesop.GoalUnsafe.below_10 t → motive_13 t),
  Aesop.GoalUnsafe.brecOn_5 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13 =
    F_8 t (Aesop.GoalUnsafe.brecOn_5.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 F_10 F_11 F_12 F_13).2
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- The sequence is strictly decreasing at infinite places distinct from `w₁`.  -/
NumberField.Units.dirichletUnitTheorem.seq_decreasing : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (w₁ : NumberField.InfinitePlace K) {B : ℕ}
  (hB : NumberField.mixedEmbedding.minkowskiBound K 1 < ↑(NumberField.mixedEmbedding.convexBodyLTFactor K) * ↑B)
  {n m : ℕ},
  n < m →
    ∀ (w : NumberField.InfinitePlace K),
      w ≠ w₁ →
        w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(NumberField.Units.dirichletUnitTheorem.seq K w₁ hB m)) <
          w ((algebraMap (NumberField.RingOfIntegers K) K) ↑(NumberField.Units.dirichletUnitTheorem.seq K w₁ hB n))
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- Eta-expanded form of `AEMeasurable.div` -/
AEMeasurable.fun_div : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace G] [inst_1 : Div G] {m : MeasurableSpace α} {f g : α → G}
  {μ : MeasureTheory.Measure α} [MeasurableDiv₂ G],
  AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (fun i => f i / g i) μ
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- According to `UpwardEnumerable.LT`, `a` is less than `b` if `b` is a proper transitive successor of
`a`. 'Proper' means that `b` is the `n`-th successor of `a`, where `n > 0`.

Given `LawfulUpwardEnumerable α`, no element of `α` is less than itself.
 -/
Std.PRange.UpwardEnumerable.LT : {α : Type u} → [Std.PRange.UpwardEnumerable α] → α → α → Prop
-- Mathlib.Order.Monotone.Basic
strictAnti_nat_of_succ_lt : ∀ {α : Type u} [inst : Preorder α] {f : ℕ → α}, (∀ (n : ℕ), f (n + 1) < f n) → StrictAnti f
-- Std.Sat.CNF.Basic
Std.Sat.CNF.Clause.instDecidableMemOfDecidableEq : {α : Type u_1} → {v : α} → {c : Std.Sat.CNF.Clause α} → [DecidableEq α] → Decidable (Std.Sat.CNF.Clause.Mem v c)
-- Mathlib.Data.Setoid.Basic
/-- The infimum of 2 equivalence relations r and s is the same relation as the infimum
of the underlying binary operations.  -/
Setoid.inf_def : ∀ {α : Type u_1} {r s : Setoid α}, ⇑(r ⊓ s) = ⇑r ⊓ ⇑s
-- Mathlib.Data.Set.Basic
instCoeTCElem : {α : Type u} → (s : Set α) → CoeTC (↑s) α
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLT.eq_def : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k : α)
  (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : x.Ordered) (x_2 : ∃ a ∈ x, compare a k = Ordering.lt),
  Std.DTreeMap.Internal.Impl.Const.getEntryLT k x x_1 x_2 =
    match x, x_1, x_2 with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => ⋯.elim
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he =>
      if hkky : compare k ky = Ordering.gt then Std.DTreeMap.Internal.Impl.Const.getEntryLTD k r (ky, y)
      else Std.DTreeMap.Internal.Impl.Const.getEntryLT k l ⋯ ⋯
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_subset_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, a₂ < a₁ → b₁ < b₂ → Set.Icc a₁ b₁ ⊆ Set.Ioo a₂ b₂
-- Mathlib.Topology.Semicontinuity.Basic
/-- The sum of two lower semicontinuous functions is lower semicontinuous. Formulated with
`[ContinuousAdd]`. The primed version of the lemma uses an explicit continuity assumption on
addition, for application to `EReal`.  -/
LowerSemicontinuousOn.add : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_5} [inst_1 : AddCommMonoid γ]
  [inst_2 : LinearOrder γ] [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ]
  {f g : α → γ}, LowerSemicontinuousOn f s → LowerSemicontinuousOn g s → LowerSemicontinuousOn (fun z => f z + g z) s
-- Std.Data.TreeSet.Basic
/-- Tries to retrieve the smallest element that is greater than the given element,
returning `none` if no such element exists.
 -/
Std.TreeSet.getGT? : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → α → Option α
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
/-- A subcomplex of a finite CW complex is again finite.  -/
Topology.RelCWComplex.Subcomplex.finite_subcomplex_of_finite : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D]
  [Topology.RelCWComplex.Finite C] (E : Topology.RelCWComplex.Subcomplex C), Topology.RelCWComplex.Finite ↑E
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.typesGlue_eval : ∀ {S : CategoryTheory.Functor Type uᵒᵖ (Type u)}
  {hs : CategoryTheory.Presieve.IsSheaf CategoryTheory.typesGrothendieckTopology S} {α : Type u}
  (s : S.obj (Opposite.op α)),
  CategoryTheory.typesGlue S hs α ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.eval S α s)) = s
-- Mathlib.Combinatorics.Quiver.Basic
Quiver.homOfEq_heq_right_iff : ∀ {V : Type u_1} [inst : Quiver V] {X Y X' Y' : V} (f : X ⟶ Y) (g : X' ⟶ Y') (hX : X' = X) (hY : Y' = Y),
  f ≍ Quiver.homOfEq g hX hY ↔ f ≍ g
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.smul_def : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : ContinuousAdd M₁] (f : M₁ →L[R₁] M₁) (a : M₁), f • a = f a
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
/-- The family `charPoly he hL w, w : W` separates points in `V`.  -/
BoundedContinuousFunction.separatesPoints_charPoly : ∀ {V : Type u_1} {W : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] [inst_2 : TopologicalSpace V]
  [inst_3 : AddCommGroup W] [inst_4 : Module ℝ W] [inst_5 : TopologicalSpace W] {e : AddChar ℝ Circle}
  {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} (he : Continuous ⇑e),
  e ≠ 1 →
    ∀ (hL : Continuous fun p => (L p.1) p.2),
      (∀ (v : V), v ≠ 0 → L v ≠ 0) →
        (StarSubalgebra.map (BoundedContinuousFunction.toContinuousMapStarₐ ℂ)
            (BoundedContinuousFunction.charPoly he hL)).SeparatesPoints
-- Init.Data.List.Lemmas
List.forall_mem_flatMap : ∀ {β : Type u_1} {α : Type u_2} {p : β → Prop} {l : List α} {f : α → List β},
  (∀ x ∈ List.flatMap f l, p x) ↔ ∀ a ∈ l, ∀ b ∈ f a, p b
-- Mathlib.Algebra.Homology.ShortComplex.Ab
CategoryTheory.ShortComplex.ShortExact.ab_surjective_g : ∀ {S : CategoryTheory.ShortComplex Ab}, S.ShortExact → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom S.g)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.isLongestMatchAtChain_iff_toList : ∀ {p : Char → Bool} {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAtChain p pos pos' ↔
    ∃ (h : pos ≤ pos'), ∀ c ∈ (s.slice pos pos' h).copy.toList, p c = true
-- Mathlib.Topology.Connected.Basic
Continuous.image_connectedComponent_subset : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Continuous f → ∀ (a : α), f '' connectedComponent a ⊆ connectedComponent (f a)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.ofLeGe : Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.instSMulOfIsScalarTower : (R : Type u) →
  (X : Type v) →
    [inst : CommRing R] →
      {S : Type u_1} →
        [inst_1 : Monoid S] → [inst_2 : DistribMulAction S R] → [IsScalarTower S R R] → SMul S (FreeLieAlgebra R X)
-- Std.Http.Data.Method
Std.Http.Method.mkactivity.sizeOf_spec : sizeOf Std.Http.Method.mkactivity = 1
-- Mathlib.Algebra.Group.Invertible.Defs
mul_invOf_cancel_left : ∀ {α : Type u} [inst : Monoid α] (a b : α) [inst_1 : Invertible a], a * (⅟a * b) = b
-- Init.Try
/-- If `targetOnly` is `true`, `try?` collects information using the goal target only.  -/
Lean.Try.Config.targetOnly : Lean.Try.Config → Bool
-- Mathlib.NumberTheory.Padics.PadicNumbers
_private.Mathlib.NumberTheory.Padics.PadicNumbers.0.PadicSeq.norm_eq_of_equiv_aux : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {f g : PadicSeq p} (hf : ¬f ≈ 0) (hg : ¬g ≈ 0),
  f ≈ g →
    padicNorm p (↑f (PadicSeq.stationaryPoint hf)) ≠ padicNorm p (↑g (PadicSeq.stationaryPoint hg)) →
      padicNorm p (↑g (PadicSeq.stationaryPoint hg)) < padicNorm p (↑f (PadicSeq.stationaryPoint hf)) → False
-- Mathlib.Algebra.Group.Hom.Defs
map_zsmul' : ∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : SubNegMonoid G]
  [inst_2 : SubNegMonoid H] [AddMonoidHomClass F G H] (f : F),
  (∀ (x : G), f (-x) = -f x) → ∀ (a : G) (n : ℤ), f (n • a) = n • f a
-- Std.Data.ExtDHashMap.Basic
/-- Internal implementation detail of the hash map.  -/
Std.ExtDHashMap.mk' : {α : Type u} →
  {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Quotient (Std.DHashMap.isSetoid α β) → Std.ExtDHashMap α β
-- Std.Data.TreeMap.Raw.Basic
/-- Returns the number of mappings present in the map.  -/
Std.TreeMap.Raw.size : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → ℕ
-- Mathlib.RingTheory.Perfection
/-- Perfection of `O/(p)` where `O` is the ring of integers of `K`.  -/
PreTilt : (O : Type u₂) → [CommRing O] → ℕ → Type u₂
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.unitsTypeEquivIsUnitSubmonoid.eq_1 : ∀ {M : Type u_4} [inst : Monoid M],
  Submonoid.unitsTypeEquivIsUnitSubmonoid =
    { toFun := fun x => ⟨↑x, ⋯⟩, invFun := fun x => IsUnit.unit ⋯, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Init.PropLemmas
Decidable.not_forall_not : ∀ {α : Sort u_1} {p : α → Prop} [Decidable (∃ x, p x)], (¬∀ (x : α), ¬p x) ↔ ∃ x, p x
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instIsFilteredCarrierObjPartOrdEmbIsCardinalFiltered : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ),
  CategoryTheory.IsFiltered ↑J.obj
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h_eq_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (ed : X.ExtraDegeneracy) {n : ℕ} (i : Fin (n + 1)) (j : ℕ)
  (hj : autoParam (j = ↑i.rev) CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h_eq._auto_1) {Z : C}
  (h : X.left.obj (Opposite.op { len := n + 1 }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h ed i) h =
    CategoryTheory.CategoryStruct.comp (X.left.δ₀Iter ↑i ⋯)
      (CategoryTheory.CategoryStruct.comp (ed.s j) (CategoryTheory.CategoryStruct.comp (X.left.σ₀Iter ↑i ⋯) h))
-- Mathlib.Combinatorics.Matroid.Map
Matroid.mapEquiv_indep_iff : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : α ≃ β} {I : Set β}, (M.mapEquiv f).Indep I ↔ M.Indep (⇑f.symm '' I)
-- Mathlib.Order.SuccPred.Limit
Order.isSuccPrelimit_bot : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α], Order.IsSuccPrelimit ⊥
-- Mathlib.RingTheory.MvPowerSeries.Substitution
/-- If `σ` is finite, then the nilpotent condition is enough for `HasSubst`  -/
MvPowerSeries.hasSubst_of_constantCoeff_nilpotent : ∀ {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [inst : CommRing S] [Finite σ] {a : σ → MvPowerSeries τ S},
  (∀ (s : σ), IsNilpotent (MvPowerSeries.constantCoeff (a s))) → MvPowerSeries.HasSubst a
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
/-- If `A` is a subalgebra of `S/R`, there is the natural `R`-algebra isomorphism between
`i(R) ⊗[R] A` and `A` induced by multiplication in `S`, here `i : R → S` is the structure map.
This generalizes `Algebra.TensorProduct.lid` as `i(R)` is not necessarily isomorphic to `R`.

This is the `Subalgebra` version of `Submodule.lTensorOne`  -/
Subalgebra.lTensorBot : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] → [inst_2 : Algebra R S] → (A : Subalgebra R S) → TensorProduct R ↥⊥ ↥A ≃ₐ[R] ↥A
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.ConstructibleSetData.toSet.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (S : PrimeSpectrum.ConstructibleSetData R), S.toSet = ⋃ C ∈ S, C.toSet
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Insert an element into the set, preserving balance and the BST property.
If an equivalent element is already in the set, the function `f` is used to generate
the element to insert (being passed the current value in the set).

```
insertWith f 0 {1, 2, 3} = {0, 1, 2, 3}
insertWith f 1 {1, 2, 3} = {f 1, 2, 3}
```

Using a preorder on `ℕ × ℕ` that only compares the first coordinate:

```
insertWith f (1, 1) {(0, 1), (1, 2)} = {(0, 1), f (1, 2)}
insertWith f (3, 1) {(0, 1), (1, 2)} = {(0, 1), (1, 2), (3, 1)}
```  -/
Ordnode.insertWith : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → (α → α) → α → Ordnode α → Ordnode α
-- Mathlib.Algebra.Group.EvenFunction
Function.Even.mul_even : ∀ {α : Type u_1} [inst : Neg α] {R : Type u_3} [inst_1 : Mul R] {f g : α → R},
  Function.Even f → Function.Even g → Function.Even (f * g)
-- Std.Data.TreeSet.Basic
/-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails.  -/
Std.TreeSet.any : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → (α → Bool) → Bool
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.congr : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasSubgaussianMGF X c μ → ∀ {Y : Ω → ℝ}, X =ᵐ[μ] Y → ProbabilityTheory.HasSubgaussianMGF Y c μ
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.mk.sizeOf_spec : ∀ {ι : Type u_1} [inst : SizeOf ι] (Rel : ι → ι → Prop) (next_eq : ∀ {i j j' : ι}, Rel i j → Rel i j' → j = j')
  (prev_eq : ∀ {i i' j : ι}, Rel i j → Rel i' j → i = i'),
  sizeOf { Rel := Rel, next_eq := next_eq, prev_eq := prev_eq } = 1
-- Init.Grind.Norm
Lean.Grind.natCast_add : ∀ (a b : ℕ), ↑(a + b) = ↑a + ↑b
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
Differentiable.continuousAlternatingMap_apply_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {ι : Type u_5} {c : E → F [⋀^ι]→L[𝕜] G} [Finite ι],
  Differentiable 𝕜 c → ∀ (u : ι → F), Differentiable 𝕜 fun y => (c y) u
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.ker_isNormal : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D), (CategoryTheory.Subgroupoid.ker φ).IsNormal
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.shatters_empty : ∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)}, 𝒜.Shatters ∅ ↔ 𝒜.Nonempty
-- Std.Time.Date.PlainDate
/-- Creates a new `PlainDate` by adjusting the year to the given `year` value. The month and day remain unchanged,
and any invalid days for the new year will be handled according to the `clip` behavior.
 -/
Std.Time.PlainDate.withYearClip : Std.Time.PlainDate → Std.Time.Year.Offset → Std.Time.PlainDate
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.mk.sizeOf_spec : ∀ (carrier : Type u) [str : AddCommMonoid carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SSameSide.not_wOppSide : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.SSameSide x y → ¬s.WOppSide x y
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.coconeEquiv_functor_obj_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)} (t : CategoryTheory.Limits.Cocone K),
  (CategoryTheory.WithInitial.coconeEquiv.functor.obj t).pt = t.pt.right
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_insertIfNew : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k a : α} {v : β},
  Std.DTreeMap.Const.get! (t.insertIfNew k v) a =
    if cmp k a = Ordering.eq ∧ k ∉ t then v else Std.DTreeMap.Const.get! t a
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.aestronglyMeasurable : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f : α → ε}, MeasureTheory.Integrable f μ → MeasureTheory.AEStronglyMeasurable f μ
-- Init.Guard
/-- Reducible defeq matching for `guard_hyp` values  -/
Lean.Parser.colonEqR : Lean.ParserDescr
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.eq_zero_or_isMarkovKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  [h : ProbabilityTheory.IsZeroOrMarkovKernel κ], κ = 0 ∨ ProbabilityTheory.IsMarkovKernel κ
-- Mathlib.CategoryTheory.Equivalence
/-- The inverse of the unit of an equivalence of categories.  -/
CategoryTheory.Equivalence.unitInv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (e : C ≌ D) → e.functor.comp e.inverse ⟶ CategoryTheory.Functor.id C
-- Aesop.Forward.Match.Types
/-- The match's level is the index of the maximal slot for which a hyp or
pattern substitution has been added to the match.  -/
Aesop.Match.level : Aesop.Match → Aesop.SlotIndex
-- Mathlib.NumberTheory.RamificationInertia.Basic
/-- If `p` is a maximal ideal of `R`, `S` extends `R` and `P^e` lies over `p`,
then the dimension `[S/(P^e) : R/p]`, as a natural number, is equal to `e * [S/P : R/p]`.  -/
Ideal.finrank_prime_pow_ramificationIdx : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [IsDedekindDomain S],
  P ≠ ⊥ →
    ∀ [p.IsMaximal] [P.IsPrime] (he : p.ramificationIdx' P ≠ 0),
      Module.finrank (R ⧸ p) (S ⧸ P ^ p.ramificationIdx' P) = p.ramificationIdx' P * Module.finrank (R ⧸ p) (S ⧸ P)
-- Mathlib.Algebra.Category.Grp.LargeColimits
/-- A functor `F : J ⥤ AddCommGrpCat.{w}` has a colimit if and only if `Colimits.Quot F` is
`w`-small.
 -/
AddCommGrpCat.hasColimit_iff_small_quot : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J AddCommGrpCat}
  [inst_1 : DecidableEq J], CategoryTheory.Limits.HasColimit F ↔ Small.{w, max u w} (AddCommGrpCat.Colimits.Quot F)
-- Mathlib.GroupTheory.Congruence.Defs
/-- Additive congruence relations preserve negation.  -/
AddCon.neg : ∀ {M : Type u_1} [inst : AddGroup M] (c : AddCon M) {x y : M}, c x y → c (-x) (-y)
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.nontrivial_tensorProduct_iff_right : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_1}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.FaithfullyFlat R M],
  Nontrivial (TensorProduct R M N) ↔ Nontrivial N
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.map_neg : ∀ {Γ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : PartialOrder Γ] [inst_1 : AddGroup R] [inst_2 : AddGroup S]
  (f : R →+ S) {x : HahnSeries Γ R}, (-x).map f = -x.map f
-- Lean.Elab.DefView
Lean.Elab.DefParsed.mk.inj : ∀ {fullHeaderRef : Lean.Syntax}
  {headerProcessedSnap : Lean.Language.SnapshotTask (Option Lean.Elab.HeaderProcessedSnapshot)}
  {fullHeaderRef_1 : Lean.Syntax}
  {headerProcessedSnap_1 : Lean.Language.SnapshotTask (Option Lean.Elab.HeaderProcessedSnapshot)},
  { fullHeaderRef := fullHeaderRef, headerProcessedSnap := headerProcessedSnap } =
      { fullHeaderRef := fullHeaderRef_1, headerProcessedSnap := headerProcessedSnap_1 } →
    fullHeaderRef = fullHeaderRef_1 ∧ headerProcessedSnap = headerProcessedSnap_1
-- Init.Data.Dyadic.Basic
Dyadic.instDecidableLE : DecidableLE Dyadic
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
/-- Given an injective resolution `R` of an object `Y` of an abelian category,
this is a constructor for elements in `Ext X Y n` which takes as an input
a "cocycle" `f : X ⟶ R.cocomplex.X n`.  -/
CategoryTheory.InjectiveResolution.extMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        {X Y : C} →
          (R : CategoryTheory.InjectiveResolution Y) →
            {n : ℕ} →
              (f : X ⟶ R.cocomplex.X n) →
                (m : ℕ) →
                  n + 1 = m →
                    CategoryTheory.CategoryStruct.comp f (R.cocomplex.d n m) = 0 → CategoryTheory.Abelian.Ext X Y n
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_inv : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α], UniformContinuous fun x => x⁻¹
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- (Implementation)
An auxiliary structure used to prove `Scheme.exists_hom_hom_comp_eq_comp_of_locallyOfFiniteType`.
See the section docstring.  -/
AlgebraicGeometry.ExistsHomHomCompEqCompAux : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    {S X : AlgebraicGeometry.Scheme} →
      (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) →
        (D ⟶ (CategoryTheory.Functor.const I).obj S) → (X ⟶ S) → Type (u + 1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
      k ∈ List.map Sigma.fst l → (m.insertMany l).getKey? k' = some k
-- Mathlib.FieldTheory.Fixed
/-- `minpoly G F x` is the minimal polynomial of `(x : F)` over `FixedPoints.subfield G F`.  -/
FixedPoints.minpoly : (G : Type u) →
  [inst : Group G] →
    (F : Type v) →
      [inst_1 : Field F] → [inst_2 : MulSemiringAction G F] → [Fintype G] → F → Polynomial ↥(FixedPoints.subfield G F)
-- Mathlib.Topology.Connected.Clopen
frontier_eq_empty_iff : ∀ {α : Type u} [inst : TopologicalSpace α] [PreconnectedSpace α] {s : Set α}, frontier s = ∅ ↔ s = ∅ ∨ s = Set.univ