mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Compactness.SigmaCompact
/-- In a topological space with sigma compact topology, if `f` is a function that sends each
point `x` to a neighborhood of `x`, then for some countable set `s`, the neighborhoods `f x`,
`x ∈ s`, cover the whole space.  -/
countable_cover_nhds_of_sigmaCompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [SigmaCompactSpace X] {f : X → Set X},
  (∀ (x : X), f x ∈ nhds x) → ∃ s, s.Countable ∧ ⋃ x ∈ s, f x = Set.univ
-- Lean.Meta.Tactic.Grind.EMatch
/-- Helper function for collecting constants containing unassigned universe levels.
This functions is used by `assignUnassignedLevelMVars`
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.collectConstsWithLevelMVars : Lean.Expr → Lean.CoreM (Array Lean.Expr)
-- Mathlib.MeasureTheory.Function.Egorov
MeasureTheory.Egorov.tendstoUniformlyOn_sdiff_iUnionNotConvergentSeq : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [inst : PseudoEMetricSpace β]
  {μ : MeasureTheory.Measure α} {s : Set α} {ε : ℝ} {f : ι → α → β} {g : α → β} [inst_1 : SemilatticeSup ι]
  [inst_2 : Nonempty ι] [inst_3 : Countable ι] (hε : 0 < ε) (hf : ∀ (n : ι), Measurable fun a => edist (f n a) (g a))
  (hsm : MeasurableSet s) (hs : μ s ≠ ⊤)
  (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))),
  TendstoUniformlyOn f g Filter.atTop (s \ MeasureTheory.Egorov.iUnionNotConvergentSeq hε hf hsm hs hfg)
-- Mathlib.Data.Finset.Basic
Finset.empty_toList : ∀ {α : Type u_1} {s : Finset α}, s.toList.isEmpty = true ↔ s = ∅
-- Std.Time.Internal.UnitVal
Std.Time.Internal.UnitVal.instSub : {α : ℚ} → Sub (Std.Time.Internal.UnitVal α)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.Iso.reindex_adjMatrix : ∀ (α : Type u_1) {V : Type u_2} {W : Type u_3} {G : SimpleGraph V} [inst : DecidableRel G.Adj] [inst_1 : Zero α]
  [inst_2 : One α] {H : SimpleGraph W} [inst_3 : DecidableRel H.Adj] (f : G ≃g H),
  (Matrix.reindex ↑f ↑f) (SimpleGraph.adjMatrix α G) = SimpleGraph.adjMatrix α H
-- Init.Sym.Lemmas
Lean.Sym.Int8.lt_eq_true : ∀ (a b : Int8), decide (a < b) = true → (a < b) = True
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instModule' : {α : Type u} →
  {β : Type v} →
    {𝕜 : Type u_1} →
      [inst : NormedField 𝕜] →
        [inst_1 : TopologicalSpace α] →
          [inst_2 : SeminormedAddCommGroup β] →
            [NormedSpace 𝕜 β] → Module (BoundedContinuousFunction α 𝕜) (BoundedContinuousFunction α β)
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.SimpKind : Type
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_eq_size_eq_zero : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β}, m.isEmpty = (m.size == 0)
-- Mathlib.RingTheory.Polynomial.GaussNorm
_private.Mathlib.RingTheory.Polynomial.GaussNorm.0.Polynomial.mul_gaussNorm_le_gaussNorm_mul : ∀ {c : ℝ} {R : Type u_3} [inst : Ring R] {v : AbsoluteValue R ℝ},
  IsNonarchimedean ⇑v →
    0 < c →
      ∀ (p q : Polynomial R), Polynomial.gaussNorm v c p * Polynomial.gaussNorm v c q ≤ Polynomial.gaussNorm v c (p * q)
