mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- `PUnit` is a left identity for product of measurable spaces up to a measurable equivalence.  -/
MeasurableEquiv.punitProd : {α : Type u_1} → [inst : MeasurableSpace α] → PUnit.{u_6 + 1} × α ≃ᵐ α
-- Mathlib.Order.Hom.CompleteLattice
/-- The proposition that a `sInfHom` commutes with arbitrary infima/meets  -/
sInfHom.map_sInf' : ∀ {α : Type u_8} {β : Type u_9} [inst : InfSet α] [inst_1 : InfSet β] (self : sInfHom α β) (s : Set α),
  self.toFun (sInf s) = sInf (self.toFun '' s)
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.theta_eq_zero_iff : ∀ {x : ℝ}, Chebyshev.theta x = 0 ↔ x < 2
-- Lean.Meta.Tactic.Grind.Arith.Util
/-- Returns `true` if `e` is of the form `@instHAdd Nat instAddNat`  -/
Lean.Meta.Grind.Arith.isInstAddNat : Lean.Expr → Bool
-- Mathlib.Topology.Category.TopCat.Opens
Topology.IsInducing.le_functorObj_iff : ∀ {X Y : TopCat} {f : X ⟶ Y} (hf : Topology.IsInducing ⇑(CategoryTheory.ConcreteCategory.hom f))
  {U : TopologicalSpace.Opens ↑X} {V : TopologicalSpace.Opens ↑Y},
  V ≤ hf.functorObj U ↔ (TopologicalSpace.Opens.map f).obj V ≤ U
-- Mathlib.Analysis.Distribution.Support
Distribution.isVanishingOn_delta : ∀ {E : Type u_11} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {n : ℕ∞}
  (x : E), Distribution.IsVanishingOn ⇑(Distribution.delta x) {x}ᶜ
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.coercions : Lean.Option Bool
-- Mathlib.GroupTheory.Coxeter.Matrix
/-- **Alias** of `CoxeterMatrix.I`.

---

The Coxeter matrix of type I₂(m).

The corresponding Coxeter-Dynkin diagram is:
```
     m + 2
    o --- o
```
 -/
CoxeterMatrix.I₂ₙ : ℕ → CoxeterMatrix (Fin 2)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- If `x` isn't in `f`'s domain, `f.eval x` produces a brand new value not in `f`'s range.  -/
HahnEmbedding.Partial.eval_ne : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] {seed : HahnEmbedding.Seed K M R} (f : HahnEmbedding.Partial seed)
  [inst_12 : IsOrderedAddMonoid R] [inst_13 : Archimedean R] {x : M},
  x ∉ (↑f).domain → ∀ (y : ↥(↑f).domain), f.eval x ≠ ↑↑f y
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.ExtractMonadResult.mk.inj : ∀ {m returnType expectedType m_1 returnType_1 expectedType_1 : Lean.Expr},
  { m := m, returnType := returnType, expectedType := expectedType } =
      { m := m_1, returnType := returnType_1, expectedType := expectedType_1 } →
    m = m_1 ∧ returnType = returnType_1 ∧ expectedType = expectedType_1
-- Init.Data.Vector.Lemmas
Vector.foldl_toArray : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} (f : β → α → β) {init : β} {xs : Vector α n},
  Array.foldl f init xs.toArray = Vector.foldl f init xs
-- Lean.Meta.Tactic.LibrarySearch
Lean.Meta.LibrarySearch.DeclMod.ofNat_ctorIdx : ∀ (x : Lean.Meta.LibrarySearch.DeclMod), Lean.Meta.LibrarySearch.DeclMod.ofNat x.ctorIdx = x
-- Init.Data.List.MapIdx
List.mapFinIdx_eq_zipIdx_map : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : ℕ) → α → i < l.length → β},
  l.mapFinIdx f =
    List.map
      (fun x =>
        match x with
        | ⟨(x, i), m⟩ => f i x ⋯)
      l.zipIdx.attach
