mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Basic
/-- Checks whether a key is present in a map and inserts a value for the key if it was not found.
If the returned `Bool` is `true`, then the returned map is unaltered. If the `Bool` is `false`,
then the returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `contains` followed by `insertIfNew`.
 -/
Std.DTreeMap.containsThenInsertIfNew : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → (a : α) → β a → Bool × Std.DTreeMap α β cmp
-- Mathlib.RingTheory.WittVector.Identities
WittVector.iterate_verschiebung_mul : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p] (x y : WittVector p R) (i j : ℕ),
  (⇑WittVector.verschiebung)^[i] x * (⇑WittVector.verschiebung)^[j] y =
    (⇑WittVector.verschiebung)^[i + j] ((⇑WittVector.frobenius)^[j] x * (⇑WittVector.frobenius)^[i] y)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.leibniz_inv : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {K : Type u_4}
  [inst_3 : Field K] [inst_4 : Module K M] [inst_5 : Algebra R K] (D : Derivation R K M) (a : K), D a⁻¹ = -a⁻¹ ^ 2 • D a
-- Init.Data.UInt.Lemmas
UInt32.lt_of_le_of_ne : ∀ {a b : UInt32}, a ≤ b → a ≠ b → a < b
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
/-- The derived category obtained using the constructed localized category of cochain complexes
with respect to quasi-isomorphisms. This should be used only while proving statements
which do not involve the derived category.  -/
HasDerivedCategory.standard : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [inst_1 : CategoryTheory.Abelian C] → HasDerivedCategory C
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_neg : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] (f : P →ᴬ[R] W), ⇑(-f) = -⇑f
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- If `h` commutes with `f₊ g` and `t` is another left Kan lift of `g` along `f`, then
`t.whisker h` is a left Kan lift of `h ≫ g` along `f`.  -/
CategoryTheory.Bicategory.LanLift.CommuteWith.isKanWhisker : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      (f : b ⟶ a) →
        (g : c ⟶ a) →
          [inst_1 : CategoryTheory.Bicategory.HasLeftKanLift f g] →
            (t : CategoryTheory.Bicategory.LeftLift f g) →
              t.IsKan →
                {x : B} → (h : x ⟶ c) → [CategoryTheory.Bicategory.LanLift.CommuteWith f g h] → (t.whisker h).IsKan
-- Mathlib.CategoryTheory.Elements
/-- Constructor for the type `F.Elements` when `F` is a functor to types.  -/
CategoryTheory.Functor.elementsMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → (F : CategoryTheory.Functor C (Type w)) → (X : C) → F.obj X → F.Elements
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.instAddCommGroupCarrierMkOfSMul' : {R : Type u} →
  [inst : Ring R] → {A : AddCommGrpCat} → (φ : R →+* CategoryTheory.End A) → AddCommGroup ↑(ModuleCat.mkOfSMul' φ)
-- Mathlib.NumberTheory.Real.Irrational
not_irrational_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], ¬Irrational (OfNat.ofNat n)
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomAddAct.vadd_Lp_val : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : VAdd M α] [inst_3 : MeasureTheory.VAddInvariantMeasure M α μ]
  [inst_4 : MeasurableConstVAdd M α] (c : Mᵈᵃᵃ) (f : ↥(MeasureTheory.Lp E p μ)), ↑(c +ᵥ f) = c +ᵥ ↑f
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinOrder.zpow : ∀ {G : Type u_1} [inst : Group G] {x : G}, IsOfFinOrder x → ∀ {i : ℤ}, IsOfFinOrder (x ^ i)
-- Init.Control.State
/-- Modifies the value returned by a computation. Typically used via the `<$>` operator.
 -/
