mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instIsMonHomμ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : CategoryTheory.BraidedCategory C]
  [inst_5 : CategoryTheory.BraidedCategory D] [inst_6 : F.LaxBraided] (M N : C) [inst_7 : CategoryTheory.MonObj M]
  [inst_8 : CategoryTheory.MonObj N], CategoryTheory.IsMonHom (CategoryTheory.Functor.LaxMonoidal.μ F M N)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.isoMk₀_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 0}
  (e :
    F.obj' 0 CategoryTheory.ComposableArrows.homMk₀._proof_1 ≅ G.obj' 0 CategoryTheory.ComposableArrows.homMk₀._proof_1)
  (i : Fin (0 + 1)),
  (CategoryTheory.ComposableArrows.isoMk₀ e).inv.app i =
    match i with
    | ⟨0, isLt⟩ => e.inv
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.MulStruct.δ_succ_succ_map_assoc : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g fg : X.PtSimplex n x} {i : Fin n}
  (self : f.MulStruct g fg i) {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ.succ) (CategoryTheory.CategoryStruct.comp self.map h) =
    CategoryTheory.CategoryStruct.comp f.map h
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformGroup.uniformContinuous_div : ∀ {α : Type u_3} {inst : UniformSpace α} {inst_1 : Group α} [self : IsUniformGroup α],
  UniformContinuous fun p => p.1 / p.2
-- Mathlib.NumberTheory.Pell
/-- If `d` is a positive integer that is not a square, then there is a nontrivial solution
to the Pell equation `x^2 - d*y^2 = 1`.  -/
Pell.exists_of_not_isSquare : ∀ {d : ℤ}, 0 < d → ¬IsSquare d → ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.pairwise_toList_upwardEnumerableLt : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α], List.Pairwise (fun a b => Std.PRange.UpwardEnumerable.LT a b) r.toList
-- Mathlib.Order.Interval.Set.Basic
Set.left_notMem_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ∉ Set.Ioc a b
-- Init.Data.Int.Gcd
Int.gcd_self : ∀ {a : ℤ}, a.gcd a = a.natAbs
-- Mathlib.Order.Heyting.Basic
Prod.instCompl.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Compl α] [inst_1 : Compl β], Prod.instCompl = { compl := fun a => (a.1ᶜ, a.2ᶜ) }
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given an AddMonoidHom `f : M →+ N` and Submonoid `S ⊆ M` such that `f(S) ⊆ AddUnits N`, for all
`w, z : N` and `y ∈ S`, we have `w - f y = z ↔ w = f y + z`.  -/
AddSubmonoid.LocalizationMap.add_neg_left : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {f : M →+ N}
  (h : ∀ (y : ↥S), IsAddUnit (f ↑y)) (y : ↥S) (w z : N),
  w + ↑(-(IsAddUnit.liftRight (f.domRestrict S) h) y) = z ↔ w = f ↑y + z
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeSemigroup.toFreeMonoid_of : ∀ {α : Type u_1} (x : α), FreeSemigroup.toFreeMonoid (FreeSemigroup.of x) = FreeMonoid.of x
-- Init.Data.UInt.Lemmas
UInt16.ofFin_mul : ∀ (a b : Fin UInt16.size), UInt16.ofFin (a * b) = UInt16.ofFin a * UInt16.ofFin b
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.affineSpan_faceOpposite_eq_orthRadius_insphere : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) [Fact (Module.finrank ℝ V = n)]
  (i : Fin (n + 1)), affineSpan ℝ (Set.range (s.faceOpposite i).points) = s.insphere.orthRadius (s.touchpoint ∅ i)
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.isoEquivBialgEquiv_symm_apply : ∀ {R : Type u} [inst : CommRing R] {X Y : Type v} [inst_1 : CommRing X] [inst_2 : Bialgebra R X] [inst_3 : CommRing Y]
  [inst_4 : Bialgebra R Y] (e : X ≃ₐc[R] Y), CommBialgCat.isoEquivBialgEquiv.symm e = CommBialgCat.isoMk e
