mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.instIsIsoFunctorOppositeHomFullSubcategoryIsSheafAppSheafCounitSheafificationAdjunction : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  (P : CategoryTheory.Sheaf J D), CategoryTheory.IsIso ((CategoryTheory.sheafificationAdjunction J D).counit.app P).hom
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_keysArray : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α],
  m.keysArray.isEmpty = m.isEmpty
-- Mathlib.Order.Copy
/-- A function to create a provable equal copy of a coframe with possibly different definitional
equalities.  -/
Coframe.copy : {α : Type u} →
  (c : Order.Coframe α) →
    (le : α → α → Prop) →
      le = LE.le →
        (top : α) →
          top = ⊤ →
            (bot : α) →
              bot = ⊥ →
                (sup : α → α → α) →
                  sup = max →
                    (inf : α → α → α) →
                      inf = min →
                        (sdiff : α → α → α) →
                          sdiff = SDiff.sdiff →
                            (hnot : α → α) →
                              hnot = HNot.hnot →
                                (sSup : Set α → α) →
                                  sSup = SupSet.sSup → (sInf : Set α → α) → sInf = InfSet.sInf → Order.Coframe α
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.toSubmonoid_injective : ∀ {R : Type u} [inst : NonAssocSemiring R], Function.Injective Subsemiring.toSubmonoid
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isBoundary₂_iff : ∀ {G : Type u_1} {A : Type u_2} [inst : Group G] [inst_1 : AddCommGroup A] [inst_2 : DistribMulAction G A]
  (x : G × G →₀ A),
  groupHomology.IsBoundary₂ x ↔
    ∃ y,
      (y.sum fun g a =>
          (((fun₀ | (g.2.1, g.2.2) => a) - fun₀ | (g.1 * g.2.1, g.2.2) => g.1 • a) +
              fun₀ | (g.1, g.2.1 * g.2.2) => g.1 • a) -
            fun₀ | (g.1, g.2.1) => g.1 • a) =
        x
-- Mathlib.Order.CompleteLattice.Basic
sInf_apply_eq_sInf_image : ∀ {α : Type u_8} {β : α → Type u_9} [inst : (i : α) → InfSet (β i)] {s : Set ((a : α) → β a)} {a : α},
  sInf s a = sInf (Function.eval a '' s)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
commutative_of_cyclic_center_quotient : ∀ {G : Type u_2} {G' : Type u_3} [inst : Group G] [inst_1 : Group G'] [IsCyclic G'] (f : G →* G'),
  f.ker ≤ Subgroup.center G → ∀ (a b : G), a * b = b * a
-- Mathlib.Data.Ordmap.Invariants
Ordnode.Bounded.to_lt : ∀ {α : Type u_1} [inst : Preorder α] {t : Ordnode α} {x y : α}, t.Bounded ↑x ↑y → x < y
-- Mathlib.FieldTheory.ChevalleyWarning
_private.Mathlib.FieldTheory.ChevalleyWarning.0.termQ : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_le_rpow_iff : ∀ {x y : NNReal} {z : ℝ}, 0 < z → (x ^ z ≤ y ^ z ↔ x ≤ y)
-- Std.Internal.Do.ExceptPost
/-- Componentwise partial order on `EPost.Cons`, via `PProd`.  -/
Std.Internal.Do.instPartialOrderCons : {eh : Type u_1} →
  {et : Type u_2} →
    [Lean.Order.PartialOrder eh] → [Lean.Order.PartialOrder et] → Lean.Order.PartialOrder (EPost.Cons✝ eh et)
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
coe_finsetBasisOfLinearIndependentOfCardEqFinrank : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {s : Finset V}
  (hs : s.Nonempty) (lin_ind : LinearIndependent K Subtype.val) (card_eq : s.card = Module.finrank K V),
  ⇑(finsetBasisOfLinearIndependentOfCardEqFinrank hs lin_ind card_eq) = Subtype.val
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Stream.mk.injEq : ∀ (state state_1 : Std.Mutex Std.Http.Body.Channel.State✝),
  ({ state := state } = { state := state_1 }) = (state = state_1)
