mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finsupp.Multiset
Finsupp.card_toMultiset : ∀ {α : Type u_1} (f : α →₀ ℕ), (Finsupp.toMultiset f).card = f.sum fun x => id
-- Mathlib.Algebra.BigOperators.Finprod
/-- The product of `f i` over `i ∈ {a, b}`, `a ≠ b`, is equal to `f a * f b`.  -/
finprod_mem_pair : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {a b : α},
  a ≠ b → ∏ᶠ (i : α) (_ : i ∈ {a, b}), f i = f a * f b
-- Mathlib.GroupTheory.QuotientGroup.Basic
/-- If two normal subgroups `M` and `N` of `G` are the same, their quotient groups are
isomorphic.  -/
QuotientAddGroup.quotientAddEquivOfEq : {G : Type u} →
  [inst : AddGroup G] → {M N : AddSubgroup G} → [inst_1 : M.Normal] → [inst_2 : N.Normal] → M = N → G ⧸ M ≃+ G ⧸ N
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Return.mk : {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} →
  {w : ℕ} →
    (result : aig.ExtendingRefVecEntry w) →
      Std.Tactic.BVDecide.BVExpr.Cache (↑result).aig → Std.Tactic.BVDecide.BVExpr.Return aig w
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
QuadraticMap.Equivalent.sigPos_eq : ∀ {R : Type u_1} {M : Type u_2} {M' : Type u_3} [inst : AddCommGroup M] [inst_1 : AddCommGroup M'] [inst_2 : CommRing R]
  [inst_3 : LinearOrder R] [inst_4 : Module R M] {Q : QuadraticForm R M} [inst_5 : Module R M']
  {Q' : QuadraticForm R M'}, QuadraticMap.Equivalent Q Q' → sigPos Q = sigPos Q'
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.norm_prod_eq_sup'_of_pairwise_ne : ∀ {M : Type u_1} {ι : Type u_2} [inst : SeminormedCommGroup M] [IsUltrametricDist M] {s : Finset ι} {f : ι → M}
  (hs' : s.Nonempty), ((↑s).Pairwise fun i j => ‖f i‖ ≠ ‖f j‖) → ‖∏ i ∈ s, f i‖ = s.sup' hs' fun i => ‖f i‖
-- Init.Data.String.Defs
/-- Accesses the indicated byte in the UTF-8 encoding of a string slice.

At runtime, this function is implemented by efficient, constant-time code.
 -/
String.Slice.getUTF8Byte : (s : String.Slice) → (p : String.Pos.Raw) → p < s.rawEndPos → UInt8
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Append.0.Std.IterM.toArray_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) (it' : Std.IterM m β)
  (out : β) (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_le_iff_le_mul' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LE α] [MulLeftMono α] {a b c : α}, a / b ≤ c ↔ a ≤ b * c
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.kahler_comp_rightAngleRotation' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), -(Complex.I * (Complex.I * (o.kahler x) y)) = (o.kahler x) y
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.instInhabitedGCongrLemma.default : Mathlib.Tactic.GCongr.GCongrLemma
-- Init.Grind.Config
/-- Maximum degree of polynomials processed by the `ring` solver.
 -/
Lean.Grind.Config.ringMaxDegree : Lean.Grind.Config → ℕ
-- Mathlib.CategoryTheory.Limits.Sifted
CategoryTheory.IsSifted.colim_preservesLimitsOfShape_pempty_of_isSifted : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] [CategoryTheory.IsSifted C],
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) CategoryTheory.Limits.colim
-- Mathlib.Algebra.Group.Hom.Basic
OneHom.inv_apply : ∀ {M : Type u_8} {N : Type u_9} [inst : One M] [inst_1 : InvOneClass N] (f : OneHom M N) (x : M), f⁻¹ x = (f x)⁻¹
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.contains_alter_of_beq_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : Option β → Option β},
  (k == k') = false → (Std.ExtDHashMap.Const.alter m k f).contains k' = m.contains k'
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.uniformContinuous : ∀ {F : Type u_1} {β : Type v} {γ : Type w} [inst : UniformSpace β] [inst_1 : UniformSpace γ] [inst_2 : Zero γ]
  [inst_3 : FunLike F β γ] [ZeroAtInftyContinuousMapClass F β γ] (f : F), UniformContinuous ⇑f
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip.0.Std.IterM.step_intermediateZip.match_3.eq_2 : ∀ {α₁ β₁ : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₁ m β₁]
  (motive : Option { out // ∃ it, it.IsPlausibleOutput out } → Sort u_3)
  (out₁ : { out // ∃ it, it.IsPlausibleOutput out }) (h_1 : Unit → motive none)
  (h_2 : (out₁ : { out // ∃ it, it.IsPlausibleOutput out }) → motive (some out₁)),
  (match some out₁ with
    | none => h_1 ()
    | some out₁ => h_2 out₁) =
    h_2 out₁
-- Mathlib.Computability.AkraBazzi.AkraBazzi
AkraBazziRecurrence.isTheta_deriv_rpow_p_mul_one_add_smoothingFn : ∀ {p : ℝ},
  p ≠ 0 →
    (fun x => ‖deriv (fun z => z ^ p * (1 + AkraBazziRecurrence.smoothingFn z)) x‖) =Θ[Filter.atTop] fun z =>
      z ^ (p - 1)
-- Std.Time.Date.Unit.Month
_private.Std.Time.Date.Unit.Month.0.Std.Time.Month.Ordinal.cumulativeSizes.eq_1 : Std.Time.Month.Ordinal.cumulativeSizes✝ =
  ⟨#[0, 31, 59, 90, 120, 151, 181, 212, 243, 273, 304, 334], Std.Time.Month.Ordinal.cumulativeSizes._proof_1✝⟩
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
cotTerm_identity : ∀ {x : ℂ}, x ∈ Complex.integerComplement → ∀ (n : ℕ), cotTerm x n = 2 * x * (1 / ((x + (↑n + 1)) * (x - (↑n + 1))))
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.ofSubsingleton_apply_apply : ∀ (R : Type u) {ι : Type v} (M₂ : Type w₂) (M₃ : Type w₃) [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] [inst_5 : TopologicalSpace M₂]
  [inst_6 : TopologicalSpace M₃] [inst_7 : Subsingleton ι] (i : ι) (f : M₂ →L[R] M₃) (x : ι → M₂),
  ((ContinuousMultilinearMap.ofSubsingleton R M₂ M₃ i) f) x = f (x i)
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instNontrivial : ∀ (A : Type u_3) (E : Type u_4) [Nontrivial E], Nontrivial (WithCStarModule A E)
-- Mathlib.CategoryTheory.Category.ULift
/-- One half of the equivalence between `C` and `ULiftHom C`.  -/
CategoryTheory.ULiftHom.up : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor C (CategoryTheory.ULiftHom C)
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHomClass.eq_1 : ∀ (F : Type u_8) (M : Type u_9) (X : Type u_10) (Y : Type u_11) [inst : VAdd M X] [inst_1 : VAdd M Y]
  [inst_2 : FunLike F X Y], AddActionHomClass F M X Y = AddActionSemiHomClass F id X Y
-- Std.Data.DTreeMap.Raw.Lemmas
_private.Std.Data.DTreeMap.Raw.Lemmas.0.Std.DTreeMap.Raw.equiv_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp},
  t₁.Equiv t₂ ↔ t₁.inner.Equiv t₂.inner
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.norm : ∀ {α : Type u_1} {x : MeasurableSpace α} {β : Type u_5} [inst : SeminormedAddCommGroup β] {f : α → β},
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => ‖f x‖
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.commSemiring : {R : Type u} → [inst : CommSemiring R] → CommSemiring (Polynomial R)
-- Lean.Meta.Transform
Lean.instInhabitedTransformStep : Inhabited Lean.TransformStep
-- Mathlib.Data.List.Sigma
List.Perm.kunion_right : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {l₁ l₂ : List (Sigma β)},
  l₁.Perm l₂ → ∀ (l : List (Sigma β)), (l₁.kunion l).Perm (l₂.kunion l)
-- Mathlib.Algebra.Ring.BooleanRing
Bool.sub_eq_xor : ∀ (b c : Bool), b - c = (b ^^ c)
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
lineMap_mono_left : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : PartialOrder k] [IsOrderedRing k] [inst_3 : AddCommGroup E]
  [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E] [IsStrictOrderedModule k E] {a a' b : E}
  {r : k}, a ≤ a' → r ≤ 1 → (AffineMap.lineMap a b) r ≤ (AffineMap.lineMap a' b) r
-- Mathlib.Data.Set.Basic
Set.inter_eq_left : ∀ {α : Type u} {s t : Set α}, s ∩ t = s ↔ s ⊆ t
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instOne : {Γ : Type u_1} →
  {R : Type u_3} → [Zero Γ] → [inst : PartialOrder Γ] → [inst_1 : Zero R] → [One R] → One (HahnSeries Γ R)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
DifferentiableWithinAt.cpow_const : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {s : Set E} {c : ℂ},
  DifferentiableWithinAt ℂ f s x → f x ∈ Complex.slitPlane → DifferentiableWithinAt ℂ (fun x => f x ^ c) s x
-- Mathlib.Topology.Sequences
Continuous.seqContinuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → SeqContinuous f
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_lt_two_mul : ∀ {k : Type u_4} [inst : Field k] [inst_1 : LinearOrder k] [IsOrderedRing k] [inst_3 : FloorRing k] {a : k},
  2⁻¹ < a → ↑⌈a⌉ < 2 * a
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.direction_orthRadius_le_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p q : P},
  (s.orthRadius p).direction ≤ (s.orthRadius q).direction ↔ ∃ r, q -ᵥ s.center = r • (p -ᵥ s.center)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.instRing : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (Q : QuadraticForm R M) → Ring (CliffordAlgebra Q)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.leftHomologyMap_congr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology],
  CategoryTheory.ShortComplex.leftHomologyMap φ₁ = CategoryTheory.ShortComplex.leftHomologyMap φ₂
-- Mathlib.Analysis.Normed.Module.Bases
/-- The `nnnorm` of any projection is bounded by the basis constant.  -/
UnconditionalSchauderBasis.nnnorm_proj_le_nnnormProjBound : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {β : Type u_3} (b : UnconditionalSchauderBasis β 𝕜 X) [CompleteSpace X] (A : Finset β),
  ‖GeneralSchauderBasis.proj b A‖₊ ≤ b.nnnormProjBound
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
_private.Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes.0.CategoryTheory.Limits.WalkingPair.swap.match_1.eq_1 : ∀ (motive : CategoryTheory.Limits.WalkingPair → Sort u_1) (h_1 : Unit → motive CategoryTheory.Limits.WalkingPair.left)
  (h_2 : Unit → motive CategoryTheory.Limits.WalkingPair.right),
  (match CategoryTheory.Limits.WalkingPair.left with
    | CategoryTheory.Limits.WalkingPair.left => h_1 ()
    | CategoryTheory.Limits.WalkingPair.right => h_2 ()) =
    h_1 ()
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_eq_back?_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.maxKey? = t.keysArray.back?
-- Init.Data.Nat.Bitwise.Lemmas
Nat.zero_or : ∀ (x : ℕ), 0 ||| x = x
-- Init.Data.UInt.Lemmas
UInt16.ofNatLT_mod : ∀ {a b : ℕ} (ha : a < 2 ^ 16) (hb : b < 2 ^ 16), UInt16.ofNatLT (a % b) ⋯ = UInt16.ofNatLT a ha % UInt16.ofNatLT b hb
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.comp_snd_assoc : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  {X Y Z : CategoryTheory.Limits.CategoricalPullback F G} (f : X.Hom Y) (g : Y.Hom Z) {Z_1 : C} (h : Z.snd ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).snd h =
    CategoryTheory.CategoryStruct.comp f.snd (CategoryTheory.CategoryStruct.comp g.snd h)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The union of all closed cells equals `C`. Use `CWComplex.union` instead.  -/
Topology.CWComplex.union' : ∀ {X : Type u} {inst : TopologicalSpace X} {C : Set X} [self : Topology.CWComplex C],
  ⋃ n, ⋃ j, ↑(Topology.CWComplex.map n j) '' Metric.closedBall 0 1 = C
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.referencesProvider : Lean.Lsp.ServerCapabilities → Bool
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.AlmostIntegral
IsAlmostIntegral.isIntegral_of_nonZeroDivisors_le_comap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {s : S},
  IsAlmostIntegral R s →
    ∀ [IsNoetherianRing R], nonZeroDivisors R ≤ Submonoid.comap (algebraMap R S) (nonZeroDivisors S) → IsIntegral R s
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
/-- The convergents coincide in the expected way at the squashed position if the partial denominator
at the squashed position is not zero.  -/
GenContFract.succ_nth_conv_eq_squashGCF_nth_conv : ∀ {K : Type u_1} {n : ℕ} {g : GenContFract K} [inst : Field K],
  (∀ {b : K}, g.partDens.get? n = some b → b ≠ 0) → g.convs (n + 1) = (g.squashGCF n).convs n
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardDistinctFactors_prod : ∀ {ι : Type u_2} {s : Finset ι} {f : ι → ℕ},
  (↑s).Pairwise (Function.onFun Nat.Coprime f) →
    ArithmeticFunction.cardDistinctFactors (∏ i ∈ s, f i) = ∑ i ∈ s, ArithmeticFunction.cardDistinctFactors (f i)
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.vadd_univ : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : AddGroup α] [inst_2 : AddAction α β]
  [inst_3 : Fintype β] {s : Finset α}, s.Nonempty → s +ᵥ Finset.univ = Finset.univ
-- Mathlib.Data.Fintype.Quotient
Trunc.finChoice_eq : ∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι] {α : ι → Sort u_2} (f : (i : ι) → α i),
  (Trunc.finChoice fun i => Trunc.mk (f i)) = Trunc.mk f
-- Mathlib.Topology.Metrizable.Basic
TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace : ∀ {X : Type u_5} {t : TopologicalSpace X} [self : TopologicalSpace.MetrizableSpace X],
  TopologicalSpace.PseudoMetrizableSpace X
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_injective : Function.Injective Real.Angle.toReal
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.smul_restrictAppIso_hom_apply : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules)
  (U : X.Opens) (r : ↑(X.presheaf.obj (Opposite.op U))) (x : ↑((M.restrict f).presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).hom) (r • x) =
    (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appIso f U).inv) r •
      (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).hom) x
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.mkₐ.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R),
  AdicCompletion.mkₐ I = AlgHom.ofLinearMap (AdicCompletion.mk I R) ⋯ ⋯
