mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.getElem_leftInvSeq_alternatingWord : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i j : B) (p k : ℕ)
  (h : k < 2 * p),
  (cs.leftInvSeq (CoxeterSystem.alternatingWord i j (2 * p)))[k] =
    cs.wordProd (CoxeterSystem.alternatingWord j i (2 * k + 1))
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sin_sub_sin : ∀ (x y : ℂ), Complex.sin x - Complex.sin y = 2 * Complex.sin ((x - y) / 2) * Complex.cos ((x + y) / 2)
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.associatorImpl_inv_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y Z : CategoryTheory.Dial C),
  (X.associatorImpl Y Z).inv.f =
    CategoryTheory.Limits.prod.lift
      (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
-- Mathlib.Data.DFinsupp.Defs
/-- **Alias** of `DFinsupp.support_single`. -/
DFinsupp.support_single_ne_zero : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {i : ι} {b : β i}, b ≠ 0 → (fun₀ | i => b).support = {i}
-- Mathlib.MeasureTheory.Constructions.ClosedCompactCylinders
MeasureTheory.closedCompactCylinders.isCompact : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {t : Set ((i : ι) → X i)}
  (ht : t ∈ MeasureTheory.closedCompactCylinders X), IsCompact (MeasureTheory.closedCompactCylinders.set ht)
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.modify_id : ∀ {σ : Type u_2} {m : Type u_2 → Type u_1} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m],
  modify id = pure PUnit.unit
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- **Alias** of `MeasureTheory.integral_deriv_smul_comp_Ioi`.

---

Change-of-variables formula for `Ioi` integrals of vector-valued functions, proved by taking
limits from the result for finite intervals.  -/
MeasureTheory.integral_comp_smul_deriv_Ioi : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E} {a : ℝ},
  ContinuousOn f (Set.Ici a) →
    Filter.Tendsto f Filter.atTop Filter.atTop →
      (∀ x ∈ Set.Ioi a, HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
        ContinuousOn g (f '' Set.Ioi a) →
          MeasureTheory.IntegrableOn g (f '' Set.Ici a) MeasureTheory.volume →
            MeasureTheory.IntegrableOn (fun x => f' x • (g ∘ f) x) (Set.Ici a) MeasureTheory.volume →
              ∫ (x : ℝ) in Set.Ioi a, f' x • (g ∘ f) x = ∫ (u : ℝ) in Set.Ioi (f a), g u
-- Mathlib.Data.DFinsupp.Submonoid
/-- A variant of `AddSubmonoid.mem_iSup_iff_exists_dfinsupp` with the RHS fully unfolded.  -/
AddSubmonoid.mem_iSup_iff_exists_dfinsupp' : ∀ {ι : Type u} {γ : Type w} [inst : DecidableEq ι] [inst_1 : AddCommMonoid γ] (S : ι → AddSubmonoid γ)
  [inst_2 : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)] (x : γ), x ∈ iSup S ↔ ∃ f, (f.sum fun x xi => ↑xi) = x
-- Init.Core
DoResultBC.continue.inj : ∀ {σ : Type u} {a a_1 : σ}, DoResultBC.continue a = DoResultBC.continue a_1 → a = a_1
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.mem_nhdsWithin_iff : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s t : Set α},
  s ∈ nhdsWithin x t ↔ ∃ ε > 0, Metric.eball x ε ∩ t ⊆ s
-- Mathlib.NumberTheory.Wilson
ZMod.prod_Ico_one_prime : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)], ∏ x ∈ Finset.Ico 1 p, ↑x = -1
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RooSlice.instToIterator : {α : Type u_1} →
  {β : Type v} →
    [inst : Ord α] →
      Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.Const.RooSliceData α β)) Id
        (Std.Iterators.Types.Map (Std.DTreeMap.Internal.RxoIterator α fun x => β) Id Id (fun ⦃x⦄ => monadLift) fun b =>
          pure (b.fst, b.snd))
        (α × β)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.leftUnitor_monoidal_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X₁ X₂ : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₁).hom
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₂).hom)
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X₁
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X₂)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)).hom
          h))
