mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.VectorBundle.Basic
/-- Rewrite `ContinuousLinearMap.inCoordinates` using continuous linear equivalences.  -/
ContinuousLinearMap.inCoordinates_eq : ∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : (x : B) → AddCommMonoid (E x)]
  [inst_1 : NormedAddCommGroup F] [inst_2 : TopologicalSpace B] [inst_3 : (x : B) → TopologicalSpace (E x)]
  {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} [inst_4 : NontriviallyNormedField 𝕜₁] [inst_5 : NontriviallyNormedField 𝕜₂]
  {σ : 𝕜₁ →+* 𝕜₂} {B' : Type u_7} [inst_6 : TopologicalSpace B'] [inst_7 : NormedSpace 𝕜₁ F]
  [inst_8 : (x : B) → Module 𝕜₁ (E x)] [inst_9 : TopologicalSpace (Bundle.TotalSpace F E)] {F' : Type u_8}
  [inst_10 : NormedAddCommGroup F'] [inst_11 : NormedSpace 𝕜₂ F'] {E' : B' → Type u_9}
  [inst_12 : (x : B') → AddCommMonoid (E' x)] [inst_13 : (x : B') → Module 𝕜₂ (E' x)]
  [inst_14 : TopologicalSpace (Bundle.TotalSpace F' E')] [inst_15 : FiberBundle F E] [inst_16 : VectorBundle 𝕜₁ F E]
  [inst_17 : (x : B') → TopologicalSpace (E' x)] [inst_18 : FiberBundle F' E'] [inst_19 : VectorBundle 𝕜₂ F' E']
  {x₀ x : B} {y₀ y : B'} {ϕ : E x →SL[σ] E' y} (hx : x ∈ (trivializationAt F E x₀).baseSet)
  (hy : y ∈ (trivializationAt F' E' y₀).baseSet),
  ContinuousLinearMap.inCoordinates F E F' E' x₀ x y₀ y ϕ =
    ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜₂ (trivializationAt F' E' y₀) y hy) ∘SL
      ϕ ∘SL ↑(Bundle.Trivialization.continuousLinearEquivAt 𝕜₁ (trivializationAt F E x₀) x hx).symm
-- Mathlib.CategoryTheory.FinCategory.Basic
CategoryTheory.discreteFintype : {α : Type u_1} → [Fintype α] → Fintype (CategoryTheory.Discrete α)
-- Mathlib.RingTheory.Adjoin.FG
Subalgebra.fg_of_fg_toSubmodule : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S : Subalgebra R A},
  (Subalgebra.toSubmodule S).FG → S.FG
-- Mathlib.Data.List.Basic
List.cons_subset_of_subset_of_mem : ∀ {α : Type u} {a : α} {l m : List α}, a ∈ m → l ⊆ m → a :: l ⊆ m
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddGroupHom.extension_def : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] {H : Type u_2} [inst_1 : SeminormedAddCommGroup H]
  [inst_2 : T0Space H] [inst_3 : CompleteSpace H] (f : NormedAddGroupHom G H) (v : G),
  f.extension ↑v = UniformSpace.Completion.extension ⇑f ↑v
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
/-- Pushout cocones from `X` are the same thing as binary cofans in `Under X`.  -/
CategoryTheory.Limits.pushoutCoconeEquivBinaryCofan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          CategoryTheory.Limits.PushoutCocone f g ≌
            CategoryTheory.Limits.BinaryCofan (CategoryTheory.Under.mk f) (CategoryTheory.Under.mk g)
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
/-- A section `F.obj (op j) → F.obj (op (Order.succ j))` to the restriction
`F.obj (op (Order.succ j)) → F.obj (op j)` when `j` is not maximal.  -/
CategoryTheory.Functor.WellOrderInductionData.succ : {J : Type u} →
  [inst : LinearOrder J] →
    [inst_1 : SuccOrder J] →
      {F : CategoryTheory.Functor Jᵒᵖ (Type v)} →
        F.WellOrderInductionData → (j : J) → ¬IsMax j → F.obj (Opposite.op j) → F.obj (Opposite.op (Order.succ j))
