mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.getArithState : Lean.Meta.Sym.SymM Lean.Meta.Sym.Arith.State
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
ContinuousCohomology.cochainsMap_f : ∀ {k : Type u} {G H : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] [inst_5 : Group H] [inst_6 : TopologicalSpace H]
  [inst_7 : IsTopologicalGroup H] {X : TopRep k G} {Y : TopRep k H} (φ : H →ₜ* G) (f : TopRep.res (↑φ) X ⟶ Y) (i : ℕ),
  (ContinuousCohomology.cochainsMap φ f).f i =
    TopRep.invariantsResMap (↑φ) (ContinuousCohomology.resolutionMap φ f (i + 1))
-- Mathlib.Algebra.Group.Pi.Basic
Pi.commMonoid.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → CommMonoid (f i)],
  Pi.commMonoid = { toMonoid := Pi.monoid, mul_comm := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.Retract
CategoryTheory.ShortComplex.quasiIso_of_retract : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ T₁ S₂ T₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : T₁.HasHomology]
  [inst_4 : S₂.HasHomology] [inst_5 : T₂.HasHomology] {f₁ : S₁ ⟶ T₁} {f₂ : S₂ ⟶ T₂}
  (h : CategoryTheory.RetractArrow f₁ f₂) [hf₂ : CategoryTheory.ShortComplex.QuasiIso f₂],
  CategoryTheory.ShortComplex.QuasiIso f₁
-- Mathlib.RingTheory.Multiplicity
emultiplicity_eq_iff_multiplicity_eq_of_ne_one : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {n : ℕ}, n ≠ 1 → (emultiplicity a b = ↑n ↔ multiplicity a b = n)
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- Composition of chain maps.  -/
HomologicalComplex.comp : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → (A B C : HomologicalComplex V c) → A.Hom B → B.Hom C → A.Hom C
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.adapt_ReaderT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ρ ρ' α : Type u} {x : ReaderT ρ' m α}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.arg ρ ps)} [inst : Std.Do.WP m ps] (f : ρ → ρ'),
  ⦃fun r => (Std.Do.wp x).apply (fun a x => Q.1 a r, Q.2) (f r)⦄ ReaderT.adapt f x ⦃Q⦄
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.instSliceableImplRicSlice : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      Std.Ric.Sliceable (Std.DTreeMap.Internal.Impl α fun x => β) α (Std.DTreeMap.Internal.Const.RicSlice α β)
-- Mathlib.Computability.DFA
DFA.comap_step : ∀ {α : Type u} {σ : Type v} {α' : Type u_1} (f : α' → α) (M : DFA α σ) (s : σ) (a : α'),
  (DFA.comap f M).step s a = M.step s (f a)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstr.h : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr → Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Limits.WeightedCone.mk_pt : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {W : CategoryTheory.Functor J (Type w)} {F : CategoryTheory.Functor J C} (pt : C)
  (π : ⦃j : J⦄ → W.obj j → (pt ⟶ F.obj j))
  (hπ :
    ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂),
      CategoryTheory.CategoryStruct.comp (π x) (F.map f) = π ((CategoryTheory.ConcreteCategory.hom (W.map f)) x)),
  (CategoryTheory.Limits.WeightedCone.mk pt π hπ).pt = pt
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeFVar : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit
-- Mathlib.Dynamics.FixedPoints.Basic
/-- If `x` is a fixed point of `f ∘ g` and `g`, then it is a fixed point of `f`.  -/
Function.IsFixedPt.left_of_comp : ∀ {α : Type u_1} {f g : α → α} {x : α}, Function.IsFixedPt (f ∘ g) x → Function.IsFixedPt g x → Function.IsFixedPt f x
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instRingQuotient : {R : Type u_1} → [inst : Ring R] → (c : RingCon R) → Ring c.Quotient
-- Mathlib.Analysis.Convex.MetricSpace
/-- A convex metric space is a real convex space with a compatible metric structure.
Concretely, we ask for `dist(∑ tᵢ xᵢ, ∑ tᵢ yᵢ) ≤ ∑ tᵢ dist(xᵢ, yᵢ)`,
which is what one would expect from the triangle inequality.

In particular, convex subsets of normed affine spaces are convex metric spaces.

Note that there is a separate notion of
[convex metric spaces](https://en.wikipedia.org/wiki/Convex_metric_space) in the literature
that has little to do with this definition.  -/
Convexity.IsConvexDist : (X : Type u_2) → [inst₁ : Convexity.ConvexSpace ℝ X] → [inst₂ : MetricSpace X] → Prop
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Unitization.isQuasiregular_inr_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalRing A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (a : A), IsQuasiregular ↑a ↔ IsQuasiregular a
-- Mathlib.Analysis.CStarAlgebra.ContinuousMap
ContinuousMap.instCommCStarAlgebra : {α : Type u_1} →
  {A : Type u_2} →
    [inst : TopologicalSpace α] → [CompactSpace α] → [inst_2 : CommCStarAlgebra A] → CommCStarAlgebra C(α, A)
-- Mathlib.RingTheory.Ideal.Int
Int.absNorm_under_dvd_absNorm : ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] (I : Ideal S),
  Ideal.absNorm (Ideal.under ℤ I) ∣ Ideal.absNorm I
-- Mathlib.RingTheory.LaurentSeries
/-- `R⸨X⸩` is notation for `LaurentSeries R`.  -/
LaurentSeries.«term_⸨X⸩» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Order.Group.Indicator
Set.mulIndicator_mono : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : One M] {s : Set α} {f g : α → M},
  f ≤ g → s.mulIndicator f ≤ s.mulIndicator g
