mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey!_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insert! k v t).maxKey! =
        t.maxKey?.elim k fun k' => if (compare k' k).isLE = true then k else k'
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_eraseₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α β} (htb : t.Balanced),
  t.Ordered → (Std.DTreeMap.Internal.Impl.eraseₘ k t htb).toListModel.Perm (Std.Internal.List.eraseKey k t.toListModel)
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
/-- The underlying object of the bicategory.  -/
CategoryTheory.Bicategory.Pith.as : {B : Type u₁} → CategoryTheory.Bicategory.Pith B → B
-- Init.Data.Vector.Perm
Vector.perm_toArray_iff : ∀ {α : Type u_1} {n : ℕ} (xs : Array α) (ys : Vector α n),
  xs.Perm ys.toArray ↔ ∃ (h : xs.size = n), (Vector.mk xs h).Perm ys
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_ratCast : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (q : ℚ),
  ArchimedeanClass.stdPart ↑q = ↑q
-- Mathlib.RingTheory.Lasker
/-- **Alias** of `Submodule.IsMinimalPrimaryDecomposition`.

---

A `Finset` of submodules is a minimal primary decomposition of `N` if the submodules `Nᵢ`
intersect to `N`, are primary, the `√Ann(M/Nᵢ)` are distinct, and each `Nᵢ` is necessary.  -/
Ideal.IsMinimalPrimaryDecomposition : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Submodule R M → Finset (Submodule R M) → Prop
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.contDiff_sin : ∀ {n : WithTop ℕ∞}, ContDiff ℝ n Real.sin
-- Init.Data.Option.Lemmas
Option.merge_join : ∀ {α : Type u_1} {o o' : Option (Option α)} {f : α → α → α},
  Option.merge f o.join o'.join = (Option.merge (Option.merge f) o o').join
-- Mathlib.Data.Finsupp.Basic
Finsupp.sumElim_eq_add : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (f : α →₀ M) (g : β →₀ M),
  f.sumElim g = Finsupp.mapDomain Sum.inl f + Finsupp.mapDomain Sum.inr g
-- Mathlib.NumberTheory.LSeries.Basic
/-- If `f` and `g` agree on large `n : ℕ` and the `LSeries` of `f` converges at `s`,
then so does that of `g`.  -/
LSeriesSummable.congr' : ∀ {f g : ℕ → ℂ} (s : ℂ), f =ᶠ[Filter.atTop] g → LSeriesSummable f s → LSeriesSummable g s
-- Mathlib.Algebra.Order.Ring.Cone
RingConeClass.toSubsemiringClass : ∀ {S : Type u_1} {R : outParam (Type u_2)} [inst : Ring R] [inst_1 : SetLike S R] [self : RingConeClass S R],
  SubsemiringClass S R