-- Mathlib.Combinatorics.Quiver.Push
Quiver.PushQuiver.arrow.sizeOf_spec : ∀ {V : Type u} [inst : Quiver V] {W : Type u₂} {σ : V → W} [inst_1 : SizeOf V] [inst_2 : SizeOf W] {X Y : V}
  (f : X ⟶ Y), sizeOf (Quiver.PushQuiver.arrow f) = 1 + sizeOf X + sizeOf Y + sizeOf f
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
borel_comap : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {t : TopologicalSpace β}, borel α = MeasurableSpace.comap f (borel β)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGet_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {hk : k ∈ t₁} (h : t₁.Equiv t₂), Std.DTreeMap.Const.get t₁ k hk = Std.DTreeMap.Const.get t₂ k ⋯
-- Mathlib.Order.Bounded
Set.bounded_ge_inter_not_ge : ∀ {α : Type u_1} {s : Set α} [inst : SemilatticeInf α] (a : α),
  Set.Bounded (fun x1 x2 => x1 ≥ x2) (s ∩ {b | ¬a ≤ b}) ↔ Set.Bounded (fun x1 x2 => x1 ≥ x2) s
-- Init.Data.UInt.Lemmas
USize.ofNatLT_bitVecToNat : ∀ (n : BitVec System.Platform.numBits), USize.ofNatLT n.toNat ⋯ = { toBitVec := n }
-- Mathlib.Order.Partition.Finpartition
Finpartition.card_mono : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} {P Q : Finpartition a},
  P ≤ Q → Q.parts.card ≤ P.parts.card
-- Mathlib.MeasureTheory.Integral.DivergenceTheorem
_private.Mathlib.MeasureTheory.Integral.DivergenceTheorem.0.MeasureTheory.«term__¹» : Lean.TrailingParserDescr
-- Std.Do.Triple.SpecLemmas
Std.Do.Iter.foldM_filterM : ∀ {ps : Std.Do.PostShape} {α β δ : Type w} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [LawfulMonad o] [inst_8 : Std.Do.WPMonad o ps] [inst_9 : Std.IteratorLoop α Id n]
  [inst_10 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id n] [Std.LawfulIteratorLoop α Id o]
  [inst_13 : MonadLiftT n o] [LawfulMonadLiftT n o] {f : β → n (ULift.{w, 0} Bool)} {g : δ → β → o δ} {init : δ}
  {it : Std.Iter β} {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond δ ps},
  ⦃P⦄
      Std.Iter.foldM
        (fun d b => do
          let __do_lift ← liftM (f b)
          if __do_lift.down = true then g d b else pure d)
        init it ⦃Q⦄ →
    ⦃P⦄ Std.IterM.foldM g init (Std.Iter.filterM f it) ⦃Q⦄
-- Mathlib.Order.Filter.Pointwise
Filter.map_div : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : DivisionMonoid β] [inst_2 : FunLike F α β]
  [MonoidHomClass F α β] (m : F) {f g : Filter α}, Filter.map (⇑m) (f / g) = Filter.map (⇑m) f / Filter.map (⇑m) g
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.subtypeVal_coe : ∀ {β : Type u_3} [inst : Lattice β] [inst_1 : BoundedOrder β] {P : β → Prop} (Pbot : P ⊥) (Ptop : P ⊤)
  (Psup : ∀ ⦃x y : β⦄, P x → P y → P (x ⊔ y)) (Pinf : ∀ ⦃x y : β⦄, P x → P y → P (x ⊓ y)),
  ⇑(BoundedLatticeHom.subtypeVal Pbot Ptop Psup Pinf) = Subtype.val
-- Init.Data.UInt.Basic
USize.size_le : USize.size ≤ 2 ^ 64
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- If two affine maps agree on a set that spans the entire space, then they are equal.  -/
AffineMap.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₁} {f g : P₁ →ᵃ[k] P₂}, affineSpan k s = ⊤ → Set.EqOn (⇑f) (⇑g) s → f = g
-- Mathlib.Data.Fin.Tuple.Basic
Fin.cons_inj : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u} {x₀ y₀ : α 0} {x y : (i : Fin n) → α i.succ},
  Fin.cons x₀ x = Fin.cons y₀ y ↔ x₀ = y₀ ∧ x = y
