mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_filter : ∀ {α : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {β : Type w} [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {f : β → Bool} {it : Std.IterM m β},
  (Std.IterM.filter f it).toList = List.filter f <$> it.toList
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.mapAddMonoidHom.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {Z : Type u_6} [inst_1 : AddZeroClass Y]
  [inst_2 : AddZeroClass Z] (f : Y →+ Z),
  LocallyConstant.mapAddMonoidHom f = { toFun := LocallyConstant.map ⇑f, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Order.Filter.Map
Filter.comap_sup : ∀ {α : Type u_1} {β : Type u_2} {g₁ g₂ : Filter β} {m : α → β},
  Filter.comap m (g₁ ⊔ g₂) = Filter.comap m g₁ ⊔ Filter.comap m g₂
-- Mathlib.Order.UpperLower.Relative
IsRelUpperSet.mem_of_le : ∀ {α : Type u_1} {s : Set α} {a b : α} {P : α → Prop} [inst : LE α], IsRelUpperSet s P → a ∈ s → a ≤ b → P b → b ∈ s
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.yn_modEq_a_sub_one : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.yn a1 n ≡ n [MOD a - 1]
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.basisFun.eq_1 : ∀ (p : ENNReal) (𝕜 : Type u_1) (ι : Type u_2) [inst : Finite ι] [inst_1 : Ring 𝕜],
  PiLp.basisFun p 𝕜 ι = Module.Basis.ofEquivFun (WithLp.linearEquiv p 𝕜 (ι → 𝕜))
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.succ_iSup_eq_lsub_iff : ∀ {ι : Type u_3} (f : ι → Ordinal.{max u_4 u_3}), Order.succ (iSup f) = Ordinal.lsub f ↔ ∃ i, f i = iSup f
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.blsub_lt_ord_of_isRegular : ∀ {o : Ordinal.{max u_1 u_2}} {f : (a : Ordinal.{max u_1 u_2}) → a < o → Ordinal.{max u_1 u_2}}
  {c : Cardinal.{max u_1 u_2}},
  c.IsRegular → o.card < c → (∀ (i : Ordinal.{max u_1 u_2}) (hi : i < o), f i hi < c.ord) → o.blsub f < c.ord
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_eq_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : LawfulBEq α]
  [inst_1 : Inhabited α] {k : α}, k ∈ m → m.getKey! k = k
-- Mathlib.NumberTheory.Bernoulli
bernoulli'_zero : bernoulli' 0 = 1
-- Mathlib.LinearAlgebra.FreeProduct.Basic
LinearAlgebra.FreeProduct.ringCon'.eq_1 : ∀ {I : Type u} [inst : DecidableEq I] (R : Type v) [inst_1 : CommSemiring R] (A : I → Type w)
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)],
  LinearAlgebra.FreeProduct.ringCon' R A = ringConGen (LinearAlgebra.FreeProduct.rel' R A)
-- Mathlib.Algebra.Algebra.RestrictScalars
/-- `Module.restrictScalars` forms a scalar tower.  -/
IsScalarTower.restrictScalars : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) [inst : Semiring S] [inst_1 : AddCommMonoid M] [inst_2 : CommSemiring R]
  [inst_3 : Algebra R S] [inst_4 : Module S M], IsScalarTower R S M
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesMapIso_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology],
  (CategoryTheory.ShortComplex.cyclesMapIso e).inv = CategoryTheory.ShortComplex.cyclesMap e.inv
-- Mathlib.Algebra.GCDMonoid.FinsetLemmas
/-- An analogue of `Nat.factorization_lcm` for `Finset.lcm`.  -/
Finset.factorization_lcm : ∀ {ι : Type u_1} {f : ι → ℕ} {s : Finset ι},
  (∀ k ∈ s, f k ≠ 0) → ∀ (p : ℕ), (s.lcm f).factorization p = s.sup fun a => (f a).factorization p
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.trinomial_leading_coeff' : ∀ {R : Type u_1} [inst : Semiring R] {k m n : ℕ} {u v w : R},
  k < m → m < n → (Polynomial.trinomial k m n u v w).coeff n = w