-- Mathlib.Data.Nat.Nth
Nat.filter_range_nth_eq_insert_of_infinite : ∀ {p : ℕ → Prop} [inst : DecidablePred p],
  (Set.ofPred p).Infinite →
    ∀ (k : ℕ),
      {n ∈ Finset.range (Nat.nth p (k + 1)) | p n} = insert (Nat.nth p k) ({n ∈ Finset.range (Nat.nth p k) | p n})
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.instNeg : {α : Type u} → Neg (FreeAddGroup α)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRatCheck.match_3.splitter : {n : ℕ} →
  (motive : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n → ℕ × Array ℕ → Sort u_1) →
    (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) →
      (ratHint : ℕ × Array ℕ) →
        ((clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))) →
            (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) →
              (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
                (id : ℕ) →
                  (rupHints : Array ℕ) →
                    motive
                      { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }
                      (id, rupHints)) →
          motive f ratHint
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- In the canonical isometric isomorphism between a Hilbert sum `E` of `G : ι → Type*` and
`lp G 2`, a finitely-supported vector in `lp G 2` is the image of the associated finite sum of
elements of `E`.  -/
IsHilbertSum.linearIsometryEquiv_symm_apply_dfinsupp_sum_single : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {G : ι → Type u_4} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_5 : CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E}
  [inst_6 : DecidableEq ι] [inst_7 : (i : ι) → DecidableEq (G i)] (hV : IsHilbertSum 𝕜 G V) (W₀ : Π₀ (i : ι), G i),
  hV.linearIsometryEquiv.symm (W₀.sum (lp.single 2)) = W₀.sum fun i => ⇑(V i)
-- Mathlib.Algebra.Star.Unitary
unitarySubgroupUnitsEquiv_apply_coe : ∀ {M : Type u_5} [inst : Monoid M] [inst_1 : StarMul M] (x : ↥(unitarySubgroup Mˣ)),
  ↑(unitarySubgroupUnitsEquiv x) = ↑↑x
-- Mathlib.RingTheory.PrincipalIdealDomain
isPrincipalIdealRing_pi_iff : ∀ {ι : Type u_5} [Finite ι] {R : ι → Type u_4} [inst : (i : ι) → Semiring (R i)],
  IsPrincipalIdealRing ((i : ι) → R i) ↔ ∀ (i : ι), IsPrincipalIdealRing (R i)
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.BasicConstructibleSetData.map_comp : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring T] (φ : S →+* T) (ψ : R →+* S) (C : PrimeSpectrum.BasicConstructibleSetData R),
  PrimeSpectrum.BasicConstructibleSetData.map (φ.comp ψ) C =
    PrimeSpectrum.BasicConstructibleSetData.map φ (PrimeSpectrum.BasicConstructibleSetData.map ψ C)
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.minEntry?.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α fun x => β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k : α) →
                (v : β) →
                  (r : Std.DTreeMap.Internal.Impl α fun x => β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r)) →
            ((size : ℕ) →
                (k : α) →
                  (v : β) →
                    (size_1 : ℕ) →
                      (k_1 : α) →
                        (v_1 : β) →
                          (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                            motive
                              (Std.DTreeMap.Internal.Impl.inner size k v
                                (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)) →
              motive x
-- Mathlib.Analysis.SpecialFunctions.Log.ERealExp
EReal.exp_strictMono : StrictMono EReal.exp
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.Δ_of_isShortNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsShortNF], W.Δ = -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, 2 ≤ f.support.card → f.eraseLead ≠ 0
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
/-- The connecting homomorphism `X.ω₁.obj (mk₁ g) ⟶ (X.ω₁.obj (mk₁ f))⟦(1 : ℤ)⟧`
of a spectral object `X` in a pretriangulated category when `f : i ⟶ j` and `g : j ⟶ k`
are composable.  -/
CategoryTheory.Triangulated.SpectralObject.δ : {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.Limits.HasZeroObject C] →
          [inst_3 : CategoryTheory.HasShift C ℤ] →
            [inst_4 : CategoryTheory.Preadditive C] →
              [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                [inst_6 : CategoryTheory.Pretriangulated C] →
                  (X : CategoryTheory.Triangulated.SpectralObject C ι) →
                    {i j k : ι} →
                      (f : i ⟶ j) →
                        (g : j ⟶ k) →
                          X.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ g) ⟶
                            (CategoryTheory.shiftFunctor C 1).obj (X.ω₁.obj (CategoryTheory.ComposableArrows.mk₁ f))
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasAntidiagonal.antidiagonal_subtype_ext_iff : ∀ {A : Type u_1} [inst : AddCancelMonoid A] [inst_1 : Finset.HasAntidiagonal A] {n : A}
  {p q : ↥(Finset.HasAntidiagonal.antidiagonal n)}, p = q ↔ (↑p).1 = (↑q).1
-- Mathlib.RingTheory.Derivation.Basic
Derivation.leibniz_div_const : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {K : Type u_4}
  [inst_3 : Field K] [inst_4 : Module K M] [inst_5 : Algebra R K] (D : Derivation R K M) (a b : K),
  D b = 0 → D (a / b) = b⁻¹ • D a
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.CommComon.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C) [comon : CategoryTheory.ComonObj X]
  [comm : CategoryTheory.IsCommComonObj X] (X_1 : C) (comon_1 : CategoryTheory.ComonObj X_1)
  (comm_1 : CategoryTheory.IsCommComonObj X_1),
  ({ X := X, comon := comon, comm := comm } = { X := X_1, comon := comon_1, comm := comm_1 }) =
    (X = X_1 ∧ comon ≍ comon_1)