-- Mathlib.Data.Int.ModEq
Int.modEq_iff_eq_of_div_eq : ∀ {n a b : ℤ}, a / n = b / n → (a ≡ b [ZMOD n] ↔ a = b)
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_mono : Monotone ENat.ceil
-- Init.Data.UInt.Lemmas
UInt32.ofNatTruncate_uInt8ToNat : ∀ (n : UInt8), UInt32.ofNatClamp n.toNat = n.toUInt32
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The canonical isomorphism `K.X 0 ≅ K.opcycles 0` for a cochain complex `K`
indexed by `ℕ`.  -/
CochainComplex.opcycles₀Iso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (K : CochainComplex C ℕ) → [inst_2 : HomologicalComplex.HasHomology K 0] → K.X 0 ≅ HomologicalComplex.opcycles K 0
-- Mathlib.Analysis.Seminorm
Seminorm.ball_zero' : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : SMul 𝕜 E] {r : ℝ} (x : E),
  0 < r → Seminorm.ball 0 x r = Set.univ
-- Mathlib.CategoryTheory.Filtered.Basic
/-- The morphisms to `sup O H`.
 -/
CategoryTheory.IsFiltered.toSup : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsFiltered C] →
      (O : Finset C) →
        (H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))) →
          {X : C} → X ∈ O → (X ⟶ CategoryTheory.IsFiltered.sup O H)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ranAdjunction_unit_app : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] (G : CategoryTheory.Functor D H),
  (L.ranAdjunction H).unit.app G =
    (L.ran.obj (L.comp G)).liftOfIsRightKanExtension (L.ranCounit.app (L.comp G)) G
      (CategoryTheory.CategoryStruct.id (L.comp G))
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.dirac_ne_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] {a : α}, MeasureTheory.Measure.dirac a ≠ 0
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYonedaIsoYoneda_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.shrinkYonedaIsoYoneda.hom.app X =
    (CategoryTheory.NatIso.ofComponents (fun Y => CategoryTheory.shrinkYonedaObjObjEquiv.toIso) ⋯).hom
-- Mathlib.Order.Monotone.Defs
StrictMono.monotone : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {f : α → β}, StrictMono f → Monotone f
-- Mathlib.Topology.Algebra.Group.Basic
Continuous.zsmul : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G]
  [inst_3 : TopologicalSpace α] {f : α → G}, Continuous f → ∀ (z : ℤ), Continuous (z • f)
-- Lean.LocalContext
Lean.LocalDeclKind.noConfusionType : Sort v✝ → Lean.LocalDeclKind → Lean.LocalDeclKind → Sort v✝
-- Init.Data.UInt.Lemmas
UInt8.add_neg_eq_sub : ∀ {a b : UInt8}, a + -b = a - b
-- Mathlib.NumberTheory.LucasLehmer
/-- If `2 ^ p - 1` is prime, then `p` is prime.  -/
Nat.Prime.of_mersenne : ∀ {p : ℕ}, Nat.Prime (mersenne p) → Nat.Prime p
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- Eta-expanded form of `MeasureTheory.lintegral_indicator_one` -/
MeasureTheory.lintegral_indicator_fun_one : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → ∫⁻ (a : α), s.indicator (fun x => 1) a ∂μ = μ s
-- Mathlib.Topology.Order.OrderClosed
Icc_mem_nhdsLE : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b : α},
  a < b → Set.Icc a b ∈ nhdsWithin b (Set.Iic b)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_eq_default : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α}
  [inst_1 : Inhabited (β a)], a ∉ m → m.get! a = default