-- Mathlib.Order.Category.Semilat
SemilatSupCat.of.sizeOf_spec : ∀ (X : Type u) [isSemilatticeSup : SemilatticeSup X] [isOrderBot : OrderBot X],
  sizeOf { X := X, isSemilatticeSup := isSemilatticeSup, isOrderBot := isOrderBot } =
    1 + sizeOf X + sizeOf isSemilatticeSup + sizeOf isOrderBot
-- Mathlib.CategoryTheory.Sites.LocalProperties
/-- A sheaf morphism is an isomorphism if it becomes one after pulling back along each
element of a covering family.  -/
CategoryTheory.Sheaf.isIso_of_coversTop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {K : CategoryTheory.GrothendieckTopology C}
  {A : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} A] {ι : Type u_3} {X : ι → C},
  K.CoversTop X →
    ∀ {F G : CategoryTheory.Sheaf K A} {f : F ⟶ G},
      (∀ (i : ι), CategoryTheory.IsIso ((K.overPullback A (X i)).map f)) → CategoryTheory.IsIso f
-- Mathlib.Logic.Equiv.Bool
Bool.not_rightInverse : Function.RightInverse not not
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
/-- The commutation natural isomorphism
`t.eTruncGE.obj a ⋙ t.eTruncLT.obj b ≅ t.eTruncLT.obj b ⋙ t.eTruncGE.obj a`
for all `a` and `b` in `EInt`.  -/
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                [CategoryTheory.IsTriangulated C] →
                  (a b : EInt) → (t.eTruncGE.obj a).comp (t.eTruncLT.obj b) ≅ (t.eTruncLT.obj b).comp (t.eTruncGE.obj a)
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `alter` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.Const.alterₘ : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      [Std.OrientedOrd α] →
        α →
          (Option β → Option β) →
            (t : Std.DTreeMap.Internal.Impl α fun x => β) → t.Balanced → Std.DTreeMap.Internal.Impl α fun x => β
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
/-- This is the map from `i`-chains to `j`-cycles induced by the differential in the complex of
inhomogeneous chains.  -/
groupHomology.toCycles : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → (i j : ℕ) → (groupHomology.inhomogeneousChains A).X i ⟶ groupHomology.cycles A j
-- Mathlib.NumberTheory.LSeries.Injectivity
/-- If the `LSeries` of `f` and of `g` converge somewhere and agree on large real arguments,
then `f n = g n` whenever `n ≠ 0`.  -/
LSeries.eq_of_LSeries_eventually_eq : ∀ {f g : ℕ → ℂ},
  LSeries.abscissaOfAbsConv f < ⊤ →
    LSeries.abscissaOfAbsConv g < ⊤ →
      ((fun x => LSeries f ↑x) =ᶠ[Filter.atTop] fun x => LSeries g ↑x) → ∀ {n : ℕ}, n ≠ 0 → f n = g n
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_ofNat_mul : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {a k : ℕ} [inst_1 : a.AtLeastTwo],
  (OfNat.ofNat a * p).coeff k = OfNat.ofNat a * p.coeff k