-- Mathlib.MeasureTheory.Measure.AEDisjoint
MeasureTheory.AEDisjoint.of_null_left : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  μ s = 0 → MeasureTheory.AEDisjoint μ s t
-- Mathlib.Data.NNReal.Defs
NNReal.one_lt_coe : ∀ {r : NNReal}, 1 < ↑r ↔ 1 < r
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.RCond.min : ∀ {l : BoxIntegral.IntegrationParams} {ι : Type u_2} {r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)},
  l.RCond r₁ → l.RCond r₂ → l.RCond fun x => min (r₁ x) (r₂ x)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) {k k' : α},
  (↑m).WF →
    ∀ [inst_4 : Inhabited β] {f : Option β → Option β},
      Std.DHashMap.Internal.Raw₀.Const.get! (Std.DHashMap.Internal.Raw₀.Const.alter m k f) k' =
        if (k == k') = true then (f (Std.DHashMap.Internal.Raw₀.Const.get? m k)).get!
        else Std.DHashMap.Internal.Raw₀.Const.get! m k'
-- Mathlib.Algebra.Order.Ring.Cone
RingCone.nonneg_toSubsemiring : ∀ {T : Type u_1} [inst : Ring T] [inst_1 : PartialOrder T] [inst_2 : IsOrderedRing T],
  (RingCone.nonneg T).toSubsemiring = Subsemiring.nonneg T
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_erase_eq_iff_not_compare_eq_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, (t.erase k).maxKey? = t.maxKey? ↔ ∀ {km : α}, t.maxKey? = some km → ¬cmp k km = Ordering.eq
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.Precylinder.LeftHomotopy.h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {P : HomotopicalAlgebra.Precylinder X} {Y : C}
  {f g : X ⟶ Y} (self : P.LeftHomotopy f g), CategoryTheory.CategoryStruct.comp P.i₀ self.h = f
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.union_insert_right_equiv_insert_union : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α] {p : (a : α) × β a},
  (↑m₁).WF → (↑m₂).WF → (↑(m₁.union (m₂.insert p.fst p.snd))).Equiv ↑((m₁.union m₂).insert p.fst p.snd)
-- Mathlib.Algebra.Group.Basic
/-- To show a property of all powers of `g` it suffices to show it is closed under multiplication
by `g` and `g⁻¹` on the right. For subgroups generated by more than one element, see
`Subgroup.closure_induction_right`.  -/
zpow_induction_right : ∀ {G : Type u_3} [inst : Group G] {g : G} {P : G → Prop},
  P 1 → (∀ (a : G), P a → P (a * g)) → (∀ (a : G), P a → P (a * g⁻¹)) → ∀ (n : ℤ), P (g ^ n)
-- Mathlib.Algebra.Group.Action.Faithful
vadd_left_injective' : ∀ {M : Type u_1} {α : Type u_3} [inst : VAdd M α] [FaithfulVAdd M α], Function.Injective fun x1 x2 => x1 +ᵥ x2
-- Mathlib.NumberTheory.LSeries.ZMod
/-- The L-function of a function on `ZMod 1` is a scalar multiple of the Riemann zeta function.  -/
ZMod.LFunction_modOne_eq : ∀ (Φ : ZMod 1 → ℂ) (s : ℂ), ZMod.LFunction Φ s = Φ 0 * riemannZeta s
-- Mathlib.GroupTheory.Exponent
AddMonoid.exponent_eq_zero_iff : ∀ {G : Type u} [inst : AddMonoid G], AddMonoid.exponent G = 0 ↔ ¬AddMonoid.ExponentExists G
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_toIcoMod : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a₁ a₂ b : α), toIcoMod hp a₁ (toIcoMod hp a₂ b) = toIcoMod hp a₁ b
-- Lean.Message
Lean.NamingContext.openDecls : Lean.NamingContext → List Lean.OpenDecl
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.algebra : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (S : Subalgebra R A) → Algebra R ↥S
-- Init.Data.UInt.Bitwise
USize.and_lt_add_one : ∀ {b c : USize}, c ≠ -1 → b &&& c < c + 1
-- Mathlib.Order.Filter.AtTopBot.Ring
Filter.Tendsto.atTop_mul_atBot₀ : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] {l : Filter β}
  {f g : β → α},
  Filter.Tendsto f l Filter.atTop → Filter.Tendsto g l Filter.atBot → Filter.Tendsto (fun x => f x * g x) l Filter.atBot
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_subsingleton_iff : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Nontrivial R] [Subsingleton M] (f : ι → M), LinearIndependent R f ↔ IsEmpty ι
-- Mathlib.RingTheory.Polynomial.GaussNorm
Polynomial.gaussNorm.eq_1 : ∀ {R : Type u_1} {F : Type u_2} [inst : Semiring R] [inst_1 : FunLike F R ℝ] (v : F) (c : ℝ) (p : Polynomial R),
  Polynomial.gaussNorm v c p = if h : p.support.Nonempty then p.support.sup' h fun i => v (p.coeff i) * c ^ i else 0
