mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.of_add : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : SMul R V] [inst_2 : AddCommMonoid V]
  (x y : HahnSeries Γ V), (HahnModule.of R) (x + y) = (HahnModule.of R) x + (HahnModule.of R) y
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.opFunctor_map_τ₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : (CategoryTheory.Square C)ᵒᵖ} (φ : X ⟶ Y),
  (CategoryTheory.Square.opFunctor.map φ).τ₃ = φ.unop.τ₃.op
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.exact₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.exact₁._auto_1), (X.sc₁ f g fg h n₀ n₁ hn₁).Exact
-- Init.NotationExtra
«termExists_,_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.instHasZeroMorphismsFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (D : Type u') →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        [CategoryTheory.Limits.HasZeroMorphisms D] → CategoryTheory.Limits.HasZeroMorphisms (CategoryTheory.Functor C D)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.decidableLT : {α : Type u_1} → [inst : Preorder α] → [DecidableLT α] → DecidableLT (WithZero α)
-- Mathlib.CategoryTheory.Iso
/-- Composition of the two directions of an isomorphism is the identity on the source.  -/
CategoryTheory.Iso.hom_inv_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (self : X ≅ Y) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp self.inv h) = h
-- Mathlib.Algebra.Group.Semiconj.Units
Units.conj_pow' : ∀ {M : Type u_1} [inst : Monoid M] (u : Mˣ) (x : M) (n : ℕ), (↑u⁻¹ * x * ↑u) ^ n = ↑u⁻¹ * x ^ n * ↑u
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.orderIsoOfIso_symm_apply : ∀ {X : SSet} {A : X.Subcomplex} {Y : SSet} {B : Y.Subcomplex} (e : X ≅ Y) (hA : B.preimage e.hom = A) (y : B.N),
  (RelIso.symm (SSet.Subcomplex.N.orderIsoOfIso e hA)) y = { toN := (SSet.N.orderIsoOfIso e).symm y.toN, notMem := ⋯ }
-- Mathlib.LinearAlgebra.Dimension.Free
Module.Free.exists_linearMap_injective_of_lift_rank_lt : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  {N' : Type v'} [inst_4 : AddCommMonoid N'] [inst_5 : Module R N'],
  Cardinal.lift.{v', v} (Module.rank R M) < Cardinal.lift.{v, v'} (Module.rank R N') → ∃ f, Function.Injective ⇑f
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapConeWhisker.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C}
  {E : CategoryTheory.Functor K J} {c : CategoryTheory.Limits.Cone F},
  H.mapConeWhisker =
    CategoryTheory.Limits.Cone.ext (CategoryTheory.Iso.refl (H.mapCone (CategoryTheory.Limits.Cone.whisker E c)).pt) ⋯