-- Mathlib.RingTheory.Ideal.Maps
Ideal.symm_apply_mem_of_equiv_iff : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {I : Ideal R} {f : R ≃+* S} {y : S},
  f.symm y ∈ I ↔ y ∈ Ideal.map f I
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.coe_inclusion : ∀ {M : Type u_1} [inst : MulOneClass M] {S T : Submonoid M} (h : S ≤ T) (a : ↥S), ↑((Submonoid.inclusion h) a) = ↑a
-- Mathlib.Probability.Density
ProbabilityTheory.IndepFun.add_hasPDF' : ∀ {Ω : Type u_1} {G : Type u_2} {mΩ : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [inst : AddGroup G]
  {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant]
  {X Y : Ω → G} [MeasureTheory.SFinite μ] [MeasureTheory.HasPDF X ℙ μ] [MeasureTheory.HasPDF Y ℙ μ],
  MeasureTheory.SigmaFinite (MeasureTheory.Measure.map X ℙ) →
    MeasureTheory.SigmaFinite (MeasureTheory.Measure.map Y ℙ) →
      ProbabilityTheory.IndepFun X Y ℙ → MeasureTheory.HasPDF (X + Y) ℙ μ
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.toList_formPerm_isRotated_self : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (l : List α),
  2 ≤ l.length → l.Nodup → ∀ x ∈ l, l.formPerm.toList x ~r l
-- Init.Data.Array.Erase
Array.eraseIdx_set_eq : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {a : α} {h : i < xs.size}, (xs.set i a h).eraseIdx i ⋯ = xs.eraseIdx i h
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mapIsometry_symm_apply_carrier : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : MetricSpace Y] (f : X ≃ᵢ Y) (D : Delone.DeloneSet Y),
  ((Delone.DeloneSet.mapIsometry f).symm D).carrier = ⇑f.symm '' D.carrier
-- Mathlib.MeasureTheory.Group.FoelnerFilter
/-- If there exists a non-trivial Følner filter with respect to some group `G` acting on a measure
space `X`, then there exists a `G`-invariant finitely additive probability measure on `X`.  -/
IsFoelner.amenable : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : Group G]
  [inst_2 : MulAction G X] {ι : Type u_3} {l : Filter ι} {F : ι → Set X} [MeasureTheory.SMulInvariantMeasure G X μ]
  [l.NeBot],
  IsFoelner G μ l F →
    ∃ m,
      m Set.univ = 1 ∧
        (∀ (s t : Set X), MeasurableSet t → Disjoint s t → m (s ∪ t) = m s + m t) ∧
          ∀ (g : G) (s : Set X), m (g • s) = m s