-- Mathlib.Analysis.Seminorm
Seminorm.mk.sizeOf_spec : ∀ {𝕜 : Type u_12} {E : Type u_13} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E]
  [inst_3 : SizeOf 𝕜] [inst_4 : SizeOf E] (toAddGroupSeminorm : AddGroupSeminorm E)
  (smul' : ∀ (a : 𝕜) (x : E), toAddGroupSeminorm.toFun (a • x) = ‖a‖ * toAddGroupSeminorm.toFun x),
  sizeOf { toAddGroupSeminorm := toAddGroupSeminorm, smul' := smul' } = 1 + sizeOf toAddGroupSeminorm
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.instSMulNatSubtypeMem : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → (I : TwoSidedIdeal R) → SMul ℕ ↥I
-- Mathlib.Data.Set.Operations
Set.mem_image2 : ∀ {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {s : Set α} {t : Set β} {c : γ},
  c ∈ Set.image2 f s t ↔ ∃ a ∈ s, ∃ b ∈ t, f a b = c
-- Mathlib.LinearAlgebra.TensorPower.Symmetric
/-- The multilinear map that takes `ι`-indexed elements of `M` and
returns their symmetric tensor power. Denoted `⨂ₛ[R] i, f i`.  -/
SymmetricPower.tprod : (R : Type u) →
  {ι : Type u} →
    [inst : CommSemiring R] →
      {M : Type v} →
        [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → MultilinearMap R (fun x => M) (SymmetricPower R ι M)
-- Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover
TopCat.Presheaf.generateEquivalenceOpensLe_counitIso : ∀ {X : TopCat} {ι : Type u_2} (U : ι → TopologicalSpace.Opens ↑X) {Y : TopologicalSpace.Opens ↑X} (hY : Y = iSup U),
  (TopCat.Presheaf.generateEquivalenceOpensLe U hY).counitIso = CategoryTheory.eqToIso ⋯
-- Mathlib.Algebra.Group.ULift
ULift.rightCancelSemigroup.eq_1 : ∀ {α : Type u} [inst : RightCancelSemigroup α],
  ULift.rightCancelSemigroup = Function.Injective.rightCancelSemigroup ⇑Equiv.ulift ⋯ ⋯
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} ⦃α β : X ≅ Y⦄, α.hom = β.hom → α = β
-- Lean.Parser.Types
Lean.Parser.ParserInfo.collectKinds : Lean.Parser.ParserInfo → Lean.Parser.SyntaxNodeKindSet → Lean.Parser.SyntaxNodeKindSet
-- Mathlib.Topology.Defs.Filter
/-- In a compact space, `Set.univ` is a compact set.  -/
CompactSpace.isCompact_univ : ∀ {X : Type u_1} {inst : TopologicalSpace X} [self : CompactSpace X], IsCompact Set.univ
-- Mathlib.Data.List.ReduceOption
List.reduceOption.eq_1 : ∀ {α : Type u_1}, List.reduceOption = List.filterMap id
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- **Alias** of `Subgroup.IsFinitelyNormallyGenerated`.

---

`N.IsFinitelyNormallyGenerated` says that the subgroup `N` is the normal closure
of a finite set.  -/
Subgroup.IsNormalClosureFG : {G : Type u_1} → [inst : Group G] → Subgroup G → Prop
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.reuse.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {var : Lean.FVarId} {i : Lean.Compiler.LCNF.CtorInfo} {updateHeader : Bool}
  {args : Array (Lean.Compiler.LCNF.Arg pu)}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_19} {var_1 : Lean.FVarId}
  {i_1 : Lean.Compiler.LCNF.CtorInfo} {updateHeader_1 : Bool} {args_1 : Array (Lean.Compiler.LCNF.Arg pu)}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_19},
  Lean.Compiler.LCNF.LetValue.reuse var i updateHeader args h =
      Lean.Compiler.LCNF.LetValue.reuse var_1 i_1 updateHeader_1 args_1 h_1 →
    var = var_1 ∧ i = i_1 ∧ updateHeader = updateHeader_1 ∧ args = args_1
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- Given graph homomorphisms from each connected component of `G` to `H`, this is the graph
homomorphism from `G` to `H`.  -/
SimpleGraph.homOfConnectedComponents : {V : Type u} →
  {V' : Type v} →
    (G : SimpleGraph V) → {H : SimpleGraph V'} → ((c : G.ConnectedComponent) → c.toSimpleGraph →g H) → G →g H
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.FunctorsInverting.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {W : CategoryTheory.MorphismProperty C} {F₁ F₂ : W.FunctorsInverting D}, F₁.obj = F₂.obj → F₁ = F₂
-- Init.Data.Int.DivMod.Lemmas
Int.add_mul_fmod_self_right : ∀ (a b c : ℤ), (a + b * c).fmod c = a.fmod c
-- Mathlib.ModelTheory.FinitelyGenerated
/-- A structure is countably generated if it is the closure of a countable subset.  -/
FirstOrder.Language.Structure.CG : (L : FirstOrder.Language) → (M : Type u_1) → [L.Structure M] → Prop
-- Mathlib.Probability.Distributions.Uniform
MeasureTheory.pdf.IsUniform.pdf_eq : ∀ {E : Type u_1} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} {Ω : Type u_2} {x : MeasurableSpace Ω}
  {ℙ : MeasureTheory.Measure Ω} {X : Ω → E} {s : Set E},
  MeasurableSet s → MeasureTheory.pdf.IsUniform X s ℙ μ → MeasureTheory.pdf X ℙ μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • 1)
