mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.t_fst_snd : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t 𝒰 f g i j)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g) (𝒰.f j))
          (𝒰.f i))
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.f j) f) g)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
        (𝒰.f j))
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g)
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintInfo.label : Lean.Elab.InlayHintInfo → Lean.Elab.InlayHintLabel
-- Mathlib.Algebra.BigOperators.GroupWithZero.Finset
Set.indicator_pi_one_apply : ∀ {ι : Type u_1} {M₀ : Type u_4} {α : ι → Type u_5} [inst : CommMonoidWithZero M₀] (s : Finset ι)
  (t : (i : ι) → Set (α i)) (f : (i : ι) → α i), ((↑s).pi t).indicator 1 f = ∏ i ∈ s, (t i).indicator 1 (f i)
-- Mathlib.Algebra.Category.Ring.Colimits
_private.Mathlib.Algebra.Category.Ring.Colimits.0.RingCat.Colimits.descFunLift.match_1.eq_4 : ∀ {J : Type u_1} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat)
  (motive : RingCat.Colimits.Prequotient F → Sort u_2) (x : RingCat.Colimits.Prequotient F)
  (h_1 : (j : J) → (x : ↑(F.obj j)) → motive (RingCat.Colimits.Prequotient.of j x))
  (h_2 : Unit → motive RingCat.Colimits.Prequotient.zero) (h_3 : Unit → motive RingCat.Colimits.Prequotient.one)
  (h_4 : (x : RingCat.Colimits.Prequotient F) → motive x.neg)
  (h_5 : (x y : RingCat.Colimits.Prequotient F) → motive (x.add y))
  (h_6 : (x y : RingCat.Colimits.Prequotient F) → motive (x.mul y)),
  (match x.neg with
    | RingCat.Colimits.Prequotient.of j x => h_1 j x
    | RingCat.Colimits.Prequotient.zero => h_2 ()
    | RingCat.Colimits.Prequotient.one => h_3 ()
    | x.neg => h_4 x
    | x.add y => h_5 x y
    | x.mul y => h_6 x y) =
    h_4 x
-- Init.Data.Nat.Lemmas
Nat.eq_zero_of_two_mul_le : ∀ {n : ℕ}, 2 * n ≤ n → n = 0
-- Init.Data.Repr
instReprUInt64 : Repr UInt64
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- The morphism in the derived category which corresponds to an element in `Ext X Y a`.  -/
CategoryTheory.Abelian.Ext.hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        {X Y : C} →
          [inst_3 : HasDerivedCategory C] →
            {a : ℕ} →
              CategoryTheory.Abelian.Ext X Y a →
                CategoryTheory.ShiftedHom ((DerivedCategory.singleFunctor C 0).obj X)
                  ((DerivedCategory.singleFunctor C 0).obj Y) ↑a
-- Mathlib.GroupTheory.OrderOfElement
CharP.orderOf_eq_two_iff : ∀ {R : Type u_6} [inst : Ring R] [Nontrivial R] [NoZeroDivisors R] (p : ℕ),
  p ≠ 2 → ∀ [CharP R p] {x : R}, orderOf x = 2 ↔ x = -1
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxKey!.induct_unfolding : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited α] (motive : Std.DTreeMap.Internal.Impl α β → α → Prop),
  motive Std.DTreeMap.Internal.Impl.leaf
      (panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.maxKey!" 436 13
        "Map is empty") →
    (∀ (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β),
        motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) k) →
      (∀ (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1)
          (l_1 r : Std.DTreeMap.Internal.Impl α β),
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)
              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxKey! →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))
              (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxKey!) →
        ∀ (a : Std.DTreeMap.Internal.Impl α β), motive a a.maxKey!
-- Mathlib.Analysis.RCLike.Lemmas
Polynomial.aeval_conj : ∀ {K : Type u_1} [inst : RCLike K] (p : Polynomial ℝ) (z : K),
  (Polynomial.aeval ((starRingEnd K) z)) p = (starRingEnd K) ((Polynomial.aeval z) p)
