mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.foldM_eq_foldlM_keysArray : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {δ : Type w}
  {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m'] {f : δ → α → m' δ} {init : δ},
  Std.DHashMap.foldM (fun d a x => f d a) init m = Array.foldlM f init m.keysArray
-- Init.Sym.Simp.SimprocDSL
/-- Simplify control-flow expressions (`if-then-else`, `match`, `cond`, `dite`).
Visits only conditions and discriminants. Intended as a `pre` simproc.  -/
Lean.Parser.Sym.Simp.control : Lean.ParserDescr
-- Mathlib.Topology.ContinuousMap.Ideals
WeakDual.CharacterSpace.continuousMapEval_bijective : ∀ (X : Type u_1) (𝕜 : Type u_2) [inst : TopologicalSpace X] [CompactSpace X] [T2Space X] [inst_3 : RCLike 𝕜],
  Function.Bijective ⇑(WeakDual.CharacterSpace.continuousMapEval X 𝕜)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.nonempty_interior : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H),
  (interior (Set.range ↑I)).Nonempty
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.insert_Ico_left_eq_Ico_sub_one : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Sub α]
  [PredSubOrder α] {a b : α} [NoMinOrder α], a ≤ b → insert (a - 1) (Finset.Ico a b) = Finset.Ico (a - 1) b
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succMany.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] (n : ℕ) (a : α),
  Std.PRange.succMany n a = (Std.PRange.succMany? n a).get ⋯
-- Mathlib.MeasureTheory.Measure.Dirac
/-- If `f` is a map with countable codomain, then `μ.map f` is a sum of Dirac measures.  -/
MeasureTheory.Measure.map_eq_sum : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] [Countable β]
  [MeasurableSingletonClass β] (μ : MeasureTheory.Measure α) (f : α → β),
  Measurable f →
    MeasureTheory.Measure.map f μ = MeasureTheory.Measure.sum fun b => μ (f ⁻¹' {b}) • MeasureTheory.Measure.dirac b
-- Mathlib.Data.Nat.PSub
Nat.ppred_eq_none : ∀ {n : ℕ}, n.ppred = none ↔ n = 0
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instDivInvMonoid : {α : Type u_1} → [DivInvMonoid α] → DivInvMonoid αᵐᵒᵖ
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.toLogFun_nil : ∀ (basis : Tactic.ComputeAsymptotics.Basis), Tactic.ComputeAsymptotics.UnitMonomial.toLogFun [] basis = 0
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.isImage_preimage_prod : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) (s : Set B), e.IsImage (proj ⁻¹' s) (s ×ˢ Set.univ)
-- Mathlib.Order.Preorder.Finite
/-- A version of `Finite.exists_maximalFor` with the (weaker) hypothesis that the image of `s`
is finite rather than `s` itself.  -/
Set.Finite.exists_maximalFor' : ∀ {ι : Type u_1} {α : Type u_2} [inst : LE α] [IsTrans α LE.le] (f : ι → α) (s : Set ι),
  (f '' s).Finite → s.Nonempty → ∃ i, MaximalFor (fun x => x ∈ s) f i
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.loopyOn_closure_eq : ∀ {α : Type u_2} (E X : Set α), (Matroid.loopyOn E).closure X = E
-- Mathlib.LinearAlgebra.BilinearMap
/-- Composing a linear map `P → Q` and a bilinear map `M → N → P` to
form a bilinear map `M → N → Q`.

See `LinearMap.compr₂ₛₗ` for a version of this which does not support towers of scalars but which
does support semi-linear maps.  -/
LinearMap.compr₂ : {A : Type u_1} →
  {R : Type u_2} →
    [inst : Semiring A] →
      [inst_1 : CommSemiring R] →
        {M : Type u_5} →
          {Nₗ : Type u_8} →
            {Pₗ : Type u_9} →
              {Qₗ : Type u_10} →
                [inst_2 : AddCommMonoid M] →
                  [inst_3 : AddCommMonoid Nₗ] →
                    [inst_4 : AddCommMonoid Pₗ] →
                      [inst_5 : AddCommMonoid Qₗ] →
                        [inst_6 : Module R Nₗ] →
                          [inst_7 : Module R Pₗ] →
                            [inst_8 : Module R Qₗ] →
                              [inst_9 : Module A Pₗ] →
                                [inst_10 : SMulCommClass R A Pₗ] →
                                  [inst_11 : Module R A] →
                                    [inst_12 : Module A M] →
                                      [inst_13 : Module A Qₗ] →
                                        [inst_14 : SMulCommClass R A Qₗ] →
                                          [IsScalarTower R A Qₗ] →
                                            [IsScalarTower R A Pₗ] →
                                              (M →ₗ[A] Nₗ →ₗ[R] Pₗ) → (Pₗ →ₗ[A] Qₗ) → M →ₗ[A] Nₗ →ₗ[R] Qₗ
-- Mathlib.Data.Sign.Defs
SignType.LE.zero : SignType.zero.LE SignType.zero
-- Mathlib.Data.Int.Cast.Basic
Int.cast_negSucc : ∀ {R : Type u} [inst : AddGroupWithOne R] (n : ℕ), ↑(Int.negSucc n) = -↑(n + 1)
-- Mathlib.LinearAlgebra.CrossProduct
/-- The cross product satisfies the Leibniz lie property.  -/
leibniz_cross : ∀ {R : Type u_1} [inst : CommRing R] (u v w : Fin 3 → R),
  (crossProduct u) ((crossProduct v) w) = (crossProduct ((crossProduct u) v)) w + (crossProduct v) ((crossProduct u) w)
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.eq_self_or_eq_top_of_le : ∀ {K : Type u} [inst : Field K] {A : ValuationSubring K} [Ring.KrullDimLE 1 ↥A] {B : ValuationSubring K},
  A ≤ B → A = B ∨ B = ⊤
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasProd.mul_disjoint : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a b : α}
  [ContinuousMul α] {s t : Set β},
  Disjoint s t → HasProd (f ∘ Subtype.val) a → HasProd (f ∘ Subtype.val) b → HasProd (f ∘ Subtype.val) (a * b)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_neg : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (x : WithVal v), (-x).ofVal = -x.ofVal
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.measure_univ_ne_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ Set.univ ≠ 0 ↔ μ ≠ 0
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- A `NonUnitalSubring` `t` includes `closure s` if and only if it includes `s`.  -/
NonUnitalSubring.closure_le : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : Set R} {t : NonUnitalSubring R},
  NonUnitalSubring.closure s ≤ t ↔ s ⊆ ↑t
