mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- The commutation isomorphisms of `Adjunction.RightAdjointCommShift.iso` are compatible with
the unit of the adjunction.
 -/
CategoryTheory.Adjunction.RightAdjointCommShift.compatibilityUnit_iso : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddGroup A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] (a : A),
  CategoryTheory.Adjunction.CommShift.CompatibilityUnit adj (CategoryTheory.Functor.commShiftIso F a)
    (CategoryTheory.Adjunction.RightAdjointCommShift.iso adj a)
-- Mathlib.Data.ENat.Basic
ENat.toNat_natCast : ∀ (n : ℕ), (↑n).toNat = n
-- Lean.Elab.DefView
Lean.Elab.DefKind.isExample : Lean.Elab.DefKind → Bool
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.finsupp_support_eq_support : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R), p.coeff.support = p.support
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_symm_comp_map_map_comp_assoc : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {N₁ : Type u_14}
  {N₂ : Type u_15} {N₃ : Type u_16} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid M₁] [inst_6 : AddCommMonoid M₂]
  [inst_7 : AddCommMonoid M₃] [inst_8 : AddCommMonoid N₁] [inst_9 : AddCommMonoid N₂] [inst_10 : AddCommMonoid N₃]
  [inst_11 : Module R M₁] [inst_12 : Module R M₂] [inst_13 : Module R M₃] [inst_14 : Module R N₁]
  [inst_15 : Module R N₂] [inst_16 : Module R N₃] (f₁ : M₁ →ₗ[R] N₁) (f₂ : M₂ →ₗ[R] N₂) (f₃ : M₃ →ₗ[R] N₃)
  (f₂₃ : M →ₗ[R] TensorProduct R M₂ M₃) (f : N →ₗ[R] TensorProduct R M₁ M),
  ↑(TensorProduct.assoc R N₁ N₂ N₃).symm ∘ₗ TensorProduct.map f₁ (TensorProduct.map f₂ f₃ ∘ₗ f₂₃) ∘ₗ f =
    TensorProduct.map (TensorProduct.map f₁ f₂) f₃ ∘ₗ
      ↑(TensorProduct.assoc R M₁ M₂ M₃).symm ∘ₗ TensorProduct.map LinearMap.id f₂₃ ∘ₗ f
-- Mathlib.NumberTheory.Cyclotomic.Basic
CyclotomicField.isCyclotomicExtension : ∀ (n : ℕ) [NeZero n] (K : Type w) [inst : Field K] [NeZero ↑n], IsCyclotomicExtension {n} K (CyclotomicField n K)
-- Mathlib.Analysis.Normed.Group.Lemmas
eventually_norm_sub_lt : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (x₀ : E) {ε : ℝ}, 0 < ε → ∀ᶠ (x : E) in nhds x₀, ‖x - x₀‖ < ε
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.divCoeffs.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.divCoeffs c = Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.divCoeffs c_1) =
    (c = c_1)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.equivLaxMonoidalFunctorPUnit_inverse_obj_laxMonoidal_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.AddMon C) (x x_1 : CategoryTheory.Discrete PUnit.{w + 1}),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidalObj A) x
      x_1 =
    CategoryTheory.AddMonObj.add
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.mem_inf : ∀ {R : Type u} [inst : NonAssocRing R] {p p' : Subring R} {x : R}, x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'
-- Mathlib.Data.Nat.Hyperoperation
_private.Mathlib.Data.Nat.Hyperoperation.0.hyperoperation.match_1.eq_2 : ∀ (motive : ℕ → ℕ → ℕ → Sort u_1) (m : ℕ) (h_1 : (x k : ℕ) → motive 0 x k) (h_2 : (m : ℕ) → motive 1 m 0)
  (h_3 : (x : ℕ) → motive 2 x 0) (h_4 : (n x : ℕ) → motive n.succ.succ.succ x 0)
  (h_5 : (n m k : ℕ) → motive n.succ m k.succ),
  (match 1, m, 0 with
    | 0, x, k => h_1 x k
    | 1, m, 0 => h_2 m
    | 2, x, 0 => h_3 x
    | n.succ.succ.succ, x, 0 => h_4 n x
    | n.succ, m, k.succ => h_5 n m k) =
    h_2 m
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_inter!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k fallback : α},
        Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.inter! m₂).getKeyD k fallback = fallback
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
/-- Coercion `ℝ → Angle` as an additive homomorphism.  -/
Real.Angle.coeHom : ℝ →+ Real.Angle
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.weightedVSubVSubWeights_self : ∀ (k : Type u_1) [inst : Ring k] {ι : Type u_4} [inst_1 : DecidableEq ι] (i : ι),
  Finset.weightedVSubVSubWeights k i i = 0
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- `val_v(v) = 1`, when `v` is regarded as a fractional ideal.  -/
FractionalIdeal.count_self : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R),
  FractionalIdeal.count K v ↑v.asIdeal = 1
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_nonempty : ∀ {α : Type u} {s : Set α} (hs : s.Finite), hs.toFinset.Nonempty ↔ s.Nonempty
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContinuousOn.continuousOn_iteratedFDeriv : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} {f : E → F}
  {n : WithTop ℕ∞} {k : ℕ}, ContDiffOn 𝕜 n f s → IsOpen s → ↑k ≤ n → ContinuousOn (iteratedFDeriv 𝕜 k f) s