-- Lean.Data.JsonRpc
/-- A notification message. A processed notification message must not send a response back. They work like events.  -/
Lean.JsonRpc.Message.notification : String → Option Lean.Json.Structured → Lean.JsonRpc.Message
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α} {v : β}, (m.insert k v).getKeyD k fallback = k
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl) Prove that the lifted cone is limiting.  -/
CategoryTheory.Comonad.ForgetCreatesLimits'.liftedConeIsLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {T : CategoryTheory.Comonad C} →
          {D : CategoryTheory.Functor J T.Coalgebra} →
            (c : CategoryTheory.Limits.Cone (D.comp T.forget)) →
              (t : CategoryTheory.Limits.IsLimit c) →
                [inst_2 : CategoryTheory.Limits.PreservesLimit (D.comp T.forget) T.toFunctor] →
                  [inst_3 : CategoryTheory.Limits.PreservesLimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] →
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Comonad.ForgetCreatesLimits'.liftedCone c t)
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
csSup_neg : ∀ {M : Type u_1} [inst : ConditionallyCompleteLattice M] [inst_1 : AddGroup M] [AddLeftMono M] [AddRightMono M]
  {s : Set M}, s.Nonempty → BddBelow s → sSup (-s) = -sInf s
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
AddSubsemigroup.decidableMemCentralizer : {M : Type u_1} →
  {S : Set M} →
    [inst : AddSemigroup M] →
      (a : M) → [Decidable (∀ b ∈ S, b + a = a + b)] → Decidable (a ∈ AddSubsemigroup.centralizer S)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.toList_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ},
  Std.ExtDTreeMap.Const.toList (Std.ExtDTreeMap.filterMap (fun k v => f k v) t) =
    List.filterMap (fun p => Option.map (fun x => (p.1, x)) (f p.1 p.2)) (Std.ExtDTreeMap.Const.toList t)