-- Init.Data.Array.BasicAux
_private.Init.Data.Array.BasicAux.0.List.toArrayAux.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Array α → Sort u_2) (xs : Array α) (h_1 : (xs : Array α) → motive [] xs)
  (h_2 : (a : α) → (as : List α) → (xs : Array α) → motive (a :: as) xs),
  (match [], xs with
    | [], xs => h_1 xs
    | a :: as, xs => h_2 a as xs) =
    h_1 xs
-- Mathlib.Order.Category.PartOrd
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
PartOrd.Hom.Simps.hom : (X Y : PartOrd) → X.Hom Y → ↑X →o ↑Y
-- Mathlib.Algebra.Order.Archimedean.Class
/-- The product over a set of an elements in distinct classes is in the lowest class.  -/
MulArchimedeanClass.mk_prod : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {ι : Type u_2}
  [inst_3 : LinearOrder ι] {s : Finset ι} (hnonempty : s.Nonempty) {a : ι → M},
  StrictMonoOn (MulArchimedeanClass.mk ∘ a) ↑s →
    MulArchimedeanClass.mk (∏ i ∈ s, a i) = MulArchimedeanClass.mk (a (s.min' hnonempty))
-- Mathlib.Topology.Algebra.Group.Matrix
/-- The natural map from `SL n A` to `GL n A` is inducing, i.e. the topology on
`SL n A` is the pullback of the topology from `GL n A`.  -/
Matrix.SpecialLinearGroup.isInducing_toGL : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [IsTopologicalRing R], Topology.IsInducing ⇑Matrix.SpecialLinearGroup.toGL
-- Mathlib.GroupTheory.Commensurable
AddSubgroup.Commensurable.equivalence : ∀ {G : Type u_1} [inst : AddGroup G], Equivalence AddSubgroup.Commensurable
-- Mathlib.Tactic.ITauto
/-- `⊢ ⊤`  -/
Mathlib.Tactic.ITauto.Proof.triv : Mathlib.Tactic.ITauto.Proof
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.ext_iff : ∀ {G : Type u} {inst : AddGroup G} {inst_1 : TopologicalSpace G} {x y : OpenNormalAddSubgroup G},
  x = y ↔ (↑x.toOpenAddSubgroup).carrier = (↑y.toOpenAddSubgroup).carrier
-- Mathlib.Combinatorics.SimpleGraph.Dart
SimpleGraph.Dart.symm_symm : ∀ {V : Type u_1} {G : SimpleGraph V} (d : G.Dart), d.symm.symm = d
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of the forward direction of `SimpleGraph.Walk.isTrail_mapLe`. -/
SimpleGraph.Walk.IsTrail.of_mapLe : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v},
  (SimpleGraph.Walk.mapLe h p).IsTrail → p.IsTrail
-- Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean
NNReal.le_gm_and_am_le : ∀ {x y : NNReal}, x ≤ y → x ≤ NNReal.sqrt (x * y) ∧ (x + y) / 2 ≤ y
-- Mathlib.Analysis.Calculus.Deriv.Slope
/-- The derivative of a monotone function is nonnegative.  -/
Monotone.deriv_nonneg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [OrderTopology 𝕜] {g : 𝕜 → 𝕜}, Monotone g → 0 ≤ deriv g x
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.equivalence_functor : ∀ {I : Type u₁} {J : Type u₂} (e : I ≃ J),
  (CategoryTheory.Discrete.equivalence e).functor = CategoryTheory.Discrete.functor (CategoryTheory.Discrete.mk ∘ ⇑e)
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- **Alias** of `MonoidAlgebra.mapAlgHom_single`. -/
MonoidAlgebra.mapRangeAlgHom_single : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Monoid M] (f : A →ₐ[R] B) (m : M)
  (a : A), (MonoidAlgebra.mapAlgHom M f) (MonoidAlgebra.single m a) = MonoidAlgebra.single m (f a)
