mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.eval_map : ∀ (S : CategoryTheory.Functor Type uᵒᵖ (Type u)) (α β : Type u) (f : β ⟶ α) (s : (fun X => X) (S.obj (Opposite.op α)))
  (x : (fun X => X) β),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eval S β ((CategoryTheory.ConcreteCategory.hom (S.map f.op)) s)))
      x =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.eval S α s)) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.Logic.Equiv.Sum
/-- Combine two `Equiv`s using `Sum` in the domain and `PSum` in the codomain.  -/
Equiv.sumPSum : {α₂ : Sort u_3} → {β₂ : Sort u_6} → {α₁ : Type u_9} → {β₁ : Type u_10} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ⊕ β₁ ≃ α₂ ⊕' β₂
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.SymmStruct.iso_hom_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w}
  {I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C} (self : I.SymmStruct)
  (i j : ι) {Z : C} (h : I.right ((CategoryTheory.Limits.MultispanShape.prod ι).snd (j, i)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.iso i j).hom (CategoryTheory.CategoryStruct.comp (I.snd (j, i)) h) =
    CategoryTheory.CategoryStruct.comp (I.fst (i, j)) h
-- Init.Grind.Ring.Basic
/-- Two numerals in a semiring are equal iff they are congruent module `p` in the natural numbers.  -/
Lean.Grind.IsCharP.ofNat_ext_iff : ∀ {α : Type u} {inst : Lean.Grind.Semiring α} (p : outParam ℕ) [self : Lean.Grind.IsCharP α p] {x y : ℕ},
  OfNat.ofNat x = OfNat.ofNat y ↔ x % p = y % p
-- Mathlib.Order.Cover
CovBy.Ioc_eq : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, b ⋖ a → Set.Ioc b a = {a}
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Triangle.affineSpan_pair_eq_orthRadius_insphere : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) [Fact (Module.finrank ℝ V = 2)] {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        line[ℝ, t.points i₂, t.points i₃] = (Affine.Simplex.insphere t).orthRadius (Affine.Simplex.touchpoint t ∅ i₁)
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Inner
Measurable.inner : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {x : MeasurableSpace α} [inst_3 : MeasurableSpace E] [OpensMeasurableSpace E]
  [SecondCountableTopology E] {f g : α → E}, Measurable f → Measurable g → Measurable fun t => inner 𝕜 (f t) (g t)
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.Decl.relabel.eq_3 : ∀ {α β : Type} (r : α → β) (lhs rhs : Std.Sat.AIG.Fanin),
  Std.Sat.AIG.Decl.relabel r (Std.Sat.AIG.Decl.gate lhs rhs) = Std.Sat.AIG.Decl.gate lhs rhs
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.Prod.snd_mapId_inv : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C] (x : B × C),
  ((CategoryTheory.Bicategory.Prod.snd B C).mapId x).inv =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id x.2)
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.cRank_zero : ∀ {R : Type uR} {m : Type u_1} {n : Type u_2} [inst : Semiring R] [Nontrivial R], Matrix.cRank 0 = 0
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.compl_range_path : ∀ {x y : Circle}, x ≠ y → (Set.range ⇑(x.path y))ᶜ = ⇑(y.path x) '' Set.Ioo 0 1
-- Mathlib.LinearAlgebra.Matrix.Invertible
/-- A copy of `invOf_mul_cancel_left` for rectangular matrices.  -/
Matrix.invOf_mul_cancel_left : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring α]
  (A : Matrix n n α) (B : Matrix n m α) [inst_3 : Invertible A], ⅟A * (A * B) = B