-- Mathlib.Algebra.Group.Prod
AddMonoidHom.fst.eq_1 : ∀ (M : Type u_3) (N : Type u_4) [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.fst M N = { toFun := Prod.fst, map_zero' := ⋯, map_add' := ⋯ }
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {l : List ((a : α) × β a)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → ∀ {h' : k' ∈ t.insertMany l}, (t.insertMany l).getKey k' h' = k
-- Lean.EnvExtension
Lean.SimplePersistentEnvExtensionDescr.addImportedFn : {α σ : Type} → Lean.SimplePersistentEnvExtensionDescr α σ → Array (Array α) → σ
-- Std.Data.DHashMap.RawDef
/-- Checks if all elements satisfy the predicate, short-circuiting if a predicate fails.  -/
Std.DHashMap.Raw.all : {α : Type u} → {β : α → Type v} → Std.DHashMap.Raw α β → ((a : α) → β a → Bool) → Bool
-- Mathlib.Order.Fin.Tuple
Fin.insertNthOrderIso_zero : ∀ {n : ℕ} (α : Fin (n + 1) → Type u_2) [inst : (i : Fin (n + 1)) → LE (α i)],
  Fin.insertNthOrderIso α 0 = Fin.consOrderIso α
-- Mathlib.Data.Fin.SuccPred
/-- A version of the right-to-left implication of `castPred_lt_castPred_iff`
that deduces `i ≠ last n` from `i < j`.  -/
Fin.castPred_lt_castPred : ∀ {n : ℕ} {i j : Fin (n + 1)} (h : i < j) (hj : j ≠ Fin.last n), i.castPred ⋯ < j.castPred hj
-- Mathlib.CategoryTheory.Action.Basic
CategoryTheory.Functor.mapAction_map_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {W : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} W] (F : CategoryTheory.Functor V W) (G : Type u_3) [inst_2 : Monoid G]
  {X Y : Action V G} (f : X ⟶ Y), ((F.mapAction G).map f).hom = F.map f.hom
-- Mathlib.Algebra.Group.Defs
add_comm : ∀ {G : Type u_1} [inst : AddCommMagma G] (a b : G), a + b = b + a
-- Mathlib.Combinatorics.Quiver.Symmetric
/-- A prefunctor canonically defines a prefunctor of the symmetrifications.  -/
Prefunctor.symmetrify : {U : Type u_1} →
  {V : Type u_2} → [inst : Quiver U] → [inst_1 : Quiver V] → U ⥤q V → Quiver.Symmetrify U ⥤q Quiver.Symmetrify V
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.le_prod_iff : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {H : AddSubgroup G} {K : AddSubgroup N}
  {J : AddSubgroup (G × N)},
  J ≤ H.prod K ↔ AddSubgroup.map (AddMonoidHom.fst G N) J ≤ H ∧ AddSubgroup.map (AddMonoidHom.snd G N) J ≤ K
-- Init.Data.SInt.Bitwise
Int8.toInt64_xor : ∀ (a b : Int8), (a ^^^ b).toInt64 = a.toInt64 ^^^ b.toInt64
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge' : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (c₀ : OmegaCompletePartialOrder.Chain (α →𝒄 β)) (c₁ : OmegaCompletePartialOrder.Chain α) (z : β),
  (∀ (j i : ℕ), (c₀ i) (c₁ j) ≤ z) ↔ ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubgroup.ofAddUnitsEquivType.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubgroup (AddUnits M)),
  S.ofAddUnitsEquivType =
    { toFun := fun x => ⟨S.addUnit_of_mem_ofAddUnits ⋯, ⋯⟩, invFun := fun x => ⟨↑↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
      map_add' := ⋯ }
-- Mathlib.Order.SuccPred.Basic
/-- **Alias** of the forward direction of `Order.succ_le_iff_isMax`. -/
IsMax.of_succ_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a : α}, Order.succ a ≤ a → IsMax a
-- Mathlib.Algebra.BigOperators.Group.Finset.Interval
Finset.sum_Icc_of_even_eq_range : ∀ {α : Type u_1} [inst : AddCommGroup α] {f : ℤ → α},
  Function.Even f → ∀ (N : ℕ), ∑ m ∈ Finset.Icc (-↑N) ↑N, f m = 2 • ∑ m ∈ Finset.range (N + 1), f ↑m - f 0
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- For any valuation `v` compatible with the valuative relation on `R`, the closed `r`-ball
around zero `{x | v.restrict x ≤ r}` is open in the valuative topology.  -/
Valuation.isOpen_closedBall : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible]
  {r : (MonoidWithZeroHom.ofClass v).ValueGroup₀}, r ≠ 0 → IsOpen {x | v.restrict x ≤ r}
