mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Lemmas
Lean.Grind.dite_cond_eq_false' : ∀ {α : Sort u} {c : Prop} {x : Decidable c} {a : c → α} {b : ¬c → α} {r : α} (h₁ : c = False), b ⋯ = r → dite c a b = r
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- Expressing `HasDerivWithinAt f f' s x` in terms of `HasFDerivWithinAt`  -/
hasDerivWithinAt_iff_hasFDerivWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} [inst_4 : ContinuousSMul 𝕜 F] {f' : F},
  HasDerivWithinAt f f' s x ↔ HasFDerivWithinAt f (ContinuousLinearMap.toSpanSingleton 𝕜 f') s x
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.denseRange_comap_iff_ker_le_nilRadical : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S),
  DenseRange (PrimeSpectrum.comap f) ↔ RingHom.ker f ≤ nilradical R
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.image_zeroLocus : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U : X.Opens}
  (s : Set ↑(X.presheaf.obj (Opposite.op U))),
  ⇑f '' X.zeroLocus s =
    Y.zeroLocus (⇑(CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appIso f U).inv) '' s) ∩ Set.range ⇑f
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
Topology.ContinuousMapGeneratedBy.mk.sizeOf_spec : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [inst_1 : TopologicalSpace Y]
  {Z : Type v'} [inst_2 : TopologicalSpace Z] [inst_3 : SizeOf ι] [inst_4 : (a : ι) → SizeOf (X a)] [inst_5 : SizeOf Y]
  [inst_6 : SizeOf Z] (toFun : Y → Z) (prop : Topology.ContinuousGeneratedBy X toFun),
  sizeOf { toFun := toFun, prop := prop } = 1
-- Mathlib.Order.Basic
update_le_update_iff : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (π i)] {x y : (i : ι) → π i}
  {i : ι} {a b : π i}, Function.update x i a ≤ Function.update y i b ↔ a ≤ b ∧ ∀ (j : ι), j ≠ i → x j ≤ y j
-- Mathlib.Topology.Algebra.Group.Basic
continuousSub_of_discreteTopology : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : Sub H] [DiscreteTopology H], ContinuousSub H
-- Lean.Elab.DocString
Lean.Doc.Context.mk : Lean.Doc.SuggestionMode → Lean.Doc.Context
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roc_eq_toList_roo : ∀ {m n : ℤ}, (m<...=n).toList = (m<...n + 1).toList
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.op_whiskerLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C)
  {Y Z : C} (f : Y ⟶ Z),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).op =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft (Opposite.op X) f.op
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inlX_d_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i j k : ι) (hij : c.Rel i j) (hjk : c.Rel j k) {Z : C}
  (h : HomologicalComplex.homotopyCofiber.X φ j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inlX φ j i hij)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.d φ i j) h) =
    CategoryTheory.CategoryStruct.comp
      (-CategoryTheory.CategoryStruct.comp (F.d j k) (HomologicalComplex.homotopyCofiber.inlX φ k j hjk) +
        CategoryTheory.CategoryStruct.comp (φ.f j) (HomologicalComplex.homotopyCofiber.inrX φ j))
      h
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.Simp.DischargeWrapper : Type
-- Mathlib.Data.Prod.Basic
Prod.map_bijective : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Nonempty α] [Nonempty β] {f : α → γ} {g : β → δ},
  Function.Bijective (Prod.map f g) ↔ Function.Bijective f ∧ Function.Bijective g
-- Init.Data.BitVec.Bitblast
/-- The low `(w - wn)` bits of `n` obey the invariant for division.  -/
BitVec.DivModState.Lawful.hdiv : ∀ {w : ℕ} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w},
  BitVec.DivModState.Lawful args qr → args.n.toNat >>> qr.wn = args.d.toNat * qr.q.toNat + qr.r.toNat
