mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.sum_mem_biSup : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_4}
  {s : Finset ι} {f : ι → M} {p : ι → Submodule R M}, (∀ i ∈ s, f i ∈ p i) → ∑ i ∈ s, f i ∈ ⨆ i ∈ s, p i
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinite_mul_of_infinite_not_infinitesimal : ∀ {x y : ℝ*}, x.Infinite → ¬y.Infinitesimal → (x * y).Infinite
-- Mathlib.Algebra.Group.Hom.Defs
iterate_map_zpow : ∀ {M : Type u_10} {F : Type u_11} [inst : Group M] [inst_1 : FunLike F M M] [MonoidHomClass F M M] (f : F) (n : ℕ)
  (x : M) (k : ℤ), (⇑f)^[n] (x ^ k) = (⇑f)^[n] x ^ k
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
/-- In any concrete category, we can test equality of morphisms by pointwise evaluations.  -/
CategoryTheory.ConcreteCategory.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C}
  (f g : X ⟶ Y),
  (∀ (x : CC X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.Data.Finset.Sups
Finset.compls_infs_eq_diffs : ∀ {α : Type u_2} [inst : BooleanAlgebra α] [inst_1 : DecidableEq α] (s t : Finset α), s.compls ⊼ t = t.diffs s
-- Mathlib.Analysis.Normed.Lp.ProdLp
_private.Mathlib.Analysis.Normed.Lp.ProdLp.0.WithLp.isUniformInducing_ofLp_aux : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β], IsUniformInducing WithLp.ofLp
-- Mathlib.Data.ENNReal.Real
ENNReal.toNNReal_pos : ∀ {a : ENNReal}, a ≠ 0 → a ≠ ⊤ → 0 < a.toNNReal
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalCommCStarAlgebra.toSMulCommClass : ∀ {A : Type u_1} [self : NonUnitalCommCStarAlgebra A], SMulCommClass ℂ A A
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.sinKernel_undef : ∀ (a : UnitAddCircle) {x : ℝ}, x ≤ 0 → HurwitzZeta.sinKernel a x = 0
-- Mathlib.CategoryTheory.Sites.Coverage
/-- The main theorem of this file: Given a coverage `K` on `C`,
a `Type*`-valued presheaf on `C` is a sheaf for `K` if and only if it is a sheaf for
the associated Grothendieck topology.
 -/
CategoryTheory.Presieve.isSheaf_coverage : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C] (K : CategoryTheory.Coverage C)
  (P : CategoryTheory.Functor Cᵒᵖ (Type u_1)),
  CategoryTheory.Presieve.IsSheaf K.toGrothendieck P ↔
    ∀ {X : C}, ∀ R ∈ K.coverings X, CategoryTheory.Presieve.IsSheafFor P R
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α},
  k ∈ m₂ → (m₁ ∩ m₂).get? k = m₁.get? k
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.isScalarTower : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} {O : Type u_6} [inst : Semiring R] [inst_1 : SMulZeroClass N R]
  [inst_2 : SMulZeroClass O R] [inst_3 : SMul N O] [IsScalarTower N O R], IsScalarTower N O (AddMonoidAlgebra R M)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.convertYearAndEra : Std.Time.Year.Offset → Std.Time.Year.Era → Std.Time.Year.Offset
-- Mathlib.Logic.Function.FromTypes
Function.FromTypes.inhabited : {n : ℕ} → {p : Fin n → Type u} → {τ : Type u} → [Inhabited τ] → Inhabited (Function.FromTypes p τ)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
UniformContinuous.add : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α]
  [inst_3 : UniformSpace β] {f g : β → α},
  UniformContinuous f → UniformContinuous g → UniformContinuous fun x => f x + g x