-- Std.Internal.UV.System
/-- Gets information about the current user's group.
 -/
Std.Internal.UV.System.osGetGroup : UInt64 → IO (Option Std.Internal.UV.System.GroupInfo)
-- Init.Grind.Norm
Lean.Grind.smul_int_eq_mul : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (i : ℤ) (a : α), i • a = ↑i * a
-- Mathlib.Data.Seq.Computation
/-- `length s` gets the number of steps of a terminating computation  -/
Computation.length : {α : Type u} → (s : Computation α) → [h : s.Terminates] → ℕ
-- Init.Data.BitVec.Lemmas
BitVec.xor_eq_zero_iff : ∀ {w : ℕ} {x y : BitVec w}, x ^^^ y = 0#w ↔ x = y
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_mul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] (s t : Finset α), ↑(s * t) = ↑s * ↑t
-- Mathlib.Topology.Homotopy.Equiv
Homeomorph.symm_toHomotopyEquiv : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  h.symm.toHomotopyEquiv = h.toHomotopyEquiv.symm
-- Mathlib.Topology.Category.TopCat.Sphere
/-- `𝔹 n` denotes the `n`-ball, the interior of the `n`-disk.  -/
TopCat.term𝔹_ : Lean.ParserDescr
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.iUnion_subset : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), π.iUnion ⊆ ↑I
-- Init.System.ST
ST.Out.state : {σ α : Type} → ST.Out σ α → Void σ
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsDenseSubsite.isLocallyFull : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D)
  [CategoryTheory.Functor.IsDenseSubsite J K G], G.IsLocallyFull K
-- Std.Time.Time.Unit.Millisecond
Std.Time.Millisecond.instDecidableLeOrdinal : {x y : Std.Time.Millisecond.Ordinal} → Decidable (x ≤ y)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.trans_symm_cancel_left : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [inst_6 : RingHomInvPair σ₁₃ σ₃₁]
  [inst_7 : RingHomInvPair σ₃₁ σ₁₃] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃}
  [inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
  [inst_10 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] [inst_11 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (e : M₁ ≃ₛₗ[σ₁₂] M₂)
  (f : M₁ ≃ₛₗ[σ₁₃] M₃), e.trans (e.symm.trans f) = f
-- Mathlib.Data.Part
Part.instMod : {α : Type u_1} → [Mod α] → Mod (Part α)
-- Mathlib.RingTheory.MvPowerSeries.GaussNorm
MvPowerSeries.gaussNorm_add_le_max : ∀ {R : Type u_1} {σ : Type u_2} (v : R → ℝ) (c : σ → ℝ) [inst : Semiring R] (f g : MvPowerSeries σ R),
  0 ≤ c →
    (∀ (a : R), v a ≥ 0) →
      IsNonarchimedean v →
        MvPowerSeries.HasGaussNorm v c f →
          MvPowerSeries.HasGaussNorm v c g →
            MvPowerSeries.gaussNorm v c (f + g) ≤ max (MvPowerSeries.gaussNorm v c f) (MvPowerSeries.gaussNorm v c g)
-- Init.Omega.IntList
Lean.Omega.IntList.mul_nil_left : ∀ {ys : List ℤ}, [] * ys = []
-- Aesop.RuleTac.Basic
/-- A `RuleTac` which generates only a single `RuleApplication`.
 -/
Aesop.SingleRuleTac : Type
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.Hom.residueFieldMap_congr'_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} {x₁ x₂ : ↥X} (e : x₁ = x₂) {Z : CommRingCat} (h : X.residueField x₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x₁)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr e).hom h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).hom
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x₂) h)
-- Mathlib.CategoryTheory.Monad.Algebra
/-- Compatibility with the structure morphism, for a morphism of coalgebras.  -/
CategoryTheory.Comonad.Coalgebra.Hom.h : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} {A B : G.Coalgebra}
  (self : A.Hom B),
  CategoryTheory.CategoryStruct.comp A.a (G.map self.f) = CategoryTheory.CategoryStruct.comp self.f B.a
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Cell.getEntry?.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (p : (a : α) × β a)
  (h_1 : Unit → motive none) (h_2 : (p : (a : α) × β a) → motive (some p)),
  (match some p with
    | none => h_1 ()
    | some p => h_2 p) =
    h_2 p