-- Lean.Parser.Term
Lean.Parser.Term.letMVar : Lean.Parser.Parser
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α} {v : β k},
  t.isEmpty = true → (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.minKey! = k
-- Mathlib.Data.List.GetD
List.getD_map : ∀ {α : Type u} {β : Type v} (l : List α) (d : α) {n : ℕ} (f : α → β), (List.map f l).getD n (f d) = f (l.getD n d)
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- By `Quotient.lift_unique'` (not `Quotient.lift`) we have that `quotientFunctor V` is an
epimorphism.  -/
SSet.Truncated.HomotopyCategory.lift_unique' : ∀ (V : SSet.Truncated 2) {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D]
  (F₁ F₂ : CategoryTheory.Functor V.HomotopyCategory D),
  (SSet.Truncated.HomotopyCategory.quotientFunctor V).comp F₁ =
      (SSet.Truncated.HomotopyCategory.quotientFunctor V).comp F₂ →
    F₁ = F₂
-- Lean.Server.References
/-- All declarations of this module.  -/
Lean.Server.Ilean.decls : Lean.Server.Ilean → Lean.Lsp.Decls
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor_obj_inr : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (b : CategoryTheory.Limits.Bicone (CategoryTheory.Limits.pairFunction X Y)),
  (CategoryTheory.Limits.Bicone.toBinaryBiconeFunctor.obj b).inr = b.ι CategoryTheory.Limits.WalkingPair.right
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.dual_singleton_zero : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R}, PointedCone.dual p {0} = ⊤
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.pointwiseLeftKanExtensionUnit_app : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [inst_3 : L.HasPointwiseLeftKanExtension F] (X : C),
  (L.pointwiseLeftKanExtensionUnit F).app X =
    CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L (L.obj X)).comp F)
      (CategoryTheory.CostructuredArrow.mk (CategoryTheory.CategoryStruct.id (L.obj X)))
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.instSemiring : {𝕜 : Type u_2} →
  {α : Type u_5} →
    [inst : Preorder α] →
      [LocallyFiniteOrder α] → [DecidableEq α] → [inst_3 : Semiring 𝕜] → Semiring (IncidenceAlgebra 𝕜 α)
-- Mathlib.Order.RelIso.Basic
RelEmbedding.toEmbedding : {α : Type u_5} → {β : Type u_6} → {r : α → α → Prop} → {s : β → β → Prop} → r ↪r s → α ↪ β
-- Std.Async.UDP
Std.Async.UDP.Socket.native : Std.Async.UDP.Socket → Std.Internal.UV.UDP.Socket
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.addLeftCosetsCompSubtypeVal : {G : Type u} → [inst : AddGroup G] → (H I : AddSubgroup G) → AddAction (↥I) (G ⧸ H)
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.append.induct_unfolding : ∀ (p₂ : Lean.Grind.Linarith.Poly) (motive : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Prop),
  motive Lean.Grind.Linarith.Poly.nil p₂ →
    (∀ (k : ℤ) (v : Lean.Grind.Linarith.Var) (p : Lean.Grind.Linarith.Poly),
        motive p (p.append p₂) →
          motive (Lean.Grind.Linarith.Poly.add k v p) (Lean.Grind.Linarith.Poly.add k v (p.append p₂))) →
      ∀ (p₁ : Lean.Grind.Linarith.Poly), motive p₁ (p₁.append p₂)
-- Mathlib.Algebra.Module.ULift
ULift.vaddLeft.eq_1 : ∀ {R : Type u} {M : Type v} [inst : VAdd R M], ULift.vaddLeft = { vadd := fun s x => s.down +ᵥ x }
-- Mathlib.LinearAlgebra.Determinant
LinearEquiv.coe_ofIsUnitDet : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {M' : Type u_3}
  [inst_3 : AddCommGroup M'] [inst_4 : Module R M'] {ι : Type u_4} [inst_5 : DecidableEq ι] [inst_6 : Fintype ι]
  {f : M →ₗ[R] M'} {v : Module.Basis ι R M} {v' : Module.Basis ι R M'} (h : IsUnit ((LinearMap.toMatrix v v') f).det),
  ↑(LinearEquiv.ofIsUnitDet h) = f
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Raw.WF.constGetThenInsertIfNew?₀ : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α fun x => β}
  {h : 0 < m.buckets.size} {a : α} {b : β},
  m.WF → (↑(Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? ⟨m, h⟩ a b).2).WF
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- The mates equivalence commutes with horizontal composition of squares.  -/
CategoryTheory.Bicategory.mateEquiv_hcomp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e f : B} {g : a ⟶ d} {h : b ⟶ e} {k : c ⟶ f} {l₁ : a ⟶ b}
  {r₁ : b ⟶ a} {l₂ : d ⟶ e} {r₂ : e ⟶ d} {l₃ : b ⟶ c} {r₃ : c ⟶ b} {l₄ : e ⟶ f} {r₄ : f ⟶ e}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂)
  (adj₃ : CategoryTheory.Bicategory.Adjunction l₃ r₃) (adj₄ : CategoryTheory.Bicategory.Adjunction l₄ r₄)
  (α : CategoryTheory.CategoryStruct.comp g l₂ ⟶ CategoryTheory.CategoryStruct.comp l₁ h)
  (β : CategoryTheory.CategoryStruct.comp h l₄ ⟶ CategoryTheory.CategoryStruct.comp l₃ k),
  (CategoryTheory.Bicategory.mateEquiv (adj₁.comp adj₃) (adj₂.comp adj₄))
      (CategoryTheory.Bicategory.leftAdjointSquare.hcomp α β) =
    CategoryTheory.Bicategory.rightAdjointSquare.hcomp ((CategoryTheory.Bicategory.mateEquiv adj₁ adj₂) α)
      ((CategoryTheory.Bicategory.mateEquiv adj₃ adj₄) β)