-- Mathlib.LinearAlgebra.FixedSubmodule
LinearEquiv.fixedReduce_mk : ∀ {R : Type u_4} {V : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] (e : V ≃ₗ[R] V) (x : V),
  e.fixedReduce (Submodule.Quotient.mk x) = Submodule.Quotient.mk (e x)
-- Mathlib.Lean.Environment
/-- Like `findConstVal?`, but only finds the `ConstantVal` for `decl` in `env` if its kind satisfies
`p`. Otherwise, returns `none`.

Blocks on everything but the constant's body (if any), which is not accessible through the result.
 -/
Lean.Environment.findConstValOfKind? : Lean.Environment → (Lean.ConstantKind → Bool) → Lean.Name → optParam Bool false → Option Lean.ConstantVal
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.toContinuousLinearMap_mk' : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} (e : V ≃L[R] W)
  (he : ∀ (g : G), ↑e ∘SL ρ g = σ g ∘SL ↑e), ↑(ContRepresentation.Equiv.mk e he).toContinuousLinearEquiv = ↑e
-- Mathlib.Order.CompleteBooleanAlgebra
Order.Frame.toHeytingAlgebra : {α : Type u_1} → [self : Order.Frame α] → HeytingAlgebra α
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Precomp.map_zero_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (F : CategoryTheory.ComposableArrows C n) {X : C}
  (f : X ⟶ F.left), CategoryTheory.ComposableArrows.Precomp.map F f 0 0 ⋯ = CategoryTheory.CategoryStruct.id X
-- Mathlib.Order.RelIso.Basic
RelHomClass.mk : ∀ {F : Type u_5} {α : outParam (Type u_6)} {β : outParam (Type u_7)} {r : outParam (α → α → Prop)}
  {s : outParam (β → β → Prop)} [inst : FunLike F α β], (∀ (f : F) {a b : α}, r a b → s (f a) (f b)) → RelHomClass F r s
-- Mathlib.RingTheory.KrullDimension.Zero
/-- **Alias** of `Ring.KrullDimLE.minimalPrimes_eq_setOfPred_isPrime`. -/
Ring.KrullDimLE.minimalPrimes_eq_setOf_isPrime : ∀ (R : Type u_1) [inst : CommSemiring R] [Ring.KrullDimLE 0 R], minimalPrimes R = {I | I.IsPrime}
-- Init.Data.SInt.Lemmas
Int32.add_assoc : ∀ (a b c : Int32), a + b + c = a + (b + c)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_mul_eq_prod_mul_of_exists : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] {f : α →₀ M} {g : α → M → N}
  {n₁ n₂ : N}, ∀ a ∈ f.support, g a (f a) * n₁ = g a (f a) * n₂ → f.prod g * n₁ = f.prod g * n₂
-- Lean.Environment
Lean.instInhabitedImportState : Inhabited Lean.ImportState
-- Mathlib.Order.GameAdd
Prod.GameAdd.snd : ∀ {α : Type u_1} {β : Type u_2} {rα : α → α → Prop} {rβ : β → β → Prop} {a : α} {b₁ b₂ : β},
  rβ b₁ b₂ → Prod.GameAdd rα rβ (a, b₁) (a, b₂)
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.semilength_insidePart_lt : ∀ {p : DyckWord}, p ≠ 0 → p.insidePart.semilength < p.semilength
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.neg.eq_1 : ∀ (G : Type u_4) [inst : MeasurableSpace G] [inst_1 : InvolutiveNeg G] [inst_2 : MeasurableNeg G],
  MeasurableEquiv.neg G = { toEquiv := Equiv.neg G, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
MeasureTheory.setIntegral_countable : ∀ {X : Type u_2} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] [MeasurableSingletonClass X] {μ : MeasureTheory.Measure X} (f : X → E) {s : Set X},
  s.Countable → MeasureTheory.IntegrableOn f s μ → ∫ (x : X) in s, f x ∂μ = ∑' (x : ↑s), μ.real {↑x} • f ↑x