-- Mathlib.RingTheory.WittVector.Isocrystal
/-- Type synonym for `K(p, k)` to carry the standard 1-dimensional isocrystal structure
of slope `m : ℤ`.
 -/
WittVector.StandardOneDimIsocrystal : (p : ℕ) → [Fact (Nat.Prime p)] → (k : Type u_1) → [CommRing k] → ℤ → Type u_1
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.closure_pow : ∀ {M : Type u_3} [inst : Monoid M] {s : Set M} {n : ℕ}, 1 ∈ s → n ≠ 0 → Submonoid.closure (s ^ n) = Submonoid.closure s
-- Mathlib.Algebra.Order.Ring.Archimedean
ArchimedeanClass.instNeg : {R : Type u_1} → [inst : LinearOrder R] → [inst_1 : Field R] → [inst_2 : IsOrderedRing R] → Neg (ArchimedeanClass R)
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
mabs_eq_one : ∀ {α : Type u_1} [inst : Group α] [inst_1 : LinearOrder α] [MulLeftMono α] {a : α} [MulRightMono α], |a|ₘ = 1 ↔ a = 1
-- Init.System.ST
instMonadEST : (ε σ : Type) → Monad (EST ε σ)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.CommSemiring.toSemiring : Lean.Meta.Grind.Arith.CommRing.CommSemiring → Lean.Meta.Grind.Arith.CommRing.Semiring
-- Mathlib.Analysis.Complex.Circle
Circle.exp_pi_ne_one : Circle.exp Real.pi ≠ 1
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
/-- The morphism in simplicial homology that is induced by a morphism
of simplicial sets.  -/
SSet.homologyMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        {X Y : SSet} →
          (X ⟶ Y) →
            (R : C) → [inst_3 : CategoryTheory.CategoryWithHomology C] → (n : ℕ) → X.homology R n ⟶ Y.homology R n
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.tendsto_approxOn : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α]
  [inst_2 : OpensMeasurableSpace α] [inst_3 : MeasurableSpace β] {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α}
  (h₀ : y₀ ∈ s) [inst_4 : TopologicalSpace.SeparableSpace ↑s] {x : β},
  f x ∈ closure s →
    Filter.Tendsto (fun n => (MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x) Filter.atTop (nhds (f x))
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : TopologicalSpace α] (μ : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] (c : NNReal), MeasureTheory.IsFiniteMeasureOnCompacts (c • μ)
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.touchpoint_map : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {V₂ : Type u_3} {P₂ : Type u_4} [inst_4 : NormedAddCommGroup V₂]
  [inst_5 : InnerProductSpace ℝ V₂] [inst_6 : MetricSpace P₂] [inst_7 : NormedAddTorsor V₂ P₂] {n : ℕ}
  [inst_8 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ (f : P →ᵃⁱ[ℝ] P₂) (i : Fin (n + 1)), (s.map f.toAffineMap ⋯).touchpoint signs i = f (s.touchpoint signs i)
-- Init.Control.StateCps
StateCpsT.runK_bind_set : ∀ {σ : Type u} {m : Type u → Type v} {β γ : Type u} (f : PUnit.{u + 1} → StateCpsT σ m β) (s s' : σ) (k : β → σ → m γ),
  (set s' >>= f).runK s k = (f PUnit.unit).runK s' k
-- Mathlib.Data.Seq.Defs
Stream'.Seq.eq_or_mem_of_mem_cons : ∀ {α : Type u} {a b : α} {s : Stream'.Seq α}, a ∈ Stream'.Seq.cons b s → a = b ∨ a ∈ s
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- This is an internal lemma used inside the default of `PseudoMetricSpace.edist`.  -/
_private.Mathlib.Topology.MetricSpace.Pseudo.Defs.0.dist_nonneg' : ∀ {α : Sort u_3} {x y : α} (dist : α → α → ℝ),
  (∀ (x : α), dist x x = 0) →
    (∀ (x y : α), dist x y = dist y x) → (∀ (x y z : α), dist x z ≤ dist x y + dist y z) → 0 ≤ dist x y
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.closure_eq_of_le : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) {k : Set G}, k ⊆ ↑K → K ≤ Subgroup.closure k → Subgroup.closure k = K
-- Mathlib.Computability.Primrec.Basic
Primcodable.ofDenumerable : (α : Type u_1) → [Denumerable α] → Primcodable α
-- Lean.Meta.Constructions.CtorElim
_private.Lean.Meta.Constructions.CtorElim.0.Lean.withMkPULiftUp : Lean.Expr → (Lean.Expr → Lean.MetaM Lean.Expr) → Lean.MetaM Lean.Expr
-- Init.Data.Int.DivMod.Lemmas
Int.mul_ediv_cancel_of_dvd : ∀ {a b : ℤ}, b ∣ a → b * (a / b) = a
-- Mathlib.Data.Finset.Basic
Finset.Nonempty.not_empty_toList : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → ¬s.toList.isEmpty = true
-- Mathlib.Data.Fintype.Sum
/-- Any injection from a finset `s` in a fintype `α` to a finset `t` of the same cardinality as `α`
can be extended to a bijection between `α` and `t`.  -/
Finset.exists_equiv_extend_of_card_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] {t : Finset β},
  Fintype.card α = t.card →
    ∀ {s : Finset α} {f : α → β}, Finset.image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.comp_one : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : MulOne M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (f : N →* P), f.comp 1 = 1