-- Lean.Data.Json.Basic
Lean.Json.getArr? : Lean.Json → Except String (Array Lean.Json)
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
CategoryTheory.Idempotents.whiskeringLeftObjToKaroubiFullyFaithful.eq_1 : ∀ {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],
  CategoryTheory.Idempotents.whiskeringLeftObjToKaroubiFullyFaithful =
    {
      preimage := fun {F G} τ =>
        {
          app := fun P =>
            CategoryTheory.CategoryStruct.comp (F.map P.decompId_i)
              (CategoryTheory.CategoryStruct.comp (τ.app P.X) (G.map P.decompId_p)),
          naturality := ⋯ },
      map_preimage := ⋯, preimage_map := ⋯ }
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.algHom_ext : ∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] {I : Ideal A}
  [inst_3 : I.IsTwoSided] {S : Type u_5} [inst_4 : Semiring S] [inst_5 : Algebra R₁ S] ⦃f g : A ⧸ I →ₐ[R₁] S⦄,
  f.comp (Ideal.Quotient.mkₐ R₁ I) = g.comp (Ideal.Quotient.mkₐ R₁ I) → f = g
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.Context.mk : Lean.PrettyPrinter.Delaborator.OptionsPerPos →
  Lean.Name → List Lean.OpenDecl → Bool → Lean.SubExpr → ℕ → ℕ → Lean.PrettyPrinter.Delaborator.Context
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoComp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) {D : Type u_4}
  [inst_4 : CategoryTheory.Category.{v_2, u_4} D] [inst_5 : CategoryTheory.HasShift D B]
  (F : CategoryTheory.Functor C D) [inst_6 : F.CommShift B] {E : Type u_5}
  [inst_7 : CategoryTheory.Category.{v_3, u_5} E] [inst_8 : CategoryTheory.HasShift E B]
  (G : CategoryTheory.Functor D E) [inst_9 : G.CommShift B],
  CategoryTheory.NatTrans.CommShift (CategoryTheory.NatTrans.PullbackShift.natIsoComp φ F G).hom A
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.mk.sizeOf_spec : ∀ {R : Type u} [inst : SizeOf R] (a₁ a₂ a₃ a₄ a₆ : R),
  sizeOf { a₁ := a₁, a₂ := a₂, a₃ := a₃, a₄ := a₄, a₆ := a₆ } =
    1 + sizeOf a₁ + sizeOf a₂ + sizeOf a₃ + sizeOf a₄ + sizeOf a₆
-- Mathlib.Analysis.LocallyConvex.Separation
/-- A version of the **Hahn-Banach theorem**: given disjoint convex sets `s`, `t` where `s` is
compact and `t` is closed, there is a continuous linear functional which strongly separates them.  -/
geometric_hahn_banach_compact_closed : ∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {s t : Set E}
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E],
  Convex ℝ s →
    IsCompact s → Convex ℝ t → IsClosed t → Disjoint s t → ∃ f u v, (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ b ∈ t, v < f b
-- Mathlib.CategoryTheory.Galois.Basic
/-- A mono between objects with equally sized fibers is an iso.  -/
CategoryTheory.PreGaloisCategory.isIso_of_mono_of_eq_card_fiber : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {X Y : C} (f : X ⟶ Y)
  [CategoryTheory.Mono f], Nat.card (F.obj X).obj = Nat.card (F.obj Y).obj → CategoryTheory.IsIso f
-- Init.Data.Array.Attach
Array.pmap_eq_map_attach : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {xs : Array α} (H : ∀ a ∈ xs, p a),
  Array.pmap f xs H = Array.map (fun x => f ↑x ⋯) xs.attach
-- Aesop.Stats.Basic
Aesop.ScriptGenerated.mk : Aesop.ScriptGenerated.Method → Bool → Bool → Aesop.ScriptGenerated
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomLeft_tensor_assoc : ∀ {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.MonoidalRightAction C D] {z z' : D} (f : z ⟶ z') (x y : C) {Z : D}
  (h :
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj z'
        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f
        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y))
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso z x y).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f x) y)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso z' x y).inv h))
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpolyAux.congr_simp : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [inst : CommRing R]
  [inst_1 : AddCommGroup L] [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  (φ φ_1 : L →ₗ[R] Module.End R M),
  φ = φ_1 →
    ∀ [inst_5 : Fintype ι] [inst_6 : Fintype ιM] [inst_7 : DecidableEq ι] {inst_8 : DecidableEq ιM}
      [inst_9 : DecidableEq ιM] (b b_1 : Module.Basis ι R L),
      b = b_1 → ∀ (bₘ bₘ_1 : Module.Basis ιM R M), bₘ = bₘ_1 → φ.polyCharpolyAux b bₘ = φ_1.polyCharpolyAux b_1 bₘ_1
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.term.parenthesizer : Lean.PrettyPrinter.CategoryParenthesizer
-- Mathlib.Order.NonemptyFiniteChains
PartialOrder.NonemptyFiniteChains.mem_map_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : PartialOrder X] [inst_1 : PartialOrder Y]
  (s : PartialOrder.NonemptyFiniteChains X) (f : X →o Y) (y : Y), y ∈ (s.map f).finset ↔ ∃ x ∈ s.finset, f x = y