-- Mathlib.Algebra.Group.PUnit
PUnit.neg_eq : ∀ (x : PUnit.{u_1 + 1}), -x = PUnit.unit
-- Mathlib.Algebra.Lie.Weights.IsSimple
LieAlgebra.IsKilling.invtSubmoduleToLieIdeal.congr_simp : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : FiniteDimensional K L] [inst_5 : LieAlgebra.IsKilling K L] {H : LieSubalgebra K L}
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L]
  (q q_1 : Submodule K (Module.Dual K ↥H)) (e_q : q = q_1)
  (hq : ∀ (i : ↥LieSubalgebra.root), q ∈ Module.End.invtSubmodule ↑((LieAlgebra.IsKilling.rootSystem H).reflection i)),
  LieAlgebra.IsKilling.invtSubmoduleToLieIdeal q hq = LieAlgebra.IsKilling.invtSubmoduleToLieIdeal q_1 ⋯
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
/-- The "commutative" square of functors involving the underlying functors
of the localizer morphisms `CochainComplex.Plus.localizerMorphism C`
and `HomotopyCategory.Plus.localizerMorphism C`.  -/
_private.Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives.0.HomotopyCategory.Plus.isRightDerivabilityStructure.iso : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (CochainComplex.Plus.localizerMorphism C).functor.comp
          (HomotopyCategory.Plus.isRightDerivabilityStructure.R✝ C).functor ≅
        (HomotopyCategory.Plus.isRightDerivabilityStructure.L✝ C).functor.comp
          (HomotopyCategory.Plus.localizerMorphism C).functor
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.inclusion_self : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S : Subalgebra R A},
  Subalgebra.inclusion ⋯ = AlgHom.id R ↥S
-- Mathlib.NumberTheory.ModularForms.Basic
/-- The `n`-th power of a modular form, as a modular form of weight `n * k`.  -/
ModularForm.pow : {Γ : Subgroup (GL (Fin 2) ℝ)} → [Γ.HasDetPlusMinusOne] → {k : ℤ} → ModularForm Γ k → (n : ℕ) → ModularForm Γ (↑n * k)
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIdsM.Context : Type
-- Mathlib.LinearAlgebra.Finsupp.Span
Finsupp.iSup_lsingle_range : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  ⨆ a, (Finsupp.lsingle a).range = ⊤
-- Mathlib.NumberTheory.Divisors
Int.mem_divisors : ∀ {x z : ℤ}, x ∈ z.divisors ↔ x ∣ z ∧ z ≠ 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {k : α} (h' : k ∈ t), t.getKey k h' = k
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.map_cast_binomial_real_singleton : ∀ {R : Type u_1} [inst : MeasurableSpace R] [inst_1 : AddMonoidWithOne R] [MeasurableSingletonClass R] [CharZero R]
  (n k : ℕ) (p : ↑unitInterval),
  (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial n p)).real {↑k} =
    ↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)
-- Init.Prelude
/-- The `<*>` operator is overloaded using the function `Seq.seq`.

While `<$>` from the class `Functor` allows an ordinary function to be mapped over its contents,
`<*>` allows a function that's “inside” the functor to be applied. When thinking about `f` as
possible side effects, this captures evaluation order: `seq` arranges for the effects that produce
the function to occur prior to those that produce the argument value.

For most applications, `Applicative` or `Monad` should be used rather than `Seq` itself.
 -/
Seq : (Type u → Type v) → Type (max (u + 1) v)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp)
  (e_t : t = t_1) (a a_1 : α) (e_a : a = a_1) (h : a ∈ t), t.get a h = t_1.get a_1 ⋯
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.instFunLike : {α : Type u_2} → {β : Type u_3} → [inst : Bornology α] → [inst_1 : Bornology β] → FunLike (LocallyBoundedMap α β) α β
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- If every element belongs to at least `n` Finsets, then the sum of their sizes is at least `n`
times how many they are.  -/
Finset.le_sum_card : ∀ {α : Type u_2} [inst : DecidableEq α] {B : Finset (Finset α)} {n : ℕ} [inst_1 : Fintype α],
  (∀ (a : α), n ≤ {b ∈ B | a ∈ b}.card) → Fintype.card α * n ≤ ∑ s ∈ B, s.card
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_ssubset_Icc_right : ∀ {α : Type u_1} [inst : Preorder α] {a₁ a₂ b₁ b₂ : α}, b₂ ≤ a₂ → b₂ ≤ b₁ → a₁ < a₂ → Set.Icc b₁ a₁ ⊂ Set.Icc b₂ a₂
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
MulRingNorm.mk : {R : Type u_2} →
  [inst : NonAssocRing R] →
    (toMulRingSeminorm : MulRingSeminorm R) → (∀ (x : R), toMulRingSeminorm.toFun x = 0 → x = 0) → MulRingNorm R
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.instMin.eq_1 : ∀ {α : Type u} [inst : Group α],
  GroupTopology.instMin =
    {
      min := fun x y =>
        { toTopologicalSpace := x.toTopologicalSpace ⊓ y.toTopologicalSpace, toIsTopologicalGroup := ⋯ } }
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- Define the first primitive quadratic character on `ZMod 8`, `χ₈`.
It corresponds to the extension `ℚ(√2)/ℚ`.  -/
ZMod.χ₈ : MulChar (ZMod 8) ℤ
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.instMonObjTensorObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] →
        {M N : C} →
          [CategoryTheory.MonObj M] →
            [CategoryTheory.MonObj N] → CategoryTheory.MonObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.End.mulActionRight : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → MulAction (CategoryTheory.End Y) (X ⟶ Y)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_diff_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α], m₁.isEmpty = true → (m₁ \ m₂).isEmpty = true