-- Mathlib.Topology.Algebra.Group.ClosedSubgroup
ClosedSubgroup.mk : {G : Type u} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] → (toSubgroup : Subgroup G) → IsClosed toSubgroup.carrier → ClosedSubgroup G
-- Mathlib.Topology.Constructions
isClosedMap_ofMul : ∀ {X : Type u} [inst : TopologicalSpace X], IsClosedMap ⇑Additive.ofMul
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_shiftLeft : ∀ (a b : USize) (h : System.Platform.numBits = 64), (a <<< b).toBitVec64 h = a.toBitVec64 h <<< (b.toBitVec64 h % 64)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.exradius_map : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [inst_4 : NormedAddCommGroup V₂]
  [inst_5 : InnerProductSpace ℝ V₂] [inst_6 : MetricSpace P₂] [inst_7 : NormedAddTorsor V₂ P₂] {n : ℕ}
  [inst_8 : NeZero n] (s : Affine.Simplex ℝ P n) (f : P →ᵃⁱ[ℝ] P₂), (s.map f.toAffineMap ⋯).exradius = s.exradius
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.neg.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr),
  (Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.neg c = Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.neg c_1) =
    (c = c_1)
-- Lean.Meta.Tactic.Grind.Arith.Util
_private.Lean.Meta.Tactic.Grind.Arith.Util.0.Lean.Meta.Grind.Arith.CollectDecVars.alreadyVisited.unsafe_impl_2 : {α : Type u_1} → α → UInt64
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.postcomposeWhiskerLeftMapCone_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C}
  {H H' : CategoryTheory.Functor C D} (α : H ≅ H') (c : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Functor.postcomposeWhiskerLeftMapCone α c).hom.hom = α.hom.app c.pt
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.getThenInsertIfNew?.match_1.splitter : {α : Type u_3} →
  {β : α → Type u_1} →
    (k : α) →
      (motive : Option (β k) → Sort u_2) →
        (x : Option (β k)) → (Unit → motive none) → ((b : β k) → motive (some b)) → motive x
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.instCoeSortType : (R : Type u) → [inst : CommSemiring R] → CoeSort (CommRing.Pic R) (Type u)
-- Aesop.RuleTac.Forward
Aesop.RuleTac.forward : Aesop.RuleTerm → Aesop.UnorderedArraySet Aesop.PremiseIndex → Bool → Aesop.RuleTac
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.one_add_omega0 : 1 + Ordinal.omega0 = Ordinal.omega0
-- Mathlib.Data.Finset.SMulAntidiagonal
Set.IsPWO.smul : ∀ {G : Type u_1} {P : Type u_2} [inst : Preorder G] [inst_1 : Preorder P] [inst_2 : SMul G P] [IsOrderedSMul G P]
  {s : Set G} {t : Set P}, s.IsPWO → t.IsPWO → (s • t).IsPWO
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
/-- a section of the augmentation in dimension `0`  -/
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject.Augmented C} →
      X.ExtraDegeneracy → (X.right ⟶ X.left.obj (Opposite.op { len := 0 }))
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend_op_d : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c') (i' j' : ι'),
  (K.op.extend e.op).d i' j' =
    CategoryTheory.CategoryStruct.comp ((K.extendOpIso e).hom.f i')
      (CategoryTheory.CategoryStruct.comp ((K.extend e).d j' i').op ((K.extendOpIso e).inv.f j'))
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.aleph_mul_aleph : ∀ (o₁ o₂ : Ordinal.{u_1}), Cardinal.aleph o₁ * Cardinal.aleph o₂ = Cardinal.aleph (max o₁ o₂)
-- Init.Data.List.Perm
List.Perm.eraseP : ∀ {α : Type u_1} (f : α → Bool) {l₁ l₂ : List α},
  List.Pairwise (fun a b => f a = true → f b = true → False) l₁ →
    l₁.Perm l₂ → (List.eraseP f l₁).Perm (List.eraseP f l₂)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_norm_eq_idemFst_of_L1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β]
  (x : WithLp 1 (α × β)), ‖x‖ = ‖WithLp.idemFst x‖ + ‖WithLp.idemSnd x‖
-- Mathlib.Algebra.WithConv
WithConv.toConv_listSum : ∀ {A : Type u_2} [inst : AddCommMonoid A] (l : List A), WithConv.toConv l.sum = (List.map WithConv.toConv l).sum
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.toFilterDistortioniUnion.eq_1 : ∀ {ι : Type u_1} [inst : Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι) (c : NNReal)
  (π₀ : BoxIntegral.Prepartition I),
  l.toFilterDistortioniUnion I c π₀ = l.toFilterDistortion I c ⊓ Filter.principal {π | π.iUnion = π₀.iUnion}
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
_private.Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1.0.MeasureTheory.q : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [MeasureTheory.SigmaFinite (μ.trim hm)] {hs : MeasurableSet s}
  {hμs : μ s ≠ ⊤} {x : G}, MeasureTheory.MemLp (↑↑(MeasureTheory.condExpIndSMul hm hs hμs x)) 1 μ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (not_mem : k ∉ t₂) {h' : k ∈ t₁ ∪ t₂}, (t₁ ∪ t₂).getKey k h' = t₁.getKey k ⋯
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_ofList_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)},
  (Std.ExtTreeMap.ofList l cmp).size ≤ l.length
-- Mathlib.Tactic.Linarith.Frontend
/-- A map of keys to values, where the keys are `Expr` up to defeq and one key can be
associated to multiple values.  -/
Mathlib.Tactic.Linarith.ExprMultiMap : Type u_1 → Type u_1
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Convenience shortcut for `Rep.hom_bijective.injective`.  -/
Rep.hom_injective : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G},
  Function.Injective Rep.Hom.hom
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Nat.reduceXor : Lean.Meta.Simp.DSimproc
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a fallback : α}, m.contains a = false → m.getKeyD a fallback = fallback
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.instCoeENat : Coe ℕ∞ Cardinal.{u_1}
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
PositiveLinearMap.map_smul_of_tower : ∀ {R : Type u_1} {E₁ : Type u_2} {E₂ : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid E₁]
  [inst_2 : PartialOrder E₁] [inst_3 : AddCommMonoid E₂] [inst_4 : PartialOrder E₂] [inst_5 : Module R E₁]
  [inst_6 : Module R E₂] {S : Type u_5} [inst_7 : SMul S E₁] [inst_8 : SMul S E₂] [LinearMap.CompatibleSMul E₁ E₂ S R]
  (f : E₁ →ₚ[R] E₂) (c : S) (x : E₁), f (c • x) = c • f x
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.isLeast_leastExt : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E]
  (i : (Module.rank F E).ord.ToType),
  IsLeast
    {k |
      (Field.Emb.Cardinal.wellOrderedBasis F E) k ∉
        IntermediateField.adjoin F
          (⇑(Field.Emb.Cardinal.wellOrderedBasis F E) ∘ Field.Emb.Cardinal.leastExt F E '' Set.Iio i)}
    (Field.Emb.Cardinal.leastExt F E i)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  {k k' : α} {f : β → β},
  Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.Const.modify t k f) k' =
    if cmp k k' = Ordering.eq then Option.map f (Std.ExtDTreeMap.Const.get? t k) else Std.ExtDTreeMap.Const.get? t k'
