mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.PD.congr_simp : ∀ (l : Type u_4) (R : Type u₂) {inst : DecidableEq l} [inst_1 : DecidableEq l] [inst_2 : CommRing R] (a a_1 : l ⊕ l),
  a = a_1 → ∀ (a_2 a_3 : l ⊕ l), a_2 = a_3 → LieAlgebra.Orthogonal.PD l R a a_2 = LieAlgebra.Orthogonal.PD l R a_1 a_3
-- Mathlib.Algebra.Module.Equiv.Defs
/-- Reinterpret an element of a type of semilinear equivalences as a semilinear equivalence.  -/
SemilinearEquivClass.semilinearEquiv : {R : Type u_1} →
  {S : Type u_6} →
    {M : Type u_7} →
      {M₂ : Type u_9} →
        {F : Type u_14} →
          [inst : Semiring R] →
            [inst_1 : Semiring S] →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module S M₂] →
                      {σ : R →+* S} →
                        {σ' : S →+* R} →
                          [inst_6 : RingHomInvPair σ σ'] →
                            [inst_7 : RingHomInvPair σ' σ] →
                              [inst_8 : EquivLike F M M₂] → [SemilinearEquivClass F σ M M₂] → F → M ≃ₛₗ[σ] M₂
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- Weights for expressing `lineMap` as an affine combination.  -/
Finset.affineCombinationLineMapWeights : {k : Type u_1} → [Ring k] → {ι : Type u_4} → [DecidableEq ι] → ι → ι → k → ι → k
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- Candidate `tensorHom`. This defaults to the one that corresponds to
`DayConvolution.map` through `convolutions'`.  -/
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorHom : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {V : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} V} →
        {inst_2 : CategoryTheory.MonoidalCategory C} →
          {inst_3 : CategoryTheory.MonoidalCategory V} →
            {D : Type u₃} →
              {inst_4 : CategoryTheory.Category.{v₃, u₃} D} →
                [self : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] →
                  {d₁ d₂ d₁' d₂' : D} →
                    (d₁ ⟶ d₂) →
                      (d₁' ⟶ d₂') →
                        (CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorObj
                            C V d₁ d₁' ⟶
                          CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorObj
                            C V d₂ d₂')
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsLeftUniformAddGroup.mk : ∀ {G : Type u_7} [inst : UniformSpace G] [inst_1 : AddGroup G] [toIsTopologicalAddGroup : IsTopologicalAddGroup G],
  uniformity G = Filter.comap (fun x => -x.1 + x.2) (nhds 0) → IsLeftUniformAddGroup G
-- Mathlib.Algebra.GroupWithZero.Defs
/-- If `x` is multiplicative with respect to `f`, then so is any `x^n`.  -/
pow_mul_apply_eq_pow_mul : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {M : Type u_2} [inst_1 : Monoid M] (f : M₀ → M) {x : M₀},
  (∀ (y : M₀), f (x * y) = f x * f y) → ∀ (n : ℕ) (y : M₀), f (x ^ n * y) = f x ^ n * f y
-- Batteries.Data.List.Lemmas
List.isChain_of_isChain_cons : ∀ {α : Type u_1} {R : α → α → Prop} {b : α} {l : List α}, List.IsChain R (b :: l) → List.IsChain R l
-- Init.Data.SInt.Bitwise
Int64.toInt32_or : ∀ (a b : Int64), (a ||| b).toInt32 = a.toInt32 ||| b.toInt32
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.isCardinalFiltered_iff_aux₂ : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {κ : Cardinal.{w}} [Fact κ.IsRegular],
  (∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)) →
    (∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
        HasCardinalLT ι κ → ∃ l a b, ∀ (i : ι), CategoryTheory.CategoryStruct.comp (f i) a = b) →
      ∀ {ι : Type w} {j : ι → J} {k : J} (f₁ f₂ : (i : ι) → j i ⟶ k),
        HasCardinalLT ι κ →
          ∃ l a, ∀ (i : ι), CategoryTheory.CategoryStruct.comp (f₁ i) a = CategoryTheory.CategoryStruct.comp (f₂ i) a
-- Mathlib.Data.Rat.Lemmas
Rat.mul_num : ∀ (q₁ q₂ : ℚ), (q₁ * q₂).num = q₁.num * q₂.num / ↑((q₁.num * q₂.num).natAbs.gcd (q₁.den * q₂.den))
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
/-- Note that this is not a duplicate instance, since `IsIntegrallyClosed R` is instead defined
as `IsIntegrallyClosed R R (FractionRing R)`.  -/
IsIntegrallyClosed.instIsIntegralClosure : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_3} [inst_1 : CommRing K] [inst_2 : Algebra R K]
  [ifr : IsFractionRing R K] [iic : IsIntegrallyClosed R], IsIntegralClosure R R K
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- A list with negative sum must have positive length.  -/
List.length_pos_of_sum_neg : ∀ {M : Type u_4} [inst : AddMonoid M] [inst_1 : Preorder M] (L : List M), L.sum < 0 → 0 < L.length
-- Mathlib.FieldTheory.KrullTopology
/-- For a field extension `L/K`, `galGroupBasis K L` is the group filter basis on `Gal(L/K)`
whose sets are `Gal(L/E)` for finite subextensions `E/K`.  -/
galGroupBasis : (K : Type u_1) →
  (L : Type u_2) → [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → GroupFilterBasis Gal(L/K)
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.IntroResult.done : Lean.Meta.Grind.Goal → Lean.Meta.Grind.IntroResult✝
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.EMatchTheoremKind.toAttributeCore : Lean.Meta.Grind.EMatchTheoremKind → String
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData}
  (γ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂) [inst_2 : S₁.HasLeftHomology]
  [inst_3 : S₂.HasLeftHomology],
  CategoryTheory.ShortComplex.cyclesMap φ =
    CategoryTheory.CategoryStruct.comp h₁.cyclesIso.hom (CategoryTheory.CategoryStruct.comp γ.φK h₂.cyclesIso.inv)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpIndL1Fin_ae_eq_condExpIndSMul : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s : Set α} [inst_1 : NormedSpace ℝ G] (hm : m ≤ m0) [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)]
  (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (x : G),
  ↑↑(MeasureTheory.condExpIndL1Fin hm hs hμs x) =ᵐ[μ] ↑↑(MeasureTheory.condExpIndSMul hm hs hμs x)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₆_of_isCharThreeJNeZeroNF_of_char_three : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] [CharP R 3], W.b₆ = W.a₆