-- Mathlib.NumberTheory.LSeries.RiemannZeta
completedZeta_eq_tsum_of_one_lt_re : ∀ {s : ℂ}, 1 < s.re → completedRiemannZeta s = ↑Real.pi ^ (-s / 2) * Complex.Gamma (s / 2) * ∑' (n : ℕ), 1 / ↑n ^ s
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.instPreorder : Preorder ℚ
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instMin : {E : Type u_3} → [inst : AddCommGroup E] → Min (AddGroupSeminorm E)
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.algHom_ext : ∀ {R : Type u_1} {S : Type v₃} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {R' : Type u_6}
  (S' : Type u_7) [inst_3 : CommSemiring R'] [inst_4 : CommSemiring S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
  [inst_7 : Algebra R' S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  [H : Algebra.IsPushout R S R' S'] {A : Type u_8} [inst_11 : Semiring A] [inst_12 : Algebra R A] {f g : S' →ₐ[R] A},
  f.comp (IsScalarTower.toAlgHom R R' S') = g.comp (IsScalarTower.toAlgHom R R' S') →
    f.comp (IsScalarTower.toAlgHom R S S') = g.comp (IsScalarTower.toAlgHom R S S') → f = g
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_mul_single_le : ∀ {Γ : Type u_1} {R : Type u_2} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] (x : HahnSeries Γ R) (a : Γ) (r : R),
  (x * (HahnSeries.single a) r).cardSupp ≤ x.cardSupp
-- Mathlib.Algebra.BigOperators.Ring.Finset
Finset.sum_range_succ_mul_sum_range_succ : ∀ {R : Type u_4} [inst : NonUnitalNonAssocSemiring R] (m n : ℕ) (f g : ℕ → R),
  (∑ i ∈ Finset.range (m + 1), f i) * ∑ i ∈ Finset.range (n + 1), g i =
    (∑ i ∈ Finset.range m, f i) * ∑ i ∈ Finset.range n, g i + f m * ∑ i ∈ Finset.range n, g i +
        (∑ i ∈ Finset.range m, f i) * g n +
      f m * g n
-- Init.Data.Array.Perm
Array.Perm.extract : ∀ {α : Type u_1} {xs ys : Array α},
  xs.Perm ys →
    ∀ {lo hi : ℕ},
      (∀ i < lo, xs[i]? = ys[i]?) → (∀ (i : ℕ), hi ≤ i → xs[i]? = ys[i]?) → (xs.extract lo hi).Perm (ys.extract lo hi)
-- Mathlib.Analysis.Calculus.FDeriv.Pow
fderivWithin_pow_ring' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  {s : Set 𝔸} {x : 𝔸} (n : ℕ),
  UniqueDiffWithinAt 𝕜 s x →
    fderivWithin 𝕜 (fun x => x ^ n) s x =
      ∑ i ∈ Finset.range n, MulOpposite.op (x ^ i) • x ^ (n.pred - i) • ContinuousLinearMap.id 𝕜 𝔸
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.inf_adj : ∀ {V : Type u} {G : SimpleGraph V} {G₁ G₂ : G.Subgraph} {a b : V}, (G₁ ⊓ G₂).Adj a b ↔ G₁.Adj a b ∧ G₂.Adj a b
-- Mathlib.Algebra.Module.Torsion.PrimaryComponent
Ideal.primaryComponent.map_ker_eq : ∀ {A : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommRing A] (I : Ideal A) [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module A M₁] [inst_4 : Module A M₂] (φ : M₁ →ₗ[A] M₂),
  Submodule.map (Ideal.primaryComponent M₁ I).subtype (Ideal.primaryComponent.map I φ).ker =
    Submodule.map φ.ker.subtype (Ideal.primaryComponent (↥φ.ker) I)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.instBEqPoly.beq.eq_1 : Lean.Grind.Linarith.instBEqPoly.beq Lean.Grind.Linarith.Poly.nil Lean.Grind.Linarith.Poly.nil = true
-- Mathlib.Analysis.Complex.ReImTopology
Complex.closure_preimage_re : ∀ (s : Set ℝ), closure (Complex.re ⁻¹' s) = Complex.re ⁻¹' closure s
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_left_symm : ∀ {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] [inst_2 : CategoryTheory.Limits.HasProducts A]
  {P Q : CategoryTheory.Functor Cᵒᵖ A} {M : A} [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  (f : P ⟶ Q) (g : Q ⟶ Φ.skyscraperPresheaf M),
  Φ.skyscraperPresheafHomEquiv.symm (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (Φ.presheafFiber.map f) (Φ.skyscraperPresheafHomEquiv.symm g)
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.add_def : ∀ {ι : Type u_1} {M : ι → Type u_5} [inst : (i : ι) → Add (M i)] (f g : (i : ι) → M i), f + g = fun i => f i + g i
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.Hom.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : AlgebraicGeometry.PresheafedSpace C}
  (base : ↑X ⟶ ↑Y) (c : Y.presheaf ⟶ (TopCat.Presheaf.pushforward C base).obj X.presheaf) (base_1 : ↑X ⟶ ↑Y)
  (c_1 : Y.presheaf ⟶ (TopCat.Presheaf.pushforward C base_1).obj X.presheaf),
  ({ base := base, c := c } = { base := base_1, c := c_1 }) = (base = base_1 ∧ c ≍ c_1)
-- Init.Data.Nat.ToString
Nat.digitChar_eq_f : ∀ {n : ℕ}, n.digitChar = 'f' ↔ n = 15
-- Lean.Setup
/-- The package to which the module belongs \(if any\).  -/
Lean.ModuleSetup.package? : Lean.ModuleSetup → Option Lean.PkgId
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.extendComp_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (s : CategoryTheory.Limits.Cone F) {X Y : C} (f : X ⟶ Y) (g : Y ⟶ s.pt),
  (s.extendComp f g).hom.hom = CategoryTheory.CategoryStruct.id X
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.type_lt_cardinal : (Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.univ.{u, u + 1}
-- ProofWidgets.Compat
ProofWidgets.instTypeNameExprWithCtx : TypeName ProofWidgets.ExprWithCtx
-- Init.MetaTypes
Lean.Meta.TransparencyMode.none.sizeOf_spec : sizeOf Lean.Meta.TransparencyMode.none = 1
-- Init.Data.Int.DivMod.Lemmas
Int.natAbs_ediv : ∀ (a b : ℤ), (a / b).natAbs = a.natAbs / b.natAbs + if 0 ≤ a ∨ b = 0 ∨ b ∣ a then 0 else 1
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.brecOn.eq : ∀ {motive_1 : Lean.Widget.MsgEmbed → Sort u} {motive_2 : Lean.Widget.TaggedText Lean.Widget.MsgEmbed → Sort u}
  {motive_3 :
    Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
        (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren) →
      Sort u}
  {motive_4 : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u}
  {motive_5 : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u} (t : Lean.Widget.MsgEmbed)
  (F_1 : (t : Lean.Widget.MsgEmbed) → t.below → motive_1 t)
  (F_2 : (t : Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Lean.Widget.MsgEmbed.below_1 t → motive_2 t)
  (F_3 :
    (t :
        Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
          (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)) →
      Lean.Widget.MsgEmbed.below_2 t → motive_3 t)
  (F_4 : (t : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) → Lean.Widget.MsgEmbed.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) → Lean.Widget.MsgEmbed.below_4 t → motive_5 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 = F_1 t (Lean.Widget.MsgEmbed.brecOn.go t F_1 F_2 F_3 F_4 F_5).2
-- Mathlib.MeasureTheory.Function.AEEqOfLIntegral
MeasureTheory.lintegral_eq_lintegral_of_isPiSystem_of_univ_mem : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set (Set α)} {f g : α → ENNReal},
  m0 = MeasurableSpace.generateFrom s →
    IsPiSystem s →
      Set.univ ∈ s →
        (∀ t ∈ s, ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ) →
          ∫⁻ (x : α), f x ∂μ ≠ ⊤ → ∀ {t : Set α}, MeasurableSet t → ∫⁻ (x : α) in t, f x ∂μ = ∫⁻ (x : α) in t, g x ∂μ
-- Mathlib.Data.Finset.NAry
/-- Symmetric statement to `Finset.image_image₂_antidistrib_right`.  -/
Finset.image_image₂_right_anticomm : ∀ {α : Type u_1} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {δ : Type u_7} [inst : DecidableEq β']
  [inst_1 : DecidableEq γ] {s : Finset α} {t : Finset β} [inst_2 : DecidableEq δ] {f : α → β' → γ} {g : β → β'}
  {f' : β → α → δ} {g' : δ → γ},
  (∀ (a : α) (b : β), f a (g b) = g' (f' b a)) →
    Finset.image₂ f s (Finset.image g t) = Finset.image g' (Finset.image₂ f' t s)
-- Std.Http.Data.Method
Std.Http.instBEqMethod : BEq Std.Http.Method
-- Init.Data.Int.Order
Int.nonpos_of_mul_nonpos_left : ∀ {a b : ℤ}, a * b ≤ 0 → 0 < b → a ≤ 0
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The cocone for `CostructuredArrow.proj L Y ⋙ F` attached to `E : LeftExtension L F`.
The point of this cocone is `E.right.obj Y`  -/
CategoryTheory.Functor.LeftExtension.coconeAt : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} →
                L.LeftExtension F →
                  (Y : D) → CategoryTheory.Limits.Cocone ((CategoryTheory.CostructuredArrow.proj L Y).comp F)
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb_and : ∀ {w : ℕ} {y x : BitVec w} {hi lo : ℕ},
  BitVec.extractLsb lo hi (x &&& y) = BitVec.extractLsb lo hi x &&& BitVec.extractLsb lo hi y
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakKernels
CategoryTheory.Limits.weakKernel.condition_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasWeakKernel f] {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.weakKernel.ι f) (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Algebra.Module.SpanRank
Submodule.rank_eq_spanRank_of_free : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [StrongRankCondition R], Module.rank R M = ⊤.spanRank
-- Mathlib.Logic.Equiv.Defs
Equiv.ofBijective_symm_apply_apply : ∀ {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Bijective f) (x : α), (Equiv.ofBijective f hf).symm (f x) = x
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.Hom.iUnion_support_ker_openCover_map_comp : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [AlgebraicGeometry.QuasiCompact f] (𝒰 : X.OpenCover) [Finite 𝒰.I₀],
  ⋃ i, ↑(AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.CategoryStruct.comp (𝒰.f i) f)).support = ↑f.ker.support
-- Mathlib.Order.Filter.Pi
Filter.mem_coprodᵢ_iff : ∀ {ι : Type u_1} {α : ι → Type u_2} {f : (i : ι) → Filter (α i)} {s : Set ((i : ι) → α i)},
  s ∈ Filter.coprodᵢ f ↔ ∀ (i : ι), ∃ t₁ ∈ f i, Function.eval i ⁻¹' t₁ ⊆ s
-- Mathlib.Data.Matrix.Diagonal
Matrix.transpose_intCast : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : AddGroupWithOne α] (d : ℤ), (↑d).transpose = ↑d
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getD_eq_fallback : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α}
  {fallback : β}, a ∉ t → t.getD a fallback = fallback