-- Mathlib.Geometry.Manifold.WhitneyEmbedding
/-- Baby version of the **Whitney weak embedding theorem**: if `M` admits a finite covering by
supports of bump functions, then for some `n` it can be immersed into the `n`-dimensional
Euclidean space.  -/
SmoothBumpCovering.exists_immersion_euclidean : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E] {H : Type uH}
  [inst_3 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_4 : TopologicalSpace M]
  [inst_5 : ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] {ι : Type u_1} [Finite ι]
  (f : SmoothBumpCovering ι I M),
  ∃ n e,
    ContMDiff I (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (↑⊤) e ∧
      Function.Injective e ∧ ∀ (x : M), Function.Injective ⇑(mfderiv% e x)
-- Mathlib.MeasureTheory.PiSystem
/-- From a set of indices `S : Set ι` and a family of sets of sets `π : ι → Set (Set α)`,
define the set of sets that can be written as `⋂ x ∈ t, f x` for some finset `t ⊆ S` and sets
`f x ∈ π x`. If `π` is a family of π-systems, then it is a π-system.  -/
piiUnionInter : {α : Type u_3} → {ι : Type u_4} → (ι → Set (Set α)) → Set ι → Set (Set α)
-- Std.Internal.Do.Order.Basic
Lean.Order.iSup_le : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] {ι : Type v} (f : ι → α) (x : α),
  (∀ (i : ι), Lean.Order.PartialOrder.rel (f i) x) → Lean.Order.PartialOrder.rel (Lean.Order.iSup f) x
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.le_comap_map : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : MonoidHomClass F M N] {f : F}, S ≤ Submonoid.comap f (Submonoid.map f S)
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Combinatorial viewpoint on a composition of `n`, by seeing it as non-empty blocks of
consecutive integers in `{0, ..., n-1}`. We register every block by its left end-point, yielding
a finset containing `0`. As this does not make sense for `n = 0`, we add `n` to this finset, and
get a finset of `{0, ..., n}` containing `0` and `n`. This is the data in the structure
`CompositionAsSet n`.  -/
CompositionAsSet : ℕ → Type
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.ite_then_not_ite'' : ∀ {w : ℕ} (c0 c1 : Bool) {a b : BitVec w},
  (bif c0 then ~~~bif c1 then b else ~~~a else a) = bif c0 && c1 then ~~~b else a
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.rightComm_symm_tmul : ∀ (R : Type uR) {S : Type uS} (B : Type uB) {M : Type uM} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R]
  [inst_1 : Semiring B] [inst_2 : Algebra R B] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module B M]
  [inst_6 : IsScalarTower R B M] [inst_7 : AddCommMonoid P] [inst_8 : AddCommMonoid Q] [inst_9 : Module R Q]
  [inst_10 : CommSemiring S] [inst_11 : Module S M] [inst_12 : Module S P] [inst_13 : Algebra S B]
  [inst_14 : IsScalarTower S B M] [inst_15 : SMulCommClass R S M] [inst_16 : SMulCommClass S R M] (m : M) (p : P)
  (q : Q), (TensorProduct.AlgebraTensorModule.rightComm R S B M P Q).symm (m ⊗ₜ[R] q ⊗ₜ[S] p) = m ⊗ₜ[S] p ⊗ₜ[R] q
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.fst_iso_of_right_embedding_range_subset : ∀ {X Y S : TopCat} (f : X ⟶ S) {g : Y ⟶ S},
  Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom g) →
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom f) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom g) →
      CategoryTheory.IsIso (CategoryTheory.Limits.pullback.fst f g)
-- Init.Data.UInt.Lemmas
UInt64.toNat_one : UInt64.toNat 1 = 1
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Reinterpret `f : α → β` as an element of `α →ᵤ[𝔖] β`.  -/
UniformOnFun.ofFun : {α : Type u_1} → {β : Type u_2} → (𝔖 : Set (Set α)) → (α → β) ≃ UniformOnFun α β 𝔖
-- Mathlib.Order.RelSeries
RelSeries.snoc_cast_castSucc : ∀ {α : Type u_1} {r : SetRel α α} (s : RelSeries r) (a : α) (h : (s.last, a) ∈ r) (i : Fin (s.length + 1)),
  (s.snoc a h).toFun (Fin.cast ⋯ i.castSucc) = s.toFun i
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_lt_rpow_left_iff_of_base_lt_one : ∀ {x y z : ℝ}, 0 < x → x < 1 → (x ^ y < x ^ z ↔ z < y)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.zoom_toList : ∀ {α : Type u_1} {cut : α → Ordering} {t' : RBTree.RBNode α} {p' : RBTree.RBNode.Path α} {t : RBTree.RBNode α},
  RBTree.RBNode.zoom cut t = (t', p') → p'.withList t'.toList = t.toList
