mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : Preorder α} {inst_1 : Preorder β} {inst_2 : Mul α} {inst_3 : Mul β}
  {toMulEquiv : α ≃* β} {map_le_map_iff' : ∀ {a b : α}, toMulEquiv.toFun a ≤ toMulEquiv.toFun b ↔ a ≤ b}
  {toMulEquiv_1 : α ≃* β} {map_le_map_iff'_1 : ∀ {a b : α}, toMulEquiv_1.toFun a ≤ toMulEquiv_1.toFun b ↔ a ≤ b},
  { toMulEquiv := toMulEquiv, map_le_map_iff' := map_le_map_iff' } =
      { toMulEquiv := toMulEquiv_1, map_le_map_iff' := map_le_map_iff'_1 } →
    toMulEquiv = toMulEquiv_1
-- Mathlib.SetTheory.Ordinal.Notation
ONote.opowAux.eq_def : ∀ (e a0 a : ONote) (x x_1 : ℕ),
  e.opowAux a0 a x x_1 =
    match x, x_1 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m
-- Mathlib.Data.Set.Lattice
Set.subset_sInter_iff : ∀ {α : Type u_1} {S : Set (Set α)} {t : Set α}, t ⊆ ⋂₀ S ↔ ∀ t' ∈ S, t ⊆ t'
-- Init.Internal.Order.Basic
Lean.Order.instMonoBindOption : Lean.Order.MonoBind Option
-- Mathlib.Data.List.Permutation
List.length_permutations : ∀ {α : Type u_1} (l : List α), l.permutations.length = l.length.factorial
-- Mathlib.Data.Multiset.FinsetOps
Multiset.ndinsert_le : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s t : Multiset α}, Multiset.ndinsert a s ≤ t ↔ s ≤ t ∧ a ∈ t
-- Mathlib.GroupTheory.Sylow
/-- Surjective group homomorphisms map Sylow subgroups to Sylow subgroups.  -/
Sylow.mapSurjective : {p : ℕ} →
  {G : Type u_1} →
    [inst : Group G] →
      [Finite G] →
        {G' : Type u_2} →
          [inst_2 : Group G'] → {f : G →* G'} → Function.Surjective ⇑f → [Fact (Nat.Prime p)] → Sylow p G → Sylow p G'
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_pos_iff : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [ExistsAddOfLE R] [PosMulStrictMono R]
  [MulPosStrictMono R] [AddLeftStrictMono R] [AddLeftReflectLT R], 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0
-- Mathlib.Data.Num.Basic
instReprNum : Repr Num
-- Init.Data.Array.Lemmas
Array.toList_range' : ∀ {start size step : ℕ}, (Array.range' start size step).toList = List.range' start size step
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.IsStableUnderTransfiniteCompositionOfShape.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W W_1 : CategoryTheory.MorphismProperty C),
  W = W_1 →
    ∀ (J : Type w) [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J],
      W.IsStableUnderTransfiniteCompositionOfShape J = W_1.IsStableUnderTransfiniteCompositionOfShape J
-- Mathlib.GroupTheory.Perm.Subgroup
Equiv.Perm.sumCongrHom.decidableMemRange : {α : Type u_1} →
  {β : Type u_2} →
    [DecidableEq α] →
      [DecidableEq β] → [Fintype α] → [Fintype β] → DecidablePred fun x => x ∈ (Equiv.Perm.sumCongrHom α β).range
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVUnOp.eval_reverse : ∀ {w : ℕ}, Std.Tactic.BVDecide.BVUnOp.reverse.eval = BitVec.reverse
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_mod : ∀ (a b : UInt32), a < 256 → b < 256 → (a % b).toUInt8 = a.toUInt8 % b.toUInt8
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.mapDomain_comp : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {G' : Type u_3} {G'' : Type u_4} {f : G → G'} {g : G' → G''}
  {v : SkewMonoidAlgebra k G},
  (SkewMonoidAlgebra.mapDomain (g ∘ f)) v = (SkewMonoidAlgebra.mapDomain g) ((SkewMonoidAlgebra.mapDomain f) v)
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
aestronglyMeasurable_derivWithin_Ici : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : ℝ → F) [CompleteSpace F]
  (μ : MeasureTheory.Measure ℝ), MeasureTheory.AEStronglyMeasurable (fun x => derivWithin f (Set.Ici x) x) μ