-- Init.Data.Vector.Lemmas
Vector.getElem_toArray : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (h : i < xs.toArray.size), xs.toArray[i] = xs[i]
-- Mathlib.Algebra.Algebra.Spectrum.Pi
quasispectrum.mem_iff_of_isUnit : ∀ {A : Type u_2} {R : Type u_4} [inst : CommSemiring R] [inst_1 : NonUnitalRing A] [inst_2 : Module R A] {a : A} {r : R}
  (hr : IsUnit r), r ∈ quasispectrum R a ↔ ¬IsQuasiregular (-(hr.unit⁻¹ • a))
-- Mathlib.NumberTheory.LSeries.PrimesInAP
/-- **Alias** of `Nat.infinite_setOfPred_prime_and_eq_mod`.

---

**Dirichlet's Theorem** on primes in arithmetic progression: if `q` is a positive
integer and `a : ZMod q` is a unit, then there are infinitely many prime numbers `p`
such that `(p : ZMod q) = a`.  -/
Nat.infinite_setOf_prime_and_eq_mod : ∀ {q : ℕ} [NeZero q] {a : ZMod q}, IsUnit a → {p | Nat.Prime p ∧ ↑p = a}.Infinite
-- Init.Data.List.Attach
List.pmap_eq_map : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : α → β} {l : List α} (H : ∀ a ∈ l, p a),
  List.pmap (fun a x => f a) l H = List.map f l
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Multiset.disjoint_list_sum_right : ∀ {α : Type u_6} {a : Multiset α} {l : List (Multiset α)}, Disjoint a l.sum ↔ ∀ b ∈ l, Disjoint a b
-- Mathlib.Topology.Separation.Basic
continuousAt_update_of_ne : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [T1Space X] [inst_2 : DecidableEq X]
  [inst_3 : TopologicalSpace Y] {f : X → Y} {x x' : X} {y : Y},
  x' ≠ x → (ContinuousAt (Function.update f x y) x' ↔ ContinuousAt f x')
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.grind.warning : Lean.Option Bool
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
_private.Mathlib.Combinatorics.SimpleGraph.Finsubgraph.0.SimpleGraph.«term_→fg_» : Lean.TrailingParserDescr
-- Mathlib.Order.WithBot
WithTop.map_toDual : ∀ {α : Type u_1} {β : Type u_2} (f : αᵒᵈ → βᵒᵈ) (a : WithTop α),
  WithTop.map f (WithTop.toDual a) = WithTop.map (⇑OrderDual.toDual ∘ f) a
-- Init.Grind.Attr
/-- The `=_` modifier instructs `grind` to check that the conclusion of the theorem is an equality,
and then uses the right-hand side of the equality as a pattern. This may fail if not all of the arguments appear
in the right-hand side.
 -/
Lean.Parser.Attr.grindEqRhs : Lean.ParserDescr
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.single_mul_single : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : MulSemiringAction G k] {a₁ a₂ : G}
  {b₁ b₂ : k},
  SkewMonoidAlgebra.single a₁ b₁ * SkewMonoidAlgebra.single a₂ b₂ = SkewMonoidAlgebra.single (a₁ * a₂) (b₁ * a₁ • b₂)
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- Arithmetic progressions of length three are reflected under `2`-Freiman homomorphisms.  -/
ThreeAPFree.of_image : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {s A : Set α} {t : Set β}
  {f : α → β}, IsAddFreimanHom 2 s t f → Set.InjOn f s → A ⊆ s → ThreeAPFree (f '' A) → ThreeAPFree A
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.tensorHom.eq_1 : ∀ {R : Type u} [inst : CommSemiring R] {M N : SemimoduleCat R} {M' N' : SemimoduleCat R} (f : M ⟶ N) (g : M' ⟶ N'),
  SemimoduleCat.MonoidalCategory.tensorHom f g =
    SemimoduleCat.ofHom (TensorProduct.map (SemimoduleCat.Hom.hom f) (SemimoduleCat.Hom.hom g))
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.aestronglyMeasurable : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι} {β : Type u_3}
  [inst_1 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [l.IsCountablyGenerated] [l.NeBot]
  {f : α → β} {φ : ι → Set α},
  MeasureTheory.AECover μ l φ →
    (∀ (i : ι), MeasureTheory.AEStronglyMeasurable f (μ.restrict (φ i))) → MeasureTheory.AEStronglyMeasurable f μ
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- Given an `R`-submodule `p` of `M`, and `R`-algebra `A`, we obtain an `A`-submodule of
`A ⊗[R] M` by `p.baseChange A`. This is then the surjective `A`-linear map
`A ⊗[R] M → p.baseChange A`.  -/
Submodule.toBaseChange : {R : Type u_1} →
  {M : Type u_2} →
    (A : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] → (p : Submodule R M) → TensorProduct R A ↥p →ₗ[A] ↥(Submodule.baseChange A p)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.instInhabitedTacticFinishedSnapshot : Inhabited Lean.Elab.Tactic.TacticFinishedSnapshot
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.liesOver_iff : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {φ : L →+* ℂ} {ψ : K →+* ℂ},
  NumberField.ComplexEmbedding.LiesOver φ ψ ↔ φ.comp (algebraMap K L) = ψ
-- Mathlib.CategoryTheory.Limits.Types.Yoneda
CategoryTheory.Limits.whiskeringLimYonedaIsoCones_hom_app_app_hom_apply_app : ∀ (J : Type v) [inst : CategoryTheory.SmallCategory J] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C]
  (X : CategoryTheory.Functor J C) (X_1 : Cᵒᵖ)
  (a : CategoryTheory.Limits.limit (X.comp (CategoryTheory.coyoneda.obj (Opposite.op (Opposite.unop X_1))))) (j : J),
  ((CategoryTheory.ConcreteCategory.hom (((CategoryTheory.Limits.whiskeringLimYonedaIsoCones J C).hom.app X).app X_1))
          a).app
      j =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π (X.comp (CategoryTheory.coyoneda.obj X_1)) j)) a
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_eq_isSome_getKey? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α}, m.contains a = (m.getKey? a).isSome
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.codisjoint_map : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N},
  Function.Surjective ⇑f →
    ∀ {H K : AddSubgroup G}, Codisjoint H K → Codisjoint (AddSubgroup.map f H) (AddSubgroup.map f K)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {fallback : β}, (m₁ ∩ m₂).getD k fallback = if k ∈ m₂ then m₁.getD k fallback else fallback
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getEntry!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α) [inst_1 : Inhabited ((a : α) × β a)],
  Std.Internal.List.getEntry! a [] =
    panicWithPosWithDecl "Std.Data.Internal.List.Associative" "Std.Internal.List.getEntry!" 67 10
      "key is not present in associative list"
