mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Bicategory.Adjunction.homEquiv₁.eq_1 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {b c d : B} {l : b ⟶ c} {r : c ⟶ b}
  (adj : CategoryTheory.Bicategory.Adjunction l r) {g : b ⟶ d} {h : c ⟶ d},
  adj.homEquiv₁ =
    {
      toFun := fun γ =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft r γ)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator r l h).inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight adj.counit h)
              (CategoryTheory.Bicategory.leftUnitor h).hom)),
      invFun := fun β =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor g).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight adj.unit g)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator l r g).hom
              (CategoryTheory.Bicategory.whiskerLeft l β))),
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
/-- Given `P : ObjectProperty C`, a family of categories `J a`, this
is the transfinite iteration of `Q ↦ Q.strictLimitsClosureStep J`.  -/
CategoryTheory.ObjectProperty.strictLimitsClosureIter : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.ObjectProperty C →
      {α : Type t} →
        (J : α → Type u') →
          [(a : α) → CategoryTheory.Category.{v', u'} (J a)] →
            {β : Type w'} →
              [inst_2 : LinearOrder β] → [SuccOrder β] → [WellFoundedLT β] → β → CategoryTheory.ObjectProperty C
-- Init.Data.Iterators.Producers.Monadic.List
_private.Init.Data.Iterators.Producers.Monadic.List.0.Std.Iterators.Types.ListIterator.instIterator.match_1.splitter : {m : Type u_1 → Type u_2} →
  {α : Type u_1} →
    (motive : Std.IterStep (Std.IterM m α) α → Sort u_3) →
      (x : Std.IterStep (Std.IterM m α) α) →
        ((it' : Std.IterM m α) → (out : α) → motive (Std.IterStep.yield it' out)) →
          ((it : Std.IterM m α) → motive (Std.IterStep.skip it)) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.subgroupOf_bot_eq_bot : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.subgroupOf ⊥ = ⊥
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.map_subtype_le : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} (K : Subgroup ↥H), Subgroup.map H.subtype K ≤ H
-- Mathlib.Order.Filter.AtTopBot.Field
/-- If `f` tends to infinity along a nontrivial filter,
`fun x ↦ r * f x` tends to negative infinity if and only if `r < 0`.  -/
Filter.tendsto_const_mul_atBot_iff_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {l : Filter β}
  {f : β → α} {r : α} [l.NeBot],
  Filter.Tendsto f l Filter.atTop → (Filter.Tendsto (fun x => r * f x) l Filter.atBot ↔ r < 0)
-- Init.Data.Iterators.Lemmas.Consumers.Access
_private.Init.Data.Iterators.Lemmas.Consumers.Access.0.Std.Iter.atIdxSlow?_eq_match.match_3.eq_3 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- A diffeomorphism is a homeomorphism.  -/
Diffeomorph.toHomeomorph : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_4} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                {H : Type u_5} →
                  [inst_5 : TopologicalSpace H] →
                    {G : Type u_7} →
                      [inst_6 : TopologicalSpace G] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {J : ModelWithCorners 𝕜 F G} →
                            {M : Type u_9} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {N : Type u_11} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace G N] → {n : WithTop ℕ∞} → Diffeomorph I J M N n → M ≃ₜ N
-- Mathlib.Analysis.SpecificLimits.ArithmeticGeometric
arithGeom_same_eq_mul_div : ∀ {R : Type u_1} {a b : R} [inst : Field R], a ≠ 1 → ∀ (n : ℕ), arithGeom a b b n = b * (a ^ (n + 1) - 1) / (a - 1)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_right_mono₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀}
  [ZeroLEOneClass G₀], 1 ≤ a → Monotone fun n => a ^ n
-- Mathlib.Data.Rel
/-- Codomain of a relation, aka range.  -/
SetRel.cod : {α : Type u_1} → {β : Type u_2} → SetRel α β → Set β
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.mem_map_of_mem : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) {K : Subgroup G} {x : G},
  x ∈ K → f x ∈ Subgroup.map f K
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_inter_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF), m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.inter m₂ ⋯).getKey? k = none
-- Mathlib.Order.RelClasses
WellFoundedLT.eq_1 : ∀ (α : Type u_1) [inst : LT α], WellFoundedLT α = IsWellFounded α fun x1 x2 => x1 < x2
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.isEmpty.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashMap α β), m = m_1 → m.isEmpty = m_1.isEmpty
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
/-- **Alias** of `CategoryTheory.GrothendieckTopology.Point.presheafToSheafCompSheafFiberIso`.