-- Batteries.Data.Int
Int.ofBits_zero : ∀ (f : Fin 0 → Bool), Int.ofBits f = 0
-- Lean.Structure
/-- Gets the resolution order for a structure.
 -/
Lean.getStructureResolutionOrder : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m (Array Lean.Name)
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.expandWhereStructInst : Lean.Macro
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.tensorHom_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X₁ X₂ Y₁ Y₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) {Z : C} (h : Y₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X₂ Y₂) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd X₁ Y₁)
      (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates_surjective : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  Function.Surjective (NumberField.mixedEmbedding.fundamentalCone.integerSetToAssociates K)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Functor.FullyFaithful.homMulEquiv.eq_1 : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v, u_1} C]
  [inst_1 : CategoryTheory.CartesianMonoidalCategory C] [inst_2 : CategoryTheory.Category.{w, u_2} D]
  [inst_3 : CategoryTheory.CartesianMonoidalCategory D] {M X : C} [inst_4 : CategoryTheory.MonObj M]
  (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal] (hF : F.FullyFaithful),
  CategoryTheory.Functor.FullyFaithful.homMulEquiv F hF = { toEquiv := hF.homEquiv, map_mul' := ⋯ }
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy
CategoryTheory.Limits.FormalCoproduct.cechIsoAugmentedCechNerve_hom_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  (U : CategoryTheory.Limits.FormalCoproduct C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T),
  (U.cechIsoAugmentedCechNerve hT).hom.left = (U.cechIsoCechNerve hT).hom
-- Mathlib.Data.Tree.Basic
instReprBinaryTree : {α : Type u_1} → [Repr α] → Repr (BinaryTree α)
-- Mathlib.Tactic.Widget.StringDiagram
/-- Given a 2-morphism, return a string diagram. Otherwise `none`.  -/
Mathlib.Tactic.Widget.StringDiagram.stringM? : Lean.Expr → Lean.MetaM (Option ProofWidgets.Html)
-- Mathlib.FieldTheory.SeparableClosure
Field.sepDegree_self : ∀ (F : Type u) [inst : Field F], Field.sepDegree F F = 1
-- Mathlib.RingTheory.GradedAlgebra.RingHom
GradedRingHom.comp_id : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] {𝒜 : ι → σ} {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ), f.comp (GradedRingHom.id 𝒜) = f
-- Mathlib.Algebra.Group.Hom.Basic
/-- Multiplication by a natural `n` on a commutative additive monoid,
considered as a morphism of additive monoids.  -/
nsmulAddMonoidHom : {α : Type u_1} → [inst : AddCommMonoid α] → ℕ → α →+ α
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_id_const : ∀ {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F''] {c : F''},
  c ≠ 0 → (fun x => x) =o[nhds 0] fun _x => c
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.WalkingParallelPair.ofNat : ℕ → CategoryTheory.Limits.WalkingParallelPair
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.not_congr : ∀ (w : ℕ) (x x' : BitVec w), x = x' → ~~~x' = ~~~x
-- Std.Async.System
Std.Async.System.instInhabitedUserId : Inhabited Std.Async.System.UserId
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.coe_map_inv_mul_map : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  [inst_3 : CommRing S] (f : R →+* S) (g : GL n R), (↑g)⁻¹.map ⇑f * (↑g).map ⇑f = 1
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.integral_def : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) (f : MeasureTheory.SimpleFunc α F),
  MeasureTheory.SimpleFunc.integral μ f = MeasureTheory.SimpleFunc.setToSimpleFunc (MeasureTheory.weightedSMul μ) f
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.toSemigroup_toMul_mul : ∀ {R : Type u_1} {A : Type u_6} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] {𝒜 : ι → Submodule R A} [inst_5 : GradedAlgebra 𝒜] (g f : 𝒜 →ₐᵍ[R] 𝒜),
  g * f = g.comp f