-- Mathlib.Order.Filter.Map
Filter.eventuallyEq_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : α → β} {f₁ f₂ : β → γ},
  f₁ =ᶠ[Filter.map m f] f₂ ↔ f₁ ∘ m =ᶠ[f] f₂ ∘ m
-- Mathlib.Data.Int.GCD
/-- The extended GCD `b` value in the equation `gcd x y = x * a + y * b`.  -/
Nat.gcdB : ℕ → ℕ → ℤ
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.NatTrans.CommShift₂.instIdFunctor : ∀ {C₁ : Type u_1} {C₂ : Type u_3} {D : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C₂] [inst_2 : CategoryTheory.Category.{v_5, u_5} D] {M : Type u_6}
  [inst_3 : AddCommMonoid M] [inst_4 : CategoryTheory.HasShift C₁ M] [inst_5 : CategoryTheory.HasShift C₂ M]
  [inst_6 : CategoryTheory.HasShift D M] {G₁ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)}
  (h : CategoryTheory.CommShift₂Setup D M) [inst_7 : G₁.CommShift₂ h],
  CategoryTheory.NatTrans.CommShift₂ (CategoryTheory.CategoryStruct.id G₁) h
-- Mathlib.CategoryTheory.Sites.Sheaf
CategoryTheory.Presheaf.isSheaf_iff_isSheaf_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {B : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C)
  (P : CategoryTheory.Functor Cᵒᵖ A) (s : CategoryTheory.Functor A B)
  [CategoryTheory.Limits.HasLimitsOfSize.{v₁, max v₁ u₁, v₂, u₂} A]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{v₁, max v₁ u₁, v₂, v₃, u₂, u₃} s] [s.ReflectsIsomorphisms],
  CategoryTheory.Presheaf.IsSheaf J P ↔ CategoryTheory.Presheaf.IsSheaf J (P.comp s)