---

The fiber functor on sheaves is obtained from the fiber functor on presheaves
by localization with respect to the class of morphisms `J.W`.  -/
CategoryTheory.GrothendieckTopology.Point.presheafToSheafCompSheafFiber : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (Φ : J.Point) →
        (A : Type u') →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            [CategoryTheory.Limits.HasProducts A] →
              [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
                [inst_4 : CategoryTheory.HasWeakSheafify J A] →
                  (CategoryTheory.presheafToSheaf J A).comp Φ.sheafFiber ≅ Φ.presheafFiber
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Subtracting the second vector passed to `oangle` from the first vector then swapping the
vectors does not change the sign of the angle.  -/
Orientation.oangle_sign_sub_left_swap : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), (o.oangle (x - y) x).sign = (o.oangle x y).sign
-- Aesop.Util.OrderedHashSet
Aesop.OrderedHashSet.toArray : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Aesop.OrderedHashSet α → Array α
-- Mathlib.Order.DirSupClosed
DirSupInaccOn.mono : ∀ {α : Type u_1} {s : Set α} {D₁ D₂ : Set (Set α)} [inst : Preorder α],
  D₁ ⊆ D₂ → DirSupInaccOn D₂ s → DirSupInaccOn D₁ s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_inter_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF), m₂.WF → m₂.isEmpty = true → (m₁.inter m₂ ⋯).isEmpty = true
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_nonneg' : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {f : ι → N} {s : Finset ι}
  [AddLeftMono N], (∀ (i : ι), 0 ≤ f i) → 0 ≤ ∑ i ∈ s, f i
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.isoEquivAlgEquiv_apply : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : CommRing X] [inst_2 : Algebra R X] [inst_3 : CommRing Y]
  [inst_4 : Algebra R Y] (i : CommAlgCat.of R X ≅ CommAlgCat.of R Y),
  CommAlgCat.isoEquivAlgEquiv i = CommAlgCat.algEquivOfIso i
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.map₁_one : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (φ : A ⟶ Rep.res 1 B), groupHomology.map 1 φ 1 = 0
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.pointReflection_symm : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (x : P),
  (AffineIsometryEquiv.pointReflection 𝕜 x).symm = AffineIsometryEquiv.pointReflection 𝕜 x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get?_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∪ t₂).get? k = t₂.get? k
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
/-- The zero locus of a set of sections over a compact open of a scheme is `X` if and only if
`s` is contained in the nilradical of `Γ(X, U)`.  -/
AlgebraicGeometry.Scheme.zeroLocus_eq_univ_iff_subset_nilradical_of_isCompact : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  IsCompact ↑U →
    ∀ (s : Set ↑(X.presheaf.obj (Opposite.op U))),
      X.zeroLocus s = Set.univ ↔ s ⊆ ↑(nilradical ↑(X.presheaf.obj (Opposite.op U)))
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k a : α} {v : β},
  (m.insertIfNew k v)[a]! = if (k == a) = true ∧ k ∉ m then v else m[a]!
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- A version of `MonoidHom.domRestrict` as a homomorphism.  -/
MonoidHom.domRestrictHom : {M : Type u_1} →
  [inst : MulOneClass M] →
    {S : Type u_5} →
      [inst_1 : SetLike S M] →
        [inst_2 : SubmonoidClass S M] → (M' : S) → (A : Type u_6) → [inst_3 : CommMonoid A] → (M →* A) →* ↥M' →* A
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiable_ofNat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (n : ℕ) [inst_7 : OfNat F n], Differentiable 𝕜 (OfNat.ofNat n)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.hasDerivAt_arcsin : ∀ {x : ℝ}, x ≠ -1 → x ≠ 1 → HasDerivAt Real.arcsin (1 / √(1 - x ^ 2)) x
-- Mathlib.Data.Ordmap.Invariants
Ordnode.insert.eq_2 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] (x : α) (sz : ℕ) (l : Ordnode α) (x_2 : α) (r : Ordnode α),
  Ordnode.insert x (Ordnode.node sz l x_2 r) =
    match cmpLE x x_2 with
    | Ordering.lt => (Ordnode.insert x l).balanceL x_2 r
    | Ordering.eq => Ordnode.node sz l x r
    | Ordering.gt => l.balanceR x_2 (Ordnode.insert x r)
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instNontrivialSubtypeMemAddSubgroup : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : StarRing R] [Nontrivial R], Nontrivial ↥(selfAdjoint R)
-- Mathlib.Data.Set.Card
/-- A `Set` of a subsingleton type has cardinality at most one.  -/
Set.ncard_le_one_of_subsingleton : ∀ {α : Type u_1} [Subsingleton α] (s : Set α), s.ncard ≤ 1
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.unfold_smul : ∀ {α : Type u_1} [inst : AddCommMonoid α] (n : ℕ) (x y : α), Mathlib.Tactic.Abel.smul n x = y → n • x = y
-- Mathlib.LinearAlgebra.Dimension.Basic
/-- Two linearly equivalent vector spaces have the same dimension.  -/
LinearEquiv.rank_eq : ∀ {R : Type u} {M M₁ : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (f : M ≃ₗ[R] M₁), Module.rank R M = Module.rank R M₁
-- Mathlib.Tactic.Linarith.Frontend
/-- Override the list of preprocessors.  -/
Mathlib.Tactic.Linarith.LinarithConfig.preprocessors : Mathlib.Tactic.Linarith.LinarithConfig → List Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor
-- Init.Data.SInt.Lemmas
Int16.toInt64_ne_neg_one : ∀ (a : Int16), a ≠ -1 → a.toInt64 ≠ -1
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExProd.mul.inj : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {x : Q(«$α»)} {e : Q(ℕ)}
  {b : Q(«$α»)} {a : Mathlib.Tactic.Ring.Common.ExBase BaseType sα x} {a_1 : Mathlib.Tactic.Ring.Common.ExProdNat e}
  {a_2 : Mathlib.Tactic.Ring.Common.ExProd BaseType sα b} {a_3 : Mathlib.Tactic.Ring.Common.ExBase BaseType sα x}
  {a_4 : Mathlib.Tactic.Ring.Common.ExProdNat e} {a_5 : Mathlib.Tactic.Ring.Common.ExProd BaseType sα b},
  Mathlib.Tactic.Ring.Common.ExProd.mul a a_1 a_2 = Mathlib.Tactic.Ring.Common.ExProd.mul a_3 a_4 a_5 →
    a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.botCharacteristic : ∀ {G : Type u_1} [inst : AddGroup G], ⊥.Characteristic
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.inv_le_dual : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B] (I : FractionalIdeal (nonZeroDivisors B) L), I⁻¹ ≤ FractionalIdeal.dual A K I
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
/-- The higher `Tor` groups for `X` and `Y` are zero if `Y` is projective.  -/
Rep.isZero_Tor_succ_of_projective : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (X Y : Rep.{u, u, u} k G) [CategoryTheory.Projective Y] (n : ℕ),
  CategoryTheory.Limits.IsZero (((Rep.Tor k G (n + 1)).obj X).obj Y)