-- Mathlib.Algebra.GroupWithZero.Defs
CancelCommMonoidWithZero.mk.inj : ∀ {M₀ : Type u_2} {toCommMonoidWithZero : CommMonoidWithZero M₀} {toIsLeftCancelMulZero : IsLeftCancelMulZero M₀}
  {toCommMonoidWithZero_1 : CommMonoidWithZero M₀} {toIsLeftCancelMulZero_1 : IsLeftCancelMulZero M₀},
  { toCommMonoidWithZero := toCommMonoidWithZero, toIsLeftCancelMulZero := toIsLeftCancelMulZero } =
      { toCommMonoidWithZero := toCommMonoidWithZero_1, toIsLeftCancelMulZero := toIsLeftCancelMulZero_1 } →
    toCommMonoidWithZero = toCommMonoidWithZero_1
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.ClassifyResult.nonCommRing.sizeOf_spec : ∀ (id : ℕ), sizeOf (Lean.Meta.Sym.Arith.ClassifyResult.nonCommRing id) = 1 + sizeOf id
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
ContinuousMap.Homotopy.eq_path_of_eq_image : ∀ {X₁ X₂ Y : TopCat} {f : C(↑X₁, ↑Y)} {g : C(↑X₂, ↑Y)} {x₀ x₁ : ↑X₁} {x₂ x₃ : ↑X₂} {p : Path x₀ x₁} {q : Path x₂ x₃}
  (hfg : ∀ (t : ↑unitInterval), f (p t) = g (q t)),
  (FundamentalGroupoid.fundamentalGroupoidFunctor.map (TopCat.ofHom f)).map ⟦p⟧ =
    CategoryTheory.CategoryStruct.comp (ContinuousMap.Homotopy.hcast ⋯)
      (CategoryTheory.CategoryStruct.comp
        ((FundamentalGroupoid.fundamentalGroupoidFunctor.map (TopCat.ofHom g)).map ⟦q⟧)
        (ContinuousMap.Homotopy.hcast ⋯))
-- Mathlib.Data.Nat.Bits
Nat.bit_add' : ∀ (b : Bool) (n m : ℕ), Nat.bit b (n + m) = Nat.bit b n + Nat.bit false m
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.Push.instHasInvolutiveReverse : {V : Type u_2} →
  [inst : Quiver V] →
    {V' : Type u_4} → (σ : V → V') → [h : Quiver.HasInvolutiveReverse V] → Quiver.HasInvolutiveReverse (Quiver.Push σ)