-- Mathlib.Algebra.Lie.Basic
sum_lie_sum : ∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] {ι : Type u_1}
  {κ : Type u_3} (s : Finset ι) (t : Finset κ) (f : ι → L) (g : κ → M),
  ⁅∑ i ∈ s, f i, ∑ j ∈ t, g j⁆ = ∑ i ∈ s, ∑ j ∈ t, ⁅f i, g j⁆
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
addEquivOfAddOrderOfEq_symm_apply_gen : ∀ {G : Type u_2} {G' : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup G'] {g : G}
  (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {g' : G'} (hg' : ∀ (x : G'), x ∈ AddSubgroup.zmultiples g')
  (h : addOrderOf g = addOrderOf g'), (addEquivOfAddOrderOfEq hg hg' h).symm g' = g
-- Mathlib.Topology.Order.IsLUB
Dense.isLUB_inter_iff : ∀ {α : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIicTopology α] {s t : Set α},
  Dense s → IsOpen t → ∀ {x : α}, IsLUB (t ∩ s) x ↔ IsLUB t x
-- Mathlib.LinearAlgebra.InvariantBasisNumber
card_le_of_injective' : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R] {α : Type u_1} {β : Type u_2} [inst_2 : Fintype α]
  [inst_3 : Fintype β] (f : (α →₀ R) →ₗ[R] β →₀ R), Function.Injective ⇑f → Fintype.card α ≤ Fintype.card β
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomAddAct.instAddActionAEEqFun.eq_1 : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : AddMonoid M] [inst_3 : AddAction M α] [inst_4 : MeasurableConstVAdd M α]
  [inst_5 : MeasureTheory.VAddInvariantMeasure M α μ],
  DomAddAct.instAddActionAEEqFun = { toVAdd := DomAddAct.instVAddAEEqFun, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Data.Num.Lemmas
Num.ofNat'_succ : ∀ {n : ℕ}, Num.ofNat' (n + 1) = Num.ofNat' n + 1
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.count_ofSums_zero : ∀ {n : ℕ} {l : Multiset ℕ} (hl : l.sum = n), Multiset.count 0 (Nat.Partition.ofSums n l hl).parts = 0
-- Lean.Expr
/-- Natural number and string literal values.

They are not really needed, but provide a more compact representation in memory
for these two kinds of literals, and are used to implement efficient reduction
in the elaborator and kernel. The "raw" natural number `2` can be represented
as `Expr.lit (.natVal 2)`. Note that, it is definitionally equal to:
```lean
Expr.app (.const `Nat.succ []) (.app (.const `Nat.succ []) (.const `Nat.zero []))
```
 -/
Lean.Expr.lit : Lean.Literal → Lean.Expr
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.diff_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp}, t₁.diff t₂ = t₁ \ t₂
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.cellFrontier_subset_closedCell`. -/
Topology.CWComplex.cellFrontier_subset_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (i : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.cellFrontier n i ⊆ Topology.RelCWComplex.closedCell n i
-- Mathlib.Logic.Encodable.Basic
Bool.encodable : Encodable Bool
-- Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
Lean.Meta.Grind.Arith.Linear.getStructId : Lean.Meta.Grind.Arith.Linear.LinearM ℕ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.isEmpty_of_isEmpty_insertMany : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} {ρ : Type w}
  [inst : ForIn Id ρ (α × β)] [EquivBEq α] [LawfulHashable α] {l : ρ},
  (Std.DHashMap.Const.insertMany m l).isEmpty = true → m.isEmpty = true