-- Mathlib.ModelTheory.Topology.Types
_private.Mathlib.ModelTheory.Topology.Types.0.CompleteType.instCompactSpaceCompleteType : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type u_1}, CompactSpace (T.CompleteType α)
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.mk.sizeOf_spec : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : SizeOf G] (toFun : TopologicalSpace.Compacts G → NNReal)
  (mono' : ∀ (K₁ K₂ : TopologicalSpace.Compacts G), ↑K₁ ⊆ ↑K₂ → toFun K₁ ≤ toFun K₂)
  (sup_disjoint' :
    ∀ (K₁ K₂ : TopologicalSpace.Compacts G),
      Disjoint ↑K₁ ↑K₂ → IsClosed ↑K₁ → IsClosed ↑K₂ → toFun (K₁ ⊔ K₂) = toFun K₁ + toFun K₂)
  (sup_le' : ∀ (K₁ K₂ : TopologicalSpace.Compacts G), toFun (K₁ ⊔ K₂) ≤ toFun K₁ + toFun K₂),
  sizeOf { toFun := toFun, mono' := mono', sup_disjoint' := sup_disjoint', sup_le' := sup_le' } = 1
-- Init.Data.Int.Order
Int.add_one_le_of_lt : ∀ {a b : ℤ}, a < b → a + 1 ≤ b
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.singleOneAlgHom_apply : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] (a : A), MonoidAlgebra.singleOneAlgHom a = MonoidAlgebra.single 1 a
-- Mathlib.Algebra.Group.Int.Units
Int.isUnit_iff_natAbs_eq : ∀ {u : ℤ}, IsUnit u ↔ u.natAbs = 1
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- If `L` is a `σ`-semilinear map, and `f` has Fréchet derivative `f'` at `x`, then `L ∘ f ∘ σ⁻¹`
has Fréchet derivative `L ∘ f'` at `σ x`.  -/
HasDerivAt.comp_semilinear : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {σ : 𝕜 →+* 𝕜} (σ' : 𝕜 →+* 𝕜) [RingHomIsometric σ]
  [RingHomInvPair σ σ'] {F' : Type u_1} [inst_5 : NormedAddCommGroup F'] [inst_6 : NormedSpace 𝕜 F'] (L : F →SL[σ] F'),
  HasDerivAt f f' x → HasDerivAt (⇑L ∘ f ∘ ⇑σ') (L f') (σ x)
-- Init.Data.UInt.Basic
/-- Decides whether one 64-bit unsigned integer is strictly less than another. Usually accessed via the
`DecidableLT UInt64` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `(if (6 : UInt64) < 7 then "yes" else "no") = "yes"`
 * `(if (5 : UInt64) < 5 then "yes" else "no") = "no"`
 * `show ¬((7 : UInt64) < 7) by decide`
 -/
UInt64.decLt : (a b : UInt64) → Decidable (a < b)
-- Mathlib.Analysis.Complex.Norm
Complex.norm_mul : ∀ (z w : ℂ), ‖z * w‖ = ‖z‖ * ‖w‖
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instBEqDSimpCacheKey.beq : Lean.Elab.Tactic.Grind.DSimpCacheKey → Lean.Elab.Tactic.Grind.DSimpCacheKey → Bool
-- Mathlib.RingTheory.Artinian.Module
Ideal.quotientInfRingEquivPiQuotient.congr_simp : ∀ {R : Type u_2} [inst : CommRing R] {ι : Type u_3} [inst_1 : Finite ι] (f : ι → Ideal R)
  (hf : Pairwise (Function.onFun IsCoprime f)),
  Ideal.quotientInfRingEquivPiQuotient f hf = Ideal.quotientInfRingEquivPiQuotient f hf
-- Mathlib.Algebra.Polynomial.HasseDeriv
Polynomial.natDegree_hasseDeriv : ∀ {R : Type u_1} [inst : Semiring R] [IsAddTorsionFree R] (p : Polynomial R) (n : ℕ),
  ((Polynomial.hasseDeriv n) p).natDegree = p.natDegree - n
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.conePointsIsoOfEquivalence_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  {s : CategoryTheory.Limits.Cone F} {G : CategoryTheory.Functor K C} {t : CategoryTheory.Limits.Cone G}
  (P : CategoryTheory.Limits.IsLimit s) (Q : CategoryTheory.Limits.IsLimit t) (e : J ≌ K) (w : e.functor.comp G ≅ F),
  (P.conePointsIsoOfEquivalence Q e w).hom =
    Q.lift
      ((CategoryTheory.Limits.Cone.equivalenceOfReindexing e.symm
              ((e.inverse.isoWhiskerLeft w).symm ≪≫ e.invFunIdAssoc G)).functor.obj
        s)
-- Mathlib.Combinatorics.Additive.Dissociation
not_addDissociated_iff_exists_disjoint : ∀ {α : Type u_1} [inst : AddCommGroup α] {s : Set α},
  ¬AddDissociated s ↔ ∃ t u, ↑t ⊆ s ∧ ↑u ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ ∑ a ∈ t, a = ∑ a ∈ u, a
-- Mathlib.Order.Circular
/-- **Alias** of `btw_of_sbtw`. -/
SBtw.sbtw.btw : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c : α}, sbtw a b c → btw a b c
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.mem_sInf : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {S : Set (Submodule R M)} {x : M}, x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
-- Mathlib.Analysis.Fourier.AddCircle
coeFn_fourierLp : ∀ {T : ℝ} [hT : Fact (0 < T)] (p : ENNReal) [inst : Fact (1 ≤ p)] (n : ℤ),
  ↑↑(fourierLp p n) =ᵐ[AddCircle.haarAddCircle] ⇑(fourier n)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.lift_tprod : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)], PiTensorProduct.lift (PiTensorProduct.tprod R) = LinearMap.id