-- Lean.Elab.Open
Lean.Elab.OpenDecl.State.mk.injEq : ∀ (openDecls : List Lean.OpenDecl) (currNamespace : Lean.Name) (openDecls_1 : List Lean.OpenDecl)
  (currNamespace_1 : Lean.Name),
  ({ openDecls := openDecls, currNamespace := currNamespace } =
      { openDecls := openDecls_1, currNamespace := currNamespace_1 }) =
    (openDecls = openDecls_1 ∧ currNamespace = currNamespace_1)
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.mul_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x y : CategoryTheory.CatCenter C) (X : C) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((x * y).app X) h =
    CategoryTheory.CategoryStruct.comp (x.app X) (CategoryTheory.CategoryStruct.comp (y.app X) h)
-- Lean.Elab.DefView
/-- Syntax of top-level tactic block if any, for checking reuse of `tacSnap?`.  -/
Lean.Elab.HeaderProcessedSnapshot.tacStx? : Lean.Elab.HeaderProcessedSnapshot → Option Lean.Syntax
-- Init.Data.List.Lemmas
List.getLast?_flatten : ∀ {α : Type u_1} {L : List (List α)}, L.flatten.getLast? = List.findSome? (fun l => l.getLast?) L.reverse
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.evenToNeg_comp_evenToNeg : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q Q' : QuadraticForm R M) (h : Q' = -Q) (h' : Q = -Q'),
  (CliffordAlgebra.evenToNeg Q' Q h').comp (CliffordAlgebra.evenToNeg Q Q' h) = AlgHom.id R ↥(CliffordAlgebra.even Q)
-- Lean.Data.Json.FromToJson.Basic
Lean.Array.toJson : {α : Type u_1} → [Lean.ToJson α] → Array α → Lean.Json
-- Mathlib.Order.CompactlyGenerated.Basic
IsCompactlyGenerated.mk : ∀ {α : Type u_3} [inst : CompleteLattice α],
  (∀ (x : α), ∃ s, (∀ x ∈ s, IsCompactElement x) ∧ sSup s = x) → IsCompactlyGenerated α
-- Batteries.Data.List.Lemmas
List.isPrefixOf?.eq_3 : ∀ {α : Type u} [inst : BEq α] (a : α) (as : List α) (b : α) (bs : List α),
  (a :: as).isPrefixOf? (b :: bs) = if (a == b) = true then as.isPrefixOf? bs else none
-- Mathlib.RingTheory.HopfAlgebra.Convolution
HopfAlgebra.antipode_comp_mul_comp_comm : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A],
  HopfAlgebraStruct.antipode R ∘ₗ LinearMap.mul' R A ∘ₗ ↑(TensorProduct.comm R A A) =
    LinearMap.mul' R A ∘ₗ TensorProduct.map (HopfAlgebraStruct.antipode R) (HopfAlgebraStruct.antipode R)
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
SubMulAction.ofStabilizer.isPretransitive_iff_of_conj : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {a b : α} {g : G},
  b = g • a →
    (MulAction.IsPretransitive ↥(MulAction.stabilizer G a) ↥(SubMulAction.ofStabilizer G a) ↔
      MulAction.IsPretransitive ↥(MulAction.stabilizer G b) ↥(SubMulAction.ofStabilizer G b))