-- Mathlib.GroupTheory.Exponent
mul_notMem_of_exponent_two : ∀ {G : Type u} [inst : Group G], Monoid.exponent G = 2 → ∀ {x y : G}, x ≠ 1 → y ≠ 1 → x ≠ y → x * y ∉ {x, y, 1}
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph_one_eq_top : SimpleGraph.cycleGraph 1 = ⊤
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.eval.eq_1 : ∀ {aig : Std.Sat.AIG ℕ} (assign : ℕ → Bool) (state : Std.Sat.AIG.toCNF.State✝ aig),
  Std.Sat.AIG.toCNF.State.eval✝ assign state = Std.Sat.CNF.eval assign (Std.Sat.AIG.toCNF.State.cnf✝ state)
-- Mathlib.Data.Fintype.Card
Fintype.card_ne_zero : ∀ {α : Type u_1} [inst : Fintype α] [Nonempty α], Fintype.card α ≠ 0
-- Mathlib.NumberTheory.GaussSum
/-- Replacing `ψ` by `mulShift ψ a` multiplies the Gauss sum by `χ⁻¹ a`.  -/
gaussSum_mulShift_eq : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] (χ : MulChar R R')
  (ψ : AddChar R R') (a : Rˣ), gaussSum χ (ψ.mulShift ↑a) = χ⁻¹ ↑a * gaussSum χ ψ
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.FixPoint.State.modified : Lean.Elab.Term.MutualClosure.FixPoint.State → Bool
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.unop : C ⥤ D` creates limits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` creates colimits.  -/
CategoryTheory.Limits.createsColimitsOfSizeOfUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) →
          [CategoryTheory.CreatesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.unop] →
            CategoryTheory.CreatesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.baseChange_negAddY : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Jacobian R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P Q : Fin 3 → A), (W'.baseChange B).negAddY (⇑f ∘ P) (⇑f ∘ Q) = f ((W'.baseChange A).negAddY P Q)