-- Mathlib.Data.Sym.Sym2.Finsupp
Finsupp.sym2Mul_apply_mk : ∀ {α : Type u_1} {M₀ : Type u_2} [inst : CommMonoidWithZero M₀] {f : α →₀ M₀} (a b : α), f.sym2Mul s(a, b) = f a * f b
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} {I : CategoryTheory.InjectiveResolution Z} {Z' : C}
  {I' : CategoryTheory.InjectiveResolution Z'} {f : Z ⟶ Z'} (self : I.Hom I' f) {Z_1 : C} (h : I'.cocomplex.X 0 ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (I.ι.f 0) (CategoryTheory.CategoryStruct.comp (self.hom.f 0) h) =
    CategoryTheory.CategoryStruct.comp (((CochainComplex.single₀ C).map f).f 0)
      (CategoryTheory.CategoryStruct.comp (I'.ι.f 0) h)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.InjectiveTheorem.levelParams : Lean.Meta.Grind.InjectiveTheorem → Array Lean.Name
-- Init.Data.Array.Lemmas
Array.getElem?_append_right : ∀ {α : Type u_1} {xs ys : Array α} {i : ℕ}, xs.size ≤ i → (xs ++ ys)[i]? = ys[i - xs.size]?
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
/-- The number of mixed embeddings over an infinite place is twice the number of ramified places
over the place.  -/
NumberField.InfinitePlace.ramifiedPlacesOver_ncard : ∀ {K : Type u_4} (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  (v : NumberField.InfinitePlace K),
  2 * (NumberField.InfinitePlace.ramifiedPlacesOver L v).ncard =
    (NumberField.ComplexEmbedding.mixedEmbeddingsOver L v.embedding).ncard
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- For `X : Truncated C n` and `m ≤ n`, `X ^⦋m⦌ₙ` is the `m`-th term of X. The
proof `p : m ≤ n` can also be provided using the syntax `X ^⦋m, p⦌ₙ`.  -/
CategoryTheory.CosimplicialObject.Truncated.mkNotation : Lean.TrailingParserDescr
-- Init.Data.String.Defs
String.toByteArray_ofList : ∀ {l : List Char}, (String.ofList l).toByteArray = l.utf8Encode
-- Mathlib.Algebra.Category.Ring.Limits
/-- A choice of limit cone for a functor into `CommSemiRingCat`.
(Generally, you'll just want to use `limit F`.)
 -/
CommSemiRingCat.limitCone : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommSemiRingCat) →
      [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommSemiRingCat)).sections] → CategoryTheory.Limits.Cone F
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isBigO_abs_abs`. -/
Asymptotics.IsBigO.of_abs_abs : ∀ {α : Type u_1} {l : Filter α} {u v : α → ℝ}, ((fun x => |u x|) =O[l] fun x => |v x|) → u =O[l] v
-- Mathlib.SetTheory.Ordinal.Veblen
/-- **Alias** of `Ordinal.iterate_veblen_lt_gamma_zero`.

---

`veblen (veblen … (veblen 0 0) … 0) 0 < Γ₀`  -/
Ordinal.iterate_veblen_lt_gamma0 : ∀ (n : ℕ), (fun a => Ordinal.veblen a 0)^[n] 0 < Ordinal.gamma 0
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.erase_ne : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) {n i : ℕ}, i ≠ n → (Polynomial.erase n p).coeff i = p.coeff i
-- Mathlib.Data.List.Fold
/-- **First Bird–Wadler duality theorem** for commutative functions.  -/
List.foldl_eq_foldr : ∀ {α : Type u_1} {l : List α} {a : α} {f : α → α → α} [hf : Std.Commutative f] [Std.Associative f],
  List.foldl f a l = List.foldr f a l
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_mor₃ : ∀ {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]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (j : C),
  ((t.triangleLEGT n).obj j).mor₃ = (t.truncGTδLE n).app j
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.uncurry_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X Y : C}
  [inst_2 : CategoryTheory.Closed A] (g : Y ⟶ A ⟹ X),
  CategoryTheory.MonoidalClosed.uncurry g =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g)
      ((CategoryTheory.ihom.ev A).app X)
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- **Cauchy-Goursat theorem for a rectangle**: the integral of a complex differentiable function
over the boundary of a rectangle equals zero. More precisely, if `f` is continuous on a closed
rectangle and is complex differentiable on the corresponding open rectangle, then its integral over
the boundary of the rectangle equals zero.  -/
Complex.integral_boundary_rect_eq_zero_of_continuousOn_of_differentiableOn : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (z w : ℂ),
  ContinuousOn f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) →
    DifferentiableOn ℂ f (Set.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im)) →
      (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) - ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) +
            Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) -
          Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) =
        0
-- Mathlib.LinearAlgebra.Prod
Submodule.prod_eq_bot_iff : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] {p₁ : Submodule R M} {p₂ : Submodule R M₂},
  p₁.prod p₂ = ⊥ ↔ p₁ = ⊥ ∧ p₂ = ⊥
-- Mathlib.CategoryTheory.Sites.LeftExact
CategoryTheory.toSheafify_plusPlusIsoSheafify_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w)
  [inst_1 : CategoryTheory.Category.{t, w} D]
  [inst_2 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] {FD : D → D → Type u_1}
  {CD : D → Type t} [inst_4 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_5 : CategoryTheory.ConcreteCategory D FD]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [inst_7 : (CategoryTheory.forget D).ReflectsIsomorphisms]
  [inst_8 :
    ∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  (P : CategoryTheory.Functor Cᵒᵖ D) {Z : CategoryTheory.Functor Cᵒᵖ D} (h : CategoryTheory.sheafify J P ⟶ Z),
  CategoryTheory.CategoryStruct.comp (J.toSheafify P)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.plusPlusIsoSheafify J D P).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.toSheafify J P) h
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Summable.comp_injective : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace α] [inst_1 : AddCommGroup α] [IsUniformAddGroup α]
  {f : β → α} [CompleteSpace α] {i : γ → β}, Summable f → Function.Injective i → Summable (f ∘ i)
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The canonical morphism from the limit of `F` to the limit of `E ⋙ F`.
 -/
CategoryTheory.Limits.limit.pre : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} C] →
            (F : CategoryTheory.Functor J C) →
              [inst_3 : CategoryTheory.Limits.HasLimit F] →
                (E : CategoryTheory.Functor K J) →
                  [inst_4 : CategoryTheory.Limits.HasLimit (E.comp F)] →
                    CategoryTheory.Limits.limit F ⟶ CategoryTheory.Limits.limit (E.comp F)
-- Mathlib.Data.Fin.Basic
Fin.one_lt_last : ∀ {n : ℕ} [NeZero n], 1 < Fin.last (n + 1)
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Equiv.mk.inj : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} {inst : AddGroup N} {inst_1 : AddGroup E} {inst_2 : AddGroup G}
  {S : AddGroupExtension N E G} {E' : Type u_4} {inst_3 : AddGroup E'} {S' : AddGroupExtension N E' G}
  {toAddEquiv : E ≃+ E'} {inl_comm : ⇑toAddEquiv ∘ ⇑S.inl = ⇑S'.inl}
  {rightHom_comm : ⇑S'.rightHom ∘ ⇑toAddEquiv = ⇑S.rightHom} {toAddEquiv_1 : E ≃+ E'}
  {inl_comm_1 : ⇑toAddEquiv_1 ∘ ⇑S.inl = ⇑S'.inl} {rightHom_comm_1 : ⇑S'.rightHom ∘ ⇑toAddEquiv_1 = ⇑S.rightHom},
  { toAddEquiv := toAddEquiv, inl_comm := inl_comm, rightHom_comm := rightHom_comm } =
      { toAddEquiv := toAddEquiv_1, inl_comm := inl_comm_1, rightHom_comm := rightHom_comm_1 } →
    toAddEquiv = toAddEquiv_1
-- Mathlib.AlgebraicGeometry.LimitsOver
AlgebraicGeometry.instHasColimitOverScheme : ∀ {S : AlgebraicGeometry.Scheme} {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J]
  (F : CategoryTheory.Functor J (CategoryTheory.Over S))
  [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (CategoryTheory.Over.Hom.left (F.map f))]
  [(F.comp ((CategoryTheory.Over.forget S).comp AlgebraicGeometry.Scheme.forget)).IsLocallyDirected] [Quiver.IsThin J]
  [Small.{u, u_1} J], CategoryTheory.Limits.HasColimit F
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.IsRegularMono.uniq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y W : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.IsRegularMono f] (k : W ⟶ Y)
  (h :
    CategoryTheory.CategoryStruct.comp k (CategoryTheory.IsRegularMono.left f) =
      CategoryTheory.CategoryStruct.comp k (CategoryTheory.IsRegularMono.right f))
  (m : W ⟶ X), CategoryTheory.CategoryStruct.comp m f = k → m = CategoryTheory.IsRegularMono.lift f k h
-- Mathlib.CategoryTheory.Bicategory.Free
_private.Mathlib.CategoryTheory.Bicategory.Free.0.CategoryTheory.FreeBicategory.liftHom.match_1.eq_3 : ∀ {B : Type u_1} [inst : Quiver B] (motive : (x x_1 : CategoryTheory.FreeBicategory B) → (x ⟶ x_1) → Sort u_3)
  (x x_1 b : B) (f : CategoryTheory.FreeBicategory.Hom x b) (g : CategoryTheory.FreeBicategory.Hom b x_1)
  (h_1 : (x x_2 : B) → (f : x ⟶ x_2) → motive x x_2 (CategoryTheory.FreeBicategory.Hom.of f))
  (h_2 : (a : B) → motive a a (CategoryTheory.FreeBicategory.Hom.id a))
  (h_3 :
    (x x_2 b : B) →
      (f : CategoryTheory.FreeBicategory.Hom x b) →
        (g : CategoryTheory.FreeBicategory.Hom b x_2) → motive x x_2 (f.comp g)),
  (match x, x_1, f.comp g with
    | x, x_2, CategoryTheory.FreeBicategory.Hom.of f => h_1 x x_2 f
    | a, .(a), CategoryTheory.FreeBicategory.Hom.id .(a) => h_2 a
    | x, x_2, f.comp g => h_3 x x_2 b f g) =
    h_3 x x_1 b f g
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_replaceEntry_of_true : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β},
  Std.Internal.List.containsKey k l = true →
    (k == a) = true → Std.Internal.List.getValue? a (Std.Internal.List.replaceEntry k v l) = some v
-- Init.Core
instBEqOption.beq : {α : Type u_1} → [BEq α] → Option α → Option α → Bool
-- Mathlib.Order.Bounds.Defs
/-- The set of upper bounds of a set.  -/
upperBounds : {α : Type u_1} → [LE α] → Set α → Set α
-- Mathlib.GroupTheory.Subgroup.Center
AddSubgroup.center_sum : ∀ {G : Type u_1} [inst : AddGroup G] {H : Type u_2} [inst_1 : AddGroup H],
  AddSubgroup.center (G × H) = (AddSubgroup.center G).prod (AddSubgroup.center H)
-- Mathlib.Analysis.Normed.Algebra.DualNumber
DualNumber.exp_smul_eps : ∀ {R : Type u_1} [inst : CommRing R] [Algebra ℚ R] [inst_2 : UniformSpace R] [inst_3 : IsTopologicalRing R] [T2Space R]
  (r : R), NormedSpace.exp (r • DualNumber.eps) = 1 + r • DualNumber.eps
-- Mathlib.RingTheory.HopfAlgebra.Convolution
AlgHom.convInv : {R : Type u_1} →
  {A : Type u_2} →
    {C : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : CommSemiring C] → [inst_3 : Bialgebra R C] → [inst_4 : HopfAlgebra R A] → Inv (WithConv (A →ₐ[R] C))
-- Init.Data.String.Lemmas.Basic
String.Slice.toByteArray_copy_slice : ∀ {s : String.Slice} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂},
  (s.slice p₁ p₂ h).copy.toByteArray = s.copy.toByteArray.extract p₁.offset.byteIdx p₂.offset.byteIdx
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.module : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_4} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {N : Type u_6} →
                  [inst_4 : TopologicalSpace N] →
                    [inst_5 : ChartedSpace H N] →
                      {n : WithTop ℕ∞} →
                        {V : Type u_10} →
                          [inst_6 : NormedAddCommGroup V] →
                            [inst_7 : NormedSpace 𝕜 V] → Module 𝕜 (ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V n)
-- Mathlib.Order.Lattice.Nat
Nat.sInf_upward_closed_eq_succ_iff : ∀ {s : Set ℕ}, (∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s) → ∀ (k : ℕ), sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.SavedState.mk.inj : ∀ {term : Lean.Elab.Term.SavedState} {tactic : Lean.Elab.Tactic.State} {term_1 : Lean.Elab.Term.SavedState}
  {tactic_1 : Lean.Elab.Tactic.State},
  { term := term, tactic := tactic } = { term := term_1, tactic := tactic_1 } → term = term_1 ∧ tactic = tactic_1
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.div_inter_subset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s t₁ t₂ : Finset α}, s / (t₁ ∩ t₂) ⊆ s / t₁ ∩ (s / t₂)
-- Lean.Parser.Term
Lean.Parser.Term.typeOf : Lean.Parser.Parser
-- Mathlib.Order.Filter.Tendsto
Filter.tendsto_inf : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x : Filter α} {y₁ y₂ : Filter β},
  Filter.Tendsto f x (y₁ ⊓ y₂) ↔ Filter.Tendsto f x y₁ ∧ Filter.Tendsto f x y₂
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
FundamentalGroupoidFunctor.prodIso_hom : ∀ (A : TopCat) (B : TopCat), (FundamentalGroupoidFunctor.prodIso A B).hom = FundamentalGroupoidFunctor.prodToProdTop A B
-- Mathlib.Algebra.Group.Commute.Defs
Commute.instSymm : ∀ {S : Type u_3} [inst : Mul S], Std.Symm Commute
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.powerMap_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {U V : CategoryTheory.Limits.FormalCoproduct C} (f : U ⟶ V)
  (α : Type t) [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C],
  (CategoryTheory.Limits.FormalCoproduct.powerMap f α).φ = fun i => CategoryTheory.Limits.Pi.map fun a => f.φ (i a)
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffOn.analyticOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F}, ContDiffOn 𝕜 ⊤ f s → AnalyticOn 𝕜 f s
-- Mathlib.Algebra.Tropical.Basic
Tropical.mul_eq_zero_iff : ∀ {R : Type u_1} [inst : AddCommMonoid R] {a b : Tropical (WithTop R)}, a * b = 0 ↔ a = 0 ∨ b = 0
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
/-- The subalgebra of symmetric `MvPolynomial`s.  -/
MvPolynomial.symmetricSubalgebra : (σ : Type u_5) → (R : Type u_6) → [inst : CommSemiring R] → Subalgebra R (MvPolynomial σ R)
-- Init.Data.BitVec.Bitblast
BitVec.divRec_zero : ∀ {w : ℕ} {args : BitVec.DivModArgs w} (qr : BitVec.DivModState w), BitVec.divRec 0 args qr = qr
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∉ m₁ → (m₁ ∪ m₂).get? k = m₂.get? k
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.singleton.inj : ∀ {ι : Type u_1} {M : ι → Type u_2} {inst : (i : ι) → Monoid (M i)} {i : ι} {x : M i} {a : x ≠ 1} {x_1 : M i}
  {a_1 : x_1 ≠ 1}, Monoid.CoprodI.NeWord.singleton x a = Monoid.CoprodI.NeWord.singleton x_1 a_1 → x = x_1
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.const_mul : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace M] [inst_1 : Mul M] {m : MeasurableSpace α} {f : α → M}
  {μ : MeasureTheory.Measure α} [MeasurableMul M], AEMeasurable f μ → ∀ (c : M), AEMeasurable (fun x => c * f x) μ
-- Mathlib.Order.Interval.Set.OrderIso
OrderIso.preimage_Icc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (a b : β),
  ⇑e ⁻¹' Set.Icc a b = Set.Icc (e.symm a) (e.symm b)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α},
      cmp k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
          k ∈ List.map Sigma.fst l → (t.insertMany l).getKey? k' = some k
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.coe_toWeightBasisInt_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [inst_5 : CharZero R] (i : ↥b.support), ↑(b.toWeightBasisInt i) = P.root ↑i
-- Mathlib.Order.Lattice
toDual_sup : ∀ {α : Type u} [inst : Max α] (a b : α), OrderDual.toDual (a ⊔ b) = OrderDual.toDual a ⊓ OrderDual.toDual b
-- Mathlib.FieldTheory.Relrank
/-- If `A ≤ B`, then `IntermediateField.relrank A B` is `[B : A]`  -/
IntermediateField.relfinrank_eq_finrank_of_le : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A B : IntermediateField F E}
  (h : A ≤ B), A.relfinrank B = Module.finrank ↥A ↥(IntermediateField.extendScalars h)
-- Mathlib.NumberTheory.SmoothNumbers
/-- If `p ∉ s` is a prime and `n` is `s`-factored, then `p` and `n` are coprime.  -/
Nat.Prime.factoredNumbers_coprime : ∀ {s : Finset ℕ} {p n : ℕ}, Nat.Prime p → p ∉ s → n ∈ Nat.factoredNumbers s → p.Coprime n
-- Mathlib.Logic.Relation
/-- A sufficient condition for the Church-Rosser property.  -/
Relation.church_rosser : ∀ {α : Type u_1} {r : α → α → Prop} {a b c : α},
  (∀ (a b c : α), r a b → r a c → ∃ d, Relation.ReflGen r b d ∧ Relation.ReflTransGen r c d) →
    Relation.ReflTransGen r a b → Relation.ReflTransGen r a c → Relation.Join (Relation.ReflTransGen r) b c