-- Mathlib.NumberTheory.LSeries.PrimesInAP
_private.Mathlib.NumberTheory.LSeries.PrimesInAP.0.ArithmeticFunction.vonMangoldt.F₀.eq_1 : ∀ (n : ℕ), ArithmeticFunction.vonMangoldt.F₀✝ n = (if Nat.Prime n then 0 else ArithmeticFunction.vonMangoldt n) / ↑n
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_inter_eq_size_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (∀ a ∈ t₂, a ∈ t₁) → (t₁ ∩ t₂).size = t₂.size
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_mabs : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] (a : M),
  MulArchimedeanClass.mk |a|ₘ = MulArchimedeanClass.mk a
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.IsSFiniteKernel.mk : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β},
  (∃ κs, (∀ (n : ℕ), ProbabilityTheory.IsFiniteKernel (κs n)) ∧ κ = ProbabilityTheory.Kernel.sum κs) →
    ProbabilityTheory.IsSFiniteKernel κ
-- Mathlib.Order.Filter.Pi
Filter.mem_of_pi_mem_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {s : (i : ι) → Set (α i)} [∀ (i : ι), (f i).NeBot]
  {I : Set ι}, I.pi s ∈ Filter.pi f → ∀ {i : ι}, i ∈ I → s i ∈ f i
-- Lean.Meta.Sym.Arith.Poly
_private.Lean.Meta.Sym.Arith.Poly.0.Lean.Grind.CommRing.Mon.sharesVar.match_3.eq_2 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (x : Lean.Grind.CommRing.Mon)
  (h_1 : (x : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit x)
  (h_2 : (x : Lean.Grind.CommRing.Mon) → motive x Lean.Grind.CommRing.Mon.unit)
  (h_3 :
    (pw₁ : Lean.Grind.CommRing.Power) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (pw₂ : Lean.Grind.CommRing.Power) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)),
  (x = Lean.Grind.CommRing.Mon.unit → False) →
    (match x, Lean.Grind.CommRing.Mon.unit with
      | Lean.Grind.CommRing.Mon.unit, x => h_1 x
      | x, Lean.Grind.CommRing.Mon.unit => h_2 x
      | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => h_3 pw₁ m₁ pw₂ m₂) =
      h_2 x
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsUnramified.stabilizer_eq_bot : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K}, NumberField.InfinitePlace.IsUnramified k w → MulAction.stabilizer Gal(K/k) w = ⊥
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.varsToConstants.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u'} {γ : Type u_1} (l : ℕ) (f : L.Functions l) (ts : Fin l → L.Term (γ ⊕ α)),
  (FirstOrder.Language.func f ts).varsToConstants = FirstOrder.Language.func (Sum.inl f) fun i => (ts i).varsToConstants