-- Mathlib.Analysis.Seminorm
Seminorm.neg_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) (r : ℝ) (x : E), -p.closedBall x r = p.closedBall (-x) r
-- Mathlib.Topology.DiscreteSubset
/-- The union of finitely many discrete closed subsets is discrete.  -/
IsDiscrete.iUnion : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : Sort u_3} [Finite ι] {s : ι → Set X},
  (∀ (i : ι), IsDiscrete (s i)) → (∀ (i : ι), IsClosed (s i)) → IsDiscrete (⋃ i, s i)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.instIsIsoHomHomMon : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : CategoryTheory.CommMon C} {f : M ⟶ N} [CategoryTheory.IsIso f],
  CategoryTheory.IsIso f.hom.hom
-- Init.Data.Range.Polymorphic.SInt
ISize.instRxcLawfulHasSize : Std.Rxc.LawfulHasSize ISize
-- Mathlib.Data.TypeVec
TypeVec.const.eq_2 : ∀ {β : Type u_1} (x : β) (n : ℕ) (x_4 : TypeVec.{u_2} n.succ),
  TypeVec.const x x_4 Fin2.fz =
    match (motive := (x : ℕ) → (x_1 : TypeVec.{u_2} x) → (x_2 : Fin2 x) → x_1 x_2 → TypeVec.repeat x β x_2) n.succ, x_4,
      Fin2.fz with
    | n.succ, α, a.fs => TypeVec.const x α.drop a
    | n.succ, x_1, Fin2.fz => fun x_2 => x
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_sub : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5}
  {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h}
  [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [inst_2 : (i : ι) → FunLike (H i) (G i) C]
  [inst_3 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_4 : IsDirectedOrder ι] [inst_5 : Nonempty ι]
  [inst_6 : (i : ι) → AddGroup (G i)] [inst_7 : AddGroup C]
  [inst_8 : ∀ (i j : ι) (h : i ≤ j), AddMonoidHomClass (T h) (G i) (G j)] [∀ (i : ι), AddMonoidHomClass (H i) (G i) C]
  (g : (i : ι) → H i) (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)) (x y : DirectLimit G f),
  DirectLimit.lift f (fun x => ⇑(g x)) h (x - y) =
    DirectLimit.lift f (fun x => ⇑(g x)) h x - DirectLimit.lift f (fun x => ⇑(g x)) h y
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_mul_right : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] (a : α), UniformContinuous fun b => b * a
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.HasZeroObject.instSubsingletonIsoOfNat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C] (X : C),
  Subsingleton (X ≅ 0)
-- Init.Data.Vector.Lemmas
Vector.mem_push_of_mem : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {x : α} (y : α), x ∈ xs → x ∈ xs.push y
-- Mathlib.Analysis.Real.Pi.Bounds
Real.pi_lt_d2 : Real.pi < 3.15
-- Mathlib.GroupTheory.Sylow
Sylow.subtype.congr_simp : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] (P P_1 : Sylow p G) (e_P : P = P_1) {N : Subgroup G} (h : ↑P ≤ N),
  P.subtype h = P_1.subtype ⋯
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.addCommMonoid : {α : Type u} → [AddCommMonoid α] → AddCommMonoid (WithTop α)
-- Mathlib.Topology.Category.LightProfinite.Limits
LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology : CompHausLike.HasExplicitFiniteCoproducts fun Y => TotallyDisconnectedSpace ↑Y ∧ SecondCountableTopology ↑Y
-- Mathlib.RingTheory.Polynomial.Opposites
Polynomial.opRingEquiv_symm_C : ∀ {R : Type u_1} [inst : Semiring R] (a : Rᵐᵒᵖ),
  (Polynomial.opRingEquiv R).symm (Polynomial.C a) = MulOpposite.op (Polynomial.C (MulOpposite.unop a))
-- Mathlib.Data.W.Constructions
_private.Mathlib.Data.W.Constructions.0.WType.ofNat.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive Nat.zero) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod.eq_1 : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] (f : α →₀ M) (g : α → M → N),
  f.prod g = ∏ a ∈ f.support, g a (f a)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.isTopCompl_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [K.HasOrthogonalProjection], Submodule.IsTopCompl K Kᗮ