-- Mathlib.Topology.Instances.AddCircle.Defs
continuousAt_toIocMod : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [inst_3 : Archimedean 𝕜] [inst_4 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {p : 𝕜} (hp : 0 < p) (a : 𝕜) {x : 𝕜},
  ¬x ≡ a [PMOD p] → ContinuousAt (toIocMod hp a) x
-- Aesop.Util.Basic
Aesop.forEachExprInGoal' : {ω : Type} →
  {m : Type → Type} →
    [STWorld ω m] →
      [MonadLiftT (ST ω) m] →
        [Monad m] →
          [MonadControlT Lean.MetaM m] → [MonadLiftT Lean.MetaM m] → Lean.MVarId → (Lean.Expr → m Bool) → m Unit
-- Init.Data.Int.Order
Int.lt_of_add_lt_add_right : ∀ {a b c : ℤ}, a + b < c + b → a < c
-- Mathlib.Analysis.Distribution.DerivNotation
LineDerivLeftSMul.lineDerivOp_left_smul : ∀ {R : Type u_11} {V : Type u} {E : Type v} {F : outParam (Type w)} {inst : SMul R V} {inst_1 : SMul R F}
  {inst_2 : LineDeriv V E F} [self : LineDerivLeftSMul R V E F] (r : R) (v : V) (x : E),
  LineDeriv.lineDerivOp (r • v) x = r • LineDeriv.lineDerivOp v x
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
/-- **Alias** of the forward direction of `measurable_iff_le_map`. -/
Measurable.le_map : ∀ {α : Type u_1} {β : Type u_2} {m₁ : MeasurableSpace α} {m₂ : MeasurableSpace β} {f : α → β},
  Measurable f → m₂ ≤ MeasurableSpace.map f m₁
-- Mathlib.Data.QPF.Univariate.Basic
QPF.lawfulFunctor : ∀ {F : Type u → Type v} [q : QPF F],
  (∀ (α β : Type u), Functor.mapConst = Functor.map ∘ Function.const β) → LawfulFunctor F
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
/-- A cover of a scheme is quasi-compact if every affine open of the base can be covered
by a finite union of images of quasi-compact opens of the components.
 -/
AlgebraicGeometry.QuasiCompactCover : {S : AlgebraicGeometry.Scheme} → CategoryTheory.PreZeroHypercover S → Prop
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
parallelepiped_eq_sum_segment : ∀ {ι : Type u_1} {E : Type u_3} [inst : Fintype ι] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] (v : ι → E),
  parallelepiped v = ∑ i, segment ℝ 0 (v i)
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.log_exp_eq_sub_toIocDiv : ∀ (x : ℂ), Complex.log (Complex.exp x) = x - ↑(toIocDiv Real.two_pi_pos (-Real.pi) x.im) * (2 * ↑Real.pi * Complex.I)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso_hom_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {i i' j j' : E.I₀} (u₀ : E.I₀ → F.I₀)
  (u₁ : (i j : E.I₀) → E.I₁ i j → F.I₁ (u₀ i) (u₀ j)) (z : (i j : E.I₀) → (k : E.I₁ i j) → E.Y k ⟶ F.Y (u₁ i j k))
  (hii' : i = i') (hjj' : j = j') (k : E.I₁ i j) {Z : C} (h : F.Y (u₁ i j k) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso hii' hjj' k).hom
      (CategoryTheory.CategoryStruct.comp (z i j k) h) =
    CategoryTheory.CategoryStruct.comp (z i' j' ((CategoryTheory.PreOneHypercover.congrIndexOneOfEq hii' hjj') k))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso ⋯ ⋯ (u₁ i j k)).hom
          h))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₁₂_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  CategoryTheory.CategoryStruct.comp h.p₁₂ h₁₂.p₁ = h.p₁
-- Mathlib.Order.SuccPred.Limit
/-- **Alias** of `Order.not_isSuccPrelimit_iff_mem_range_succ`. -/
Order.not_isSuccPrelimit_iff' : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : SuccOrder α] [NoMaxOrder α],
  ¬Order.IsSuccPrelimit a ↔ a ∈ Set.range Order.succ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_insertMany_empty_list_le : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} [Std.TransOrd α] {l : List ((a : α) × β a)},
  (↑(Std.DTreeMap.Internal.Impl.empty.insertMany l ⋯)).size ≤ l.length
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.mk.inj : ∀ {α : Type u} {next : Option α} {upperBound : α} {next_1 : Option α} {upperBound_1 : α},
  { next := next, upperBound := upperBound } = { next := next_1, upperBound := upperBound_1 } →
    next = next_1 ∧ upperBound = upperBound_1