-- Mathlib.Algebra.CharP.MixedCharZero
_private.Mathlib.Algebra.CharP.MixedCharZero.0.EqualCharZero.coePNatUnits : {R : Type u_1} → [inst : CommRing R] → [Fact (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I))] → Coe ℕ+ Rˣ
-- Init.Data.BitVec.Lemmas
BitVec.cpopNatRec_cast_eq_of_eq : ∀ {w v n : ℕ} {x : BitVec w} (p : w = v), (BitVec.cast p x).cpopNatRec n = x.cpopNatRec n
-- Mathlib.CategoryTheory.Triangulated.Triangulated
/-- An octahedron is a type of datum whose existence is asserted by the
octahedron axiom (TR 4). The input is given by the following diagram:
```
     u₁₃      v₂₃
  X₁ ────> X₃ ────> Z₂₃       Z₁₂⟦1⟧
   \      ^ \        \       ^
 u₁₂\ u₂₃/   \v₁₃     \w₂₃  /v₁₂⟦1⟧'
     V  /     V        V   /
      X₂       Z₁₃       X₂⟦1⟧
       \        \        ^
     v₁₂\        \w₁₃   /u₁₂⟦1⟧'
         V        V    /
          Z₁₂ ───> X₁⟦1⟧
              w₁₂
```
where `u₁₂ ≫ u₂₃ = u₁₃` and `(u₁₂,v₁₂,w₁₂), (u₁₃,v₁₃,w₁₃)` and `(u₂₃,v₂₃,w₂₃)`
are distinguished triangles.. An `Octahedron` for this data consists of
maps `m₁ : Z₁₂ ⟶ Z₁₃` and `m₃ : Z₁₃ ⟶ Z₂₃` such that `(m₁, m₃, w₂₃ ≫ v₁₂⟦1⟧')` is
a distinguished triangle and the completed diagram commutes:
```
     u₁₃      v₂₃
  X₁ ────> X₃ ────> Z₂₃ ────> Z₁₂⟦1⟧
   \      ^ \      ^  \       ^
 u₁₂\ u₂₃/   \v₁₃ /m₃  \w₂₃  /v₁₂⟦1⟧'
     V  /     V  /       V   /
      X₂       Z₁₃       X₂⟦1⟧
       \      ^  \        ^
     v₁₂\    /m₁  \w₁₃   /u₁₂⟦1⟧'
         V  /      V    /
          Z₁₂ ───> X₁⟦1⟧
              w₁₂
```
 -/