-- Init.Data.UInt.Basic
instLEUInt16 : LE UInt16
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- An isomorphism to describe the action of `LeftExtension.postcompose₂` on terms of the form
`LeftExtension.mk _ α`.  -/
CategoryTheory.Functor.LeftExtension.postcompose₂ObjMkIso : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      {D' : Type u_5} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] →
                {L : CategoryTheory.Functor C D} →
                  {F : CategoryTheory.Functor C H} →
                    (G : CategoryTheory.Functor H D') →
                      {F' : CategoryTheory.Functor D H} →
                        (α : F ⟶ L.comp F') →
                          (CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).obj
                              (CategoryTheory.Functor.LeftExtension.mk F' α) ≅
                            CategoryTheory.Functor.LeftExtension.mk (F'.comp G)
                              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α G)
                                (L.associator F' G).hom)
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_inter_Icc_eq_singleton : ∀ {α : Type u_1} [inst : PartialOrder α] {a b c : α}, a ≤ b → b ≤ c → Set.Icc a b ∩ Set.Icc b c = {b}
-- Batteries.Tactic.Alias
Batteries.Tactic.Alias.instInhabitedAliasInfo.default : Batteries.Tactic.Alias.AliasInfo
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.neg_ofPred : ∀ {α : Type u_2} [inst : Neg α] (p : α → Prop), -{x | p x} = {x | p (-x)}
-- Mathlib.Data.Set.Piecewise
Set.piecewise_eq_of_mem : ∀ {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f g : (i : α) → δ i) [inst : (j : α) → Decidable (j ∈ s)] {i : α},
  i ∈ s → s.piecewise f g i = f i
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.instCategory : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → CategoryTheory.Category.{v₁, max u₁ v₁} (CategoryTheory.Center C)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
Left.one_le_pow_of_le : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftMono M] {a : M}, 1 ≤ a → ∀ (n : ℕ), 1 ≤ a ^ n
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.prependMapGE.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (lowerBound : α) (it : Std.DTreeMap.Internal.Zipper α β) (sz : ℕ) (k : α)
  (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Zipper.prependMapGE (Std.DTreeMap.Internal.Impl.inner sz k v l r) lowerBound it =
    match compare lowerBound k with
    | Ordering.lt => Std.DTreeMap.Internal.Zipper.prependMapGE l lowerBound (Std.DTreeMap.Internal.Zipper.cons k v r it)
    | Ordering.eq => Std.DTreeMap.Internal.Zipper.cons k v r it
    | Ordering.gt => Std.DTreeMap.Internal.Zipper.prependMapGE r lowerBound it
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.exists_eq_ofArrows : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X),
  ∃ ι Y f, R = CategoryTheory.Presieve.ofArrows Y f
-- Init.Notation
/-- Maximum precedence used in term parsers, in particular for terms in
function position (`ident`, `paren`, ...)
 -/
precMax : Lean.ParserDescr
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- Converse of "angles in same segment are equal" and "opposite angles of a cyclic quadrilateral
add to π", for oriented angles mod π, with a "concyclic or collinear" conclusion.  -/
EuclideanGeometry.concyclic_or_collinear_of_two_zsmul_oangle_eq : ∀ {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},
  2 • EuclideanGeometry.oangle p₁ p₂ p₄ = 2 • EuclideanGeometry.oangle p₁ p₃ p₄ →
    EuclideanGeometry.Concyclic {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}
-- Aesop.RuleSet.Filter
Aesop.RuleFilter.name : Aesop.RuleFilter → Lean.Name
-- Mathlib.Topology.Constructions
instTopologicalSpaceSigma : {ι : Type u_5} → {X : ι → Type v} → [t₂ : (i : ι) → TopologicalSpace (X i)] → TopologicalSpace (Sigma X)
-- Lean.Meta.Tactic.Grind.Types
/-- Assign the `mvarId` using the given proof of `False`.
If type of `mvarId` is not `False`, then use `False.elim`.
 -/
Lean.MVarId.assignFalseProof : Lean.MVarId → Lean.Expr → Lean.MetaM Unit
-- Mathlib.NumberTheory.ModularForms.LFunction
_private.Mathlib.NumberTheory.ModularForms.LFunction.0.ModularForm.isBigO_comp_ofComplex_I_mul_sub_valueAtInfty : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic] {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] (f : F)
  [ModularFormClass F Γ k] (r : ℝ),
  (fun t => f (↑UpperHalfPlane.ofComplex (Complex.I * ↑t)) - UpperHalfPlane.valueAtInfty ⇑f) =O[Filter.atTop] fun t =>
    t ^ r
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM0to1.tr.match_1.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} (motive : Option (Λ × Turing.TM0.Stmt Γ) → Sort u_3) (q' : Λ) (s : Turing.TM0.Stmt Γ)
  (h_1 : Unit → motive none) (h_2 : (q' : Λ) → (s : Turing.TM0.Stmt Γ) → motive (some (q', s))),
  (match some (q', s) with
    | none => h_1 ()
    | some (q', s) => h_2 q' s) =
    h_2 q' s
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
/-- `HasMFDerivWithinAt I I' f s x f'` indicates that the function `f` between manifolds
has, at the point `x` and within the set `s`, the derivative `f'`. Here, `f'` is a continuous linear
map from the tangent space at `x` to the tangent space at `f x`.

This is a generalization of `HasFDerivWithinAt` to manifolds (as indicated by the prefix `m`).
The order of arguments is changed as the type of the derivative `f'` depends on the choice of `x`.

We require continuity in the definition, as otherwise points close to `x` in `s` could be sent by
`f` outside of the chart domain around `f x`. Then the chart could do anything to the image points,
and in particular by coincidence `writtenInExtChartAt I I' x f` could be differentiable, while
this would not mean anything relevant.  -/
HasMFDerivWithinAt : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {E' : Type u_5} →
                        [inst_6 : NormedAddCommGroup E'] →
                          [inst_7 : NormedSpace 𝕜 E'] →
                            {H' : Type u_6} →
                              [inst_8 : TopologicalSpace H'] →
                                (I' : ModelWithCorners 𝕜 E' H') →
                                  {M' : Type u_7} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        (f : M → M') →
                                          Set M → (x : M) → (TangentSpace I x →L[𝕜] TangentSpace I' (f x)) → Prop
-- Mathlib.Data.Nat.Prime.Defs
Nat.Prime.minFac_eq : ∀ {p : ℕ}, Nat.Prime p → p.minFac = p
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instNegCoeOfNegMemClass.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → Neg (R i)] [inst_2 : ∀ (i : ι), NegMemClass (S i) (R i)],
  RestrictedProduct.instNegCoeOfNegMemClass R = { neg := fun x => ⟨fun i => -x i, ⋯⟩ }
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
_private.Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion.0.Tactic.ComputeAsymptotics.Seq.FriendlyOperation.exists_fixed_point.match_1.eq_2 : ∀ {α : Type u_3} {β : Type u_1} {γ : Type u_2} (motive : Option (α × γ × β) → Sort u_4) (a : α) (c : γ) (b' : β)
  (h_1 : Unit → motive none) (h_2 : (a : α) → (c : γ) → (b' : β) → motive (some (a, c, b'))),
  (match some (a, c, b') with
    | none => h_1 ()
    | some (a, c, b') => h_2 a c b') =
    h_2 a c b'