-- Mathlib.Algebra.Category.Semigrp.Basic
MulEquiv.toMagmaCatIso.eq_1 : ∀ {X Y : Type u} [inst : Mul X] [inst_1 : Mul Y] (e : X ≃* Y),
  e.toMagmaCatIso =
    { hom := MagmaCat.ofHom e.toMulHom, inv := MagmaCat.ofHom e.symm.toMulHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Lean.Widget.UserWidget
Lean.Widget.GetWidgetSourceParams.mk.sizeOf_spec : ∀ (hash : UInt64) (pos : Lean.Lsp.Position), sizeOf { hash := hash, pos := pos } = 1 + sizeOf hash + sizeOf pos
-- Mathlib.NumberTheory.SmoothNumbers
/-- `m` is `s`-factored if and only if `m ≠ 0` and its `Finset` of prime factors
is contained in `s`.  -/
Nat.mem_factoredNumbers_iff_primeFactors_subset : ∀ {s : Finset ℕ} {m : ℕ}, m ∈ Nat.factoredNumbers s ↔ m ≠ 0 ∧ m.primeFactors ⊆ s
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint : ∀ {X : AlgebraicGeometry.Scheme} {x : ↥X}, (X.fromSpecStalk x) (IsLocalRing.closedPoint ↑(X.presheaf.stalk x)) = x
-- Std.Time.Zoned.ZoneRules
/-- Finds the `LocalTimeType` for a given wall-clock time (seconds since 1970-01-01T00:00:00 in local time).
Unlike `findLocalTimeTypeForTimestamp`, this compares each transition's UTC time adjusted by the
previous offset — necessary when converting local time to UTC.

When the wall time falls beyond all stored transitions and a `transitionRule` is present, the
recurring rule is used to determine the timezone (converting the wall time to UTC via the last
known offset before consulting the rule).
 -/
Std.Time.TimeZone.ZoneRules.findLocalTimeTypeForWallTime : Std.Time.TimeZone.ZoneRules → Std.Time.WallTime → Std.Time.TimeZone.LocalTimeType
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.poissonPMFReal_pos : ∀ {r : NNReal} {n : ℕ}, 0 < r → 0 < ProbabilityTheory.poissonPMFReal r n
-- Batteries.Data.BinomialHeap.Basic
/-- `O(log n)`. Remove the minimum element of the heap.  -/
Batteries.BinomialHeap.Imp.Heap.tail : {α : Type u_1} → (α → α → Bool) → Batteries.BinomialHeap.Imp.Heap α → Batteries.BinomialHeap.Imp.Heap α
-- Lean.Meta.Tactic.ElimInfo
/-- Given the type `t` of an alternative, determines the number of parameters
(.forall and .let)-bound, and whether the conclusion is a `motive`-application.   -/
Lean.Meta.altArity : Lean.Expr → ℕ → Lean.Expr → ℕ × Bool
-- Init.Data.UInt.Bitwise
UInt64.toNat_or : ∀ (a b : UInt64), (a ||| b).toNat = a.toNat ||| b.toNat
-- Aesop.Forward.State
/-- Erase a pattern substitution that was obtained from the given source.  -/
Aesop.RuleState.erasePatSubst : Aesop.Substitution → Aesop.PatSubstSource → Aesop.RuleState → Aesop.RuleState
-- Mathlib.Topology.Instances.Complex
Subfield.topologicalClosure.congr_simp : ∀ {α : Type u_2} [inst : Field α] [inst_1 : TopologicalSpace α] [inst_2 : IsTopologicalDivisionRing α]
  (K K_1 : Subfield α), K = K_1 → K.topologicalClosure = K_1.topologicalClosure
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.neg_snd : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : AddCommGroup β] (x : WithLp p (α × β)),
  (-x).snd = -x.snd
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.real_toNNReal : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun x => (f x).toNNReal) μ
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight_eq_mulHeight_restrict_support : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [Finite ι] (x : ι → K),
  Height.mulHeight x = Height.mulHeight fun i => x ↑i