CategoryTheory.Triangulated.Octahedron : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} →
                {u₁₂ : X₁ ⟶ X₂} →
                  {u₂₃ : X₂ ⟶ X₃} →
                    {u₁₃ : X₁ ⟶ X₃} →
                      CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃ →
                        {v₁₂ : X₂ ⟶ Z₁₂} →
                          {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                            CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈
                                CategoryTheory.Pretriangulated.distinguishedTriangles →
                              {v₂₃ : X₃ ⟶ Z₂₃} →
                                {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂} →
                                  CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈
                                      CategoryTheory.Pretriangulated.distinguishedTriangles →
                                    {v₁₃ : X₃ ⟶ Z₁₃} →
                                      {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                                        CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈
                                            CategoryTheory.Pretriangulated.distinguishedTriangles →
                                          Type v_1
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.distinguished_iff_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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] [hC : CategoryTheory.Pretriangulated C]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} (e : T₁ ≅ T₂),
  T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔
    T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Reinterpret an equivariant ring homomorphism as a ring homomorphism.  -/
MulSemiringActionHom.toRingHom : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {φ : M →* N} →
          {R : Type u_10} →
            [inst_2 : Semiring R] →
              [inst_3 : MulSemiringAction M R] →
                {S : Type u_12} → [inst_4 : Semiring S] → [inst_5 : MulSemiringAction N S] → (R →ₑ+*[φ] S) → R →+* S
-- Mathlib.Data.Matrix.Basis
/-- Additive maps from finite matrices are equal if they agree on the standard basis.

See note [partially-applied ext lemmas].  -/
Matrix.ext_addMonoidHom : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} {β : Type u_8} [inst : DecidableEq m] [inst_1 : DecidableEq n] [Finite m]
  [Finite n] [inst_4 : AddCommMonoid α] [inst_5 : AddCommMonoid β] ⦃f g : Matrix m n α →+ β⦄,
  (∀ (i : m) (j : n), f.comp (Matrix.singleAddMonoidHom i j) = g.comp (Matrix.singleAddMonoidHom i j)) → f = g
-- Mathlib.Topology.Bornology.BoundedOperation
instBoundedMul : ∀ {R : Type u_1} [inst : NonUnitalSeminormedRing R], BoundedMul R
-- Mathlib.Data.Sum.Order
Sum.le_def : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] {a b : α ⊕ β},
  a ≤ b ↔ Sum.LiftRel (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) a b
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- Eta-expanded form of `Function.HasTemperateGrowth.smul`

---

The product of two functions of temperate growth is again of temperate growth.

Version for scalar multiplication.  -/
Function.HasTemperateGrowth.fun_smul : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NontriviallyNormedField 𝕜]
  [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedSpace 𝕜 F] {f : E → 𝕜} {g : E → F},
  Function.HasTemperateGrowth f → Function.HasTemperateGrowth g → Function.HasTemperateGrowth fun i => f i • g i
-- Mathlib.Data.Ordmap.Ordnode
/-- Auxiliary definition for `findLt`.  -/
Ordnode.findLtAux : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → α → Ordnode α → α → α
-- Init.Data.UInt.IntToBitVec
UInt8.toBitVec32_toUSize : ∀ (n : UInt8) (h : System.Platform.numBits = 32), n.toUSize.toBitVec32 h = BitVec.setWidth 32 n.toBitVec
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.destruct_join.aux.eq_2 : ∀ {α : Type u} (s : Stream'.WSeq α) (S : Stream'.WSeq (Stream'.WSeq α)),
  Stream'.WSeq.destruct_join.aux (some (s, S)) = (s.append S.join).destruct.think
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.instSMul.eq_1 : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup G), H.instSMul = H.op.smul