-- Mathlib.Logic.Function.Iterate
Function.RightInverse.iterate : ∀ {α : Type u} {f g : α → α}, Function.RightInverse g f → ∀ (n : ℕ), Function.RightInverse g^[n] f^[n]
-- Mathlib.Data.Int.ModEq
Int.ModEq.pow : ∀ {n a b : ℤ} (m : ℕ), a ≡ b [ZMOD n] → a ^ m ≡ b ^ m [ZMOD n]
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.not_one_beq : ∀ (a : BitVec 1), (!1#1 == a) = (a == 0#1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_insert_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).getKey k ⋯ = k
-- Mathlib.Algebra.Group.Units.Hom
/-- Coercion `Mˣ → M` as a monoid homomorphism.  -/
Units.coeHom : (M : Type u) → [inst : Monoid M] → Mˣ →* M
-- Mathlib.Data.Num.Lemmas
PosNum.cast_le : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {m n : PosNum}, ↑m ≤ ↑n ↔ m ≤ n
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_eq_iSup_of_singleton_spans : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M),
  Submodule.span R s = ⨆ x ∈ s, R ∙ x
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.unit_pushforwardId_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : C)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.id I)]
  [inst_2 : CategoryTheory.ExponentiableMorphism (CategoryTheory.CategoryStruct.id I)]
  {Z : CategoryTheory.Functor (CategoryTheory.Over I) (CategoryTheory.Over I)}
  (h :
    (CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.CategoryStruct.id I)).comp
        (CategoryTheory.Functor.id (CategoryTheory.Over I)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj (CategoryTheory.CategoryStruct.id I)).unit
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.ChosenPullbacksAlong.pullback (CategoryTheory.CategoryStruct.id I)).whiskerLeft
          (CategoryTheory.ExponentiableMorphism.pushforwardId I).hom)
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj (CategoryTheory.CategoryStruct.id I)).unit h
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
/-- If `M` is an additive monoid object, then `Hom(-, M)` as a presheaf of additive monoids
is represented by `M`.  -/
CategoryTheory.yonedaAddMonObjRepresentableBy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (M : C) →
        [inst_2 : CategoryTheory.AddMonObj M] →
          ((CategoryTheory.yonedaAddMonObj M).comp (CategoryTheory.forget AddMonCat)).RepresentableBy M
-- Init.Data.ByteArray.Basic
ByteArray.foldlMUnsafe.fold : {β : Type v} → {m : Type v → Type w} → [Monad m] → (β → UInt8 → m β) → ByteArray → USize → USize → β → m β
-- Mathlib.RingTheory.MvPowerSeries.Substitution
/-- If `σ` is finite, then having zero constant coefficient is enough for `HasSubst`  -/
MvPowerSeries.hasSubst_of_constantCoeff_zero : ∀ {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [inst : CommRing S] [Finite σ] {a : σ → MvPowerSeries τ S},
  (∀ (s : σ), MvPowerSeries.constantCoeff (a s) = 0) → MvPowerSeries.HasSubst a
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
_private.Mathlib.MeasureTheory.Measure.Haar.Quotient.0.termμ_𝓕 : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.sndL_apply : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : Semiring 𝕜] [inst_3 : AddCommGroup α] [inst_4 : AddCommGroup β] [inst_5 : Module 𝕜 α] [inst_6 : Module 𝕜 β]
  (x : WithLp p (α × β)), (WithLp.sndL p 𝕜 α β) x = x.snd
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.initiallySmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (self : J.Point),
  CategoryTheory.InitiallySmall self.fiber.Elements
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.swap : Nat.Primrec (Nat.unpaired (Function.swap Nat.pair))
-- Mathlib.Data.PEquiv
PEquiv.trans_single_of_eq_none : ∀ {β : Type v} {γ : Type w} {δ : Type x} [inst : DecidableEq β] [inst_1 : DecidableEq γ] {b : β} (c : γ) {f : δ ≃. β},
  f.symm b = none → f.trans (PEquiv.single b c) = ⊥
-- Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory
CategoryTheory.Monoidal.functorHasLeftDual : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Groupoid C] →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} D] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          [CategoryTheory.LeftRigidCategory D] → (F : CategoryTheory.Functor C D) → CategoryTheory.HasLeftDual F
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
/-- Every exponent in the Cantor normal form `CNF b o` is less or equal to `log b o`.  -/
Ordinal.CNF.fst_le_log : ∀ {b o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}}, x ∈ Ordinal.CNF b o → x.1 ≤ Ordinal.log b o
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionItemData.uri : Lean.Lsp.ResolvableCompletionItemData → Lean.Lsp.DocumentUri
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroMod.congr_simp : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type v} [inst_2 : Field K] [inst_3 : Algebra R K]
  [inst_4 : IsFractionRing R K] (v v_1 : IsDedekindDomain.HeightOneSpectrum R),
  v = v_1 → ∀ (n : ℕ), v.valuationOfNeZeroMod n = v_1.valuationOfNeZeroMod n
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.orderTop_lt_top : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R}, x.orderTop < ⊤ ↔ x ≠ 0
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mem_mapTriangle_essImage_of_distinguished : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Limits.HasZeroObject C] [inst_6 : CategoryTheory.Limits.HasZeroObject D]
  [inst_7 : CategoryTheory.Preadditive C] [inst_8 : CategoryTheory.Preadditive D]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_10 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_11 : CategoryTheory.Pretriangulated C]
  [inst_12 : CategoryTheory.Pretriangulated D] [F.IsTriangulated] [F.mapArrow.EssSurj],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∃ T', ∃ (_ : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles), Nonempty (F.mapTriangle.obj T' ≅ T)
-- Mathlib.Analysis.Normed.Module.Alternating.Curry
/-- Currying with the same element twice gives the zero map.  -/
ContinuousAlternatingMap.curryLeft_same : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (f : E [⋀^Fin (n + 2)]→L[𝕜] F) (x : E), (f.curryLeft x).curryLeft x = 0
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.WalkingPair.swap_symm_apply_tt : CategoryTheory.Limits.WalkingPair.swap.symm CategoryTheory.Limits.WalkingPair.left =
  CategoryTheory.Limits.WalkingPair.right
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.instLocallySmallOpposite : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.LocallySmall.{w, v, u} Cᵒᵖ
-- Mathlib.MeasureTheory.Function.Holder
ContinuousLinearMap.holder.congr_simp : ∀ {α : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {p q : ENNReal} (r : ENNReal) [hpqr : p.HolderTriple q r]
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 F] [inst_6 : NormedSpace 𝕜 G]
  (B B_1 : E →L[𝕜] F →L[𝕜] G),
  B = B_1 →
    ∀ (f f_1 : ↥(MeasureTheory.Lp E p μ)),
      f = f_1 →
        ∀ (g g_1 : ↥(MeasureTheory.Lp F q μ)),
          g = g_1 → ContinuousLinearMap.holder r B f g = ContinuousLinearMap.holder r B_1 f_1 g_1
-- Mathlib.Topology.UniformSpace.Basic
UniformContinuous.prodMap : ∀ {α : Type ua} {β : Type ub} {γ : Type uc} {δ : Type ud} [inst : UniformSpace α] [inst_1 : UniformSpace β]
  [inst_2 : UniformSpace γ] [inst_3 : UniformSpace δ] {f : α → γ} {g : β → δ},
  UniformContinuous f → UniformContinuous g → UniformContinuous (Prod.map f g)
-- Init.Data.Array.Lemmas
Array.reverse_flatMap : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β},
  (Array.flatMap f xs).reverse = Array.flatMap (Array.reverse ∘ f) xs.reverse