-- Mathlib.Data.ENNReal.Operations
ENNReal.addLeftReflectLT : AddLeftReflectLT ENNReal
-- Mathlib.Topology.Specialization
Specialization.isOpen_toEquiv_preimage : ∀ {α : Type u_1} [inst : TopologicalSpace α] [AlexandrovDiscrete α] {s : Set (Specialization α)},
  IsOpen (⇑Specialization.toEquiv ⁻¹' s) ↔ IsUpperSet s
-- Mathlib.NumberTheory.Divisors
Nat.sum_divisorsAntidiagonal' : ∀ {M : Type u_1} [inst : AddCommMonoid M] (f : ℕ → ℕ → M) {n : ℕ},
  ∑ i ∈ n.divisorsAntidiagonal, f i.1 i.2 = ∑ i ∈ n.divisors, f (n / i) i
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformOnFun.gen_mem_uniformity : ∀ {α : Type u_1} (β : Type u_2) {s : Set α} [inst : UniformSpace β] (𝔖 : Set (Set α)),
  s ∈ 𝔖 → ∀ {V : Set (β × β)}, V ∈ uniformity β → UniformOnFun.gen 𝔖 s V ∈ uniformity (UniformOnFun α β 𝔖)
-- Mathlib.Tactic.NormNum.IsSquare
Mathlib.Meta.NormNum.iff_isSquare_int_of_isNat : ∀ (a : ℤ) (n : ℕ), Mathlib.Meta.NormNum.IsNat a n → (IsSquare n ↔ IsSquare a)
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.ofInjective_apply : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} (hf : Function.Injective ⇑f) {x : G},
  ↑((MonoidHom.ofInjective hf) x) = f x
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Iso.inv_hom_id_triangle_hom₁_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {A B : CategoryTheory.Pretriangulated.Triangle C} (e : A ≅ B) {Z : C} (h : B.obj₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp e.inv.hom₁ (CategoryTheory.CategoryStruct.comp e.hom.hom₁ h) = h
-- Mathlib.Order.WellQuasiOrder
instWellQuasiOrderedLEOfWellFoundedLT : ∀ {α : Type u_1} [inst : LinearOrder α] [h : WellFoundedLT α], WellQuasiOrderedLE α
-- Init.Data.Dyadic.Inv
/-- For a positive dyadic `b`, `divAtPrec a b prec * b ≤ a`.  -/
Dyadic.divAtPrec_mul_le : ∀ {a b : Dyadic}, 0 < b → ∀ (prec : ℤ), a.divAtPrec b prec * b ≤ a
-- Init.Data.Vector.Lemmas
Vector.findRevM?_toArray : ∀ {m : Type → Type} {α : Type} {n : ℕ} [inst : Monad m] {p : α → m Bool} {xs : Vector α n},
  Array.findRevM? p xs.toArray = Vector.findRevM? p xs
-- Mathlib.Combinatorics.Quiver.Prefunctor
Prefunctor.id_map : ∀ (V : Type u_1) [inst : Quiver V] {X Y : V} (f : X ⟶ Y), (𝟭q V).map f = f
-- Mathlib.Order.Hom.Lattice
LatticeHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  (f : LatticeHom β γ) (g : LatticeHom α β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Init.Data.Nat.Bitwise.Basic
Nat.bitwise_rec_lemma : ∀ {n : ℕ}, n ≠ 0 → n / 2 < n
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_modify_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF → ∀ {k : α} [inst_3 : Inhabited (β k)] {f : β k → β k}, (m.modify k f).get! k = (Option.map f (m.get? k)).get!
-- Mathlib.Topology.Algebra.Ring.Basic
RingTopology.ext_iff : ∀ {R : Type u_1} [inst : Ring R] {f g : RingTopology R}, f = g ↔ TopologicalSpace.IsOpen = TopologicalSpace.IsOpen
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_hasStrictFDerivAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {x : G} {f' : G →L[𝕜] E},
  HasStrictFDerivAt (⇑iso ∘ f) (↑iso ∘SL f') x ↔ HasStrictFDerivAt f f' x
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.simpC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.CommRing α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (k₁ : ℤ) (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon) (p₂ p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.simp_certC k₁ p₁ k₂ m₂ p₂ p c = true →
    Lean.Grind.CommRing.Poly.denote ctx p₁ = 0 →
      Lean.Grind.CommRing.Poly.denote ctx p₂ = 0 → Lean.Grind.CommRing.Poly.denote ctx p = 0
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.insert_Ioc_right_eq_Ioc_add_one : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] {a b : α} [NoMaxOrder α],
  a ≤ b → insert (b + 1) (Set.Ioc a b) = Set.Ioc a (b + 1)
-- Mathlib.Data.PNat.Prime
PNat.coprime_coe : ∀ {m n : ℕ+}, (↑m).Coprime ↑n ↔ m.Coprime n
-- Mathlib.Data.Int.Init
Int.succ_pred : ∀ (a : ℤ), a.pred.succ = a
-- Mathlib.Topology.Order
denseRange_discrete : ∀ {α : Type u_1} [inst : TopologicalSpace α] [DiscreteTopology α] {ι : Type u_3} {f : ι → α},
  DenseRange f ↔ Function.Surjective f
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.eq_of_isomorphisms_descendsAlong : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C}
  [(CategoryTheory.MorphismProperty.isomorphisms C).DescendsAlong P] [P.IsStableUnderBaseChange]
  [CategoryTheory.Limits.HasEqualizers C] [inst_4 : CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y}
  {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryTheory.CategoryStruct.comp f t = s)
  (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S),
  P v →
    CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T)
          (CategoryTheory.CategoryStruct.id S) ⋯ ⋯ =
        CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T)
          (CategoryTheory.CategoryStruct.id S) ⋯ ⋯ →
      f = g
-- Mathlib.Data.Fin.Fin2
Fin2.ofFin_succ : ∀ {n : ℕ} (i : Fin n), Fin2.ofFin i.succ = (Fin2.ofFin i).fs
-- Mathlib.Data.Set.Semiring
SetSemiring.down_subset_down : ∀ {α : Type u_1} {s t : SetSemiring α}, SetSemiring.down s ⊆ SetSemiring.down t ↔ s ≤ t
-- Init.Data.Nat.MinMax
Nat.add_max_add_right : ∀ (a b c : ℕ), max (a + c) (b + c) = max a b + c
-- Mathlib.Analysis.Normed.Module.WeakDual
WeakDual.toLinearEquiv_extendRCLikeL : ∀ {𝕜 : Type u_5} {F : Type u_7} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F],
  ↑WeakDual.extendRCLikeL =
    WeakDual.toStrongDual ≪≫ₗ StrongDual.extendRCLikeₗ ≪≫ₗ LinearEquiv.restrictScalars ℝ StrongDual.toWeakDual
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.instLocallyQuasiFiniteOfLocallyOfFiniteTypeOfUniversallyInjective : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.LocallyOfFiniteType f]
  [AlgebraicGeometry.UniversallyInjective f], AlgebraicGeometry.LocallyQuasiFinite f
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
AnalyticOn.hasFTaylorSeriesUpToOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {s : Set E} {n : WithTop ℕ∞},
  AnalyticOn 𝕜 f s → UniqueDiffOn 𝕜 s → HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) s