-- Mathlib.RingTheory.Valuation.Basic
Valuation.toMonoidWithZeroHom_one : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] [inst_2 : Nontrivial R]
  [inst_3 : NoZeroDivisors R] [inst_4 : DecidablePred fun x => x = 0], Valuation.toMonoidWithZeroHom 1 = 1
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.Pso.congr_simp : ∀ (p : Type u_2) (q : Type u_3) (R : Type u₂) {inst : DecidableEq p} [inst_1 : DecidableEq p] {inst_2 : DecidableEq q}
  [inst_3 : DecidableEq q] [inst_4 : CommRing R] (i i_1 : R),
  i = i_1 →
    ∀ (a a_1 : p ⊕ q),
      a = a_1 →
        ∀ (a_2 a_3 : p ⊕ q),
          a_2 = a_3 → LieAlgebra.Orthogonal.Pso p q R i a a_2 = LieAlgebra.Orthogonal.Pso p q R i_1 a_1 a_3
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
addRightStrictMono_of_addRightReflectLE : ∀ (N : Type u_2) [inst : Add N] [inst_1 : LinearOrder N] [AddRightReflectLE N], AddRightStrictMono N
-- Mathlib.Algebra.GroupWithZero.Action.Prod
Prod.smul_zero_mk : ∀ {M : Type u_1} {β : Type u_4} [inst : SMul M β] {α : Type u_5} [inst_1 : Monoid M] [inst_2 : AddMonoid α]
  [inst_3 : DistribMulAction M α] (a : M) (c : β), a • (0, c) = (0, a • c)
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalTacticSeq : Lean.Elab.Tactic.Tactic
-- Mathlib.Analysis.Calculus.Implicit
HasStrictFDerivAt.implicitFunctionDataOfComplemented.congr_simp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] (f f_1 : E → F) (e_f : f = f_1) (f' : E →L[𝕜] F) {a a_1 : E}
  (e_a : a = a_1) (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented),
  HasStrictFDerivAt.implicitFunctionDataOfComplemented f f' hf hf' hker =
    HasStrictFDerivAt.implicitFunctionDataOfComplemented f_1 f' ⋯ hf' hker
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.Chain.ext_iff : ∀ {α : Type u_2} [inst : Preorder α] {f g : OmegaCompletePartialOrder.Chain α}, f = g ↔ ⇑f = ⇑g
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Cases.and_1 : ∀ {σs : List (Type u_1)} {Q H₁' H₂' H₁₂' T : Std.Do.SPred σs},
  (H₁' ∧ H₂' ⊣⊢ₛ H₁₂') → (Q ∧ H₁₂' ⊢ₛ T) → (Q ∧ H₁') ∧ H₂' ⊢ₛ T
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.map_formula : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.ElementaryEmbedding M N) {α : Type u_5} (φ : L.Formula α) (x : α → M), φ.Realize (⇑f ∘ x) ↔ φ.Realize x
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.eval₂_X : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] (φ : R →+* S) (a : σ → S) (s : σ), MvPowerSeries.eval₂ φ a (MvPowerSeries.X s) = a s
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.toFun_ofFun : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} (f : α → β), (UniformOnFun.toFun 𝔖) ((UniformOnFun.ofFun 𝔖) f) = f
-- Mathlib.Algebra.BigOperators.Expect
Finset.card_mul_expect : ∀ {ι : Type u_1} {M : Type u_4} [inst : Semiring M] [inst_1 : Module ℚ≥0 M] (s : Finset ι) (f : ι → M),
  (↑s.card * s.expect fun i => f i) = ∑ i ∈ s, f i
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
FiniteDimensional.basisSingleton_repr_apply : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (ι : Type u_1)
  [inst_3 : Unique ι] (h : Module.finrank K V = 1) (v : V) (hv : v ≠ 0) (w : V),
  (FiniteDimensional.basisSingleton ι h v hv).repr w =
    fun₀ | default => ((Module.basisUnique ι h).repr w) default / ((Module.basisUnique ι h).repr v) default
-- Std.Do.PredTrans
Std.Do.PredTrans.apply_pure : ∀ {ps : Std.Do.PostShape} {α : Type u} (a : α) (Q : Std.Do.PostCond α ps), (Std.Do.PredTrans.pure a).apply Q = Q.1 a
-- Mathlib.GroupTheory.GroupAction.Quotient
/-- Cosets of the centralizer of an element embed into the set of commutators.  -/
Subgroup.quotientCentralizerEmbedding : {G : Type u_1} → [inst : Group G] → (g : G) → G ⧸ Subgroup.centralizer {g} ↪ ↑(commutatorSet G)
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
Finsupp.DegLex.instLTDegLexNat : {α : Type u_1} → [LT α] → LT (DegLex (α →₀ ℕ))