-- Mathlib.Data.Nat.Basic
Nat.div_right_comm : ∀ (a b c : ℕ), a / b / c = a / c / b
-- Mathlib.Topology.Semicontinuity.Defs
lowerSemicontinuousOn_univ_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β},
  LowerSemicontinuousOn f Set.univ ↔ LowerSemicontinuous f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.find?_toList_eq_some_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {v : β k},
  List.find? (fun x => cmp x.fst k == Ordering.eq) t.toList = some ⟨k, v⟩ ↔ t.get? k = some v
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.ext_iff : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e e' : OpenPartialHomeomorph X Y},
  e = e' ↔ (∀ (x : X), ↑e x = ↑e' x) ∧ (∀ (x : Y), ↑e.symm x = ↑e'.symm x) ∧ e.source = e'.source
-- Mathlib.Data.PNat.Defs
instOfNatPNatOfNeZeroNat : (n : ℕ) → [NeZero n] → OfNat ℕ+ n
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.preservesZeroMorphisms_of_additive : ∀ {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.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.Additive], F.PreservesZeroMorphisms
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.eq_top_iff_forall_isUniversal : ∀ {V : Type u} {G : SimpleGraph V}, G = ⊤ ↔ ∀ (v : V), G.IsUniversal v
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.ensureHasNoMVars : Lean.Expr → Lean.Elab.Tactic.TacticM Unit
-- Aesop.Tree.Data
Aesop.GoalData.unsafeQueue : {Rapp MVarCluster : Type} → Aesop.GoalData Rapp MVarCluster → Aesop.UnsafeQueue
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObject_counitIso_hom_app_left_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject.Augmented C)
  (X_1 : SimplexCategoryᵒᵖ),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObject.counitIso.hom.app X).left.app X_1 =
    CategoryTheory.CategoryStruct.comp
      (match
        match
          Opposite.unop
            (match CategoryTheory.WithTerminal.incl.obj X_1 with
            | CategoryTheory.WithTerminal.of x => Opposite.op (CategoryTheory.WithInitial.of (Opposite.unop x))
            | CategoryTheory.WithTerminal.star => Opposite.op CategoryTheory.WithInitial.star) with
        | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
        | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star,
        CategoryTheory.WithTerminal.incl.obj X_1,
        (match CategoryTheory.WithTerminal.incl.obj X_1 with
          | CategoryTheory.WithTerminal.of x => CategoryTheory.Iso.refl (CategoryTheory.WithTerminal.of x)
          | CategoryTheory.WithTerminal.star => CategoryTheory.Iso.refl CategoryTheory.WithTerminal.star).hom with
      | CategoryTheory.WithTerminal.of a, CategoryTheory.WithTerminal.of a_1, f =>
        X.left.map (CategoryTheory.WithTerminal.down f)
      | CategoryTheory.WithTerminal.of x, CategoryTheory.WithTerminal.star, x_1 => X.hom.app x
      | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x =>
        CategoryTheory.CategoryStruct.id X.right)
      (CategoryTheory.CategoryStruct.id
        (match CategoryTheory.WithTerminal.incl.obj X_1 with
        | CategoryTheory.WithTerminal.of x => X.left.obj x
        | CategoryTheory.WithTerminal.star => X.right))
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- Reindexing a matrix preserves row-stochasticity.  -/
Matrix.reindex_mem_rowStochastic_iff : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {m : Type u_3} [inst_5 : Fintype m] [inst_6 : DecidableEq m]
  {M : Matrix n n R} {e₁ e₂ : n ≃ m}, (Matrix.reindex e₁ e₂) M ∈ Matrix.rowStochastic R m ↔ M ∈ Matrix.rowStochastic R n
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.t_mul_of : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} (a : ↥A),
  HNNExtension.t * HNNExtension.of ↑a = HNNExtension.of ↑(φ a) * HNNExtension.t
-- Mathlib.Topology.LocallyClosed
IsOpenMap.coborder_preimage_subset : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenMap f → ∀ (s : Set Y), coborder (f ⁻¹' s) ⊆ f ⁻¹' coborder s
-- Lean.Data.Lsp.Extra
Lean.Lsp.instInhabitedLeanImportMetaKind : Inhabited Lean.Lsp.LeanImportMetaKind
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.Inf.adjDecidable : (V : Type u) → (G H : SimpleGraph V) → [DecidableRel G.Adj] → [DecidableRel H.Adj] → DecidableRel (G ⊓ H).Adj
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F : C ⥤ D` creates finite products, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` creates finite
coproducts.  -/
CategoryTheory.Limits.createsFiniteCoproductsOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.Limits.CreatesFiniteProducts F] → CategoryTheory.Limits.CreatesFiniteCoproducts F.op
-- Init.Data.UInt.Lemmas
USize.zero_div : ∀ {a : USize}, 0 / a = 0
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- The cocone points of two colimit cocones for naturally isomorphic functors
are themselves isomorphic.
 -/
CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G : CategoryTheory.Functor J C} →
          {s : CategoryTheory.Limits.Cocone F} →
            {t : CategoryTheory.Limits.Cocone G} →
              CategoryTheory.Limits.IsColimit s → CategoryTheory.Limits.IsColimit t → (F ≅ G) → (s.pt ≅ t.pt)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ \ m₂).getKey? k = m₁.getKey? k
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.centerEquivRootsOfUnity_apply_of_finrank_le_one : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  [inst_3 : Module.Free R V] [inst_4 : Module.Finite R V],
  Module.finrank R V ≤ 1 →
    ∀ (g : ↥(Subgroup.center (SpecialLinearGroup R V))), SpecialLinearGroup.centerEquivRootsOfUnity g = 1
-- Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
AlgebraicGeometry.sourceLocalClosure.iff_forall_exists : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X Y : AlgebraicGeometry.Scheme} [P.RespectsIso]
  {f : X ⟶ Y},
  AlgebraicGeometry.sourceLocalClosure AlgebraicGeometry.IsOpenImmersion P f ↔
    ∀ (x : ↥X), ∃ U, x ∈ U ∧ P (CategoryTheory.CategoryStruct.comp U.ι f)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Hom.instInhabited : {L : FirstOrder.Language} → {M : Type w} → [inst : L.Structure M] → Inhabited (L.Hom M M)
-- Init.Data.String.Defs
String.Slice.Pos.ext_iff : ∀ {s : String.Slice} {x y : s.Pos}, x = y ↔ x.offset = y.offset
-- Mathlib.Data.Fin.Tuple.Reflection
FinVec.sum.eq_3 : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] (n : ℕ) (v : Fin (n + 2) → α),
  FinVec.sum v = (FinVec.sum fun i => v i.castSucc) + v (Fin.last (n + 1))
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.homologicalKernel.eq_1 : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) (X : C),
  F.homologicalKernel X = ∀ (n : ℤ), CategoryTheory.Limits.IsZero (F.obj ((CategoryTheory.shiftFunctor C n).obj X))
-- Init.Data.Int.Order
Int.le_add_of_neg_le_sub_right : ∀ {a b c : ℤ}, -b ≤ a - c → c ≤ a + b
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso_inv_hom₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (X : Cᵒᵖ),
  (CategoryTheory.Pretriangulated.Opposite.contractibleTriangleIso X).inv.hom₂ = CategoryTheory.CategoryStruct.id X
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR.run.eq_3 : ∀ {α : Type u_1} (le : α → α → Bool) (n_1 : ℕ) (xs : { l // l.length = n_1 + 2 }),
  List.MergeSort.Internal.mergeSortTR.run✝ le xs =
    match List.MergeSort.Internal.splitInTwo xs with
    | (l, r) =>
      List.MergeSort.Internal.mergeTR (List.MergeSort.Internal.mergeSortTR.run✝ le l)
        (List.MergeSort.Internal.mergeSortTR.run✝ le r) le
-- Mathlib.Data.Set.Defs
/-- * `{ pat : X | p }` is notation for pattern matching in set-builder notation,
  where `pat` is a pattern that is matched by all objects of type `X`
  and `p` is a proposition that can refer to variables in the pattern.
  It is the set of all objects of type `X` which, when matched with the pattern `pat`,
  make `p` come out true.
* `{ pat | p }` is the same, but in the case when the type `X` can be inferred.

For example, `{ (m, n) : ℕ × ℕ | m * n = 12 }` denotes the set of all ordered pairs of
natural numbers whose product is 12.

Note that if the type ascription is left out and `p` can be interpreted as an extended binder,
then the extended binder interpretation will be used.  For example, `{ n + 1 | n < 3 }` will
be interpreted as `{ x : Nat | ∃ n < 3, n + 1 = x }` rather than using pattern matching.
 -/
Mathlib.Meta.macroPattSetBuilder : Lean.ParserDescr
-- Mathlib.Combinatorics.Graph.Delete
Graph.deleteEdges_le : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β} {F : Set β}, G.deleteEdges F ≤ G
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instSemiringOfMulOpposite : {M : Type u_1} → [Semiring Mᵐᵒᵖ] → Semiring Mᵈᵐᵃ
-- Mathlib.RingTheory.Multiplicity
FiniteMultiplicity.not_iff_forall : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, ¬FiniteMultiplicity a b ↔ ∀ (n : ℕ), a ^ n ∣ b