-- Mathlib.AlgebraicTopology.SimplicialObject.Op
SimplicialObject.opFunctor.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C],
  SimplicialObject.opFunctor =
    (CategoryTheory.Functor.whiskeringLeft SimplexCategoryᵒᵖ SimplexCategoryᵒᵖ C).obj SimplexCategory.rev.op
-- Mathlib.Tactic.ClickSuggestions.SectionState
Mathlib.Tactic.ClickSuggestions.instInhabitedResult : {a : Type} → [Inhabited a] → Inhabited (Mathlib.Tactic.ClickSuggestions.Result a)
-- Mathlib.Analysis.Normed.Algebra.Basic
WeakDual.CharacterSpace.instCompactSpaceElemCharacterSpaceOfProperSpace : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] [ProperSpace 𝕜], CompactSpace ↑(WeakDual.characterSpace 𝕜 A)
-- Mathlib.Probability.Kernel.MeasurableLIntegral
Measurable.lintegral_kernel_prod_right' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {f : α × β → ENNReal},
  Measurable f → Measurable fun a => ∫⁻ (b : β), f (a, b) ∂κ a
-- Init.MetaTypes
Lean.Meta.Simp.NormCastConfig : Type
-- Mathlib.Algebra.Quaternion
Quaternion.equivProd_apply : ∀ (R : Type u_1) [inst : Zero R] [inst_1 : One R] [inst_2 : Neg R] (a : QuaternionAlgebra R (-1) 0 (-1)),
  (Quaternion.equivProd R) a = (a.re, a.imI, a.imJ, a.imK)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_pi_div_two : Complex.cos (↑Real.pi / 2) = 0
-- Mathlib.NumberTheory.Padics.PadicVal.Defs
padicValNat_def' : ∀ {p n : ℕ}, p ≠ 1 → n ≠ 0 → padicValNat p n = multiplicity p n
-- Mathlib.Order.Minimal
MaximalFor.not_prop_of_gt : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] {Q : ι → Prop} {f : ι → α} {i j : ι},
  MaximalFor Q f i → f i < f j → ¬Q j
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.mrange_swap : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  MonoidHom.mrange (Monoid.Coprod.swap M N) = ⊤
-- Mathlib.Analysis.Complex.Basic
Complex.compl_Iic_zero : (Set.Iic 0)ᶜ = Complex.slitPlane
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
IsTranscendenceBasis.cardinalMk_eq_trdeg : ∀ {R : Type u_1} {A : Type w} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [Nontrivial R]
  [NoZeroDivisors A] {ι : Type w} {x : ι → A}, IsTranscendenceBasis R x → Cardinal.mk ι = Algebra.trdeg R A
-- Init.Data.Int.DivMod.Lemmas
Int.lt_ediv_iff_mul_lt : ∀ {a b c : ℤ}, 0 < c → c ∣ b → (a < b / c ↔ a * c < b)
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {U : CategoryTheory.Comonad C}
  {x y : CategoryTheory.Cokleisli U} {f g : x ⟶ y}, f = g ↔ f.of = g.of
-- Lean.Attributes
Lean.ParametricAttribute.mk : {α : Type} →
  Lean.AttributeImpl →
    Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (List Lean.Name × Lean.NameMap α) →
      Bool → Lean.ParametricAttribute α
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- Restriction of open partial homeomorphisms respects equivalence  -/
OpenPartialHomeomorph.EqOnSource.restr : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e e' : OpenPartialHomeomorph X Y}, e ≈ e' → ∀ (s : Set X), e.restr s ≈ e'.restr s
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.recoverEolWith : Array Lean.Syntax → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- Definition of the zeta function in terms of `completedRiemannZeta₀`.  -/
riemannZeta_eq_completedRiemannZeta₀ : ∀ {s : ℂ},
  s ≠ 0 →
    riemannZeta s = (completedRiemannZeta₀ s - 1 / s - 1 / (1 - s)) / (↑Real.pi ^ (-s / 2) * Complex.Gamma (s / 2))