-- Batteries.Lean.AttributeExtra
/-- Get the list of declarations tagged with the tag attribute `attr`.  -/
Lean.TagAttributeExtra.getDecls : Lean.TagAttributeExtra → Lean.Environment → Array Lean.Name
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.trivial.eq_1 : ∀ {R : Type u_5} [inst : Semiring R] [inst_1 : DecidablePred fun x => x = 0] [inst_2 : NoZeroDivisors R] {S : Type u_6}
  [inst_3 : Semiring S] [inst_4 : PartialOrder S] [inst_5 : IsOrderedRing S] [inst_6 : Nontrivial S],
  AbsoluteValue.trivial =
    { toFun := fun x => if x = 0 then 0 else 1, map_mul' := ⋯, nonneg' := ⋯, eq_zero' := ⋯, add_le' := ⋯ }
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.mul_lt_one'`.  -/
Left.mul_lt_one' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b : α}, a < 1 → b < 1 → a * b < 1
-- Mathlib.Algebra.Group.Subsemigroup.Basic
MulHom.ofDense.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : Semigroup M] [inst_1 : Semigroup N] {s : Set M} (f : M → N)
  (hs : Subsemigroup.closure s = ⊤) (hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y),
  MulHom.ofDense f hs hmul = { toFun := f, map_mul' := ⋯ }
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.brecOn.eq : ∀ {motive : Nat.Internal.Linear.Expr → Sort u} (t : Nat.Internal.Linear.Expr)
  (F_1 : (t : Nat.Internal.Linear.Expr) → Nat.Internal.Linear.Expr.below t → motive t),
  Nat.Internal.Linear.Expr.brecOn t F_1 = F_1 t (Nat.Internal.Linear.Expr.brecOn.go t F_1).2
-- Init.Data.Int.Order
Int.sub_neg_of_lt : ∀ {a b : ℤ}, a < b → a - b < 0
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.instIsIsoFunctorHom : ∀ {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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] {F G : CategoryTheory.SingleFunctors C D A} (f : F ⟶ G)
  [CategoryTheory.IsIso f] (n : A), CategoryTheory.IsIso (f.hom n)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso_inv_τ₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcyclesEIso._auto_3),
  (X.kernelSequenceOpcyclesEIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv.τ₂ = (X.opcyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom
-- Lean.SubExpr
Lean.SubExpr.GoalsLocation.mk : Lean.MVarId → Lean.SubExpr.GoalLocation → Lean.SubExpr.GoalsLocation
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.ofProp_or : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {φ₁ φ₂ : Prop},
  Lean.Order.join (Lean.Order.CompleteLattice.ofProp φ₁) (Lean.Order.CompleteLattice.ofProp φ₂) =
    Lean.Order.CompleteLattice.ofProp (φ₁ ∨ φ₂)
-- Mathlib.NumberTheory.SumTwoSquares
/-- A natural number `n` is a sum of two squares if and only if `n = a^2 * b` with natural
numbers `a` and `b` such that `-1` is a square modulo `b`.  -/
Nat.eq_sq_add_sq_iff_eq_sq_mul : ∀ {n : ℕ}, (∃ x y, n = x ^ 2 + y ^ 2) ↔ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.coe_valueGroupOrderIso_coe : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  (a : ↥(MonoidWithZeroHom.ofClass (IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuation K v)).valueGroup),
  (IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderIso K v) ↑a =
    ↑((IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupEquiv K v) a)
-- Mathlib.MeasureTheory.Function.EssSup
ae_lt_of_lt_essInf : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : ConditionallyCompleteLinearOrder β] {x : β} {f : α → β},
  x < essInf f μ →
    autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (MeasureTheory.ae μ) f) ae_lt_of_lt_essInf._auto_1 →
      ∀ᵐ (y : α) ∂μ, x < f y
-- Mathlib.Topology.Sets.Opens
/-- A set of `opens α` is a basis if the set of corresponding sets is a topological basis.  -/
TopologicalSpace.Opens.IsBasis : {α : Type u_2} → [inst : TopologicalSpace α] → Set (TopologicalSpace.Opens α) → Prop
-- Batteries.Data.String.Lemmas
String.contains_iff : ∀ (s : String) (c : Char), String.Legacy.contains s c = true ↔ c ∈ s.toList
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.comap_sup_comap_le : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H K : AddSubgroup N) (f : G →+ N),
  AddSubgroup.comap f H ⊔ AddSubgroup.comap f K ≤ AddSubgroup.comap f (H ⊔ K)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonCommand.fromJson : Lean.Json → Except String Lean.Lsp.Command