-- Mathlib.MeasureTheory.Function.LpSeminorm.Defs
/-- `ℒp` seminorm, equal to `0` for `p=0`, to `(∫ ‖f a‖^p ∂μ) ^ (1/p)` for `0 < p < ∞` and to
`essSup ‖f‖ μ` for `p = ∞`.  -/
MeasureTheory.eLpNorm : {α : Type u_1} →
  {ε : Type u_2} →
    [ENorm ε] →
      {x : MeasurableSpace α} →
        (α → ε) → ENNReal → autoParam (MeasureTheory.Measure α) MeasureTheory.eLpNorm._auto_1 → ENNReal
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddMonoidOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid Mᵃᵒᵖ], DomAddAct.instAddMonoidOfAddOpposite = inst
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toArray.go.match_1.eq_1 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (out : β) (h : it.IsPlausibleStep (Std.IterStep.yield it' out))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.yield it' out, h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_1 it' out h
-- Init.Data.Int.LemmasAux
Int.natCast_le_zero : ∀ {n : ℕ}, ↑n ≤ 0 ↔ n = 0
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- The linear isometry equivalence version of the function `op`.  -/
MulOpposite.opLinearIsometryEquiv : (R : Type u_11) →
  (H : Type u_12) → [inst : Semiring R] → [inst_1 : SeminormedAddCommGroup H] → [inst_2 : Module R H] → H ≃ₗᵢ[R] Hᵐᵒᵖ
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.ofUnitsEquivType.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] (S : Subgroup Mˣ),
  S.ofUnitsEquivType =
    { toFun := fun x => ⟨S.unit_of_mem_ofUnits ⋯, ⋯⟩, invFun := fun x => ⟨↑↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
      map_mul' := ⋯ }
-- Init.PropLemmas
exists_imp : ∀ {α : Sort u_1} {p : α → Prop} {b : Prop}, (∃ x, p x) → b ↔ ∀ (x : α), p x → b
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.fun_inv_map_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (X Y : D) (f : X ⟶ Y) {Z : D} (h : e.functor.obj (e.inverse.obj Y) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.functor.map (e.inverse.map f)) h =
    CategoryTheory.CategoryStruct.comp (e.counit.app X)
      (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (e.counitInv.app Y) h))
-- Mathlib.Order.CompleteBooleanAlgebra
/-- The infimum of `x` and `xᶜ` is at most `⊥`  -/
CompleteBooleanAlgebra.inf_compl_le_bot : ∀ {α : Type u_1} [self : CompleteBooleanAlgebra α] (x : α), x ⊓ xᶜ ≤ ⊥
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
Subsemigroup.centralizer_le : ∀ {M : Type u_1} {S T : Set M} [inst : Semigroup M], S ⊆ T → Subsemigroup.centralizer T ≤ Subsemigroup.centralizer S
-- Mathlib.Order.Hom.Basic
OrderHom.uliftRightMap_uliftLeftMap_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β),
  f.uliftRightMap.uliftLeftMap = f.uliftMap
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.add.inj : ∀ {a b a_1 b_1 : Nat.Internal.SOM.Expr}, a.add b = a_1.add b_1 → a = a_1 ∧ b = b_1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, (m.alter k f).getKey? k = if (f (m.get? k)).isSome = true then some k else none
-- Init.Grind.Lemmas
Lean.Grind.and_eq_of_eq_true_left : ∀ {a b : Prop}, a = True → (a ∧ b) = b
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.atTop_basis' : ∀ {α : Type u_3} [inst : Preorder α] [IsDirectedOrder α] (a : α), Filter.atTop.HasBasis (fun x => a ≤ x) Set.Ici
-- Mathlib.CategoryTheory.Presentable.Basic
/-- A functor `F : C ⥤ D` is `κ`-accessible (with `κ` a regular cardinal)
if it preserves colimits of shape `J` where `J` is any `κ`-filtered category.
In the mathematical literature, some assumptions are often made on the
categories `C` or `D` (e.g. the existence of `κ`-filtered colimits,
see `HasCardinalFilteredColimits` below), but here we do not
make such assumptions.  -/
CategoryTheory.Functor.IsCardinalAccessible : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → (κ : Cardinal.{w}) → [Fact κ.IsRegular] → Prop
-- Init.Data.String.Slice
/-- If `pat` matches a suffix of `s`, returns the remainder. Returns `s` unmodified
otherwise.