-- Mathlib.AlgebraicGeometry.Scheme
/-- The type of open sets of a scheme.  -/
AlgebraicGeometry.Scheme.Opens : AlgebraicGeometry.Scheme → Type u_1
-- Lean.MetavarContext
Lean.instMonadMCtxOfMonadLift : (m n : Type → Type) → [MonadLift m n] → [Lean.MonadMCtx m] → Lean.MonadMCtx n
-- Mathlib.Data.Fintype.Basic
/-- A `Nonempty` `Fintype` constructively contains an element.
 -/
truncOfNonemptyFintype : (α : Type u_4) → [Nonempty α] → [Fintype α] → Trunc α
-- Mathlib.Order.BooleanAlgebra.Basic
compl_surjective : ∀ {α : Type u} [inst : BooleanAlgebra α], Function.Surjective compl
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
hasMFDerivWithinAt_snd : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] (s : Set (M × M')) (x : M × M'),
  HasMFDerivAt[s] Prod.snd x (ContinuousLinearMap.snd 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2))
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : MeasurableSpace β] {M : Type u_3}
  [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M] (v : MeasureTheory.VectorMeasure α M) (f : α → β),
  v.map f =
    if hf : Measurable f then
      { measureOf' := fun s => if MeasurableSet s then v (f ⁻¹' s) else 0, empty' := ⋯, not_measurable' := ⋯,
        m_iUnion' := ⋯ }
    else 0
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Bool.borelSpace : BorelSpace Bool
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_insertMany_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α} {k : α},
  k ∉ m → l.contains k = false → (m.insertMany l).get? k = none
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.map_addXYZ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S)
  (P Q : Fin 3 → R), (W'.map f).addXYZ (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ W'.addXYZ P Q
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.mk.injEq : ∀ {X : Type u_1} [inst : TopologicalSpace X] {k : WithTop ℕ∞} {E : Type u_2} {H : Type u_3}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} (M : Type u) [topSpaceM : TopologicalSpace M]
  [chartedSpace : ChartedSpace H M] [isManifold : IsManifold I k M] [compactSpace : CompactSpace M]
  [boundaryless : BoundarylessManifold I M] (f : M → X) (hf : Continuous f) (M_1 : Type u)
  (topSpaceM_1 : TopologicalSpace M_1) (chartedSpace_1 : ChartedSpace H M_1) (isManifold_1 : IsManifold I k M_1)
  (compactSpace_1 : CompactSpace M_1) (boundaryless_1 : BoundarylessManifold I M_1) (f_1 : M_1 → X)
  (hf_1 : Continuous f_1),
  ({ M := M, topSpaceM := topSpaceM, chartedSpace := chartedSpace, isManifold := isManifold,
        compactSpace := compactSpace, boundaryless := boundaryless, f := f, hf := hf } =
      { M := M_1, topSpaceM := topSpaceM_1, chartedSpace := chartedSpace_1, isManifold := isManifold_1,
        compactSpace := compactSpace_1, boundaryless := boundaryless_1, f := f_1, hf := hf_1 }) =
    (M = M_1 ∧ topSpaceM ≍ topSpaceM_1 ∧ chartedSpace ≍ chartedSpace_1 ∧ f ≍ f_1)
-- Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
CategoryTheory.Functor.IsLocallyFull.of_full : ∀ {C : Type uC} [inst : CategoryTheory.Category.{vC, uC} C] {D : Type uD} [inst_1 : CategoryTheory.Category.{vD, uD} D]
  {K : CategoryTheory.GrothendieckTopology D} (G : CategoryTheory.Functor C D) [G.Full], G.IsLocallyFull K
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_eq_size_eq_zero : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β}, m.isEmpty = (m.size == 0)
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.IsBasis.delete : ∀ {α : Type u_1} {M : Matroid α} {I D X : Set α}, M.IsBasis I X → Disjoint X D → (M.delete D).IsBasis I X
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.map.congr_simp : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f f_1 : F),
  f = f_1 →
    ∀ (s s_1 : NonUnitalSubsemiring R), s = s_1 → NonUnitalSubsemiring.map f s = NonUnitalSubsemiring.map f_1 s_1
-- Init.Data.Fin.Lemmas
Fin.ofNat.congr_simp : ∀ (n : ℕ) [inst : NeZero n] (a a_1 : ℕ), a = a_1 → Fin.ofNat n a = Fin.ofNat n a_1
-- Mathlib.Topology.Algebra.Algebra
/-- Continuous algebra homomorphisms between algebras. We only put the type classes that are
necessary for the definition, although in applications `M` and `B` will be topological algebras
over the topological ring `R`.  -/
«term_→A[_]_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_equiv_top : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {F : Type u_7} [inst_2 : EquivLike F G N]
  [inst_3 : MulEquivClass F G N] (f : F), Subgroup.map ↑f ⊤ = ⊤
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- If `f : X → R → R` is continuous in the topology on `X → R →ᵤ[{spectrum R a}] → R`,
and each `f` is continuous on the spectrum and maps zero to itself, then
`x ↦ cfcₙ (f x) a` is continuous.  -/
Continuous.cfcₙ_fun : ∀ {X : Type u_1} {R : Type u_2} {A : Type u_3} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : MetricSpace R] [inst_3 : Nontrivial R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R]
  [inst_6 : NonUnitalRing A] [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A]
  [inst_10 : SMulCommClass R A A] [inst_11 : IsScalarTower R A A]
  [inst_12 : NonUnitalContinuousFunctionalCalculus R A p] [inst_13 : TopologicalSpace X] (f : X → R → R) (a : A),
  (Continuous fun x => (UniformOnFun.ofFun {quasispectrum R a}) (f x)) →
    autoParam (∀ (x : X), ContinuousOn (f x) (quasispectrum R a)) Continuous.cfcₙ_fun._auto_1 →
      autoParam (∀ (x : X), f x 0 = 0) Continuous.cfcₙ_fun._auto_3 → Continuous fun x => cfcₙ (f x) a
-- Mathlib.Algebra.BigOperators.Finprod
AddEquivClass.map_finsum : ∀ {M : Type u_2} {N : Type u_3} {α : Sort u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {F : Type u_7}
  [inst_2 : EquivLike F M N] [AddEquivClass F M N] (g : F) (f : α → M), g (∑ᶠ (i : α), f i) = ∑ᶠ (i : α), g (f i)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instStarOrderedRing : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A] {n : Type u_3}
  [inst_3 : Fintype n], StarOrderedRing (CStarMatrix n n A)
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsMulIndecomposable.apply_ne_one_iff_mem_closure : ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S] [Finite ι]
  [inst_3 : InvolutiveInv ι] [inst_4 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (i : ι),
  v i ≠ 1 →
    v i⁻¹ = (v i)⁻¹ →
      (f (v i) ≠ 1 ↔
        v i ∈ Submonoid.closure (v '' IsMulIndecomposable.baseOf v f) ∨
          (v i)⁻¹ ∈ Submonoid.closure (v '' IsMulIndecomposable.baseOf v f))