-- Mathlib.Analysis.Complex.Norm
Complex.norm_eq_zero_iff : ∀ {z : ℂ}, ‖z‖ = 0 ↔ z = 0
-- Mathlib.CategoryTheory.Presentable.Directed
/-- Given a `κ`-bounded diagram `D` in a category `J`, an object `e : J`
is terminal if `𝟙 e` belongs to `D` and for any object `j` of `D`,
there is a unique morphism `j ⟶ e` in `D`, such that these unique morphisms
are compatible with precomposition with morphisms in `D`.  -/
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal : {J : Type w} →
  [inst : CategoryTheory.SmallCategory J] →
    {κ : Cardinal.{w}} → CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ → J → Type w
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.smul_finset_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {a : α} (b : β), a • {b} = {a • b}
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
OpenPartialHomeomorph.symm_map_nhds_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X}, x ∈ e.source → Filter.map (↑e.symm) (nhds (↑e x)) = nhds x
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
ProbabilityTheory.condCDF_eq_stieltjesOfMeasurableRat_unit_prod : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (a : α),
  ProbabilityTheory.condCDF ρ a =
    ProbabilityTheory.stieltjesOfMeasurableRat (fun p r => (ProbabilityTheory.preCDF ρ r p.2).toReal) ⋯ ((), a)
