mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Free
/-- If `α` is a type, then `FreeSemigroup α` is the free semigroup generated by `α`.
This is a semigroup equipped with a function `FreeSemigroup.of : α → FreeSemigroup α` which has
the following universal property: if `M` is any semigroup, and `f : α → M` is any function,
then this function is the composite of `FreeSemigroup.of` and a unique semigroup homomorphism
`FreeSemigroup.lift f : FreeSemigroup α →ₙ* M`.

A typical element of `FreeSemigroup α` is a nonempty formal product of elements of `α`.
For example if `x` and `y` are terms of type `α` then `x * y * y * x` is a
"typical" element of `FreeSemigroup α`. In particular if `α` is empty
then `FreeSemigroup α` is also empty, and if `α` has one term
then `FreeSemigroup α` is isomorphic to `Multiplicative ℕ+`.
If `α` has two or more terms then `FreeSemigroup α` is not commutative.
One can think of `FreeSemigroup α` as the type of nonempty lists of `α`, with multiplication
given by concatenation.
 -/
FreeSemigroup : Type u → Type u
-- Mathlib.Topology.PartitionOfUnity
/-- The `tsupport`s of a partition of unity are locally finite.  -/
PartitionOfUnity.finite_tsupport : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} (ρ : PartitionOfUnity ι X s) (x₀ : X),
  {i | x₀ ∈ tsupport ⇑(ρ i)}.Finite
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_alter!_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.Const.alter! k f t) =
        (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome
-- Mathlib.MeasureTheory.SetAlgebra
MeasureTheory.generateSetAlgebra.base : ∀ {α : Type u_2} {𝒜 : Set (Set α)}, ∀ s ∈ 𝒜, MeasureTheory.generateSetAlgebra 𝒜 s
-- Mathlib.Algebra.Module.Projective
Module.Projective.mk : ∀ {R : Type u_1} [inst : Semiring R] {P : Type u_2} [inst_1 : AddCommMonoid P] [inst_2 : Module R P],
  (∃ s, Function.LeftInverse ⇑(Finsupp.linearCombination R id) ⇑s) → Module.Projective R P
-- Mathlib.Topology.Homotopy.HSpaces
IsTopologicalGroup.hSpace : (G : Type u) → [inst : TopologicalSpace G] → [inst_1 : Group G] → [IsTopologicalGroup G] → HSpace G
-- Mathlib.AlgebraicGeometry.OrderOfVanishing
_private.Mathlib.AlgebraicGeometry.OrderOfVanishing.0.AlgebraicGeometry.Scheme.ord.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X]
  [inst_1 : AlgebraicGeometry.IsLocallyNoetherian X] (f : ↑X.functionField) (z : ↥X),
  AlgebraicGeometry.Scheme.ord f z =
    if hz : Order.coheight z = 1 then
      Multiplicative.toAdd (WithZero.unzeroD 1 ((AlgebraicGeometry.Scheme.ordHom z hz) f))
    else 0
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.otherVertexOfIncident.congr_simp : ∀ {V : Type u} (G G_1 : SimpleGraph V) (e_G : G = G_1) [inst : DecidableEq V] {v v_1 : V} (e_v : v = v_1)
  {e e_1 : Sym2 V} (e_e : e = e_1) (h : e ∈ G.incidenceSet v), G.otherVertexOfIncident h = G_1.otherVertexOfIncident ⋯
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.below.constModify₀ : ∀ {α : Type u}
  {motive : {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → (a : Std.DHashMap.Raw α β) → a.WF → Prop}
  {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => β} {h : 0 < m.buckets.size} {a : α}
  {f : β → β} (a_1 : m.WF), Std.DHashMap.Raw.WF.below a_1 → motive m a_1 → Std.DHashMap.Raw.WF.below ⋯
-- Mathlib.Order.Filter.AtTopBot.Archimedean
Filter.Tendsto.atBot_zsmul_neg_const : ∀ {α : Type u_1} {R : Type u_2} {l : Filter α} {r : R} [inst : AddCommGroup R] [inst_1 : LinearOrder R]
  [IsOrderedAddMonoid R] [Archimedean R] {f : α → ℤ},
  r < 0 → Filter.Tendsto f l Filter.atBot → Filter.Tendsto (fun x => f x • r) l Filter.atTop
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.Unit_of_divided_by_X_pow_order_nonzero : ∀ {k : Type u_2} [inst : Field k] {f : PowerSeries k}, f ≠ 0 → ↑f.Unit_of_divided_by_X_pow_order = f.divXPowOrder
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.center_bot : ∀ {α : Type u_1}, ⊥.center = Set.univ
-- Mathlib.Data.Finsupp.Defs
Finsupp.equivFunOnFinite_symm_coe : ∀ {M : Type u_4} [inst : Zero M] {α : Type u_9} [inst_1 : Finite α] (f : α →₀ M), Finsupp.equivFunOnFinite.symm ⇑f = f
-- Mathlib.Data.Complex.Basic
/-- Show the imaginary number ⟨x, y⟩ as an `"x + y*I"` string

Note that the Real numbers used for x and y will show as Cauchy sequences due to the way Real
numbers are represented.
 -/
Complex.instRepr : Repr ℂ
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.map_ιE : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  {i₀' i₁' i₂' i₃' : ι} (f₁' : i₀' ⟶ i₁') (f₂' : i₁' ⟶ i₂') (f₃' : i₂' ⟶ i₃')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃')
  (γ : CategoryTheory.ComposableArrows.mk₂ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₂ f₂' f₃') (n₀ n₁ n₂ : ℤ),
  autoParam (γ = CategoryTheory.ComposableArrows.homMk₂ (α.app 1) (α.app 2) (α.app 3) ⋯ ⋯)
      CategoryTheory.Abelian.SpectralObject.map_ιE._auto_1 →
    ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.map_ιE._auto_3)
      (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.map_ιE._auto_5),
      CategoryTheory.CategoryStruct.comp (X.map f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)
          (X.ιE f₁' f₂' f₃' n₀ n₁ n₂ hn₁ hn₂) =
        CategoryTheory.CategoryStruct.comp (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂) (X.opcyclesMap f₂ f₃ f₂' f₃' γ n₁)
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
Subsemigroup.centralizer_eq_top_iff_subset : ∀ {M : Type u_1} [inst : Semigroup M] {s : Set M}, Subsemigroup.centralizer s = ⊤ ↔ s ⊆ ↑(Subsemigroup.center M)
-- Mathlib.GroupTheory.Congruence.Defs
/-- The supremum of two additive congruence relations equals the smallest additive
congruence relation containing the supremum of the underlying binary operations.  -/
AddCon.sup_def : ∀ {M : Type u_1} [inst : Add M] (c d : AddCon M), c ⊔ d = addConGen (⇑c ⊔ ⇑d)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_le_mabs : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] {a b : α}, a ≤ b → a⁻¹ ≤ b → |a|ₘ ≤ |b|ₘ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_eq_some_maxKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.maxKey? = some t.maxKey!
-- Mathlib.Condensed.Equivalence
Condensed.isSheafStonean : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] (X : Condensed A)
  [∀ (Y : CompHausᵒᵖ),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow Y Stonean.toCompHaus.op) A],
  CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology Stonean) (Stonean.toCompHaus.op.comp X.obj)
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.coe_rTensor_symm : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N ≃ₗ[R] P), ↑(LinearEquiv.rTensor M f).symm = LinearMap.rTensor M ↑f.symm
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.ext`.

---

To give an isomorphism between cones, it suffices to give an
isomorphism between their vertices which commutes with the cone maps.  -/
CategoryTheory.Limits.Cones.ext : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {c c' : CategoryTheory.Limits.Cone F} →
            (φ : c.pt ≅ c'.pt) →
              autoParam (∀ (j : J), c.π.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.π.app j))
                  CategoryTheory.Limits.Cone.ext._auto_1 →
                (c ≅ c')
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.cons_toFun : ∀ {coef exp : ℝ} {m : Tactic.ComputeAsymptotics.UnitMonomial} {basis_hd : ℝ → ℝ}
  {basis_tl : Tactic.ComputeAsymptotics.Basis},
  { coef := coef, unit := exp :: m }.toFun (basis_hd :: basis_tl) =
    basis_hd ^ exp * { coef := coef, unit := m }.toFun basis_tl
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- A continuous function with compact support is integrable on the whole space.  -/
Continuous.integrable_of_hasCompactSupport : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {f : X → E} [MeasureTheory.IsFiniteMeasureOnCompacts μ],
  Continuous f → HasCompactSupport f → MeasureTheory.Integrable f μ
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.recOneCoe_one : ∀ {α : Type u} {motive : WithOne α → Sort u_1} (h₁ : motive 1) (h₂ : (a : α) → motive ↑a),
  WithOne.recOneCoe h₁ h₂ 1 = h₁
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxEntry?.eq_3 : ∀ {α : Type u} {β : α → Type v} (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ) (k_1 : α)
  (v_1 : β k_1) (l_1 r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).maxEntry? =
    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxEntry?
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the reverse direction of `upperSemicontinuousAt_iff_frequently`. -/
UpperSemicontinuousAt.of_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β} {x : α},
  (∀ (y : β), (∃ᶠ (x' : α) in nhds x, f x' ≥ y) → f x ≥ y) → UpperSemicontinuousAt f x
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- The third projection from `PrimitiveAddChar`, showing that `χ.char` is primitive.  -/
AddChar.PrimitiveAddChar.prim : ∀ {R : Type u} [inst : CommRing R] {R' : Type v} [inst_1 : Field R'] (self : AddChar.PrimitiveAddChar R R'),
  self.char.IsPrimitive
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.keyword : Lean.Lsp.SemanticTokenType
-- Mathlib.CategoryTheory.Abelian.Preradical.Basic
CategoryTheory.Abelian.Preradical.instMonoFunctorWhiskerLeftι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C) {D : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor D C), CategoryTheory.Mono (F.whiskerLeft Φ.ι)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.ModObj.mul_smul_self_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.MonObj M] (X : C) [inst_3 : CategoryTheory.ModObj M X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul X)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator M M X).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M CategoryTheory.ModObj.smul)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul h))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_left_inj_of_comparable : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [MulRightStrictMono α] {a b c : α},
  b ≤ c ∨ c ≤ b → (c * a = b * a ↔ c = b)
-- Std.Async.System
Std.Async.System.GroupInfo.mk.sizeOf_spec : ∀ (groupName : String) (groupId : Std.Async.System.GroupId) (members : Array String),
  sizeOf { groupName := groupName, groupId := groupId, members := members } =
    1 + sizeOf groupName + sizeOf groupId + sizeOf members
-- Mathlib.Data.Seq.Defs
Stream'.Seq.coeList : {α : Type u} → Coe (List α) (Stream'.Seq α)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry.match_1.congr_eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.isEmpty = false → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α β) (x_1 : x.isEmpty = false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        (h :
                            (Std.DTreeMap.Internal.Impl.inner size k v
                                  (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1).isEmpty =
                              false) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)
                            h)
  (size : ℕ) (k : α) (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r r_1 : Std.DTreeMap.Internal.Impl α β)
  (h :
    (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).isEmpty =
      false),
  x = Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1 →
    x_1 ≍ h →
      (match x, x_1 with
        | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_1 size k v r x
        | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r)) r_2,
          h_3 => h_2 size k v l size_2 k_2 v_2 l_1 r h r_2 h_3) ≍
        h_2 size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) size_1 k_1 v_1 l r ⋯ r_1 h
-- Mathlib.LinearAlgebra.PiTensorProduct.Finsupp
/-- A variant of `ofFinsuppEquiv` where all modules `M i` are the ground ring.  -/
PiTensorProduct.ofFinsuppEquiv' : {R : Type u_1} →
  {ι : Type u_2} →
    {κ : ι → Type u_3} →
      [inst : CommSemiring R] →
        [Fintype ι] →
          [DecidableEq ι] →
            [(i : ι) → DecidableEq (κ i)] →
              [DecidableEq R] → (PiTensorProduct R fun i => κ i →₀ R) ≃ₗ[R] ((i : ι) → κ i) →₀ R
-- Mathlib.Data.Finset.Sym
Finset.sym_map : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] {n : ℕ} (g : α ↪ β) (s : Finset α),
  (Finset.map g s).sym n = Finset.map { toFun := Sym.map ⇑g, inj' := ⋯ } (s.sym n)
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function has a finite power series on a ball, then so does its derivative.
This is a variant of `HasFiniteFPowerSeriesOnBall.fderiv` where the degree of `f` is `< n`
and not `< n + 1`.  -/
HasFiniteFPowerSeriesOnBall.fderiv' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E F} {r : ENNReal} {n : ℕ} {f : E → F} {x : E},
  HasFiniteFPowerSeriesOnBall f p x n r → HasFiniteFPowerSeriesOnBall (fderiv 𝕜 f) p.derivSeries x (n - 1) r
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- the functor preserves all the left homology data of the short complex  -/
CategoryTheory.Functor.PreservesLeftHomologyOf.isPreservedBy : ∀ {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.Limits.HasZeroMorphisms C}
  {inst_3 : CategoryTheory.Limits.HasZeroMorphisms D} {F : CategoryTheory.Functor C D}
  {inst_4 : F.PreservesZeroMorphisms} {S : CategoryTheory.ShortComplex C} [self : F.PreservesLeftHomologyOf S]
  (h : S.LeftHomologyData), h.IsPreservedBy F
-- Batteries.Data.Array.Pairwise
Array.pairwise_pair : ∀ {α : Type u_1} {a b : α} {R : α → α → Prop}, Array.Pairwise R #[a, b] ↔ R a b
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.ofNatCode.match_3.eq_5 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : Unit → motive 2)
  (h_4 : Unit → motive 3) (h_5 : (n : ℕ) → motive n.succ.succ.succ.succ),
  (match n.succ.succ.succ.succ with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | 2 => h_3 ()
    | 3 => h_4 ()
    | n.succ.succ.succ.succ => h_5 n) =
    h_5 n
-- Mathlib.Topology.Sheaves.Over
TopologicalSpace.Opens.sheafEquivOver_functor_obj_obj_obj : ∀ {X : Type u} [inst : TopologicalSpace X] (U : TopologicalSpace.Opens X) {A : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} A] (X_1 : CategoryTheory.Sheaf ((Opens.grothendieckTopology X).over U) A)
  (X_2 : (TopologicalSpace.Opens ↥U)ᵒᵖ),
  (U.sheafEquivOver.functor.obj X_1).obj.obj X_2 =
    X_1.obj.obj (Opposite.op (U.overEquivalence.inverse.obj (Opposite.unop X_2)))
-- Mathlib.Tactic.Set
/-- `set a := t with h` is a variant of `let a := t`. It adds the hypothesis `h : a = t` to
the local context and replaces `t` with `a` everywhere it can.

`set a := t with ← h` will add `h : t = a` instead.

`set! a := t with h` does not do any replacing.

```lean
example (x : Nat) (h : x + x - x = 3) : x + x - x = 3 := by
  set y := x with ← h2
  sorry