-- Mathlib.Algebra.Module.Torsion.Basic
Module.isTorsionBy_iff_mem_annihilator : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {a : R},
  Module.IsTorsionBy R M a ↔ a ∈ Module.annihilator R M
-- Mathlib.Algebra.Group.End
Equiv.Perm.extendDomain_inv : ∀ {α : Type u_4} {β : Type u_5} (e : Equiv.Perm α) {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p),
  (e.extendDomain f)⁻¹ = e⁻¹.extendDomain f
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- A finite sum of rationals with positive `p`-adic valuation has positive `p`-adic valuation
(if the sum is non-zero).  -/
padicValRat.sum_pos_of_pos : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {n : ℕ} {F : ℕ → ℚ},
  (∀ i < n, 0 < padicValRat p (F i)) → ∑ i ∈ Finset.range n, F i ≠ 0 → 0 < padicValRat p (∑ i ∈ Finset.range n, F i)
-- Init.Prelude
/-- Returns `a` modulo `n` as a `Fin n`.

This function exists for bootstrapping purposes. Use `Fin.ofNat` instead.
 -/
Fin.Internal.ofNat : (n : ℕ) → 0 < n → ℕ → Fin n
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.range_algebraMap_eq : ∀ (A : Type u) [inst : CommRing A] (K : Type v) [inst_1 : Field K] [inst_2 : Algebra A K] [inst_3 : IsDomain A]
  [inst_4 : ValuationRing A] [inst_5 : IsFractionRing A K],
  (ValuationRing.valuation A K).integer = (algebraMap A K).range