-- Std.Sync.CancellationContext
Std.CancellationContext.token : Std.CancellationContext → Std.CancellationToken
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.disjoint_iff_eq_or_eq : ∀ {α : Type u_1} {f g : Equiv.Perm α}, f.Disjoint g ↔ ∀ (x : α), f x = x ∨ g x = x
-- Mathlib.Probability.Kernel.Integral
ProbabilityTheory.Kernel.integral_congr_ae₂ : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f g : α → β → E}
  {μ : MeasureTheory.Measure α},
  (∀ᵐ (a : α) ∂μ, f a =ᵐ[κ a] g a) → ∫ (a : α), ∫ (b : β), f a b ∂κ a ∂μ = ∫ (a : α), ∫ (b : β), g a b ∂κ a ∂μ
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₄_app_four : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 4}
  (app₀ : f.obj' 0 _proof_361✝ ⟶ g.obj' 0 _proof_361✝) (app₁ : f.obj' 1 _proof_362✝ ⟶ g.obj' 1 _proof_362✝)
  (app₂ : f.obj' 2 _proof_363✝ ⟶ g.obj' 2 _proof_363✝) (app₃ : f.obj' 3 _proof_364✝ ⟶ g.obj' 3 _proof_364✝)
  (app₄ : f.obj' 4 _proof_365✝ ⟶ g.obj' 4 _proof_365✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝))
      _auto_405✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_363✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_363✝))
      _auto_407✝)
  (w₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_364✝) app₃ =
        CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_364✝))
      _auto_409✝)
  (w₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_365✝) app₄ =
        CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 _proof_364✝ _proof_365✝))
      _auto_411✝),
  (CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app
      ⟨4, CategoryTheory.ComposableArrows.homMk₄._proof_5⟩ =
    app₄
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
/-- Inverse of the `cos` function, returns values in the range `0 ≤ arccos x` and `arccos x ≤ π`.
It defaults to `π` on `(-∞, -1)` and to `0` to `(1, ∞)`.  -/
Real.arccos : ℝ → ℝ
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.coe_intCast : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R) (n : ℤ), ↑↑n = ↑n
-- Mathlib.CategoryTheory.Sites.Canonical
CategoryTheory.GrothendieckTopology.Subcanonical.of_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J K : CategoryTheory.GrothendieckTopology C},
  J ≤ K → ∀ [K.Subcanonical], J.Subcanonical
-- Mathlib.MeasureTheory.SetAlgebra
/-- The algebra of sets generated by `𝒜` contains `𝒜`.  -/
MeasureTheory.self_subset_generateSetAlgebra : ∀ {α : Type u_1} {𝒜 : Set (Set α)}, 𝒜 ⊆ MeasureTheory.generateSetAlgebra 𝒜
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.isClosedSubgraph_bot_iff : ∀ {α : Type u_1} {β : Type u_2} {G : Graph α β}, G.IsClosedSubgraph ⊥ ↔ G = ⊥
-- Mathlib.Analysis.Normed.Field.Lemmas
NormedField.completeSpace_iff_isComplete_closedBall : ∀ {K : Type u_4} [inst : NormedField K], CompleteSpace K ↔ IsComplete (Metric.closedBall 0 1)
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- If two affine equivalences agree on a set that spans the entire space, then they are equal.  -/
AffineEquiv.ext_on : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] {V₂ : Type u_8} {P₂ : Type u_9} [inst_4 : AddCommGroup V₂] [inst_5 : Module k V₂]
  [inst_6 : AddTorsor V₂ P₂] {s : Set P₁},
  affineSpan k s = ⊤ → ∀ (T₁ T₂ : P₁ ≃ᵃ[k] P₂), Set.EqOn (⇑T₁) (⇑T₂) s → T₁ = T₂
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
pow_div_pow_eventuallyEq_atTop : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {p q : ℕ},
  (fun x => x ^ p / x ^ q) =ᶠ[Filter.atTop] fun x => x ^ (↑p - ↑q)
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  (m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty)
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.ae_ae_of_ae_comp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} {p : β → Prop},
  (∀ᵐ (ω : β) ∂μ.bind ⇑κ, p ω) → ∀ᵐ (ω' : α) ∂μ, ∀ᵐ (ω : β) ∂κ ω', p ω
-- Init.Data.Nat.Lemmas
Nat.le_sub_of_add_le' : ∀ {n k m : ℕ}, m + n ≤ k → n ≤ k - m
-- ProofWidgets.Component.MakeEditLink
/-- Returns the number of bytes required to encode this `Char` in UTF-16.  -/
_private.ProofWidgets.Component.MakeEditLink.0.ProofWidgets.Internal.utf16Size : Char → UInt32
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.to_subtype_range : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  AlgebraicIndependent R x → AlgebraicIndependent R Subtype.val
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.expandShow : Lean.Macro
-- Mathlib.NumberTheory.ModularForms.NormTrace
_private.Mathlib.NumberTheory.ModularForms.NormTrace.0.term𝒬 : Lean.ParserDescr
-- Mathlib.Logic.Denumerable
_private.Mathlib.Logic.Denumerable.0.Nat.Subtype.ofNat.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Init.SimpLemmas
Decidable.decide.congr_simp : ∀ (p p_1 : Prop), p = p_1 → ∀ {h : Decidable p} [h_1 : Decidable p_1], decide p = decide p_1
-- Mathlib.RingTheory.Localization.Defs
/-- Everything in the image of `algebraMap` is a unit.  -/
IsLocalization.map_units : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (y : ↥M), IsUnit ((algebraMap R S) ↑y)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
IsFreeAddGroup.of.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : IsFreeAddGroup G],
  IsFreeAddGroup.of = (IsFreeAddGroup.addEquiv G).toFun ∘ FreeAddGroup.of