-- Mathlib.Data.Finset.Prod
Finset.diag_union_offDiag : ∀ {α : Type u_1} (s : Finset α) [inst : DecidableEq α], s.diag ∪ s.offDiag = s ×ˢ s
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveElabStep3.mk : Lean.Elab.TermElabM Unit → Lean.Elab.Command.InductiveElabStep3
-- Mathlib.Order.Bounds.Basic
SemilatticeInf.ofIsGLB.eq_1 : ∀ {α : Type u_1} [inst : PartialOrder α] (sup : α → α → α) (isLUB_pair : ∀ (a b : α), IsGLB {a, b} (sup a b)),
  SemilatticeInf.ofIsGLB sup isLUB_pair =
    { toPartialOrder := inst, inf := sup, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.foldl_push_apply : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {l : Std.DHashMap.Internal.AssocList α β} {acc : Array δ}
  (f : (a : α) → β a → δ),
  Std.DHashMap.Internal.AssocList.foldl (fun acc k v => acc.push (f k v)) acc l =
    acc ++ Array.map (fun p => f p.fst p.snd) l.toList.toArray
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_neg : ∀ {x : ℝ}, 0 < x → x < 1 → Real.log x < 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.mul_lt_one'`.

---

Assumes left covariance.
The lemma assuming right covariance is `Right.mul_lt_one'`.  -/
mul_lt_one' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b : α}, a < 1 → b < 1 → a * b < 1
-- Init.Data.UInt.Lemmas
UInt8.add_eq_left : ∀ {a b : UInt8}, a + b = a ↔ b = 0
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.hasExitPoint : Lean.Elab.Term.Do.Code → Bool
-- Std.Sync.Channel
/-- `for msg in ch.sync do ...` receives all messages in the channel until it is closed.  -/
Std.CloseableChannel.Sync.instForInOfMonadOfMonadLiftTBaseIO : {m : Type → Type u_1} → {α : Type} → [Monad m] → [MonadLiftT BaseIO m] → ForIn m (Std.CloseableChannel.Sync α) α
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.setBody : Lean.IR.FnBody → Lean.IR.FnBody → Lean.IR.FnBody
-- Mathlib.Data.Sign.Defs
SignType.one_le_iff : ∀ {a : SignType}, 1 ≤ a ↔ a = 1
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
is_ideal_adic_pow : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] {J : Ideal R},
  IsAdic J → ∀ {n : ℕ}, 0 < n → IsAdic (J ^ n)