-- Mathlib.Data.Set.Function
Set.injOn_iff_invFunOn_image_image_eq_self : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [inst : Nonempty α],
  Set.InjOn f s ↔ Function.invFunOn f s '' f '' s = s
-- Batteries.Data.List.Lemmas
List.mem_findIdxs_iff_getElem_sub_pos : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {s i : ℕ},
  i ∈ List.findIdxs p xs s ↔ s ≤ i ∧ ∃ (hix : i - s < xs.length), p xs[i - s] = true
-- Lean.Meta.Tactic.Grind.Attr
/-- Return theorem kind for `stx` of the form `Attr.grindThmMod`  -/
Lean.Meta.Grind.getAttrKindCore : Lean.Syntax → Lean.CoreM Lean.Meta.Grind.AttrKind
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.operator : Lean.Lsp.SemanticTokenType
-- Mathlib.Order.Partition.Finpartition
Finpartition.parts_eq_empty_iff : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} {P : Finpartition a}, P.parts = ∅ ↔ a = ⊥
-- Init.Data.UInt.Bitwise
UInt16.and_zero : ∀ {a : UInt16}, a &&& 0 = 0
-- Mathlib.Order.Hom.WithTopBot
OrderIso.withBotCongr.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] (e : α ≃o β),
  e.withBotCongr =
    {
      toEquiv :=
        (have __spread.0 := e.toOrderEmbedding.withBotMap;
          let __spread.1 := { toEquiv := e.toEquiv, map_rel_iff' := ⋯ }.withBotCongr;
          { toFun := WithBot.map ⇑e, invFun := __spread.1.invFun, left_inv := ⋯, right_inv := ⋯,
            map_rel_iff' := ⋯ }).toEquiv,
      map_rel_iff' := ⋯ }
-- Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Mathlib.Tactic.Bicategory.naturality_id : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {p : a ⟶ b} {f : b ⟶ c} {pf : a ⟶ c}
  (η_f : CategoryTheory.CategoryStruct.comp p f ≅ pf),
  CategoryTheory.Bicategory.whiskerLeftIso p (CategoryTheory.Iso.refl f) ≪≫ η_f = η_f
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.dvd_term_of_isRoot_of_dvd_terms : ∀ {S : Type v} [inst : CommRing S] {r p : S} {f : Polynomial S} (i : ℕ),
  f.IsRoot r → (∀ (j : ℕ), j ≠ i → p ∣ f.coeff j * r ^ j) → p ∣ f.coeff i * r ^ i
-- Mathlib.LinearAlgebra.Matrix.Module
/-- The induced linear map from `Mⁿ` to `Nⁿ` by a linear map `f : M → N`, this is the matrix linear
version of `LinearMap.compLeft`.  -/
LinearMap.mapMatrixModule : (ι : Type u_1) →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : Ring R] →
          [inst_1 : Fintype ι] →
            [inst_2 : DecidableEq ι] →
              [inst_3 : AddCommGroup M] →
                [inst_4 : Module R M] →
                  [inst_5 : AddCommGroup N] → [inst_6 : Module R N] → (M →ₗ[R] N) → (ι → M) →ₗ[Matrix ι ι R] ι → N