-- Init.Data.Int.Pow
Int.pow_one : ∀ (a : ℤ), a ^ 1 = a
-- Mathlib.Order.Interval.Set.SurjOn
surjOn_Ioc_of_monotone_surjective : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PartialOrder β] {f : α → β},
  Monotone f → Function.Surjective f → ∀ (a b : α), Set.SurjOn f (Set.Ioc a b) (Set.Ioc (f a) (f b))
-- Mathlib.Order.Interval.Set.Image
StrictAntiOn.image_Ioc_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : PartialOrder α] [inst_1 : Preorder β] {a b : α},
  StrictAntiOn f (Set.Icc a b) → f '' Set.Ioc a b ⊆ Set.Ico (f b) (f a)
-- Lean.Data.PersistentArray
Lean.PersistentArrayNode.leaf : {α : Type u} → Array α → Lean.PersistentArrayNode α
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.ofLinearExpr : Int.Internal.Linear.Expr → Lean.Expr
-- Init.Data.Int.Lemmas
Int.instAssociativeHMul : Std.Associative fun x1 x2 => x1 * x2
-- Mathlib.Topology.Constructions
continuous_quotient_mk' : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Setoid X}, Continuous Quotient.mk'
-- Lean.Expr
Lean.ExprStructEq.beq : Lean.ExprStructEq → Lean.ExprStructEq → Bool
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int32.reduceMod : Lean.Meta.Simp.DSimproc
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- The product of two non-zero modular forms is non-zero.  -/
ModularForm.mul_ne_zero : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne],
  (∃ h ∈ Γ.strictPeriods, 0 < h) → ∀ {a b : ℤ} {f : ModularForm Γ a} {g : ModularForm Γ b}, f ≠ 0 → g ≠ 0 → f.mul g ≠ 0
-- Mathlib.Logic.Equiv.Set
Equiv.ofInjective_symm_apply : ∀ {α : Sort u_3} {β : Type u_4} {f : α → β} (hf : Function.Injective f) (a : α),
  (Equiv.ofInjective f hf).symm ⟨f a, ⋯⟩ = a
-- Init.Data.SInt.Lemmas
ISize.not_le : ∀ {n m : ISize}, ¬n ≤ m ↔ m < n
-- Mathlib.SetTheory.Ordinal.Notation
ONote.fundamentalSequence.eq_1 : ONote.zero.fundamentalSequence = Sum.inl none
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_insertManyIfNewUnit_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α Unit} {ρ : Type w} [inst : ForIn Id ρ α] [EquivBEq α]
  [LawfulHashable α] {l : ρ} {k : α}, k ∈ m → k ∈ m.insertManyIfNewUnit l
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toList_rcc : ∀ {m n i : ℕ}, (m...=n).toList[i]? = if i < n + 1 - m then some (m + i) else none
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
/-- The compatibility of `HomotopyCategory.BinaryProduct.inverse`
with respect to the first projection.  -/
SSet.Truncated.HomotopyCategory.BinaryProduct.inverseCompMapHomotopyCategoryFstIso : (X Y : SSet.Truncated 2) →
  (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).comp
      (SSet.Truncated.mapHomotopyCategory (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)) ≅
    CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory
-- Mathlib.LinearAlgebra.Matrix.Echelon.Basic
Matrix.IsReducedRowEchelon.eq_one : ∀ {m : Type u_1} {n : Type u_2} {R : Type v} [inst : Zero R] [inst_1 : LT m] [inst_2 : LT n] [inst_3 : One R]
  {A : Matrix m n R}, A.IsReducedRowEchelon → ∀ ⦃i : m⦄ ⦃c : n⦄, A.IsLeadingEntry i c → A i c = 1
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.prod'_ε_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] {E : Type u₃}
  [inst_4 : CategoryTheory.Category.{v₃, u₃} E] [inst_5 : CategoryTheory.MonoidalCategory E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C E) [inst_6 : F.LaxMonoidal] [inst_7 : G.LaxMonoidal],
  (CategoryTheory.Functor.LaxMonoidal.ε (F.prod' G)).2 = CategoryTheory.Functor.LaxMonoidal.ε G
-- Mathlib.Order.SupIndep
Finset.SupIndep.insert : ∀ {α : Type u_1} {ι : Type u_3} [inst : Lattice α] [IsModularLattice α] [inst_2 : OrderBot α] [inst_3 : DecidableEq ι]
  {i : ι} {s : Finset ι} {f : ι → α}, s.SupIndep f → Disjoint (f i) (s.sup f) → (insert i s).SupIndep f
-- Init.Data.Nat.Basic
Nat.le_add_left : ∀ (n m : ℕ), n ≤ m + n