StateT.map : {σ : Type u} → {m : Type u → Type v} → [Monad m] → {α β : Type u} → (α → β) → StateT σ m α → StateT σ m β
-- Mathlib.Data.Set.Lattice
Set.sInter_sdiff_singleton_univ : ∀ {α : Type u_1} (s : Set (Set α)), ⋂₀ (s \ {Set.univ}) = ⋂₀ s
-- Lean.Server.FileWorker.RequestHandling
Lean.Server.FileWorker.handleFoldingRange : Lean.Lsp.FoldingRangeParams → Lean.Server.RequestM (Lean.Server.RequestTask (Array Lean.Lsp.FoldingRange))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_ofList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α},
  (Std.ExtDTreeMap.ofList l cmp).contains k = (List.map Sigma.fst l).contains k
-- Init.Data.BitVec.Lemmas
BitVec.flattenList.eq_2 : ∀ {n : ℕ} (x : BitVec n) (rest : List (BitVec n)),
  BitVec.flattenList (x :: rest) = BitVec.cast ⋯ (x ++ BitVec.flattenList rest)
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.pullbackSpecIso'_symmetry : ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] [inst_3 : Algebra R S]
  [inst_4 : Algebra R T],
  (CategoryTheory.Limits.pullbackSymmetry
          (AlgebraicGeometry.Spec (CommRingCat.of T) ↘ AlgebraicGeometry.Spec (CommRingCat.of R))
          (AlgebraicGeometry.Spec (CommRingCat.of S) ↘ AlgebraicGeometry.Spec (CommRingCat.of R)) ≪≫
        AlgebraicGeometry.pullbackSpecIso' R S T).hom =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.pullbackSpecIso' R T S).hom
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑(Algebra.TensorProduct.comm R S T)))
-- Mathlib.Order.SetNotation
Set.iInf_eq_iInter : ∀ {α : Type u} {ι : Sort v} (s : ι → Set α), iInf s = Set.iInter s
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat
CategoryTheory.Pseudofunctor.mapId'_hom_naturality_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ : B}
  {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₀) (hf : f = CategoryTheory.CategoryStruct.id b₀) (a : X ⟶ Y) {Z : ↑(F.obj b₀)}
  (h : (CategoryTheory.CategoryStruct.id (F.obj b₀)).toFunctor.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map a)
      (CategoryTheory.CategoryStruct.comp ((F.mapId' f hf).hom.toNatTrans.app Y) h) =
    CategoryTheory.CategoryStruct.comp ((F.mapId' f hf).hom.toNatTrans.app X) (CategoryTheory.CategoryStruct.comp a h)
-- Mathlib.Data.List.Defs
/-- Left-biased version of `List.map₂`. `map₂Left f as bs` applies `f` to each pair
`aᵢ ∈ as` and `bᵢ ∈ bs`. If `bs` is shorter than `as`, `f` is applied to `none`
for the remaining `aᵢ`.

```
map₂Left Prod.mk [1, 2] ['a'] = [(1, some 'a'), (2, none)]

map₂Left Prod.mk [1] ['a', 'b'] = [(1, some 'a')]

map₂Left f as bs = (map₂Left' f as bs).fst
```
 -/
List.map₂Left : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → Option β → γ) → List α → List β → List γ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_eq_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {a : α}, a ∉ t → t.getKey! a = default
-- Mathlib.Analysis.RCLike.ContinuousMap
/-- `ContinuousMap.realToRCLike` as a ⋆-algebra map.  -/
ContinuousMap.realToRCLikeStarAlgHom : (X : Type u_1) → (𝕜 : Type u_2) → [inst : TopologicalSpace X] → [inst_1 : RCLike 𝕜] → C(X, ℝ) →⋆ₐ[ℝ] C(X, 𝕜)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_insertListConst_of_contains_eq_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)}
  {k : α} (not_contains : (List.map Prod.fst toInsert).contains k = false)
  {h : Std.Internal.List.containsKey k (Std.Internal.List.insertListConst l toInsert) = true},
  Std.Internal.List.getKey k (Std.Internal.List.insertListConst l toInsert) h = Std.Internal.List.getKey k l ⋯
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.counitIso_aux_one : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C),
  CategoryTheory.MonObj.one =
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.one (CategoryTheory.CategoryStruct.id A.X)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
/-- If two lifts of circle homeomorphisms have the same translation number, then they are
semiconjugate by a `CircleDeg1Lift`. This version uses arguments `f₁ f₂ : CircleDeg1Liftˣ`
to assume that `f₁` and `f₂` are homeomorphisms.  -/
CircleDeg1Lift.units_semiconj_of_translationNumber_eq : ∀ {f₁ f₂ : CircleDeg1Liftˣ}, (↑f₁).translationNumber = (↑f₂).translationNumber → ∃ F, Function.Semiconj ⇑F ⇑↑f₁ ⇑↑f₂
-- Mathlib.Tactic.TermCongr
/-- Returns the proof that `lhs = rhs`. Fails if the `CongrResult` is inapplicable.
Throws an error if the `lhs` and `rhs` have non-defeq types.
If `pf? = none`, this returns the `rfl` proof.  -/
Mathlib.Tactic.TermCongr.CongrResult.eq : Mathlib.Tactic.TermCongr.CongrResult → Lean.MetaM Lean.Expr
-- Std.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.Equiv.drain_eq : ∀ {α₁ α₂ β : Type w} {m : Type w → Type w'} [Std.Iterator α₁ m β] [Std.Iterator α₂ m β] [inst : Std.Iterator α₁ m β]
  [inst_1 : Std.Iterator α₂ m β] [Std.Iterators.Finite α₁ m] [Std.Iterators.Finite α₂ m] [inst_4 : Monad m]
  [inst_5 : LawfulMonad m] [inst_6 : Std.IteratorLoop α₁ m m] [Std.LawfulIteratorLoop α₁ m m]
  [inst_8 : Std.IteratorLoop α₂ m m] [Std.LawfulIteratorLoop α₂ m m] {ita : Std.IterM m β} {itb : Std.IterM m β},
  ita.Equiv itb → ita.drain = itb.drain
-- Mathlib.Analysis.Calculus.FDeriv.Comp
DifferentiableWithinAt.comp' : ∀ {𝕜 : 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] {f : E → F} (x : E) {s : Set E} {g : F → G} {t : Set F},
  DifferentiableWithinAt 𝕜 g t (f x) → DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 (g ∘ f) (s ∩ f ⁻¹' t) x
-- Mathlib.Order.UpperLower.Prod
UpperSet.prod_sup_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (s₁ s₂ : UpperSet α) (t₁ t₂ : UpperSet β),
  s₁ ×ˢ t₁ ⊔ s₂ ×ˢ t₂ = (s₁ ⊔ s₂) ×ˢ (t₁ ⊔ t₂)
-- Mathlib.CategoryTheory.Equivalence
/-- The functor of an equivalence of categories is essentially surjective.  -/
CategoryTheory.Equivalence.essSurj_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} E]
  (e : C ≌ E), e.functor.EssSurj
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitEpi.comp.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z}
  (sef : CategoryTheory.SplitEpi f) (seg : CategoryTheory.SplitEpi g),
  sef.comp seg = { section_ := CategoryTheory.CategoryStruct.comp seg.section_ sef.section_, id := ⋯ }