-- Mathlib.Order.Hom.Lattice
SupHom.instOrderBot : {α : Type u_2} → {β : Type u_3} → [inst : Max α] → [inst_1 : SemilatticeSup β] → [OrderBot β] → OrderBot (SupHom α β)
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.trW_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) {X Y : C} (f : X ⟶ Y),
  P.trW f ↔
    ∃ Z g h,
      ∃ (_ : CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
        P Z
-- Mathlib.Order.Hom.WithTopBot
OrderIso.withTopCongr_refl : ∀ {α : Type u_1} [inst : PartialOrder α], (OrderIso.refl α).withTopCongr = OrderIso.refl (WithTop α)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.Mk₁.map.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X₀ X₁ : C} (f f_1 : X₀ ⟶ X₁),
  f = f_1 →
    ∀ (i j : Fin 2) (x : i ≤ j),
      CategoryTheory.ComposableArrows.Mk₁.map f i j x = CategoryTheory.ComposableArrows.Mk₁.map f_1 i j x
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtensionAt.ι_isoColimit_hom : ∀ {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} {E : L.LeftExtension F} {Y : D}
  (h : E.IsPointwiseLeftKanExtensionAt Y)
  [inst_3 : CategoryTheory.Limits.HasColimit ((CategoryTheory.CostructuredArrow.proj L Y).comp F)]
  (g : CategoryTheory.CostructuredArrow L Y),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.hom E).app g.left)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.StructuredArrow.right E).map g.hom) h.isoColimit.hom) =
    CategoryTheory.Limits.colimit.ι ((CategoryTheory.CostructuredArrow.proj L Y).comp F) g
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_const_iff_enorm : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {c : ε},
  ‖c‖ₑ ≠ ⊤ → (MeasureTheory.Integrable (fun x => c) μ ↔ ‖c‖ₑ = 0 ∨ MeasureTheory.IsFiniteMeasure μ)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.indexEquiv_apply_isComplex_fst : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (w : { w // w.IsComplex }),
  (NumberField.mixedEmbedding.indexEquiv K) (Sum.inr (w, 0)) = (↑w).embedding
-- Mathlib.NumberTheory.NumberField.FractionalIdeal
NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule : ∀ (K : Type u_1) [inst : Field K] [NumberField K]
  (I : FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K), Module.Free ℤ ↥↑I
-- Mathlib.CategoryTheory.Filtered.Basic
/-- Given a "bowtie" of morphisms
```
 j₁   j₂
 |\  /|
 | \/ |
 | /\ |
 |/  \∣
 vv  vv
 k₁  k₂
```
in a filtered category, we can construct an object `s` and two morphisms from `k₁` and `k₂` to `s`,
making the resulting squares commute.
 -/
CategoryTheory.IsFiltered.bowtie : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {j₁ j₂ k₁ k₂ : C}
  (f₁ : j₁ ⟶ k₁) (g₁ : j₁ ⟶ k₂) (f₂ : j₂ ⟶ k₁) (g₂ : j₂ ⟶ k₂),
  ∃ s α β,
    CategoryTheory.CategoryStruct.comp f₁ α = CategoryTheory.CategoryStruct.comp g₁ β ∧
      CategoryTheory.CategoryStruct.comp f₂ α = CategoryTheory.CategoryStruct.comp g₂ β
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_filterMapM : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [LawfulMonad m]
  [WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {f : β → m (Option γ)}
  (it : Std.IterM Id β), (Std.IterM.filterMapM f it).toList = List.filterMapM f it.toList.run
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.C_two : CartanMatrix.C 2 = !![2, -1; -2, 2]
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.num.injEq : ∀ (v v_1 : ℤ), (Int.Internal.Linear.Expr.num v = Int.Internal.Linear.Expr.num v_1) = (v = v_1)
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Equiv.id_indexEquiv_symm_apply : ∀ {ι : 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) (a : ι),
  (↑(RootPairing.Equiv.id P)).indexEquiv.symm a = a
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
/-- This is [grinberg_clifford_2016] Theorem 6  -/
CliffordAlgebra.contractLeft_ι_mul : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (d : Module.Dual R M) (a : M) (b : CliffordAlgebra Q),
  (CliffordAlgebra.contractLeft d) ((CliffordAlgebra.ι Q) a * b) =
    d a • b - (CliffordAlgebra.ι Q) a * (CliffordAlgebra.contractLeft d) b
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The Galois insertion formed by `affineSpan` and coercion back to a set.  -/
AffineSubspace.gi : (k : Type u_1) →
  (V : Type u_2) →
    (P : Type u_3) →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] → [S : AddTorsor V P] → GaloisInsertion (affineSpan k) SetLike.coe
-- Mathlib.Algebra.Module.ZLattice.Covolume
ZLattice.volume_image_eq_volume_div_covolume : ∀ {ι : Type u_2} [inst : Fintype ι] (L : Submodule ℤ (ι → ℝ)) [inst_1 : DiscreteTopology ↥L] [inst_2 : IsZLattice ℝ L]
  (b : Module.Basis ι ℤ ↥L) {s : Set (ι → ℝ)},
  MeasureTheory.volume (⇑(Module.Basis.ofZLatticeBasis ℝ L b).equivFun '' s) =
    MeasureTheory.volume s / ENNReal.ofReal (ZLattice.covolume L MeasureTheory.volume)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.isHashSelf_eraseₘaux : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α β) (a : α),
  Std.DHashMap.Internal.Raw.WFImp ↑m → Std.DHashMap.Internal.IsHashSelf (↑(m.eraseₘaux a)).buckets
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {km : α},
  t.minKey? = some km → t.getKey? km = some km
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.anyM_pure : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {p : β → Bool},
  Std.Iter.anyM (fun x => pure (p x)) it = pure (Std.Iter.any (fun x => p x) it)
-- Mathlib.CategoryTheory.CatCommSq
CategoryTheory.CatCommSq.iso_hom_naturality : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] (T : CategoryTheory.Functor C₁ C₂) (L : CategoryTheory.Functor C₁ C₃)
  (R : CategoryTheory.Functor C₂ C₄) (B : CategoryTheory.Functor C₃ C₄) [h : CategoryTheory.CatCommSq T L R B]
  {x y : C₁} (f : x ⟶ y),
  CategoryTheory.CategoryStruct.comp (R.map (T.map f)) ((CategoryTheory.CatCommSq.iso T L R B).hom.app y) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso T L R B).hom.app x) (B.map (L.map f))