-- Mathlib.Algebra.DirectSum.Module
/-- When indexed by only two distinct elements, `DirectSum.IsInternal` implies
the two submodules are complementary. Over a `Ring R`, this is true as an iff, as
`DirectSum.isInternal_submodule_iff_isCompl`.  -/
DirectSum.IsInternal.isCompl : ∀ {R : Type u} [inst : Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {A : ι → Submodule R M} {i j : ι},
  i ≠ j → Set.univ = {i, j} → DirectSum.IsInternal A → IsCompl (A i) (A j)
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Path.ins.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → RBTree.RBNode α → Sort u_2) (parent : RBTree.RBNode.Path α) (y : α)
  (b a : RBTree.RBNode α) (h_1 : (t : RBTree.RBNode α) → motive RBTree.RBNode.Path.root t)
  (h_2 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.red parent y b) a)
  (h_3 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.red a y parent) b)
  (h_4 :
    (parent : RBTree.RBNode.Path α) →
      (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left RBTree.RBColor.black parent y b) a)
  (h_5 :
    (a : RBTree.RBNode α) →
      (y : α) →
        (parent : RBTree.RBNode.Path α) →
          (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right RBTree.RBColor.black a y parent) b),
  (match RBTree.RBNode.Path.left RBTree.RBColor.red parent y b, a with
    | RBTree.RBNode.Path.root, t => h_1 t
    | RBTree.RBNode.Path.left RBTree.RBColor.red parent y b, a => h_2 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.red a y parent, b => h_3 a y parent b
    | RBTree.RBNode.Path.left RBTree.RBColor.black parent y b, a => h_4 parent y b a
    | RBTree.RBNode.Path.right RBTree.RBColor.black a y parent, b => h_5 a y parent b) =
    h_2 parent y b a
-- Init.Control.StateCps
StateCpsT.runK_bind_get : ∀ {σ : Type u} {m : Type u → Type v} {β γ : Type u} (f : σ → StateCpsT σ m β) (s : σ) (k : β → σ → m γ),
  (get >>= f).runK s k = (f s).runK s k
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.inter_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {T : C}
  [inst_1 : J.IsStableUnderBaseChange] [inst_2 : J.IsStableUnderComposition] (E : J.ZeroHypercover T)
  (F : J.ZeroHypercover T) [inst_3 : ∀ (i : E.I₀) (j : F.I₀), CategoryTheory.Limits.HasPullback (E.f i) (F.f j)],
  (E.inter F).toPreZeroHypercover = E.inter F.toPreZeroHypercover
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateCol_submatrix_equiv : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : DecidableEq o]
  [inst_1 : DecidableEq n] (A : Matrix m n α) (j : o) (c : l → α) (e : l ≃ m) (f : o ≃ n),
  (A.submatrix ⇑e ⇑f).updateCol j c = (A.updateCol (f j) fun i => c (e.symm i)).submatrix ⇑e ⇑f
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.foldr_eq_foldr_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w} {f : α → δ → δ}
  {init : δ}, Std.DTreeMap.Raw.foldr (fun a x d => f a d) init t = Array.foldr f init t.keysArray