-- Mathlib.RingTheory.Coprime.Lemmas
IsRelPrime.prod_right : ∀ {α : Type u_2} {I : Type u_1} [inst : CommMonoid α] [DecompositionMonoid α] {x : α} {s : I → α} {t : Finset I},
  (∀ i ∈ t, IsRelPrime x (s i)) → IsRelPrime x (∏ i ∈ t, s i)
-- Mathlib.Analysis.Real.Sqrt
/-- **Cauchy-Schwarz inequality** for finsets using square roots in `ℝ`.  -/
Real.sum_sqrt_mul_sqrt_le : ∀ {ι : Type u_2} {f g : ι → ℝ} (s : Finset ι),
  (∀ (i : ι), 0 ≤ f i) → (∀ (i : ι), 0 ≤ g i) → ∑ i ∈ s, √(f i) * √(g i) ≤ √(∑ i ∈ s, f i) * √(∑ i ∈ s, g i)
-- Mathlib.Analysis.Convex.Strict
StrictConvex.smul_mem_of_zero_mem : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s : Set E} {x : E} [AddRightStrictMono 𝕜],
  StrictConvex 𝕜 s → 0 ∈ s → x ∈ s → x ≠ 0 → ∀ {t : 𝕜}, 0 < t → t < 1 → t • x ∈ interior s
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.mapArrowRight_comp : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {f₁ : CategoryTheory.Arrow C₁}
  {f₃ f₃' : CategoryTheory.Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom)
  {f₃'' : CategoryTheory.Arrow C₃} (sq₁₃'' : G.PullbackObjObj f₁.hom f₃''.hom) (sq : f₃ ⟶ f₃') (sq' : f₃' ⟶ f₃''),
  CategoryTheory.CategoryStruct.comp (sq₁₃.mapArrowRight sq₁₃' sq) (sq₁₃'.mapArrowRight sq₁₃'' sq') =
    sq₁₃.mapArrowRight sq₁₃'' (CategoryTheory.CategoryStruct.comp sq sq')
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.measurable_condDistrib : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {s : Set Ω},
  MeasurableSet s → Measurable fun a => ((ProbabilityTheory.condDistrib Y X μ) (X a)) s
-- Mathlib.Analysis.Normed.Group.Basic
exists_norm_ne_zero : ∀ (E : Type u_5) [inst : SeminormedAddGroup E] [NontrivialTopology E], ∃ x, ‖x‖ ≠ 0
-- Lean.Linter.UnusedVariables
_private.Lean.Linter.UnusedVariables.0.Lean.Linter.UnusedVariables.hasSorry : Lean.Syntax → Bool
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.mk_toType : ∀ (o : Ordinal.{u_1}), Cardinal.mk o.ToType = o.card
-- Mathlib.Order.Interval.Set.Pi
Set.image_mulSingle_Ioc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → One (α i)] (i : ι) (a b : α i),
  Pi.mulSingle i '' Set.Ioc a b = Set.Ioc (Pi.mulSingle i a) (Pi.mulSingle i b)
-- Mathlib.AlgebraicTopology.ModelCategory.Basic
/-- Constructor for `ModelCategory C` which assumes a formulation of axioms
using weak factorization systems.  -/
HomotopicalAlgebra.ModelCategory.mk' : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C] →
      [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] →
        [inst_3 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
          [CategoryTheory.Limits.HasFiniteLimits C] →
            [CategoryTheory.Limits.HasFiniteColimits C] →
              [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty] →
                [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem
                      (HomotopicalAlgebra.trivialFibrations C)] →
                  [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem
                        (HomotopicalAlgebra.fibrations C)] →
                    HomotopicalAlgebra.ModelCategory C
-- Init.Core
not_not_of_not_imp : ∀ {a b : Prop}, ¬(a → b) → ¬¬a
-- Init.Data.List.Pairwise
List.nodup_replicate : ∀ {α : Type u_1} {n : ℕ} {a : α}, (List.replicate n a).Nodup ↔ n ≤ 1
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.CreatesLimitsOfSize.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          autoParam
              ({J : Type w} → [inst_2 : CategoryTheory.Category.{w', w} J] → CategoryTheory.CreatesLimitsOfShape J F)
              CategoryTheory.CreatesLimitsOfSize.CreatesLimitsOfShape._autoParam →
            CategoryTheory.CreatesLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F
-- Init.NotationExtra
/-- Step-wise reasoning over transitive relations.
```
calc
  a = b := pab
  b = c := pbc
  ...
  y = z := pyz
```
proves `a = z` from the given step-wise proofs. `=` can be replaced with any
relation implementing the typeclass `Trans`. Instead of repeating the right-
hand sides, subsequent left-hand sides can be replaced with `_`.
```
calc
  a = b := pab
  _ = c := pbc
  ...
  _ = z := pyz
```
It is also possible to write the *first* relation as `<lhs>\n  _ = <rhs> :=
<proof>`. This is useful for aligning relation symbols, especially on longer
identifiers:
```
calc abc
  _ = bce := pabce
  _ = cef := pbcef
  ...
  _ = xyz := pwxyz
```

`calc` works as a term, as a tactic or as a `conv` tactic.

See [Theorem Proving in Lean 4][tpil4] for more information.

[tpil4]: https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#calculational-proofs
 -/
Lean.calcTactic : Lean.ParserDescr
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.sum_eq_natDegree_of_mem_support_homogenize : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial R) {s : Fin 2 →₀ ℕ},
  s ∈ (p.homogenize p.natDegree).support → s 0 + s 1 = p.natDegree
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- Build an isomorphism in the category `Semigroup` from a `MulEquiv` between `Semigroup`s.  -/
MulEquiv.toSemigrpIso : {X Y : Type u} → [inst : Semigroup X] → [inst_1 : Semigroup Y] → X ≃* Y → (Semigrp.of X ≅ Semigrp.of Y)
-- Mathlib.Geometry.Manifold.Instances.Sphere
/-- The unit circle in `ℂ` is an analytic Lie group.  -/
instLieGroupRealEuclideanSpaceFinOfNatNatModelWithCornersSelfTopWithTopENatCircle : LieGroup (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin 1))) ⊤ Circle
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.compare_maxKeyD_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : β → β} {fallback : α},
  cmp ((Std.DTreeMap.Const.modify t k f).maxKeyD fallback) (t.maxKeyD fallback) = Ordering.eq
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableWithinAt.neg : ∀ {𝕜 : 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 : E → F}
  {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 (-f) s x
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.affineSpan_parallel_iff_vectorSpan_eq_and_eq_empty_iff_eq_empty : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s₁ s₂ : Set P},
  (affineSpan k s₁).Parallel (affineSpan k s₂) ↔ vectorSpan k s₁ = vectorSpan k s₂ ∧ (s₁ = ∅ ↔ s₂ = ∅)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instT3Space : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] {m : Type u_2} {n : Type u_3}, T3Space (CStarMatrix m n A)
-- Mathlib.NumberTheory.ArithmeticFunction.LFunction
/-- `ArithmeticFunction.ofPowerSeries` produces multiplicative power series.  -/
ArithmeticFunction.isMultiplicative_ofPowerSeries_of_isPrimePow : ∀ {R : Type u_1} [inst : CommRing R] (q : ℕ),
  IsPrimePow q →
    ∀ (f : PowerSeries R), PowerSeries.constantCoeff f = 1 → ((ArithmeticFunction.ofPowerSeries q) f).IsMultiplicative
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.mk.inj : ∀ {α : Type} {root : Std.HashMap Lean.Meta.RefinedDiscrTree.Key Lean.Meta.RefinedDiscrTree.TrieIndex}
  {tries : Array (Lean.Meta.RefinedDiscrTree.Trie α)}
  {root_1 : Std.HashMap Lean.Meta.RefinedDiscrTree.Key Lean.Meta.RefinedDiscrTree.TrieIndex}
  {tries_1 : Array (Lean.Meta.RefinedDiscrTree.Trie α)},
  { root := root, tries := tries } = { root := root_1, tries := tries_1 } → root = root_1 ∧ tries = tries_1
-- Batteries.Lean.Meta.Basic
/-- Erase any assignment or delayed assignment of the given metavariable.
 -/
Lean.MetavarContext.eraseExprMVarAssignment : Lean.MetavarContext → Lean.MVarId → Lean.MetavarContext
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.insertMany_eq_insertMany! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {l : List ((a : α) × β a)} {t : Std.DTreeMap.Internal.Impl α β}
  (h : t.Balanced), ↑(t.insertMany l h) = ↑(t.insertMany! l)
-- Init.Data.Range.Polymorphic.RangeIterator
/-- Internal state of the range iterators. Do not depend on its internals.  -/
Std.Rxo.Iterator : Type u → Type u
-- Mathlib.Data.Matrix.Block
Matrix.comp_toSquareBlock : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_14} {α : Type u_15} {b : m → α} (M : Matrix m m (Matrix n n R)) (a : α),
  ((Matrix.comp m m n n R) M).toSquareBlock (fun i => b i.1) a =
    (Matrix.reindex Equiv.prodSubtypeFstEquivSubtypeProd.symm Equiv.prodSubtypeFstEquivSubtypeProd.symm)
      ((Matrix.comp { a_1 // b a_1 = a } { a_1 // b a_1 = a } n n R) (M.toSquareBlock b a))
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.grindSeq : Lean.ParserDescr
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castAdd_Ioc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.image (Fin.castAdd m) (Finset.Ioc i j) = Finset.Ioc (Fin.castAdd m i) (Fin.castAdd m j)
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.map_eq_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (W : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D), W.map F = (W.strictMap F).isoClosure
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.pullbacks_monotone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], Monotone CategoryTheory.MorphismProperty.pullbacks
-- Lean.Environment
Lean.Kernel.instInhabitedDiagnostics.default : Lean.Kernel.Diagnostics
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.coe_top : ∀ {M : Type u_1} [inst : Mul M], ↑⊤ = Set.univ
-- Mathlib.Algebra.Regular.Opposite
isAddRightRegular_op : ∀ {R : Type u_1} [inst : Add R] {a : R}, IsAddRightRegular (AddOpposite.op a) ↔ IsAddLeftRegular a
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Path.map_arrow : ∀ {X Y : SSet} {n : ℕ} (f : X.Path n) (σ : X ⟶ Y) (i : Fin n),
  (f.map σ).arrow i = (CategoryTheory.ConcreteCategory.hom (σ.app (Opposite.op { len := 1 }))) (f.arrow i)
-- Mathlib.Algebra.Algebra.Operations
Submodule.le_div_iff : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  {I J K : Submodule R A}, I ≤ J / K ↔ ∀ x ∈ I, ∀ z ∈ K, x * z ∈ J
-- Mathlib.Data.List.Cycle
List.prev_mem : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) (x : α) (h : x ∈ l), l.prev x h ∈ l
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_int_mul_two_pi_add_pi : ∀ (n : ℤ), Real.cos (↑n * (2 * Real.pi) + Real.pi) = -1
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- Convenience constructor for a morphism in monomorphisms over `X`.  -/
CategoryTheory.MonoOver.homMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      {f g : CategoryTheory.MonoOver X} →
        (h : f.obj.left ⟶ g.obj.left) →
          autoParam (CategoryTheory.CategoryStruct.comp h g.arrow = f.arrow) CategoryTheory.MonoOver.homMk._auto_1 →
            (f ⟶ g)
-- Lean.Meta.Basic
/-- `checkpointDefEq x` executes `x` and process all postponed universe level constraints produced by `x`.
We keep the modifications only if `processPostponed` return true and `x` returned `true`.

If `mayPostpone == false`, all new postponed universe level constraints must be solved before returning.
We currently try to postpone universe constraints as much as possible, even when by postponing them we
are not sure whether `x` really succeeded or not.
 -/
Lean.Meta.checkpointDefEq : Lean.MetaM Bool → optParam Bool true → Lean.MetaM Bool
-- Lean.Meta.FunInfo
_private.Lean.Meta.FunInfo.0.Lean.Meta.whenHasVar : {α : Sort u_1} → Lean.Expr → α → (α → α) → α
-- Std.Time.DateTime.PlainDateTime
/-- Creates a new `PlainDateTime` by adjusting the month to the given `month` value.
The day is rolled over to the next valid month if necessary.
 -/
Std.Time.PlainDateTime.withMonthRollOver : Std.Time.PlainDateTime → Std.Time.Month.Ordinal → Std.Time.PlainDateTime
-- Mathlib.CategoryTheory.Center.Localization
CategoryTheory.CatCenter.localization_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (L : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W],
  CategoryTheory.CatCenter.localization 1 L W = 1