-- Lean.Meta.Match.MatcherApp.Basic
Lean.Meta.MatcherApp : Type
-- Mathlib.NumberTheory.Padics.Measure.Basic
/-- Inherit `ContinuousLinearMapClass` structure from `C(X, R) →L[R] E`.  -/
AbstractMeasure.instContinuousLinearMapClassContinuousMap : ∀ {X : Type u_1} {R : Type u_3} {E : Type u_4} [inst : TopologicalSpace X] [inst_1 : AddCommGroup E]
  [inst_2 : TopologicalSpace E] [inst_3 : CommRing R] [inst_4 : TopologicalSpace R] [inst_5 : IsTopologicalRing R]
  [inst_6 : Module R E], ContinuousLinearMapClass (AbstractMeasure X R E) R C(X, R) E
-- Init.Data.Range.Polymorphic.Stream
Std.PRange.instToStreamRooIterIteratorOfUpwardEnumerable : {α : Type u_1} → [Std.PRange.UpwardEnumerable α] → Std.ToStream (Std.Roo α) (Std.Iter α)
-- Init.Data.SInt.Lemmas
Int32.maxValue_le_iff : ∀ {a : Int32}, Int32.maxValue ≤ a ↔ a = Int32.maxValue
-- Lean.Class
Lean.ClassState.mk.sizeOf_spec : ∀ (outParamMap outLevelParamMap : Lean.SMap Lean.Name (Array ℕ)),
  sizeOf { outParamMap := outParamMap, outLevelParamMap := outLevelParamMap } =
    1 + sizeOf outParamMap + sizeOf outLevelParamMap
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- There is in fact equality: see `measurableAtom_eq_of_mem`.  -/
measurableAtom_subset_of_mem : ∀ {β : Type u_2} [inst : MeasurableSpace β] {x y : β}, x ∈ measurableAtom y → measurableAtom x ⊆ measurableAtom y
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
_private.Mathlib.RingTheory.Polynomial.Hermite.Basic.0.Polynomial.hermite.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.sign_two_zsmul_eq_sign_iff : ∀ {θ : Real.Angle}, (2 • θ).sign = θ.sign ↔ θ = ↑Real.pi ∨ |θ.toReal| < Real.pi / 2
-- Mathlib.Algebra.GroupWithZero.Defs
inv_zero : ∀ {G₀ : Type u} [inst : GroupWithZero G₀], 0⁻¹ = 0
-- Mathlib.Algebra.Group.Subgroup.Even
Subgroup.square.eq_1 : ∀ (G : Type u_1) [inst : CommGroup G], Subgroup.square G = { toSubmonoid := Submonoid.square G, inv_mem' := ⋯ }
-- Init.Data.String.Lemmas.Basic
String.getUTF8Byte_eq_getUTF8Byte_toSlice : ∀ {s : String} {p : String.Pos.Raw} {h : p < s.rawEndPos}, s.getUTF8Byte p h = s.toSlice.getUTF8Byte p ⋯
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- A permutation `g` commutes with a cycle `c` if and only if
`c.support` is invariant under `g`, and `g` acts on it as a power of `c`.  -/
Equiv.Perm.IsCycle.commute_iff : ∀ {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] {g c : Equiv.Perm α},
  c.IsCycle →
    (Commute g c ↔
      ∃ (hc' : ∀ (x : α), g x ∈ c.support ↔ x ∈ c.support),
        Equiv.Perm.ofSubtype (g.subtypePerm hc') ∈ Subgroup.zpowers c)
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
CategoryTheory.IsGrothendieckAbelian.instIsRightAdjointModuleCatMulOppositeEndPreadditiveCoyonedaObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] {G : C}, (CategoryTheory.preadditiveCoyonedaObj G).IsRightAdjoint
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_update_zero : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n : ℕ), (p.update n 0).support = p.support.erase n
-- Mathlib.Analysis.Normed.Group.SeparationQuotient
SeparationQuotient.liftNormedAddGroupHom_norm_le : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {N : Type u_3} [inst_1 : SeminormedAddCommGroup N]
  (f : NormedAddGroupHom M N) (hf : ∀ (s : M), ‖s‖ = 0 → f s = 0) {c : NNReal},
  ‖f‖ ≤ ↑c → ‖SeparationQuotient.liftNormedAddGroupHom f hf‖ ≤ ↑c
-- Init.Grind.PP
Lean.Grind.NodeDef.noConfusionType : Sort v✝ → NodeDef → NodeDef → Sort v✝
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
/-- Cochains of degree `n` from `(singleFunctor C q).obj X` to `K` identify
to `K.X p ⟶ X` when `p + n = q`.  -/
CochainComplex.HomComplex.Cochain.toSingleEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {X : C} →
          {K : CochainComplex C ℤ} →
            {p q n : ℤ} →
              p + n = q →
                CochainComplex.HomComplex.Cochain K ((CochainComplex.singleFunctor C q).obj X) n ≃+ (K.X p ⟶ X)
-- Lean.Meta.IntInstTesters
Lean.Meta.Structural.isInstDvdInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.mk : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] →
        (toFun : α → MeasureTheory.Measure β) → Measurable toFun → ProbabilityTheory.Kernel α β
-- Mathlib.Data.Finset.Sum
Finset.toLeft_union : ∀ {α : Type u_1} {β : Type u_2} {u v : Finset (α ⊕ β)} [inst : DecidableEq α] [inst_1 : DecidableEq β],
  (u ∪ v).toLeft = u.toLeft ∪ v.toLeft
-- Lean.Data.DeclarationRange
Lean.DeclarationRanges.mk.injEq : ∀ (range selectionRange range_1 selectionRange_1 : Lean.DeclarationRange),
  ({ range := range, selectionRange := selectionRange } = { range := range_1, selectionRange := selectionRange_1 }) =
    (range = range_1 ∧ selectionRange = selectionRange_1)
-- Mathlib.Combinatorics.Matroid.Circuit
/-- The fundamental cocircuit of `X` and `e` has the junk value `{e}` if `e ∉ X`  -/
Matroid.fundCocircuit_eq_of_notMem : ∀ {α : Type u_1} {X : Set α} {e : α} (M : Matroid α), e ∉ X → M.fundCocircuit e X = {e}
-- Mathlib.Topology.Compactness.CountablyCompact
CountablyCompactSpace.mk : ∀ {E : Type u_4} [inst : TopologicalSpace E], IsCountablyCompact Set.univ → CountablyCompactSpace E
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.iff_comp_injective_of_small : ∀ {R : Type v} [inst : CommRing R] {A : Type u} [inst_1 : CommRing A] [inst_2 : Algebra R A] [Small.{w, u} A],
  Algebra.FormallyUnramified R A ↔
    ∀ ⦃B : Type w⦄ [inst_4 : CommRing B] [inst_5 : Algebra R B] (I : Ideal B),
      I ^ 2 = ⊥ → Function.Injective (Ideal.Quotient.mkₐ R I).comp
-- Mathlib.AlgebraicGeometry.Morphisms.Constructors
AlgebraicGeometry.instIsZariskiLocalAtTargetDiagonalScheme : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsZariskiLocalAtTarget P],
  AlgebraicGeometry.IsZariskiLocalAtTarget P.diagonal