-- Mathlib.LinearAlgebra.Eigenspace.Triangularizable
/-- In finite dimensions, if the generalized eigenspaces of a linear endomorphism span the whole
space then the same is true of its restriction to any invariant submodule.  -/
Module.End.genEigenspace_restrict_eq_top : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {p : Submodule K V}
  {f : Module.End K V} [FiniteDimensional K V] {k : ℕ∞} (h : ∀ x ∈ p, f x ∈ p),
  ⨆ μ, (f.genEigenspace μ) k = ⊤ → ⨆ μ, (Module.End.genEigenspace (LinearMap.restrict f h) μ) k = ⊤
-- Mathlib.CategoryTheory.ComposableArrows.Two
CategoryTheory.ComposableArrows.instIsIsoOfNatNatTwoδ₂Toδ₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) [CategoryTheory.IsIso g],
  CategoryTheory.IsIso (CategoryTheory.ComposableArrows.twoδ₂Toδ₁ f g fg h)
-- Init.Data.Bool
/-- These two rules follow trivially by simp, but are needed to avoid non-termination
in false_eq and true_eq.
 -/
Bool.false_eq_true : (false = true) = False
-- Mathlib.CategoryTheory.Presentable.SharplyLT.Basic
_private.Mathlib.CategoryTheory.Presentable.SharplyLT.Basic.0.Cardinal.SharplyLT.existsIsCardinalFilteredSetOfExistsCofinal.hφ₀ : ∀ {κ₁ κ₂ : Cardinal.{w}} {X : Type w} [inst : PartialOrder X]
  (Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B)),
  (∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂), IsCofinal (Y B hB)) →
    ∀
      (m :
        (B : Set X) →
          (hB : HasCardinalLT (↑B) κ₂) →
            (C : CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X),
      (∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂) (C : CategoryTheory.CardinalDirectedPoset.SetCardinalLT κ₁ ↑B)
          (hC : C ∈ Y B hB), ∀ b ∈ ↑C, ↑b ≤ m B hB C hC) →
        ∀ (B : Set X) (hB : HasCardinalLT (↑B) κ₂) {T : Type w} (f : T → ↑B),
          HasCardinalLT T κ₁ → ∃ a, ∀ (t : T), ↑(f t) ≤ ↑a