-- Mathlib.Order.TypeTags
/-- Attach `⊥` to a type.  -/
WithBot : Type u_2 → Type u_2
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.π₃_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), CategoryTheory.ShortComplex.π₃.obj S = S.X₃
-- Mathlib.Data.Fin.Tuple.Basic
Fin.tail.eq_1 : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u} (q : (i : Fin (n + 1)) → α i) (i : Fin n), Fin.tail q i = q i.succ
-- Mathlib.Data.PFun
/-- The monad `pure` function, the total constant `x` function  -/
PFun.pure : {α : Type u_1} → {β : Type u_2} → β → α →. β
-- Mathlib.Data.ENat.Basic
ENat.toNat_eq_iff : ∀ {m : ℕ∞} {n : ℕ}, n ≠ 0 → (m.toNat = n ↔ m = ↑n)
-- Init.Data.Bool
Bool.if_true_right : ∀ (p : Prop) [h : Decidable p] (t : Bool), (if p then t else true) = (!decide p || t)
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.ComposableArrows.fourδ₄Toδ₃.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ f₄_1 : i₃ ⟶ i₄) (e_f₄ : f₄ = f₄_1) (f₃₄ : i₂ ⟶ i₄)
  (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄),
  CategoryTheory.ComposableArrows.fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄ =
    CategoryTheory.ComposableArrows.fourδ₄Toδ₃ f₁ f₂ f₃ f₄_1 f₃₄ ⋯
-- Mathlib.RingTheory.Algebraic.Cardinality
Algebra.IsAlgebraic.lift_cardinalMk_le_sigma_polynomial : ∀ (R : Type u) [inst : CommRing R] [IsDomain R] (L : Type v) [inst_2 : CommRing L] [inst_3 : IsDomain L]
  [inst_4 : Algebra R L] [Module.IsTorsionFree R L] [Algebra.IsAlgebraic R L],
  Cardinal.lift.{u, v} (Cardinal.mk L) ≤ Cardinal.mk ((p : Polynomial R) × { x // x ∈ p.aroots L })
-- Mathlib.NumberTheory.Padics.PadicNumbers
padicNormE.eq_padic_norm' : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] (q : ℚ), padicNormE ↑q = padicNorm p q
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mulSingle_eq_one_iff : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → One (G i)] [inst_3 : ∀ (i : ι), OneMemClass (S i) (G i)] (i : ι)
  {x : G i}, RestrictedProduct.mulSingle A i x = 1 ↔ x = 1
-- Mathlib.Algebra.Lie.Basis.Prod
_private.Mathlib.Algebra.Lie.Basis.Prod.0.LieAlgebra.Basis.lie_fst_eq_zero_of_mem_prodCartan : ∀ {ι₁ : Type u_1} {ι₂ : Type u_2} {L₁ : Type u_3} {L₂ : Type u_4} [inst : Finite ι₁] [inst_1 : Finite ι₂] (eι : ι₁ ≃ ι₂)
  [inst_2 : LieRing L₁] [inst_3 : LieRing L₂] {R : Type u_5} [inst_4 : CommRing R] [inst_5 : LieAlgebra R L₁]
  {H₁ : LieSubalgebra R L₁} (b₁ : LieAlgebra.Basis ι₁ H₁) [inst_6 : LieAlgebra R L₂] {H₂ : LieSubalgebra R L₂}
  (b₂ : LieAlgebra.Basis ι₂ H₂) {y : ↥(LieAlgebra.Basis.prod✝ eι b₁ b₂)},
  y ∈ LieAlgebra.Basis.prodCartan✝ eι b₁ b₂ → ∀ (x : ↥H₁), ⁅(↑y).1, ↑x⁆ = 0
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxRightLinear.δᵣ_unitality_inv : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.OplaxRightLinear C] (d : D),
  (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso (F.obj d)).inv =
    CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso d).inv)
      (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.lift_lt_omega_natCast : ∀ {o : Ordinal.{u}} {n : ℕ}, Ordinal.lift.{v, u} o < Ordinal.omega ↑n ↔ o < Ordinal.omega ↑n
-- Mathlib.Algebra.Module.Submodule.Pointwise
/-- See also `Submodule.smul_sup`.  -/
Submodule.smul_sup' : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Monoid α] [inst_4 : DistribMulAction α M] [inst_5 : SMulCommClass α R M] (a : α) (S T : Submodule R M),
  a • (S ⊔ T) = a • S ⊔ a • T
-- Mathlib.AlgebraicTopology.SimplicialObject.Op
SimplicialObject.opEquivalence_inverse : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C],
  SimplicialObject.opEquivalence.inverse = SimplicialObject.opFunctor