/-
x : Nat
y : Nat := x
h : y + y - y = 3
h2 : x = y
⊢ y + y - y = 3
-/
```
 -/
Mathlib.Tactic.tacticSet!_ : Lean.ParserDescr
-- Lean.Elab.PreDefinition.Structural.Eqns
Lean.Elab.Structural.EqnInfo.declNames : Lean.Elab.Structural.EqnInfo → Array Lean.Name
-- Lean.PrettyPrinter.Delaborator.Builtins
Lean.PrettyPrinter.Delaborator.AppImplicitArg.regular.inj : ∀ {s s_1 : Lean.Term},
  Lean.PrettyPrinter.Delaborator.AppImplicitArg.regular s = Lean.PrettyPrinter.Delaborator.AppImplicitArg.regular s_1 →
    s = s_1
-- Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
/-- If `f` is real-meromorphic on a compact interval, then `log ∘ f` is interval integrable on this
interval.
 -/
MeromorphicOn.intervalIntegrable_log : ∀ {a b : ℝ} {f : ℝ → ℝ}, MeromorphicOn f (Set.uIcc a b) → IntervalIntegrable (Real.log ∘ f) MeasureTheory.volume a b
-- Mathlib.Topology.ContinuousOn
continuousWithinAt_fst : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set (α × β)} {p : α × β},
  ContinuousWithinAt Prod.fst s p
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- A maximum clique in a graph `G` is a clique with the largest possible size.  -/
SimpleGraph.IsMaximumClique : {α : Type u_3} → [Finite α] → SimpleGraph α → Finset α → Prop
-- Mathlib.Data.Matrix.Mul
IsStablyFiniteRing.isDedekindFiniteMonoid : ∀ {R : Type u_10} {inst : MulOne R} {inst_1 : AddCommMonoid R} [self : IsStablyFiniteRing R] (n : ℕ),
  IsDedekindFiniteMonoid (Matrix (Fin n) (Fin n) R)
-- Mathlib.Topology.Filter
Filter.mem_nhds_iff : ∀ {α : Type u_2} {l : Filter α} {S : Set (Filter α)}, S ∈ nhds l ↔ ∃ t ∈ l, Set.Iic (Filter.principal t) ⊆ S
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.equiv_iff_toList_perm : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α], m₁.Equiv m₂ ↔ (Std.DHashMap.Const.toList m₁).Perm (Std.DHashMap.Const.toList m₂)
-- Mathlib.Topology.Separation.Regular
T5Space.toCompletelyNormalSpace : ∀ {X : Type u} {inst : TopologicalSpace X} [self : T5Space X], CompletelyNormalSpace X
-- Mathlib.CategoryTheory.Whiskering
/-- The isomorphism between left-whiskering on the identity functor and the identity of the functor
between the resulting functor categories.  -/
CategoryTheory.Functor.whiskeringLeftObjIdIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {E : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} E] →
        (CategoryTheory.Functor.whiskeringLeft C C E).obj (CategoryTheory.Functor.id C) ≅
          CategoryTheory.Functor.id (CategoryTheory.Functor C E)
-- Init.Data.UInt.Bitwise
UInt64.zero_shiftLeft : ∀ {a : UInt64}, 0 <<< a = 0
-- Mathlib.NumberTheory.TsumDivisorsAntidiagonal
divisorsAntidiagonalFactors_one : ∀ (x : ↥(Nat.divisorsAntidiagonal 1)), divisorsAntidiagonalFactors 1 x = (1, 1)
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
_private.Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic.0.IsCovariantDerivativeOn.differenceAux.eq_1 : ∀ {𝕜 : 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] {V : M → Type u_6} [inst_6 : (x : M) → AddCommGroup (V x)]
  [inst_7 : (x : M) → Module 𝕜 (V x)] [inst_8 : (x : M) → TopologicalSpace (V x)]
  [inst_9 : ∀ (x : M), IsTopologicalAddGroup (V x)] (cov cov' : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x)
  (σ : (x : M) → V x), IsCovariantDerivativeOn.differenceAux✝ cov cov' σ = cov σ - cov' σ
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.descCoconeMorphism_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t)
  (s : CategoryTheory.Limits.Cocone F), (h.descCoconeMorphism s).hom = h.desc s
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.Subtype.instSingleton : {α : Type u_1} → [inst : MeasurableSpace α] → [MeasurableSingletonClass α] → Singleton α (Subtype MeasurableSet)
-- Init.Data.Array.Lemmas
Array.none_eq_getElem?_iff : ∀ {α : Type u_1} {xs : Array α} {i : ℕ}, none = xs[i]? ↔ xs.size ≤ i
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.rankD.eq_1 : ∀ (arr : Array Batteries.UFNode) (i : ℕ), Batteries.UnionFind.rankD arr i = if h : i < arr.size then arr[i].rank else 0
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.eq : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {a b : α}, ↑a = ↑b ↔ a⁻¹ * b ∈ s
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.triangleMorphism₁_hom₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  (h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  (h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  (h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (h : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃),
  (CategoryTheory.Triangulated.Octahedron'.triangleMorphism₁ comm h₁₂ h₂₃ h₁₃ h).hom₁ = h.m₁
-- Mathlib.Algebra.GroupWithZero.Basic
/-- In a monoid with zero, if zero equals one, then zero is the unique element.

Somewhat arbitrarily, we define the default element to be `0`.
All other elements will be provably equal to it, but not necessarily definitionally equal.  -/
uniqueOfZeroEqOne : {M₀ : Type u_1} → [inst : MulZeroOneClass M₀] → 0 = 1 → Unique M₀