-- Mathlib.RingTheory.Ideal.Maps
Module.annihilator_eq_bot : ∀ {R : Type u_4} {M : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.annihilator R M = ⊥ ↔ FaithfulSMul R M
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
AlgebraicGeometry.LocallyRingedSpace.evaluation_eq_zero_iff_notMem_basicOpen : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) {U : TopologicalSpace.Opens ↑X.toTopCat} (x : ↥U)
  (f : ↑(X.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (X.evaluation x)) f = 0 ↔ ↑x ∉ X.toRingedSpace.basicOpen f
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A finite union of countably compact sets is countably compact.  -/
isCountablyCompact_iUnion : ∀ {E : Type u_2} [inst : TopologicalSpace E] {ι : Sort u_4} {f : ι → Set E} [Finite ι],
  (∀ (i : ι), IsCountablyCompact (f i)) → IsCountablyCompact (⋃ i, f i)
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.mk_eq_top : ∀ {M : Type u_1} [inst : AddZeroClass M] (toSubsemigroup : AddSubsemigroup M) (zero_mem' : 0 ∈ toSubsemigroup.carrier),
  { toAddSubsemigroup := toSubsemigroup, zero_mem' := zero_mem' } = ⊤ ↔ toSubsemigroup = ⊤
-- Mathlib.NumberTheory.ModularForms.Basic
/-- These are `SlashInvariantForm`'s that are holomorphic and bounded at infinity.  -/
ModularForm : Subgroup (GL (Fin 2) ℝ) → ℤ → Type
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingNorm.toAddGroupNorm : {R : Type u_2} → [inst : NonUnitalNonAssocRing R] → RingNorm R → AddGroupNorm R
-- Mathlib.SetTheory.Cardinal.Basic
/-- The lift of a supremum is the supremum of the lifts.  -/
Cardinal.lift_iSup : ∀ {ι : Type v} {f : ι → Cardinal.{w}},
  BddAbove (Set.range f) → Cardinal.lift.{u, w} (iSup f) = ⨆ i, Cardinal.lift.{u, w} (f i)
-- Lean.Data.Lsp.Basic
Lean.Lsp.WorkspaceEdit.mk.inj : ∀ {changes? : Option (Std.TreeMap Lean.Lsp.DocumentUri Lean.Lsp.TextEditBatch compare)}
  {documentChanges? : Option (Array Lean.Lsp.DocumentChange)}
  {changeAnnotations? : Option (Std.TreeMap String Lean.Lsp.ChangeAnnotation compare)}
  {changes?_1 : Option (Std.TreeMap Lean.Lsp.DocumentUri Lean.Lsp.TextEditBatch compare)}
  {documentChanges?_1 : Option (Array Lean.Lsp.DocumentChange)}
  {changeAnnotations?_1 : Option (Std.TreeMap String Lean.Lsp.ChangeAnnotation compare)},
  { changes? := changes?, documentChanges? := documentChanges?, changeAnnotations? := changeAnnotations? } =
      { changes? := changes?_1, documentChanges? := documentChanges?_1, changeAnnotations? := changeAnnotations?_1 } →
    changes? = changes?_1 ∧ documentChanges? = documentChanges?_1 ∧ changeAnnotations? = changeAnnotations?_1
-- Mathlib.Topology.Instances.Matrix
Topology.IsOpenEmbedding.matrix_map : ∀ {m : Type u_11} {n : Type u_12} {R : Type u_13} {S : Type u_14} [inst : TopologicalSpace R]
  [inst_1 : TopologicalSpace S] {f : R → S} [Finite m] [Finite n],
  Topology.IsOpenEmbedding f → Topology.IsOpenEmbedding fun x => x.map f
-- Lean.Parser.Syntax
Lean.Parser.Command.macroRhs.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RepresentationTheory.Basic
Representation.prod_apply_apply : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring k] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : Module k V] [inst_4 : AddCommMonoid W] [inst_5 : Module k W]
  (ρV : Representation k G V) (ρW : Representation k G W) (g : G) (i : V × W),
  ((ρV.prod ρW) g) i = ((ρV g) i.1, (ρW g) i.2)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- In a braided monoidal category, the functors `tensorLeft X` and