-- Mathlib.Data.Nat.Factorial.Basic
Nat.factorial_two : Nat.factorial 2 = 2
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.drop_coe : ∀ {A : Type u_1} (T : ↥(Descriptive.tree A)) (n : ℕ) (x : ↥T), ↑(Descriptive.Tree.drop T n x) = List.drop n ↑x
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback fallback' : α}, t.getD (t.minD fallback) fallback' = t.minD fallback
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitClosedBall.coe_mul : ∀ {𝕜 : Type u_1} [inst : NonUnitalSeminormedRing 𝕜] (x y : ↑(Metric.closedBall 0 1)), ↑(x * y) = ↑x * ↑y
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
/-- The partial derivative `W_Z(X, Y, Z)` with respect to `Z` of the polynomial `W(X, Y, Z)`
associated to a Weierstrass curve `W` in Jacobian coordinates.  -/
WeierstrassCurve.Jacobian.polynomialZ : {R : Type r} → [inst : CommRing R] → WeierstrassCurve.Jacobian R → MvPolynomial (Fin 3) R
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
/-- The map $n \mapsto \prod_{p \mid n} f(p)$ as an arithmetic function  -/
ArithmeticFunction.prodPrimeFactors : {R : Type u_1} → [inst : CommMonoidWithZero R] → (ℕ → R) → ArithmeticFunction R
-- Mathlib.Analysis.Normed.Group.Basic
add_mem_closedBall_add_iff : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {a b : E} {r : ℝ} {c : E},
  a + c ∈ Metric.closedBall (b + c) r ↔ a ∈ Metric.closedBall b r
-- Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage
/-- The `circleAverage (log ‖· - a‖) 0 1` equals `log⁺ ‖a‖`.
 -/