-- Mathlib.Dynamics.BirkhoffSum.Average
birkhoffAverage_one' : ∀ (R : Type u_1) {α : Type u_2} {M : Type u_3} [inst : DivisionSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (f : α → α) (g : α → M), birkhoffAverage R f g 1 = g
-- Lean.Elab.Do.Switch
Lean.Elab.Term.expandTermFor : Lean.Macro
-- Mathlib.Data.PFunctor.Multivariate.Basic
/-- The child family of types  -/
MvPFunctor.B : {n : ℕ} → (self : MvPFunctor.{u} n) → self.A → TypeVec.{u} n
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_sub_two_pi : ∀ (x : ℝ), Real.cos (x - 2 * Real.pi) = Real.cos x
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
ProbabilityTheory.BrownianReal.integral_id_projectiveFamily' : ∀ (I : Finset NNReal), ∫ (x : ↥I → ℝ), id x ∂ProbabilityTheory.BrownianReal.projectiveFamily I = 0
-- Std.Time.Format.Basic
Std.Time.Awareness.only.inj : ∀ {a a_1 : Std.Time.TimeZone}, Std.Time.Awareness.only a = Std.Time.Awareness.only a_1 → a = a_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_alter! : ∀ {α : 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.Const.alter! k f t).size =
        if k ∈ t ∧ (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isNone = true then t.size - 1
        else if k ∉ t ∧ (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true then t.size + 1 else t.size
-- Mathlib.RingTheory.Radical.NatInt
Nat.one_lt_radical_iff : ∀ {n : ℕ}, 1 < UniqueFactorizationMonoid.radical n ↔ 1 < n
-- Mathlib.Algebra.Ring.Hom.Defs
/-- Composition of ring homomorphisms is a ring homomorphism.  -/
RingHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      {x : NonAssocSemiring α} →
        {x_1 : NonAssocSemiring β} → {x_2 : NonAssocSemiring γ} → (β →+* γ) → (α →+* β) → α →+* γ
-- Mathlib.CategoryTheory.Limits.Shapes.StrongEpi
CategoryTheory.StrongMono.iff_of_arrow_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B A' B' : C} {f : B ⟶ A} {g : B' ⟶ A'}
  (e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk g), CategoryTheory.StrongMono f ↔ CategoryTheory.StrongMono g
-- Mathlib.Algebra.Lie.OfAssociative
LieModule.toEnd_pow_lie : ∀ (R : Type u) {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (x y : L)
  (z : M) (n : ℕ),
  ((LieModule.toEnd R L M) x ^ n) ⁅y, z⁆ =
    ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n,
      n.choose ij.1 • ⁅((LieAlgebra.ad R L) x ^ ij.1) y, ((LieModule.toEnd R L M) x ^ ij.2) z⁆
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.mk.inj : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S}
  {toGenerators : Algebra.Generators R S ι} {relation : σ → toGenerators.Ring}
  {span_range_relation_eq_ker : Ideal.span (Set.range relation) = toGenerators.ker}
  {toGenerators_1 : Algebra.Generators R S ι} {relation_1 : σ → toGenerators_1.Ring}
  {span_range_relation_eq_ker_1 : Ideal.span (Set.range relation_1) = toGenerators_1.ker},
  { toGenerators := toGenerators, relation := relation, span_range_relation_eq_ker := span_range_relation_eq_ker } =
      { toGenerators := toGenerators_1, relation := relation_1,
        span_range_relation_eq_ker := span_range_relation_eq_ker_1 } →
    toGenerators = toGenerators_1 ∧ relation = relation_1
-- Lean.Util.Recognizers
Lean.Expr.isHEq : Lean.Expr → Bool
-- Mathlib.Order.Filter.IsBounded
Filter.IsBoundedUnder.bddAbove_range_of_cofinite : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [IsDirectedOrder β] {f : α → β},
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) Filter.cofinite f → BddAbove (Set.range f)
-- Init.Data.String.Basic
String.head_toList : ∀ {b : String} {h : b.toList ≠ []}, b.toList.head h = b.toByteArray.utf8DecodeChar 0 ⋯
-- Mathlib.LinearAlgebra.Dimension.LinearMap
LinearMap.rank_le_range : ∀ {K : Type u} {V : Type v} {V' : Type v'} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V'] [inst_4 : Module K V'] (f : V →ₗ[K] V'), f.rank ≤ Module.rank K V'
-- Mathlib.Order.Hom.Basic
lt_map_inv_iff : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : EquivLike F α β]
  [OrderIsoClass F α β] (f : F) {a : α} {b : β}, a < EquivLike.inv f b ↔ f a < b