`tensorRight X` are isomorphic.  -/
CategoryTheory.BraidedCategory.tensorLeftIsoTensorRight : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] →
        (X : C) → CategoryTheory.MonoidalCategory.tensorLeft X ≅ CategoryTheory.MonoidalCategory.tensorRight X
-- Init.Data.List.MinMaxOn
List.isSome_minOn?_iff : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α},
  (List.minOn? f xs).isSome = true ↔ xs ≠ []
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.refl_symm : ∀ {A : Type u_1} [inst : Add A] [inst_1 : Mul A] [inst_2 : Star A], StarRingEquiv.refl.symm = StarRingEquiv.refl
-- Mathlib.Topology.CWComplex.Classical.Finite
Topology.RelCWComplex.FiniteType.mk : ∀ {X : Type u} [inst : TopologicalSpace X] {C D : Set X} [inst_1 : Topology.RelCWComplex C D],
  (∀ (n : ℕ), Finite (Topology.RelCWComplex.cell C n)) → Topology.RelCWComplex.FiniteType C
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.single_mem_cycles₁_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (g : G) (a : ↑A),
  (fun₀ | g => a) ∈ groupHomology.cycles₁ A ↔ (A.ρ g) a = a
-- Lean.Setup
/-- A Lean plugin. Plugins are shared libraries with an initialization function.  -/
Lean.Plugin : Type
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_set_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s t : Set β} {a : α}, s ⊆ t → a +ᵥ s ⊆ a +ᵥ t
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientEquivProdOfLE_symm_apply : ∀ {α : Type u_1} [inst : Group α] {s t : Subgroup α} (h_le : s ≤ t) (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t),
  (Subgroup.quotientEquivProdOfLE h_le).symm a = Quotient.map' (fun b => Quotient.out a.1 * ↑b) ⋯ a.2
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.multiplicativeClosure.below : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W : CategoryTheory.MorphismProperty C} →
      {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → W.multiplicativeClosure x → Prop} →
        {X Y : C} → {x : X ⟶ Y} → W.multiplicativeClosure x → Prop
-- Lean.Meta.Basic
Lean.Meta.instBEqInfoCacheKey.beq : Lean.Meta.InfoCacheKey → Lean.Meta.InfoCacheKey → Bool
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.isEmbedding : ∀ {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E₂] [inst_3 : Module R₂ E₂] [inst_4 : NormedAddCommGroup F]
  [inst_5 : Module R F] (f : F →ₛₗᵢ[σ₁₂] E₂), Topology.IsEmbedding ⇑f
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {k : α}, k ∉ t₁ → (t₁ ∩ t₂).get! k = default
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.isSup.inj : ∀ {lhs rhs res lhs_1 rhs_1 res_1 : ℕ},
  Mathlib.Tactic.Order.AtomicFact.isSup lhs rhs res = Mathlib.Tactic.Order.AtomicFact.isSup lhs_1 rhs_1 res_1 →
    lhs = lhs_1 ∧ rhs = rhs_1 ∧ res = res_1
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_left_split_dvd1 : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ p₃ : Int.Internal.Linear.Poly) (d : ℤ) (k : ℕ) (a : ℤ)
  (p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.cooper_dvd_left_split ctx p₁ p₂ p₃ d k →
    Int.Internal.Linear.cooper_dvd_left_split_dvd1_cert p₁ p' a ↑k = true → a ∣ Int.Internal.Linear.Poly.denote' ctx p'
-- Mathlib.Analysis.Complex.OpenMapping
/-- The *open mapping theorem* for holomorphic functions, global version: if a function `g : E → ℂ`
is analytic on a connected set `U`, then either it is constant on `U`, or it is open on `U` (in the
sense that it maps any open set contained in `U` to an open set in `ℂ`).  -/
AnalyticOnNhd.is_constant_or_isOpen : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {U : Set E} {g : E → ℂ},
  AnalyticOnNhd ℂ g U → IsPreconnected U → (∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen s → IsOpen (g '' s)