-- Init.Data.List.Attach
List.attachWith.eq_1 : ∀ {α : Type u_1} (l : List α) (P : α → Prop) (H : ∀ x ∈ l, P x), l.attachWith P H = List.pmap Subtype.mk l H
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.comapQuotientEquivOfSurj_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (c : AddCon M) {f : N →+ M}
  (hf : Function.Surjective ⇑f) (x : N), (c.comapQuotientEquivOfSurj f hf) ↑x = ↑(f x)
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_hom_comp_mapComp'_hom_whiskerRight_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f)
  (X : ↑(F.obj b₀)),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).hom.toNatTrans.app X)
      ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X)) =
    CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X)
      ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).hom.toNatTrans.app ((F.map f₀₁).toFunctor.obj X))
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.changeLevel.eq_1 : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n m : ℕ} (hm : n ∣ m),
  DirichletCharacter.changeLevel hm =
    { toFun := fun ψ => MulChar.ofUnitHom ((MulChar.toUnitHom ψ).comp (ZMod.unitsMap hm)), map_one' := ⋯,
      map_mul' := ⋯ }
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.fold_push_key : ∀ {α : Type u} {β : α → Type v} {l : Std.DHashMap.Raw α β} {acc : Array α},
  Std.DHashMap.Raw.fold (fun acc k x => acc.push k) acc l =
    acc ++ (Std.Internal.List.keys (Std.DHashMap.Internal.toListModel l.buckets)).toArray
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKeyD_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {k fallback : α}, (cmp (t.maxKeyD fallback) k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateEquiv_symm_comp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ l₂ l₃ : c ⟶ d} {r₁ r₂ r₃ : d ⟶ c}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂)
  (adj₃ : CategoryTheory.Bicategory.Adjunction l₃ r₃) (α : r₁ ⟶ r₂) (β : r₂ ⟶ r₃),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.conjugateEquiv adj₂ adj₃).symm β)
      ((CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₂).symm α) =
    (CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₃).symm (CategoryTheory.CategoryStruct.comp α β)
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.IsPushout.IsVanKampen.mono_of_mono_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  [CategoryTheory.Mono f] {H : CategoryTheory.IsPushout f g h i}, H.IsVanKampen → CategoryTheory.Mono i
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.integralNormalization_C : ∀ {R : Type u} [inst : Semiring R] {x : R}, x ≠ 0 → (Polynomial.C x).integralNormalization = 1
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Linear constraints that are not supported.
We use this information for diagnostics.
TODO: store constraints instead.
 -/
Lean.Meta.Grind.Arith.Linear.Struct.ignored : Lean.Meta.Grind.Arith.Linear.Struct → Lean.PArray Lean.Expr
-- Lean.Data.Options
_private.Lean.Data.Options.0.Lean.Options.getEmpty : Unit → Lean.Options
-- Lean.Message
/-- The list of messages already reported (i.e. saved in a `Snapshot`), in insertion order.  -/
Lean.MessageLog.reported : Lean.MessageLog → Lean.PersistentArray Lean.Message