-- Lean.Elab.Tactic.Grind.Main
/-- Filter out `+suggestions` and `+locals` from the config syntax  -/
Lean.Elab.Tactic.filterSuggestionsAndLocalsFromGrindConfig : Lean.TSyntax `Lean.Parser.Tactic.optConfig → Lean.TSyntax `Lean.Parser.Tactic.optConfig
-- Mathlib.LinearAlgebra.TensorProduct.Pi
/-- (Implementation): Inverse for `TensorProduct.piRight`.  -/
TensorProduct.piRightInv : (R : Type u_1) →
  [inst : CommSemiring R] →
    (S : Type u_2) →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (N : Type u_3) →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                [inst_5 : Module S N] →
                  [inst_6 : IsScalarTower R S N] →
                    {ι : Type u_4} →
                      (M : ι → Type u_5) →
                        [inst_7 : (i : ι) → AddCommMonoid (M i)] →
                          [inst_8 : (i : ι) → Module R (M i)] →
                            [Fintype ι] →
                              [DecidableEq ι] →
                                ((i : ι) → TensorProduct R N (M i)) →ₗ[S] TensorProduct R N ((i : ι) → M i)
-- Mathlib.CategoryTheory.Monoidal.Rigid.OfEquivalence
/-- Pull back a left dual along an equivalence.  -/
CategoryTheory.hasLeftDualOfEquivalence : {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.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              [F.Monoidal] →
                {G : CategoryTheory.Functor D C} →
                  (F ⊣ G) →
                    [F.IsEquivalence] → (X : C) → [CategoryTheory.HasLeftDual (F.obj X)] → CategoryTheory.HasLeftDual X
-- Mathlib.Algebra.Order.Monoid.OrderDual
OrderDual.isOrderedAddCancelMonoid : ∀ {α : Type u} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedCancelAddMonoid α], IsOrderedCancelAddMonoid αᵒᵈ
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.neighborFinset_eq_filter : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] {v : V} [inst_1 : DecidableRel G.Adj],
  G.neighborFinset v = {w | G.Adj v w}
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.pairwise_toList_ne : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α], List.Pairwise (fun a b => a ≠ b) r.toList
-- Mathlib.Topology.Algebra.Module.ModuleTopology
IsModuleTopology.topologicalAddGroup : ∀ (R : Type u_1) [τR : TopologicalSpace R] [inst : Semiring R] (C : Type u_6) [inst_1 : AddCommGroup C]
  [inst_2 : Module R C] [inst_3 : TopologicalSpace C] [IsModuleTopology R C], IsTopologicalAddGroup C
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- The upper shadow of a family of `r`-sets is a family of `r + 1`-sets.  -/
Set.Sized.upShadow : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {𝒜 : Finset (Finset α)} {r : ℕ},
  Set.Sized r ↑𝒜 → Set.Sized (r + 1) ↑𝒜.upShadow
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coneOpEquiv_functor_map_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} {X Y : (CategoryTheory.Limits.Cone F)ᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.Limits.coneOpEquiv.functor.map f).hom = f.unop.hom.op
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- To prove a property of a sum, it suffices to prove that
the property is additive and holds on summands.  -/
Finset.sum_induction_nonempty : ∀ {ι : Type u_1} {s : Finset ι} {M : Type u_7} [inst : AddCommMonoid M] (f : ι → M) (p : M → Prop),
  (∀ (a b : M), p a → p b → p (a + b)) → s.Nonempty → (∀ x ∈ s, p (f x)) → p (∑ x ∈ s, f x)
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableSMul₂.measurable_smul : ∀ {M : Type u_2} {α : Type u_3} {inst : SMul M α} {inst_1 : MeasurableSpace M} {inst_2 : MeasurableSpace α}
  [self : MeasurableSMul₂ M α], Measurable (Function.uncurry fun x1 x2 => x1 • x2)
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.dotId.sizeOf_spec : ∀ (stx : Lean.Syntax) (id : Lean.Name) (lctx : Lean.LocalContext) (expectedType? : Option Lean.Expr),
  sizeOf (Lean.Elab.CompletionInfo.dotId stx id lctx expectedType?) =
    1 + sizeOf stx + sizeOf id + sizeOf lctx + sizeOf expectedType?
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.charLitNoAntiquot.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- If `v` is a real infinite place, then the embedding `v.Completion →+* ℝ` is bijective.  -/
NumberField.InfinitePlace.Completion.bijective_extensionEmbeddingOfIsReal : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K} (hv : v.IsReal),
  Function.Bijective ⇑(NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal hv)