-- Init.Data.Float.Model.Float32
/-- Converts a `UInt8` to a `Float32.Model`, returning positive zero on zero.  -/
Float32.Model.ofUInt8 : UInt8 → Float32.Model
-- Mathlib.Order.WellFoundedSet
/-- In a linear order, the predicates `Set.IsPWO` and `Set.IsWF` are equivalent.  -/
Set.isPWO_iff_isWF : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Set α}, s.IsPWO ↔ s.IsWF
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBiproductData.op_bicone : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (d : CategoryTheory.Limits.BinaryBiproductData P Q), d.op.bicone = d.bicone.op
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereographic_target : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1),
  (stereographic hv).target = Set.univ
-- Init.Data.Vector.Range
Vector.zipIdx_map_snd : ∀ {α : Type u_1} {n : ℕ} (i : ℕ) (xs : Vector α n), Vector.map Prod.snd (xs.zipIdx i) = Vector.range' i n
-- Init.WF
Acc.inv : ∀ {α : Sort u} {r : α → α → Prop} {x y : α}, Acc r x → r y x → Acc r y
-- Mathlib.Geometry.Convex.ConvexSpace.Module
/-- Eta-expanded form of `Convexity.IsAffineMap.sub` -/
Convexity.IsAffineMap.fun_sub : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M]
  [inst_9 : Convexity.ConvexSpace R N] [Convexity.IsModuleConvexSpace R N] {f g : M → N},
  Convexity.IsAffineMap R f → Convexity.IsAffineMap R g → Convexity.IsAffineMap R fun i => f i - g i
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instMonoid : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] → [inst_3 : Module A V] → (ρ : Representation A G V) → Monoid (ρ.IntertwiningMap ρ)
-- Mathlib.Topology.Defs.Induced
Topology.IsOpenEmbedding.mk : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y},
  Topology.IsEmbedding f → IsOpen (Set.range f) → Topology.IsOpenEmbedding f
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Slice.Pos.find?_prop_eq_none_iff : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  pos.find? p = none ↔ ∀ (pos' : s.Pos), pos ≤ pos' → ∀ (h : pos' ≠ s.endPos), ¬p (pos'.get h)
-- Mathlib.Algebra.GroupWithZero.ProdHom
/-- Given groups with zero `G₀`, `H₀`, the natural projection homomorphism from
`WithZero (G₀ˣ × H₀ˣ)` to `G₀`, which is the group with zero that can be identified
as their product.  -/
MonoidWithZeroHom.fst : (G₀ : Type u_1) →
  (H₀ : Type u_2) → [inst : GroupWithZero G₀] → [inst_1 : GroupWithZero H₀] → WithZero (G₀ˣ × H₀ˣ) →*₀ G₀
-- Init.Sym.Lemmas
Lean.Sym.ite_false_congr : ∀ {α : Sort u} (c : Prop) {inst : Decidable c} (a b : α) (c' : Prop), c = c' → ∀ {ht : ¬c'}, (if c then a else b) = b
-- Mathlib.Order.Nucleus
/-- Restrict a nucleus to its range.  -/
Nucleus.restrict : {X : Type u_1} → [inst : Order.Frame X] → (n : Nucleus X) → FrameHom X ↑(Set.range ⇑n)
-- Mathlib.RingTheory.Noetherian.Defs
LinearMap.eventually_iSup_ker_pow_eq : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsNoetherian R M]
  (f : M →ₗ[R] M), ∀ᶠ (n : ℕ) in Filter.atTop, ⨆ m, (f ^ m).ker = (f ^ n).ker
-- Aesop.Tree.Data
Aesop.GoalData.isIrrelevant : {Rapp MVarCluster : Type} → Aesop.GoalData Rapp MVarCluster → Bool
-- Lean.Declaration
Lean.ReducibilityHints.regular : UInt32 → Lean.ReducibilityHints
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- `MeromorphicNFOn` is invariant under translation.  -/
meromorphicNFOn_comp_add_const_iff_meromorphicNFOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {U : Set 𝕜},
  MeromorphicNFOn (f ∘ fun x => x + c) U ↔ MeromorphicNFOn f (U + {c})
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_filter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  {f : α → β → Bool} {k : α} (h : t.WF)
  {h' : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filter! f t) = true},
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.filter! f t) k h' =
    Std.DTreeMap.Internal.Impl.Const.get t k ⋯
-- Mathlib.Analysis.CStarAlgebra.Matrix
/-- The metric on `Matrix m n 𝕜` arising from the operator norm given by the identification with
(continuous) linear maps of `EuclideanSpace`.  -/
Matrix.instL2OpMetricSpace : {𝕜 : Type u_1} →
  {m : Type u_2} →
    {n : Type u_3} → [RCLike 𝕜] → [Fintype m] → [Fintype n] → [DecidableEq n] → MetricSpace (Matrix m n 𝕜)
-- Mathlib.Data.Set.NAry
/-- The other direction does not hold because of the `s`-`s` cross terms on the RHS.  -/
Set.image2_distrib_subset_left : ∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {γ' : Type u_6} {δ : Type u_7} {ε : Type u_9} {s : Set α}
  {t : Set β} {u : Set γ} {f : α → δ → ε} {g : β → γ → δ} {f₁ : α → β → β'} {f₂ : α → γ → γ'} {g' : β' → γ' → ε},
  (∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)) →
    Set.image2 f s (Set.image2 g t u) ⊆ Set.image2 g' (Set.image2 f₁ s t) (Set.image2 f₂ s u)
-- Mathlib.GroupTheory.Coset.Basic
normal_iff_eq_addCosets : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), s.Normal ↔ ∀ (g : α), g +ᵥ ↑s = AddOpposite.op g +ᵥ ↑s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_alter_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {fallback : β} {f : Option β → Option β},
  Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl k fallback =
    (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).getD fallback
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCoconeWhisker_inv_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C}
  {E : CategoryTheory.Functor K J} {c : CategoryTheory.Limits.Cocone F},
  H.mapCoconeWhisker.inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.isUnit_iff_mem_nonZeroDivisors_of_mulOpposite : ∀ {R : Type u_1} [inst : Ring R] [IsArtinianRing Rᵐᵒᵖ] {a : R}, IsUnit a ↔ a ∈ nonZeroDivisors R
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.isIntertwining : ∀ {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} (φ : ρ.Equiv σ) (g : G),
  ↑φ.toContinuousLinearEquiv ∘SL ρ g = σ g ∘SL ↑φ.toContinuousLinearEquiv
-- Mathlib.Data.Set.Sups
Set.infs_infs_infs_comm : ∀ {α : Type u_2} [inst : SemilatticeInf α] (s t u v : Set α), s ⊼ t ⊼ (u ⊼ v) = s ⊼ u ⊼ (t ⊼ v)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.StAct.peek : {K : Type u_1} → {Γ : K → Type u_2} → {σ : Type u_4} → {k : K} → (σ → Option (Γ k) → σ) → Turing.TM2to1.StAct K Γ σ k
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.nnrealPart_apply : ∀ {α : Type u_2} [inst : TopologicalSpace α] (f : CompactlySupportedContinuousMap α ℝ) (x : α),
  f.nnrealPart x = (f x).toNNReal
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.Cofix.dest_mk : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : F (α ::: MvQPF.Cofix F α)),
  (MvQPF.Cofix.mk x).dest = x
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.vanishingIdeal_eq_top_iff : ∀ {R : Type u} [inst : CommSemiring R] {s : Set (PrimeSpectrum R)}, PrimeSpectrum.vanishingIdeal s = ⊤ ↔ s = ∅
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is differentiable and `f'` is antitone on `ℝ` then `f` is concave.  -/
Antitone.concaveOn_univ_of_deriv : ∀ {f : ℝ → ℝ}, Differentiable ℝ f → Antitone (deriv f) → ConcaveOn ℝ Set.univ f
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.End.mul_def : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {X : C} (xs ys : CategoryTheory.End X),
  xs * ys = CategoryTheory.CategoryStruct.comp ys xs
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommGroup.compLeft.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) {H' : Type u_6} [inst_7 : TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E H')
  (M : Type u) [inst_8 : TopologicalSpace M] [inst_9 : ChartedSpace HM M] (A A' : Type u) [inst_10 : TopologicalSpace A]
  [inst_11 : ChartedSpace H A] [inst_12 : TopologicalSpace A'] [inst_13 : ChartedSpace H' A'] [inst_14 : CommGroup A]
  [inst_15 : CommGroup A'] [inst_16 : LieGroup I (↑⊤) A] [inst_17 : LieGroup I' (↑⊤) A'] (φ : A →* A')
  (hφ : ContMDiff I I' ↑⊤ ⇑φ),
  smoothSheafCommGroup.compLeft IM I I' M A A' φ hφ =
    CategoryTheory.ObjectProperty.homMk
      { app := fun x => CommGrpCat.ofHom (ContMDiffMap.compLeftMonoidHom IM (↥(Opposite.unop x)) φ hφ),
        naturality := ⋯ }
-- Mathlib.Data.Seq.Computation
Computation.BisimO.eq_3 : ∀ {α : Type u} (R : Computation α → Computation α → Prop) (x x_1 : α ⊕ Computation α),
  (∀ (a a' : α), x = Sum.inl a → x_1 = Sum.inl a' → False) →
    (∀ (s s' : Computation α), x = Sum.inr s → x_1 = Sum.inr s' → False) → Computation.BisimO R x x_1 = False
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_37 : HAdd Std.Time.Week.Offset Std.Time.Millisecond.Offset Std.Time.Millisecond.Offset
-- Mathlib.Order.Filter.Bases.Basic
FilterBasis.mk.injEq : ∀ {α : Type u_6} (sets : Set (Set α)) (nonempty : sets.Nonempty)
  (inter_sets : ∀ {x y : Set α}, x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y) (sets_1 : Set (Set α))
  (nonempty_1 : sets_1.Nonempty) (inter_sets_1 : ∀ {x y : Set α}, x ∈ sets_1 → y ∈ sets_1 → ∃ z ∈ sets_1, z ⊆ x ∩ y),
  ({ sets := sets, nonempty := nonempty, inter_sets := inter_sets } =
      { sets := sets_1, nonempty := nonempty_1, inter_sets := inter_sets_1 }) =
    (sets = sets_1)
-- Mathlib.Analysis.Calculus.ContDiff.Basic
ContinuousLinearEquiv.contDiff : ∀ {𝕜 : 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] {n : WithTop ℕ∞}
  (f : E ≃L[𝕜] F), ContDiff 𝕜 n ⇑f
-- Mathlib.NumberTheory.Transcendental.Liouville.Residual
setOfPred_liouville_eq_iInter_iUnion : {x | Liouville x} = ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), Metric.ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b}
-- Mathlib.Algebra.Order.BigOperators.Ring.Finset
/-- If `g, h ≤ f` and `g i + h i ≤ f i`, then the product of `f` over `s` is at least the
sum of the products of `g` and `h`. This is the version for `CanonicallyOrderedAdd`.
 -/
Finset.prod_add_prod_le' : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R]
  {f g h : ι → R} {s : Finset ι} {i : ι},
  i ∈ s →
    g i + h i ≤ f i →
      (∀ j ∈ s, j ≠ i → g j ≤ f j) → (∀ j ∈ s, j ≠ i → h j ≤ f j) → ∏ i ∈ s, g i + ∏ i ∈ s, h i ≤ ∏ i ∈ s, f i
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsUpperSet.specializes_iff_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpperSet α] {a b : α}, a ⤳ b ↔ b ≤ a
-- Mathlib.Order.Directed
DirectedOn.eq_1 : ∀ {α : Type u_1} (r : α → α → Prop) (s : Set α), DirectedOn r s = ∀ x ∈ s, ∀ y ∈ s, ∃ z ∈ s, r x z ∧ r y z
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.pow.match_1.congr_eq_1 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (k : ℕ) → motive k.succ),
  k = 0 →
    (match k with
      | 0 => h_1 ()
      | 1 => h_2 ()
      | k.succ => h_3 k) ≍
      h_1 ()
-- Mathlib.Data.Multiset.UnionInter
Multiset.sub_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α), s - s ∩ t = s - t
-- Mathlib.LinearAlgebra.TensorProduct.Vanishing
Equiv.vanishesTrivially_comp : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι : Type u_4} [inst_5 : Fintype ι] {m : ι → M} {n : ι → N}
  {κ : Type u_5} [inst_6 : Fintype κ] (e : κ ≃ ι),
  TensorProduct.VanishesTrivially R (m ∘ ⇑e) (n ∘ ⇑e) ↔ TensorProduct.VanishesTrivially R m n
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Cat
CategoryTheory.Monoidal.whiskerLeft_snd : ∀ (X : CategoryTheory.Cat) {A B : CategoryTheory.Cat} (f : A ⟶ B),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).toFunctor.comp (CategoryTheory.Prod.snd ↑X ↑B) =
    (CategoryTheory.Prod.snd ↑X ↑A).comp f.toFunctor