-- Mathlib.Data.Finset.Sups
/-- The finset of elements of the form `a ⊔ b` where `a ∈ s`, `b ∈ t` and `a` and `b` are disjoint.
 -/
Finset.disjSups : {α : Type u_2} →
  [DecidableEq α] →
    [inst : SemilatticeSup α] → [inst_1 : OrderBot α] → [DecidableRel Disjoint] → Finset α → Finset α → Finset α
-- Std.Do.PostCond
Std.Do.PostShape.except.sizeOf_spec : ∀ (ε : Type u) (a : Std.Do.PostShape), sizeOf (Std.Do.PostShape.except ε a) = 1 + sizeOf ε + sizeOf a
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.prod_le_iff : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {H : Subgroup G} {K : Subgroup N}
  {J : Subgroup (G × N)}, H.prod K ≤ J ↔ Subgroup.map (MonoidHom.inl G N) H ≤ J ∧ Subgroup.map (MonoidHom.inr G N) K ≤ J
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.IsTuranMaximal.finpartition.congr_simp : ∀ {V : Type u_1} [inst : Fintype V] {G G_1 : SimpleGraph V} (e_G : G = G_1) {inst_1 : DecidableRel G.Adj}
  [inst_2 : DecidableRel G_1.Adj] {r r_1 : ℕ} (e_r : r = r_1) (h : G.IsTuranMaximal r) [inst_3 : DecidableEq V],
  h.finpartition = ⋯.finpartition
-- Init.PropLemmas
/-- Transfer decidability of `b` to decidability of `a`, if the propositions are equivalent.
This is the same as `decidable_of_iff` but the iff is flipped.  -/
decidable_of_iff' : {a : Prop} → (b : Prop) → (a ↔ b) → [Decidable b] → Decidable a
-- Mathlib.Combinatorics.Hindman
Hindman.FS.below.cons' : ∀ {M : Type u_1} [inst : AddSemigroup M] {motive : (a : Stream' M) → (a_1 : M) → Hindman.FS a a_1 → Prop}
  (a : Stream' M) (m : M) (h : Hindman.FS a.tail m), Hindman.FS.below h → motive a.tail m h → Hindman.FS.below ⋯
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
nhdsWithin_uIcc_isMeasurablyGenerated : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
  {a b x : α} [OrderClosedTopology α], (nhdsWithin x (Set.uIcc a b)).IsMeasurablyGenerated
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.coe_ofClass : ∀ {S : Type u_3} {M : Type u_4} [inst : Add M] [inst_1 : SetLike S M] [inst_2 : AddMemClass S M] (s : S),
  ↑(AddSubsemigroup.ofClass s) = ↑s
-- Mathlib.RingTheory.ZMod
/-- `ZMod n` is reduced iff `n` is square-free (or `n=0`).  -/
isReduced_zmod : ∀ {n : ℕ}, IsReduced (ZMod n) ↔ Squarefree n ∨ n = 0
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.squarefree_radical : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M}, Squarefree (UniqueFactorizationMonoid.radical a)
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_eq_finite_toFinset_sum : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) {s : Set α} (hs : s.Finite),
  ∑ᶠ (i : α) (_ : i ∈ s), f i = ∑ i ∈ hs.toFinset, f i
-- Lean.Parser.Basic
_private.Lean.Parser.Basic.0.Lean.Parser.isIdFirstOrBeginEscape : Char → Bool
-- Mathlib.RingTheory.Derivation.Basic
Derivation.instZero : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra R A] → [inst_4 : Module A M] → [inst_5 : Module R M] → Zero (Derivation R A M)
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.instHasPullbacksOfHasExplicitPullbacks : ∀ {P : TopCat → Prop} [CompHausLike.HasExplicitPullbacks P], CategoryTheory.Limits.HasPullbacks (CompHausLike P)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
RingHom.kerLift_mk : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Semiring S] (f : R →+* S) (r : R),
  f.kerLift ((Ideal.Quotient.mk (RingHom.ker f)) r) = f r