-- Mathlib.LinearAlgebra.FreeModule.Int
/-- Given a submodule `N` in Smith normal form of a free ℤ-module, it has finite index as an
additive subgroup (i.e., `N.toAddSubgroup.index ≠ 0`) if and only if the submodule basis has as
many vectors as the basis for the module.  -/
Module.Basis.SmithNormalForm.toAddSubgroup_index_ne_zero_iff : ∀ {ι : Type u_1} {M : Type u_3} {n : ℕ} [inst : AddCommGroup M] [inst_1 : Fintype ι] {N : Submodule ℤ M}
  (snf : Module.Basis.SmithNormalForm N ι n), N.toAddSubgroup.index ≠ 0 ↔ n = Fintype.card ι
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.mem_bot : ∀ {α : Type u_2} [inst : TopologicalSpace α] {x : α}, x ∈ ⊥ ↔ False
-- Init.Data.Bool
Bool.cond_eq_ite : ∀ {α : Sort u_1} (b : Bool) (t e : α), (bif b then t else e) = if b = true then t else e
-- Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
/-- The triangle `(triangle φ).rotate` is isomorphic to a triangle attached to a
degreewise split short exact sequence of cochain complexes.  -/
CochainComplex.mappingCone.triangleRotateIsoTriangleOfDegreewiseSplit : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {K L : CochainComplex C ℤ} →
          (φ : K ⟶ L) →
            (CochainComplex.mappingCone.triangle φ).rotate ≅
              CochainComplex.triangleOfDegreewiseSplit (CochainComplex.mappingCone.triangleRotateShortComplex φ)
                (CochainComplex.mappingCone.triangleRotateShortComplexSplitting φ)
-- Mathlib.Tactic.Linter.Whitespace
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.FormatError.mk : ℕ → String.Pos.Raw → ℕ → String → ℕ → String.Pos.Raw → Mathlib.Linter.FormatError✝
-- Mathlib.Topology.Algebra.FilterBasis
RingFilterBasis.mul_left' : ∀ {R : Type u} {inst : Ring R} [self : RingFilterBasis R] (x₀ : R) {U : Set R},
  U ∈ self.sets → ∃ V ∈ self.sets, V ⊆ (fun x => x₀ * x) ⁻¹' U
-- Mathlib.Data.Set.Basic
Set.Nonempty.forall_const : ∀ {α : Type u} {s : Set α}, s.Nonempty → ∀ {p : Prop}, (∀ x ∈ s, p) ↔ p
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.uliftFunctor.eq_1 : MonCat.uliftFunctor =
  { obj := fun X => MonCat.of (ULift.{u, v} ↑X),
    map := fun {x x_1} f =>
      MonCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((MonCat.Hom.hom f).comp MulEquiv.ulift.toMonoidHom)),
    map_id := ⋯, map_comp := ⋯ }
-- Mathlib.AlgebraicGeometry.Pullbacks
/-- The inclusion map of `V i j = (Uᵢ ×[Z] Y) ×[X] Uⱼ ⟶ Uᵢ ×[Z] Y`  -/
AlgebraicGeometry.Scheme.Pullback.fV : {X Y Z : AlgebraicGeometry.Scheme} →
  (𝒰 : X.OpenCover) →
    (f : X ⟶ Z) →
      (g : Y ⟶ Z) →
        [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g] →
          (i j : 𝒰.I₀) →
            AlgebraicGeometry.Scheme.Pullback.v 𝒰 f g i j ⟶
              CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g
-- Mathlib.Analysis.LocallyConvex.AbsConvex
absConvexHull.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜], absConvexHull 𝕜 = ClosureOperator.ofCompletePred (AbsConvex 𝕜) ⋯
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.one_lt_pow : ∀ {a : Ordinal.{u_1}} {n : ℕ}, 1 < a ^ n ↔ 1 < a ∧ n ≠ 0
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.neg_fst : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : AddCommGroup β] (x : WithLp p (α × β)),
  (-x).fst = -x.fst