-- Std.Internal.Do.WP.Basic
Std.Internal.Do.WP.wp_econs_le : ∀ {Pred : Type u_2} {EPred : Type u_1} {Prog : Type u} {Value : Type v} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] (x : Prog)
  (post : Value → Pred) (epost epost' : EPred),
  Lean.Order.PartialOrder.rel epost epost' →
    ∀ {pre : Pred},
      Lean.Order.PartialOrder.rel pre (Std.Internal.Do.wp x post epost) →
        Lean.Order.PartialOrder.rel pre (Std.Internal.Do.wp x post epost')
-- Mathlib.Topology.MetricSpace.Cover
/-- **Alias** of the forward direction of `Metric.isCover_iff_subset_iUnion_closedBall`. -/
Metric.IsCover.subset_iUnion_closedBall : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {ε : NNReal} {s N : Set X},
  Metric.IsCover ε s N → s ⊆ ⋃ y ∈ N, Metric.closedBall y ↑ε
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.map_toSubmodule : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] {S : NonUnitalSubalgebra R A} {f : F},
  (NonUnitalSubalgebra.map f S).toSubmodule = Submodule.map (LinearMapClass.linearMap f) S.toSubmodule
-- Lean.Meta.AppBuilder
/-- Given `hp : P` and `nhp : Not P`, returns an instance of type `e`.  -/
Lean.Meta.mkAbsurd : Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.RingTheory.Congruence.Defs
RingConGen.Rel.mul : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop} {w x y z : R},
  RingConGen.Rel r w x → RingConGen.Rel r y z → RingConGen.Rel r (w * y) (x * z)
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.expandNestedAction : Lean.Syntax → Lean.Elab.Term.Do.ToCodeBlock.M (List Lean.Syntax × Lean.Syntax)
-- Mathlib.Computability.Halting
ComputablePred.halting_problem_not_re : ∀ (n : ℕ), ¬REPred fun c => ¬(c.eval n).Dom
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integral_sub : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f g : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
  BoxIntegral.Integrable I l f vol →
    BoxIntegral.Integrable I l g vol →
      BoxIntegral.integral I l (f - g) vol = BoxIntegral.integral I l f vol - BoxIntegral.integral I l g vol
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.forIn'_toList.aux : ∀ {ρ : Type u} {α : Type v} {γ : Type x} {m : Type x → Type x'} [Monad m] {x : Membership α ρ}
  [inst : ForIn' m ρ α inferInstance] {r s : ρ} {init : γ} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} (h : r = s),
  forIn' r init f = forIn' s init fun a h' acc => f a ⋯ acc
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.flip_zero : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] [inst_10 : RingHomIsometric σ₁₃], ContinuousLinearMap.flip 0 = 0