-- Std.Sync.SharedMutex
_private.Std.Sync.SharedMutex.0.Std.SharedMutex.mk.injEq : ∀ {α : Type} (ref : IO.Ref α) (mutex : Std.BaseSharedMutex) (ref_1 : IO.Ref α) (mutex_1 : Std.BaseSharedMutex),
  ({ ref := ref, mutex := mutex } = { ref := ref_1, mutex := mutex_1 }) = (ref = ref_1 ∧ mutex = mutex_1)
-- Mathlib.Data.Set.Operations
Set.mk_mem_prod : ∀ {α : Type u} {β : Type v} {a : α} {b : β} {s : Set α} {t : Set β}, a ∈ s → b ∈ t → (a, b) ∈ s ×ˢ t
-- Std.Do.PostCond
/-- Entailment of postconditions.

This consists of:
 * Entailment of the assertion about the return value, for all possible return values.
 * Entailment of the exception conditions.

While implication of postconditions (`PostCond.imp`) results in a new postcondition, entailment is
an ordinary proposition.
 -/
Std.Do.PostCond.entails : {α : Type u_1} → {ps : Std.Do.PostShape} → Std.Do.PostCond α ps → Std.Do.PostCond α ps → Prop
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.HasGaussianLaw.fun_sub : ∀ {Ω : Type u_1} {E : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : MeasurableSpace E] [BorelSpace E] {X : Ω → E} [inst_3 : NormedSpace ℝ E] [SecondCountableTopology E]
  {Y : Ω → E},
  ProbabilityTheory.HasGaussianLaw (fun ω => (X ω, Y ω)) P → ProbabilityTheory.HasGaussianLaw (fun ω => X ω - Y ω) P
-- Mathlib.LinearAlgebra.Projection
LinearMap.ofIsCompl_eq' : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_3}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {p q : Submodule R E} (h : IsCompl p q) {φ : ↥p →ₗ[R] F}
  {ψ : ↥q →ₗ[R] F} {χ : E →ₗ[R] F}, φ = χ ∘ₗ p.subtype → ψ = χ ∘ₗ q.subtype → LinearMap.ofIsCompl h φ ψ = χ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mul : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon
-- Init.Data.BitVec.Lemmas
BitVec.toNat_setWidth_of_le : ∀ {w w' : ℕ} {b : BitVec w}, w ≤ w' → (BitVec.setWidth w' b).toNat = b.toNat
-- Mathlib.Data.Set.Lattice.Image
Set.prod_sUnion : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {C : Set (Set β)}, s ×ˢ ⋃₀ C = ⋃₀ ((fun t => s ×ˢ t) '' C)
-- Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
/-- The `derivWithin` of a sum whose derivative is absolutely and uniformly convergent sum on an
open set `s` is the sum of the derivatives of sequence of functions on the open set `s`  -/
derivWithin_tsum : ∀ {ι : Type u_1} {𝕜 : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 F] {s : Set 𝕜} {f : ι → 𝕜 → F},
  IsOpen s →
    ∀ {x : 𝕜},
      x ∈ s →
        (∀ y ∈ s, Summable fun n => f n y) →
          SummableLocallyUniformlyOn (fun n => derivWithin (fun z => f n z) s) s →
            (∀ (n : ι), ∀ r ∈ s, DifferentiableAt 𝕜 (f n) r) →
              derivWithin (fun z => ∑' (n : ι), f n z) s x = ∑' (n : ι), derivWithin (f n) s x
-- Mathlib.MeasureTheory.MeasurableSpace.Pi
/-- The product of generated σ-algebras is the one generated by boxes, if both generating sets
are countably spanning.  -/
generateFrom_pi_eq : ∀ {ι : Type u_1} {α : ι → Type u_2} [Finite ι] {C : (i : ι) → Set (Set (α i))},
  (∀ (i : ι), IsCountablySpanning (C i)) →
    MeasurableSpace.pi = MeasurableSpace.generateFrom (Set.univ.pi '' Set.univ.pi C)
-- Mathlib.RingTheory.RingHom.PurelyInseparable
/-- A ring homomorphism `f : F →+* E` is purely inseparable if `E` is purely inseparable as an
`F`-algebra.  -/
RingHom.IsPurelyInseparable : {F : Type u} → {E : Type v} → [inst : CommRing F] → [inst_1 : CommRing E] → (F →+* E) → Prop
-- Mathlib.Probability.UniformOn
ProbabilityTheory.uniformOn_self : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [MeasurableSingletonClass Ω] {s : Set Ω},
  s.Finite → s.Nonempty → (ProbabilityTheory.uniformOn s) s = 1
-- Mathlib.Tactic.ClickSuggestions.Util
Mathlib.Tactic.ClickSuggestions.instInhabitedPremise.default : Mathlib.Tactic.ClickSuggestions.Premise
-- Mathlib.Order.Lattice
SemilatticeSup.dual_dual : ∀ (α : Type u_1) [H : SemilatticeSup α], OrderDual.instSemilatticeSup αᵒᵈ = H
-- Mathlib.MeasureTheory.Integral.IntegrableOn
integrableOn_Ioc_iff_integrableOn_Ioo' : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} [inst : PartialOrder α] [MeasurableSingletonClass α]
  [inst_2 : TopologicalSpace ε'] [inst_3 : ESeminormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε']
  {f : α → ε'} {μ : MeasureTheory.Measure α} {a b : α},
  μ {b} ≠ ⊤ →
    autoParam (‖f b‖ₑ ≠ ⊤) integrableOn_Ioc_iff_integrableOn_Ioo'._auto_1 →
      (MeasureTheory.IntegrableOn f (Set.Ioc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ)
-- Batteries.Tactic.Case
/-- Find the first goal among those matching `tag` whose type unifies with `patt`.
The `renameI` array consists of names to use to rename inaccessibles.
The `patt` term is elaborated in the context where the inaccessibles have been renamed.

Returns the found goal, goals caused by elaborating `patt`, and the remaining goals.  -/
Batteries.Tactic.findGoalOfPatt : List Lean.MVarId →
  Lean.TSyntax `Lean.binderIdent →
    Option Lean.Term →
      Lean.TSyntaxArray `Lean.binderIdent → Lean.Elab.Tactic.TacticM (Lean.MVarId × List Lean.MVarId × List Lean.MVarId)
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
PadicInt.adicCompletionIntegersEquiv.eq_1 : ∀ (R : Type u_2) [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Algebra R ℚ] [inst_3 : IsFractionRing R ℚ]
  [inst_4 : IsIntegralClosure R ℤ ℚ] (p : Nat.Primes),
  PadicInt.adicCompletionIntegersEquiv R p =
    (ContinuousAlgEquiv.cast ⋯).trans
      (Rat.HeightOneSpectrum.adicCompletionIntegers.padicIntEquiv (Rat.HeightOneSpectrum.primesEquiv.symm p)).symm
-- Mathlib.Order.UpperLower.Closure
upperClosure_empty : ∀ {α : Type u_1} [inst : Preorder α], upperClosure ∅ = ⊤
-- Mathlib.Order.Bounded
Set.unbounded_gt_iff_unbounded_ge : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α] [NoMinOrder α],
  Set.Unbounded (fun x1 x2 => x1 > x2) s ↔ Set.Unbounded (fun x1 x2 => x1 ≥ x2) s
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] [inst_2 : Inhabited α] {l : List ((a : α) × β a)}
  {k a : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey! a (Std.Internal.List.eraseKey k l) =
      if (k == a) = true then default else Std.Internal.List.getKey! a l
-- Init.Data.Rat.Lemmas
Rat.inv_mul_cancel : ∀ (a : ℚ), a ≠ 0 → a⁻¹ * a = 1
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.volume_box : ∀ {ι : Type u_1} (n : ℕ) [inst : NeZero n] [inst_1 : Fintype ι] (ν : ι → ℤ),
  MeasureTheory.volume ↑(BoxIntegral.unitPartition.box n ν) = 1 / ↑n ^ Fintype.card ι
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_erase_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [inst : Inhabited α] [EquivBEq α] [LawfulHashable α]
  {k : α}, (m.erase k).get! k = default
-- Init.Data.Fin.Basic
/-- Modulus of bounded numbers with respect to a `Nat`.

The resulting value is that computed by the `%` operator on `Nat`.
 -/
Fin.modn : {n : ℕ} → Fin n → ℕ → Fin n
-- Mathlib.Order.Bounds.Image
/-- The image under a monotone function of a set which is bounded above is bounded above. See also
`BddAbove.image2`.  -/
Monotone.map_bddAbove : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → ∀ {s : Set α}, BddAbove s → BddAbove (f '' s)