-- Mathlib.Data.Finset.Basic
Finset.filter_union_filter_not_eq : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] [inst_1 : DecidableEq α] [inst_2 : (x : α) → Decidable ¬p x]
  (s : Finset α), Finset.filter p s ∪ {a ∈ s | ¬p a} = s
-- Init.Data.String.Slice
String.Slice.RevSplitIterator.atEnd : {σ : String.Slice → Type} →
  {ρ : Type} →
    {pat : ρ} →
      {s : String.Slice} → [inst : String.Slice.Pattern.ToBackwardSearcher pat σ] → String.Slice.RevSplitIterator pat s
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_maxKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {fallback fallback' : α},
        Std.Internal.List.getKeyD (Std.Internal.List.maxKeyD l fallback) l fallback' =
          Std.Internal.List.maxKeyD l fallback
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.domLCongr_apply : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : ι → Type u_5} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] (e : ι ≃ ι') (a : Π₀ (i : ι), M i),
  (DFinsupp.domLCongr e) a = DFinsupp.comapDomain' ⇑e.symm ⋯ a
-- Init.Data.ToString.Basic
ToString.mk : {α : Type u} → (α → String) → ToString α
-- Mathlib.Analysis.InnerProductSpace.PiL2
PiLp.innerProductSpace : {𝕜 : Type u_3} →
  [inst : RCLike 𝕜] →
    {ι : Type u_7} →
      [inst_1 : Fintype ι] →
        (f : ι → Type u_8) →
          [inst_2 : (i : ι) → NormedAddCommGroup (f i)] →
            [(i : ι) → InnerProductSpace 𝕜 (f i)] → InnerProductSpace 𝕜 (PiLp 2 f)
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.MatcherInfo.mk.sizeOf_spec : ∀ (numParams numDiscrs : ℕ) (altInfos : Array Lean.Meta.Match.AltParamInfo) (uElimPos? : Option ℕ)
  (discrInfos : Array Lean.Meta.Match.DiscrInfo) (overlaps : Lean.Meta.Match.Overlaps),
  sizeOf
      { numParams := numParams, numDiscrs := numDiscrs, altInfos := altInfos, uElimPos? := uElimPos?,
        discrInfos := discrInfos, overlaps := overlaps } =
    1 + sizeOf numParams + sizeOf numDiscrs + sizeOf altInfos + sizeOf uElimPos? + sizeOf discrInfos + sizeOf overlaps
-- Mathlib.RingTheory.Nilpotent.Lemmas
nilradical_eq_zero : ∀ (R : Type u_3) [inst : CommSemiring R] [IsReduced R], nilradical R = 0
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_rev_Ioi : ∀ {n : ℕ} (i : Fin n), Finset.image Fin.rev (Finset.Ioi i) = Finset.Iio i.rev
-- Mathlib.Data.ZMod.QuotientGroup
/-- **Alias** of the reverse direction of `finite_zmultiples`. -/
IsOfFinAddOrder.finite_zmultiples : ∀ {α : Type u_3} [inst : AddGroup α] {a : α}, IsOfFinAddOrder a → (↑(AddSubgroup.zmultiples a)).Finite