-- Mathlib.Data.Bool.Basic
Bool.eq_false_eq_not_eq_true : ∀ (b : Bool), (¬b = true) = (b = false)
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.interSmallerFnₘ.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : Option ((a : α) × β a) → Sort u_3) →
      (x : Option ((a : α) × β a)) → ((kv' : (a : α) × β a) → motive (some kv')) → (Unit → motive none) → motive x
-- Mathlib.Algebra.Polynomial.Sequence
Polynomial.Sequence.mk.inj : ∀ {R : Type u_1} {inst : Semiring R} {elems' : ℕ → Polynomial R} {degree_eq' : ∀ (i : ℕ), (elems' i).degree = ↑i}
  {elems'_1 : ℕ → Polynomial R} {degree_eq'_1 : ∀ (i : ℕ), (elems'_1 i).degree = ↑i},
  { elems' := elems', degree_eq' := degree_eq' } = { elems' := elems'_1, degree_eq' := degree_eq'_1 } →
    elems' = elems'_1
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_add_toENNReal : ∀ (r : ENNReal) (n : ℕ∞), ⌊r + ↑n⌋ₑ = ⌊r⌋ₑ + n
-- Mathlib.GroupTheory.Solvable
Group.instIsSolvableSubtypeMemSubgroup : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [Group.IsSolvable G], Group.IsSolvable ↥H
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeSubtype.match_3.splitter : (motive : (n : ℕ) → (P : Fin n → Prop) → DecidablePred P → { i // P i } → Sort u_1) →
  (n : ℕ) →
    (P : Fin n → Prop) →
      (inst : DecidablePred P) →
        (i : { i // P i }) →
          ((n : ℕ) →
              (P : Fin (n + 1) → Prop) → (inst : DecidablePred P) → (hp : P 0) → motive n.succ P inst ⟨⟨0, ⋯⟩, hp⟩) →
            ((n : ℕ) →
                (P : Fin (n + 1) → Prop) →
                  (inst : DecidablePred P) →
                    (i : ℕ) → (hi : i + 1 < n + 1) → (hp : P ⟨i + 1, hi⟩) → motive n.succ P inst ⟨⟨i.succ, hi⟩, hp⟩) →
              motive n P inst i
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommAlgCat.inv_op_of_unop_hom : ∀ {R : Type u} [inst : CommRing R] {A : Type u} [inst_1 : CommRing A] [inst_2 : HopfAlgebra R A],
  CommAlgCat.Hom.hom CategoryTheory.GrpObj.inv.unop = HopfAlgebra.antipodeAlgHom R A
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k ((Fin 2 → G) → ↑A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₂ A).inv
      (CategoryTheory.CategoryStruct.comp (groupCohomology.iCocycles A 2) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH2 A).moduleCatLeftHomologyData.i
        (groupCohomology.cochainsIso₂ A).inv)
      h
-- Mathlib.Data.List.AList
AList.keys_nodup : ∀ {α : Type u} {β : α → Type v} (s : AList β), s.keys.Nodup
-- Mathlib.Probability.Distributions.Uniform
PMF.toMeasure_uniformOfFinset_apply : ∀ {α : Type u_1} {s : Finset α} (hs : s.Nonempty) (t : Set α) [inst : MeasurableSpace α],
  MeasurableSet t → (PMF.uniformOfFinset s hs).toMeasure t = ↑{x ∈ s | x ∈ t}.card / ↑s.card
-- Init.Data.UInt.Lemmas
UInt64.ofNatTruncate_finVal : ∀ (n : Fin UInt64.size), UInt64.ofNatClamp ↑n = UInt64.ofFin n
-- Mathlib.Algebra.Group.Prod
Prod.instAddCancelCommMonoid : {M : Type u_3} → {N : Type u_4} → [AddCancelCommMonoid M] → [AddCancelCommMonoid N] → AddCancelCommMonoid (M × N)
-- Mathlib.Algebra.Category.Ring.Limits
CommRingCat.forget_preservesLimits : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget CommRingCat)
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.realize_toSentence_iff_toProp : ∀ {K : Type u_2} [inst : Add K] [inst_1 : Mul K] [inst_2 : Neg K] [inst_3 : Zero K] [inst_4 : One K]
  [inst_5 : FirstOrder.Ring.CompatibleRing K] (ax : FirstOrder.Field.FieldAxiom),
  K ⊨ ax.toSentence ↔ FirstOrder.Field.FieldAxiom.toProp K ax
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- The Bochner integral is linear. Note this requires `𝕜` to be a normed division ring, in order
to ensure that for `c ≠ 0`, the function `c • f` is integrable iff `f` is. For an analogous
statement for more general rings with an *a priori* integrability assumption on `f`, see
`MeasureTheory.Integrable.integral_smul`.  -/
MeasureTheory.integral_smul : ∀ {α : Type u_1} {𝕜 : Type u_4} [inst : NormedDivisionRing 𝕜] {G : Type u_5} [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace ℝ G] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst_3 : Module 𝕜 G]
  [NormSMulClass 𝕜 G] [SMulCommClass ℝ 𝕜 G] (c : 𝕜) (f : α → G), ∫ (a : α), c • f a ∂μ = c • ∫ (a : α), f a ∂μ
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.atIdxSlow?.match_1.eq_1 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] (it : Std.Iter β)
  (motive :
    (n : ℕ) →
      ((a' : Std.Iter β) →
          (b' : ℕ) →
            InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, n⟩ →
              Option β) →
        Sort u_2)
  (recur :
    (a' : Std.Iter β) →
      (b' : ℕ) →
        InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
            (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, 0⟩ →
          Option β)
  (h_1 :
    (recur :
        (a' : Std.Iter β) →
          (b' : ℕ) →
            InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, 0⟩ →
              Option β) →
      motive 0 recur)
  (h_2 :
    (k : ℕ) →
      (recur :
          (a' : Std.Iter β) →
            (b' : ℕ) →
              InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                  (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, k + 1⟩ →
                Option β) →
        motive k.succ recur),
  (match 0, recur with
    | 0, recur => h_1 recur
    | k.succ, recur => h_2 k recur) =
    h_1 recur
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic
/-- The `n`-th rescaled Chebyshev polynomial of the first kind (Vieta–Lucas polynomial) evaluates on
`2 * cos θ` to the value `2 * cos (n * θ)`.  -/
Polynomial.Chebyshev.C_two_mul_real_cos : ∀ (θ : ℝ) (n : ℤ), Polynomial.eval (2 * Real.cos θ) (Polynomial.Chebyshev.C ℝ n) = 2 * Real.cos (↑n * θ)
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Subalgebra.rank_eq_one_iff : ∀ {F : Type u_1} {E : Type u_2} [inst : CommRing F] [StrongRankCondition F] [inst_2 : Ring E] [inst_3 : Algebra F E]
  {S : Subalgebra F E} [Nontrivial E] [Module.Free F ↥S], Module.rank F ↥S = 1 ↔ S = ⊥
-- Mathlib.FieldTheory.Minpoly.Field
/-- If a subfield `F` of `E` contains all the coefficients of `minpoly E a`, then
`minpoly F a` maps to `minpoly E a` via `algebraMap F E`.  -/
minpoly.map_algebraMap : ∀ {F : Type u_3} {E : Type u_4} {A : Type u_5} [inst : Field F] [inst_1 : Field E] [inst_2 : CommRing A]
  [inst_3 : Algebra F E] [inst_4 : Algebra E A] [inst_5 : Algebra F A] [IsScalarTower F E A] {a : A},
  IsIntegral F a →
    minpoly E a ∈ Polynomial.lifts (algebraMap F E) → Polynomial.map (algebraMap F E) (minpoly F a) = minpoly E a
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.mkImpCached.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.BinaryInput),
  aig.mkImpCached input =
    { aig := (aig.mkGateCached (input.invert false true)).aig,
      ref := (aig.mkGateCached (input.invert false true)).ref.not }
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A bicone for `P Q` which is both a limit cone and a colimit cocone.  -/
CategoryTheory.Limits.BinaryBiproduct.bicone : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (P Q : C) → [CategoryTheory.Limits.HasBinaryBiproduct P Q] → CategoryTheory.Limits.BinaryBicone P Q
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.div.inj : ∀ {k : ℤ} {y? : Option Int.Internal.Linear.Var} {c : Lean.Meta.Grind.Arith.Cutsat.EqCnstr} {k_1 : ℤ}
  {y?_1 : Option Int.Internal.Linear.Var} {c_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr},
  Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.div k y? c = Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.div k_1 y?_1 c_1 →
    k = k_1 ∧ y? = y?_1 ∧ c = c_1
-- Mathlib.Data.List.Rotate
List.Nodup.rotate_eq_self_iff : ∀ {α : Type u} {l : List α}, l.Nodup → ∀ {n : ℕ}, l.rotate n = l ↔ n % l.length = 0 ∨ l = []
-- Mathlib.CategoryTheory.Monoidal.Transport
CategoryTheory.Monoidal.instIsMonoidalTransportedSymmEquivalenceTransported : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] (e : C ≌ D),
  (CategoryTheory.Monoidal.equivalenceTransported e).symm.IsMonoidal
-- Std.Http.Data.Method
Std.Http.instInhabitedMethod.default : Std.Http.Method
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.const_toFun' : ∀ {basis : Tactic.ComputeAsymptotics.Basis} {c : ℝ},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.const basis c).toFun = fun x => c
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.monomial_le_degreeOf : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (i : σ) {f : MvPolynomial σ R} {m : σ →₀ ℕ},
  m ∈ f.support → m i ≤ MvPolynomial.degreeOf i f
-- Mathlib.Analysis.Calculus.Conformal.NormedSpace
ConformalAt.const_smul : ∀ {X : Type u_1} {Y : Type u_2} [inst : NormedAddCommGroup X] [inst_1 : NormedAddCommGroup Y] [inst_2 : NormedSpace ℝ X]
  [inst_3 : NormedSpace ℝ Y] {f : X → Y} {x : X} {c : ℝ}, c ≠ 0 → ConformalAt f x → ConformalAt (c • f) x
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Sheaf.isLocallyInjective_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] {J : CategoryTheory.GrothendieckTopology C}
  {F₁ F₂ : CategoryTheory.Sheaf J D} (φ : F₁ ⟶ F₂) [CategoryTheory.IsIso φ], CategoryTheory.Sheaf.IsLocallyInjective φ
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.neg_apply : ∀ (α : Type u) [inst : AddGroup α] [inst_1 : LE α] [inst_2 : AddLeftMono α] [inst_3 : AddRightMono α] (a : α),
  (OrderIso.neg α) a = OrderDual.toDual (-a)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.constOfIsEmpty_apply : ∀ (R : Type u_1) (M : Type u_2) {N : Type u_4} (ι : Type u_6) [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] [inst_7 : IsEmpty ι] (m : N) (a : (i : ι) → (fun x => M) i),
  (ContinuousAlternatingMap.constOfIsEmpty R M ι m) a = m
-- Mathlib.CategoryTheory.Limits.FintypeCat
CategoryTheory.Limits.FintypeCat.instFiniteObjCompFintypeCatIncl : ∀ {J : Type} [inst : CategoryTheory.SmallCategory J] (K : CategoryTheory.Functor J FintypeCat) (j : J),
  Finite ((K.comp FintypeCat.incl).obj j)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The edist to a singleton is the edistance to the single point of this singleton  -/
Metric.infEDist_singleton : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α}, Metric.infEDist x {y} = edist x y
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
add_le_mul_of_right_le_left : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [ZeroLEOneClass R] [NeZero 1] [AddLeftMono R]
  [PosMulStrictMono R], 2 ≤ b → b ≤ a → a + b ≤ a * b
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.mulEquivHaarChar_refl : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalGroup G] [inst_5 : LocallyCompactSpace G],
  MeasureTheory.mulEquivHaarChar (ContinuousMulEquiv.refl G) = 1
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.triangle_distinguished : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
  X.triangle f g ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Lean.Meta.Tactic.Grind.Types
/-- Adds a new fact `prop` with proof `proof` to the queue for preprocessing and the assertion.  -/
Lean.Meta.Grind.addNewRawFact : Lean.Expr → Lean.Expr → ℕ → Lean.Meta.Grind.SplitSource → Lean.Meta.Grind.EMatchDiagSource → Lean.Meta.Grind.GoalM Unit
-- Lean.Data.LOption
Lean.LOption.undef.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α], sizeOf Lean.LOption.undef = 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_congr : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k k' : α}, cmp k k' = Ordering.eq → t.getKey? k = t.getKey? k'
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.All.upperBound? : ∀ {α : Type u_1} {p : α → Prop} {cut : α → Ordering} {x : α} {t : RBTree.RBNode α},
  RBTree.RBNode.All p t → RBTree.RBNode.upperBound? cut t = some x → p x
-- Init.System.IO
/-- Creates a new task that waits for `t` to complete and then runs the `EIO ε` action `f` on its result.
This new task has priority `prio`.

This is a version of `EIO.mapTask` that ignores the result value.

Running the resulting `EIO ε` action causes the task to be started eagerly. Unlike pure tasks
created by `Task.spawn`, tasks created by this function will run even if the last reference to the
task is dropped. The `act` should explicitly check for cancellation via `IO.checkCanceled` if it
should be terminated or otherwise react to the last reference being dropped.
 -/
EIO.chainTask : {α : Type u_1} →
  {ε : Type} →
    Task α → (α → EIO ε Unit) → optParam Task.Priority Task.Priority.default → optParam Bool false → EIO ε Unit
-- Mathlib.Data.Finset.Sigma
Finset.filter_sigma' : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (t : (i : ι) → Finset (α i)) (p : (i : ι) → α i → Prop)
  [inst : (i : ι) → DecidablePred (p i)], {x ∈ s.sigma t | p x.fst x.snd} = s.sigma fun i => Finset.filter (p i) (t i)
-- Mathlib.Algebra.Star.StarAlgHom
/-- The `Function.prod` of two morphisms is a morphism.  -/
StarAlgHom.prod : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {C : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Star A] →
                [inst_4 : Semiring B] →
                  [inst_5 : Algebra R B] →
                    [inst_6 : Star B] →
                      [inst_7 : Semiring C] →
                        [inst_8 : Algebra R C] → [inst_9 : Star C] → (A →⋆ₐ[R] B) → (A →⋆ₐ[R] C) → A →⋆ₐ[R] B × C
-- Init.Data.Nat.MinMax
Nat.max_eq_right : ∀ {a b : ℕ}, a ≤ b → max a b = b
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopic.Quotient.trans_refl : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x₀ x₁ : X} (γ : Path.Homotopic.Quotient x₀ x₁),
  γ.trans (Path.Homotopic.Quotient.refl x₁) = γ
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_congr : ∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : AddCommMonoid M] {f g : ι → M},
  s₁ = s₂ → (∀ x ∈ s₂, f x = g x) → s₁.sum f = s₂.sum g
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.le_opNorm_mul_pow_card_of_le : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  (f : ContinuousMultilinearMap 𝕜 E G) {m : (i : ι) → E i} {b : ℝ}, ‖m‖ ≤ b → ‖f m‖ ≤ ‖f‖ * b ^ Fintype.card ι
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curry_natural_left_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X X' Y : C}
  [inst_2 : CategoryTheory.Closed A] (f : X ⟶ X') (g : CategoryTheory.MonoidalCategoryStruct.tensorObj A X' ⟶ Y) {Z : C}
  (h : A ⟹ Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalClosed.curry
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f) g))
      h =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalClosed.curry g) h)
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Encodable.good.eq_1 : ∀ {α : Type u_1} (p : α → Prop) (a : α), Encodable.good✝ p (some a) = p a
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.instNormSubtypePreLpMemAddSubgroup : {α : Type u_3} → {E : α → Type u_4} → {p : ENNReal} → [inst : (i : α) → NormedAddCommGroup (E i)] → Norm ↥(lp E p)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- Extension of scalars is a functor where an `R`-module `M` is sent to `S ⊗ M` and
`l : M1 ⟶ M2` is sent to `s ⊗ m ↦ s ⊗ l m`
 -/
ModuleCat.ExtendScalars.map' : {R : Type u₁} →
  {S : Type u₂} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (f : R →+* S) →
          {M1 M2 : ModuleCat R} → (M1 ⟶ M2) → (ModuleCat.ExtendScalars.obj' f M1 ⟶ ModuleCat.ExtendScalars.obj' f M2)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.coe_inj : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L M : BooleanSubalgebra α}, ↑L = ↑M ↔ L = M
-- Mathlib.Data.Set.Insert
Set.singleton_inter_of_mem : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∈ s → {a} ∩ s = {a}
-- Mathlib.Topology.Separation.Hausdorff
t2Space_iff_of_isOpenQuotientMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {π : X → Y},
  IsOpenQuotientMap π → (T2Space Y ↔ IsClosed {q | π q.1 = π q.2})
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
/-- A supporting lemma for the **Phragmen-Lindelöf principle** in a horizontal strip. If `z : ℂ`
belongs to a horizontal strip `|Complex.im z| ≤ b`, `b ≤ π / 2`, and `a ≤ 0`, then
$$\left|exp^{a\left(e^{z}+e^{-z}\right)}\right| \le e^{a\cos b \exp^{|re z|}}.$$
 -/
Complex.norm_exp_mul_exp_add_exp_neg_le_of_abs_im_le : ∀ {a b : ℝ},
  a ≤ 0 →
    ∀ {z : ℂ},
      |z.im| ≤ b →
        b ≤ Real.pi / 2 →
          ‖Complex.exp (↑a * (Complex.exp z + Complex.exp (-z)))‖ ≤ Real.exp (a * Real.cos b * Real.exp |z.re|)
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.smul_Lp_ae_eq : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : SMul M α] [inst_3 : MeasureTheory.SMulInvariantMeasure M α μ]
  [inst_4 : MeasurableConstSMul M α] (c : Mᵈᵐᵃ) (f : ↥(MeasureTheory.Lp E p μ)),
  ↑↑(c • f) =ᵐ[μ] fun x => ↑↑f (DomMulAct.mk.symm c • x)
-- Mathlib.RingTheory.WittVector.DiscreteValuationRing
WittVector.succNthValUnits.eq_1 : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : CommRing k] [inst_1 : CharP k p] (n : ℕ) (a : kˣ)
  (A : WittVector p k) (bs : Fin (n + 1) → k),
  WittVector.succNthValUnits n a A bs =
    -↑(a⁻¹ ^ p ^ (n + 1)) *
      (A.coeff (n + 1) * ↑(a⁻¹ ^ p ^ (n + 1)) + WittVector.nthRemainder p n (WittVector.truncateFun (n + 1) A) bs)
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.nonarchAddGroupNormClass : ∀ {E : Type u_3} [inst : AddGroup E], NonarchAddGroupNormClass (NonarchAddGroupNorm E) E
-- Init.Data.List.Lemmas
List.length_filterMap_le : ∀ {α : Type u_1} {β : Type u_2} (f : α → Option β) (l : List α), (List.filterMap f l).length ≤ l.length