-- Mathlib.Combinatorics.Quiver.Covering
Quiver.starEquivCostar_apply : ∀ {U : Type u_1} [inst : Quiver U] [inst_1 : Quiver.HasInvolutiveReverse U] {u v : U} (e : u ⟶ v),
  (Quiver.starEquivCostar u) (Quiver.Star.mk e) = Quiver.Costar.mk (Quiver.reverse e)
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_eq_pi_div_two_iff : ∀ {z : ℂ}, z.arg = Real.pi / 2 ↔ z.re = 0 ∧ 0 < z.im
-- Mathlib.Algebra.Group.Equiv.Opposite
AddOpposite.opAddEquiv.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M], AddOpposite.opAddEquiv = { toEquiv := AddOpposite.opEquiv, map_add' := ⋯ }
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.coe_mk : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] (s : Set M) (h₁ : ∀ ⦃c : R⦄, 0 < c → ∀ ⦃x : M⦄, x ∈ s → c • x ∈ s)
  (h₂ : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → x + y ∈ s), ↑{ carrier := s, smul_mem' := h₁, add_mem' := h₂ } = s
-- Mathlib.Tactic.Simps.Basic
/-- Projection data used internally in `getRawProjections`.  -/
Simps.ParsedProjectionData : Type
-- Mathlib.Algebra.Group.Commutator
/-- The commutator of two elements `g₁` and `g₂`. This is a scoped instance in the
`commutatorElement` namespace to avoid clashing with other brackets.  -/
commutatorElement : {G : Type u_1} → [Group G] → Bracket G G
-- Mathlib.Combinatorics.SimpleGraph.Hasse
SimpleGraph.pathGraph_two_eq_top : SimpleGraph.pathGraph 2 = ⊤
-- Std.Data.Iterators.Producers.Vector
/-- Returns a finite iterator for the given vector.
The iterator yields the elements of the vector in order and then terminates.

The monadic version of this iterator is
`Vector.iterM`.

**Termination properties:**

* `Finite` instance: always

* `Productive` instance: always
 -/
Vector.iter : {n : ℕ} → {α : Type w} → Vector α n → Std.Iter α
-- Init.Core
/-- An equivalence relation is transitive: `r x y` and `r y z` implies `r x z`  -/
Equivalence.trans : ∀ {α : Sort u} {r : α → α → Prop}, Equivalence r → ∀ {x y z : α}, r x y → r y z → r x z
-- Mathlib.Data.Multiset.Bind
Multiset.bind_hcongr : ∀ {α : Type u_1} {β β' : Type v} {m : Multiset α} {f : α → Multiset β} {f' : α → Multiset β'},
  β = β' → (∀ a ∈ m, f a ≍ f' a) → m.bind f ≍ m.bind f'
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- A side of a right-angled triangle divided by the tangent of the opposite angle equals the
adjacent side, version subtracting vectors.  -/
InnerProductGeometry.norm_div_tan_angle_sub_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → x = 0 ∨ y ≠ 0 → ‖y‖ / Real.tan (InnerProductGeometry.angle x (x - y)) = ‖x‖
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.mk.injEq : ∀ {m : Type w → Type w'} {α : Type v} (Property : α → Prop) (small : Std.Internal.Small (Subtype Property))
  (operation : m (Std.Internal.USquash (Subtype Property))) (Property_1 : α → Prop)
  (small_1 : Std.Internal.Small (Subtype Property_1)) (operation_1 : m (Std.Internal.USquash (Subtype Property_1))),
  ({ Property := Property, small := small, operation := operation } =
      { Property := Property_1, small := small_1, operation := operation_1 }) =
    (Property = Property_1 ∧ operation ≍ operation_1)
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.ae_compProd_of_ae_ae : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} {p : α × β → Prop},
  MeasurableSet {x | p x} → (∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b)) → ∀ᵐ (x : α × β) ∂μ.compProd κ, p x
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_roi_eq_mkSlice_rci : ∀ {α : Type u_1} {xs : Array α} {lo : ℕ},
  Std.Roi.Sliceable.mkSlice xs lo<...* = Std.Rci.Sliceable.mkSlice xs (lo + 1)...*