-- Lean.Elab.Command.Scope
/-- All currently `open`ed namespaces and names.  -/
Lean.Elab.Command.Scope.openDecls : Lean.Elab.Command.Scope → List Lean.OpenDecl
-- Init.Data.Int.DivMod.Bootstrap
Int.dvd_refl : ∀ (n : ℤ), n ∣ n
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.checkClassAbbrev : Lean.Linter.MissingDocs.SimpleHandler
-- Aesop.Tree.Data
Aesop.Goal.parentMetaState : Aesop.Goal → Lean.Meta.SavedState → BaseIO Lean.Meta.SavedState
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.rightDerived_fac_app_assoc : ∀ {C : Type u_3} {D : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (RF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : F ⟶ L.comp RF) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : RF.IsRightDerivedFunctor α W] (G : CategoryTheory.Functor D H) (β : F ⟶ L.comp G) (X : C) {Z : H}
  (h : G.obj (L.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.app X)
      (CategoryTheory.CategoryStruct.comp ((RF.rightDerivedDesc α W G β).app (L.obj X)) h) =
    CategoryTheory.CategoryStruct.comp (β.app X) h
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.mk_l_inv : ∀ {C : Type u} {X : CategoryTheory.FreeMonoidalCategory C},
  ⟦CategoryTheory.FreeMonoidalCategory.Hom.l_inv X⟧ = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
-- Mathlib.Data.List.Pairwise
List.Pairwise.head!_le : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} {a : α} [inst : Inhabited α] [Std.Refl R],
  List.Pairwise R l → a ∈ l → R l.head! a
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_coe_ne_top_iff_summable_coe : ∀ {α : Type u_1} {f : α → NNReal}, ∑' (a : α), ↑(f a) ≠ ⊤ ↔ Summable fun a => ↑(f a)
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.IsMittagLeffler.toPreimages : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J}
  (s : Set (F.obj i)) [CategoryTheory.IsCofilteredOrEmpty J], F.IsMittagLeffler → (F.toPreimages s).IsMittagLeffler