Use `String.Slice.dropSuffix?` to return `none` when `pat` does not match a
prefix.

This function is generic over all currently supported patterns.

Examples:

* `"red green blue".toSlice.dropSuffix " blue" == "red green".toSlice`

* `"red green blue".toSlice.dropSuffix "bluu " == "red green blue".toSlice`

* `"red green blue".toSlice.dropSuffix 'e' == "red green blu".toSlice`

* `"red green blue".toSlice.dropSuffix Char.isLower == "red green blu".toSlice`
 -/
String.Slice.dropSuffix : {ρ : Type} → String.Slice → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → String.Slice
-- Mathlib.Topology.Connected.PathConnected
/-- The path component of the identity in an additive topological
monoid, as an additive submonoid.  -/
AddSubmonoid.pathComponentZero : (M : Type u_4) → [inst : AddMonoid M] → [inst_1 : TopologicalSpace M] → [ContinuousAdd M] → AddSubmonoid M
-- Mathlib.CategoryTheory.Monoidal.Closed.Zero
/-- If a Cartesian closed category has a zero object, each homset has exactly one element.  -/
CategoryTheory.uniqueHomsetOfZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [CategoryTheory.MonoidalClosed C] → [CategoryTheory.Limits.HasZeroObject C] → (X Y : C) → Unique (X ⟶ Y)
-- Init.SimpLemmas
Bool.and_eq_true : ∀ (a b : Bool), ((a && b) = true) = (a = true ∧ b = true)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.exists_dropn_of_mem : ∀ {α : Type u} {s : Stream'.WSeq α} {a : α}, a ∈ s → ∃ n s', some (a, s') ∈ (s.drop n).destruct
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.add_measure : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] [TopologicalSpace.PseudoMetrizableSpace ε] {f : α → ε},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable f ν → MeasureTheory.Integrable f (μ + ν)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_emptyWithCapacity : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {a : α} {c : ℕ},
  (Std.HashMap.Raw.emptyWithCapacity c)[a]? = none
-- Mathlib.Data.Fin.SuccPred
Fin.coe_succ_lt_iff_lt : ∀ {n : ℕ} {j k : Fin n}, ↑↑j < ↑↑k ↔ j < k
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.fst_inv : ∀ {α : Type u_2} [inst : CommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedMonoid α] (s : NonemptyInterval α),
  s⁻¹.toProd.1 = s.toProd.2⁻¹
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.pred.injEq : ∀ (q₁ q₂ q₁_1 q₂_1 : Turing.PartrecToTM2.Λ'), (q₁.pred q₂ = q₁_1.pred q₂_1) = (q₁ = q₁_1 ∧ q₂ = q₂_1)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Finset.exists_cycleOn : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (s : Finset α), ∃ f, f.IsCycleOn ↑s ∧ f.support ⊆ s
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
/-- Given `K ∈ ℝ` and a finite `S ⊆ G`, the connectivity `κ` of `G` with respect to `K` and `S` is
the infimum of `expansion K S A` over all finite nonempty `A ⊆ G`. Note that when `K ≤ 1`,
`expansion K S A` is nonnegative for all `A`, so the infimum exists.  -/
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.connectivity : {G : Type u_1} → [Group G] → [DecidableEq G] → ℝ → Finset G → ℝ
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicOn.meromorphicOn_closedBall_comp_sub_const_iff_meromorphicOn_closedBall`

---

`MeromorphicOn` is invariant under translation, special case where the set is a closed ball.  -/
MeromorphicOn.meromorphicOn_closedBall_fun_comp_sub_const_iff_meromorphicOn_closedBall : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {R : ℝ},
  MeromorphicOn (fun x => f (x - c)) (Metric.closedBall c R) ↔ MeromorphicOn f (Metric.closedBall 0 R)
-- Mathlib.AlgebraicGeometry.Sites.Pretopology
AlgebraicGeometry.Scheme.grothendieckTopology.eq_1 : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme),
  AlgebraicGeometry.Scheme.grothendieckTopology P = (AlgebraicGeometry.Scheme.precoverage P).toGrothendieck
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
Polynomial.valuation_X_eq_neg_one : ∀ (K : Type u_1) [inst : Field K],
  (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) (Polynomial.idealX K)) RatFunc.X = WithZero.exp (-1)