circleAverage_log_norm_sub_const_eq_posLog : ∀ {a : ℂ}, Real.circleAverage (fun x => Real.log ‖x - a‖) 0 1 = ‖a‖.posLog
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.UnitaryGroup.transpose_inv_eq_map_star : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {α : Type v} [inst_2 : CommRing α] [inst_3 : StarRing α]
  (U : ↥(Matrix.unitaryGroup n α)), (Matrix.UnitaryGroup.transpose U)⁻¹ = Matrix.UnitaryGroup.map_star U
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.add_left_cancel : ∀ {α : Type u} [inst : Add α] {x y z : WithTop α} [IsLeftCancelAdd α], x ≠ ⊤ → x + y = x + z → y = z
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.star_eq : ∀ {R : Type u_1} [inst : Star R] {x : R}, IsSelfAdjoint x → star x = x
-- Mathlib.AlgebraicGeometry.Limits
/-- The cover of `∐ X` by the `Xᵢ`.  -/
AlgebraicGeometry.sigmaOpenCover : {σ : Type v} → (g : σ → AlgebraicGeometry.Scheme) → [inst : Small.{u, v} σ] → (∐ g).OpenCover
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : LawfulBEq α]
  {f : α → β → γ} {k : α} {h' : k ∈ Std.ExtHashMap.map f m}, (Std.ExtHashMap.map f m)[k] = f k m[k]
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularWRT.comap : ∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure β}
  {pa qa : Set α → Prop} {pb qb : Set β → Prop},
  μ.InnerRegularWRT pb qb →
    ∀ {f : α → β},
      MeasurableEmbedding f →
        (∀ (U : Set α), qa U → qb (f '' U)) →
          (∀ K ⊆ Set.range f, pb K → pa (f ⁻¹' K)) → (MeasureTheory.Measure.comap f μ).InnerRegularWRT pa qa
-- Lean.Server.References
/-- URI of the module of this ILean.  -/
Lean.Server.LoadedILean.moduleUri : Lean.Server.LoadedILean → Lean.Lsp.DocumentUri
-- Mathlib.Analysis.Normed.Group.Continuity
Continuous.nnnorm' : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedGroup E] [inst_1 : TopologicalSpace α] {f : α → E},
  Continuous f → Continuous fun x => ‖f x‖₊
-- Mathlib.Data.Stream.Init
Stream'.inits_eq : ∀ {α : Type u} (s : Stream' α), s.inits = Stream'.cons [s.head] (Stream'.map (List.cons s.head) s.tail.inits)
-- Mathlib.Algebra.Order.Floor.Extended
ENat.le_ceil_self : ∀ {r : ENNReal}, r ≤ ↑⌈r⌉ₑ
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.mk_le_mk : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {S S' : NonUnitalSubsemiring R}
  (h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier) (h' : ∀ {x : R}, x ∈ S'.carrier → -x ∈ S'.carrier),
  { toNonUnitalSubsemiring := S, neg_mem' := h } ≤ { toNonUnitalSubsemiring := S', neg_mem' := h' } ↔ S ≤ S'
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.expand_mul : ∀ {R : Type u} [inst : CommSemiring R] (p q : ℕ) (f : Polynomial R),
  (Polynomial.expand R (p * q)) f = (Polynomial.expand R p) ((Polynomial.expand R q) f)
-- Mathlib.Algebra.Ring.BooleanRing
/-- Type synonym to view a Boolean ring as a Boolean algebra.  -/
AsBoolRing : Type u_4 → Type u_4
-- Mathlib.Topology.Sequences
subset_seqClosure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, s ⊆ seqClosure s
-- Init.Data.Nat.Bitwise.Lemmas
Nat.instAssociativeHAnd : Std.Associative fun x1 x2 => x1 &&& x2
-- Mathlib.CategoryTheory.Shift.ShiftedHomOpposite
/-- The bijection `ShiftedHom X Y a' ≃ (Opposite.op (Y⟦a⟧) ⟶ (Opposite.op X)⟦n⟧)`
when integers `n`, `a` and `a'` satisfy `n + a = a'`, and `X` and `Y` are objects
of a category equipped with a shift by `ℤ`.  -/
CategoryTheory.ShiftedHom.opEquiv' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {X Y : C} →
        (n a a' : ℤ) →
          n + a = a' →
            CategoryTheory.ShiftedHom X Y a' ≃
              (Opposite.op ((CategoryTheory.shiftFunctor C a).obj Y) ⟶
                (CategoryTheory.shiftFunctor Cᵒᵖ n).obj (Opposite.op X))
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.lpMeasSubgroupToLpTrim_neg : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f : ↥(MeasureTheory.lpMeasSubgroup F m p μ)),
  MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm (-f) = -MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm f
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.get?.match_1.congr : ∀ {α : Sort u} {o o' : Ordering} {lt : o = Ordering.lt → α} {eq : o = Ordering.eq → α} {gt : o = Ordering.gt → α}
  {lt' : o' = Ordering.lt → α} {eq' : o' = Ordering.eq → α} {gt' : o' = Ordering.gt → α} (ho : o = o'),
  (∀ (h : o' = Ordering.lt), lt ⋯ = lt' h) →
    (∀ (h : o' = Ordering.eq), eq ⋯ = eq' h) →
      (∀ (h : o' = Ordering.gt), gt ⋯ = gt' h) →
        (match h : o with
          | Ordering.lt => lt h
          | Ordering.gt => gt h
          | Ordering.eq => eq h) =
          match h : o' with
          | Ordering.lt => lt' h
          | Ordering.gt => gt' h
          | Ordering.eq => eq' h
-- Mathlib.RingTheory.KrullDimension.Basic
/-- **Alias** of `ringKrullDim_eq_of_ringEquiv`.

---

If `R` and `S` are isomorphic, then `ringKrullDim R = ringKrullDim S`.  -/
RingEquiv.ringKrullDim : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (e : R ≃+* S),
  ringKrullDim R = ringKrullDim S
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mul_div_le : ∀ (a b : Ordinal.{u_4}), b * (a / b) ≤ a
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.fromSingleMk.congr_simp : ∀ {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 : ℤ} (f f_1 : X ⟶ K.X q),
  f = f_1 →
    ∀ {n : ℤ} (x : p + n = q) (T : CochainComplex.HomComplex.Triplet n),
      CochainComplex.HomComplex.Cochain.fromSingleMk f x T = CochainComplex.HomComplex.Cochain.fromSingleMk f_1 x T
-- Lean.ResolveName
/-- Primitive global name resolution procedure. It does not trigger actions associated with reserved names.
Recall that Lean has reserved names. For example, a definition `foo` has a reserved name `foo.def` for theorem
containing stating that `foo` is equal to its definition. The action associated with `foo.def`
automatically proves the theorem. At the macro level, the name is resolved, but the action is not
executed.
 -/
Lean.ResolveName.resolveGlobalName : Lean.Environment → Lean.Options → Lean.Name → List Lean.OpenDecl → Lean.Name → List (Lean.Name × List String)
-- Mathlib.Algebra.Ring.Opposite
NonUnitalRingHom.op_apply_apply : ∀ {R : Type u_2} {S : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (f : R →ₙ+* S) (a : Rᵐᵒᵖ), (NonUnitalRingHom.op f) a = (↑(AddMonoidHom.mulOp f.toAddMonoidHom)).toFun a
-- Mathlib.Algebra.Group.Commute.Basic
Commute.function_commute_mul_right : ∀ {G : Type u_1} [inst : Semigroup G] {a b : G}, Commute a b → Function.Commute (fun x => x * a) fun x => x * b
-- Batteries.Lean.EStateM
_private.Batteries.Lean.EStateM.0.EStateM.bind.match_1.splitter : {ε σ α : Type u_1} →
  (motive : EStateM.Result ε σ α → Sort u_2) →
    (x : EStateM.Result ε σ α) →
      ((a : α) → (s : σ) → motive (EStateM.Result.ok a s)) →
        ((e : ε) → (s : σ) → motive (EStateM.Result.error e s)) → motive x
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.drop : ∀ {s : Substring.Raw}, s.Valid → ∀ (n : ℕ), (s.drop n).Valid
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.coe_const : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] (y : Y), ⇑(LocallyConstant.const X y) = Function.const X y
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- Given a point in an affine subspace, the set of vectors in its direction equals the set of
vectors subtracting that point on the right.  -/
AffineSubspace.coe_direction_eq_vsub_set_right : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s : AffineSubspace k P} {p : P}, p ∈ s → ↑s.direction = (fun x => x -ᵥ p) '' ↑s
-- Mathlib.Data.NNRat.Defs
NNRat.den_one : NNRat.den 1 = 1
-- Mathlib.GroupTheory.EckmannHilton
/-- `IsUnital m e` expresses that `e : X` is a left and right unit
for the binary operation `m : X → X → X`.  -/
EckmannHilton.IsUnital : {X : Type u} → (X → X → X) → X → Prop
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_filterMap : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] [inst_4 : Inhabited γ] {f : α → β → Option γ} {k : α} (h : m.WF),
  Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.filterMap f m) k =
    ((Std.DHashMap.Raw.Const.get? m k).pbind fun x h' => f (m.getKey k ⋯) x).get!
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.instUniversallyClosedToImage : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.UniversallyClosed f],
  AlgebraicGeometry.UniversallyClosed (AlgebraicGeometry.Scheme.Hom.toImage f)
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
/-- The conjugation `x ↦ ωxω` as an equivalence of Lie algebras.  -/
RootPairing.GeckConstruction.ωConj : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {P : RootPairing ι R M N} →
                    (b : P.Base) →
                      [inst_5 : DecidableEq ι] →
                        [inst_6 : Fintype ι] →
                          Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R ≃ₗ⁅R⁆ Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars_mono : ∀ (S : Type u_1) {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] {s t : Submodule R M},
  s ≤ t → Submodule.restrictScalars S s ≤ Submodule.restrictScalars S t
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.match_syntax.expand : Lean.Syntax → Lean.Elab.TermElabM Lean.Syntax
-- Std.Data.TreeSet.Raw.WF
Std.TreeSet.Raw.WF.merge : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp}, t₁.WF → (t₁.merge t₂).WF
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.coind₁Res_apply : ∀ {R : Type u_1} {V : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : IsTopologicalAddGroup V] [inst_4 : Module R V] {G : Type u_7} {H : Type u_8} [inst_5 : Group G]
  [inst_6 : TopologicalSpace G] [inst_7 : TopologicalSpace R] [inst_8 : ContinuousSMul R V] [inst_9 : Group H]
  [inst_10 : TopologicalSpace H] [inst_11 : IsTopologicalGroup G] [inst_12 : IsTopologicalGroup H] (φ : H →ₜ* G)
  (π : ContRepresentation R G V) (F : C(G, V)) (x : H), ((ContRepresentation.coind₁Res φ π) F) x = F (φ x)
-- Mathlib.FieldTheory.SeparableClosure
/-- The (infinite) inseparable degree for a general field extension `E / F` is defined
to be the degree of `E / separableClosure F E`.  -/
Field.insepDegree : (F : Type u) → (E : Type v) → [inst : Field F] → [inst_1 : Field E] → [Algebra F E] → Cardinal.{v}
-- Init.Data.Int.DivMod.Lemmas
Int.emod_add_cancel_left : ∀ {m n k i : ℤ}, (i + m) % n = (i + k) % n ↔ m % n = k % n
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.coe_comp : ∀ {X Y Z : PartOrdEmb} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Computability.TuringMachine.Tape
Turing.Dir.right : Turing.Dir
-- Std.Data.DTreeMap.Internal.Ordered
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Ordered : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → Prop
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.le_closure_toSubmonoid : ∀ {G : Type u_1} [inst : Group G] (S : Set G), Submonoid.closure S ≤ (Subgroup.closure S).toSubmonoid
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.hom_ext : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f : (i j : ι) → i ≤ j → G i → G j} (P : Type u_3) [inst_2 : CommRing P] {g₁ g₂ : Ring.DirectLimit G f →+* P},
  (∀ (i : ι), g₁.comp (Ring.DirectLimit.of G f i) = g₂.comp (Ring.DirectLimit.of G f i)) → g₁ = g₂
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.evalOptionExpr : {α : Type} → (Lean.Expr → Lean.MetaM α) → Lean.Expr → Lean.MetaM (Option α)
-- Init.Data.List.Lemmas
List.filter_filterMap : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {p : β → Bool} {l : List α},
  List.filter p (List.filterMap f l) = List.filterMap (fun x => Option.filter p (f x)) l
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.const_pos : ∀ (n : ℕ), Nat.ble 1 n = true → 0 < n.rawCast
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k k' : α} {f : Option β → Option β}, (m.alter k f)[k']? = if (k == k') = true then f m[k]? else m[k']?
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.reindexFinsetRange_self : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) [inst_3 : Fintype ι] [inst_4 : DecidableEq M] (i : ι)
  (h : optParam (b i ∈ Finset.image (⇑b) Finset.univ) ⋯), b.reindexFinsetRange ⟨b i, h⟩ = b i
-- Mathlib.Algebra.Lie.OfAssociative
/-- An associative ring gives rise to a Lie ring by taking the bracket to be the ring commutator.  -/
LieRing.ofAssociativeRing : {A : Type v} → [Ring A] → LieRing A
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
/-- The tensor product of `M` and `ι →₀ N` is linearly equivalent to `ι →₀ M ⊗[R] N`  -/
TensorProduct.finsuppRight : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring S] →
        [inst_2 : Algebra R S] →
          (M : Type u_3) →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] →
                  [inst_6 : IsScalarTower R S M] →
                    (N : Type u_4) →
                      [inst_7 : AddCommMonoid N] →
                        [inst_8 : Module R N] →
                          (ι : Type u_5) → [DecidableEq ι] → TensorProduct R M (ι →₀ N) ≃ₗ[S] ι →₀ TensorProduct R M N