-- Mathlib.Algebra.Order.Group.Abs
abs_max_le_max_abs_abs : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] {a b : G}, |max a b| ≤ max |a| |b|
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj adj' : F ⊣ G},
  adj.unit = adj'.unit → adj = adj'
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblU_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R) (u : R),
  W'.dblU (u • P) = u ^ 4 * W'.dblU P
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.diff_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m₁.Equiv m₂ → (m₁ \ m₃).Equiv (m₂ \ m₃)
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.coeffLinearEquiv_apply : ∀ (R : Type u_1) {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  (a : MonoidAlgebra S M), (MonoidAlgebra.coeffLinearEquiv R) a = a.coeff
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- This definition allows to endow `α × β` with the Lp norm with the uniformity and bornology
being defeq to the product ones. It is useful to endow a type synonym of `a × β` with the
Lp norm.  -/
WithLp.seminormedAddCommGroupToProd : (p : ENNReal) →
  [hp : Fact (1 ≤ p)] →
    (α : Type u_4) →
      (β : Type u_5) → [SeminormedAddCommGroup α] → [SeminormedAddCommGroup β] → SeminormedAddCommGroup (α × β)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork S hf c hc).iso =
    CategoryTheory.Iso.refl (CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf c hc).H
-- Lean.Meta.KExprMap
_private.Lean.Meta.KExprMap.0.Lean.Meta.updateList : {α : Type} → Lean.AssocList Lean.Expr α → Lean.Expr → α → Lean.MetaM (Lean.AssocList Lean.Expr α)
-- Lean.Parser.Term
/-- Tuple notation; `()` is short for `Unit.unit`, `(a, b, c)` for `Prod.mk a (Prod.mk b c)`, etc. 

Conventions for notations in identifiers:

 * The recommended spelling of `(a, b)` in identifiers is `mk`. -/
Lean.Parser.Term.tuple : Lean.Parser.Parser
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
/-- Etale is stable under base change.  -/
AlgebraicGeometry.Etale.etale_isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.Etale
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reverse_mul_X_pow : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (n : ℕ), (p * Polynomial.X ^ n).reverse = p.reverse
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.MonadHom.comp_toNatTrans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ T₂ T₃ : CategoryTheory.Monad C} (f : T₁ ⟶ T₂)
  (g : T₂ ⟶ T₃),
  (CategoryTheory.CategoryStruct.comp f g).toNatTrans = CategoryTheory.CategoryStruct.comp f.toNatTrans g.toNatTrans
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.IsTuranMaximal.eq_1 : ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj] (r : ℕ),
  G.IsTuranMaximal r = G.IsExtremal fun x => x.CliqueFree (r + 1)
-- Mathlib.Logic.Embedding.Set
Function.Embedding.optionEmbeddingEquiv_apply_snd_coe : ∀ (α : Type u_1) (β : Type u_2) (f : Option α ↪ β), ↑((Function.Embedding.optionEmbeddingEquiv α β) f).snd = f none
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.mkPiRing_eq_zero_iff : ∀ {R : Type u} {ι : Type v} {M : Type u_1} [inst : Fintype ι] [inst_1 : CommRing R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : TopologicalSpace R] [inst_5 : TopologicalSpace M] [inst_6 : ContinuousMul R]
  [inst_7 : ContinuousSMul R M] (z : M), ContinuousMultilinearMap.mkPiRing R ι z = 0 ↔ z = 0
-- Mathlib.Data.Finset.Sort
Finset.max'_eq_sorted_last : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {h : s.Nonempty},
  s.max' h = (s.sort fun a b => a ≤ b)[(s.sort fun a b => a ≤ b).length - 1]