mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.InitialSeg
_private.Mathlib.Order.InitialSeg.0.collapseF_lt : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder β s] (f : r ↪r s) {a a' : α},
  r a' a → s ↑(collapseF✝ f a') ↑(collapseF✝ f a)
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_eq_on_Ico : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] (n : ℤ),
  ∀ a ∈ Set.Ico (↑n) (↑n + 1), ⌊a⌋ = n
-- Init.Data.Float.Float32
instAddFloat32 : Add Float32
-- Mathlib.Data.Matrix.Basic
Matrix.diagonalAlgHom_apply : ∀ {n : Type u_3} (R : Type u_7) {α : Type u_11} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  [inst_3 : Semiring α] [inst_4 : Algebra R α] (d : n → α), (Matrix.diagonalAlgHom R) d = Matrix.diagonal d
-- Mathlib.Order.RelIso.Basic
RelIso.coe_symm_ofOnFun : ∀ {α : Type u_1} {β : Type u_2} (r : β → β → Prop) (f : α ≃ β), ⇑(RelIso.ofOnFun r f).symm = ⇑f.symm
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- If `X` is a real random variable with Gaussian law with mean `μ` and variance `v`, then `X * c`
has Gaussian law with mean `c * μ` and variance `c ^ 2 * v`.  -/
ProbabilityTheory.gaussianReal_div_const : ∀ {μ : ℝ} {v : NNReal} {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : Ω → ℝ},
  ProbabilityTheory.HasLaw X (ProbabilityTheory.gaussianReal μ v) P →
    ∀ (c : ℝ),
      ProbabilityTheory.HasLaw (fun ω => X ω / c) (ProbabilityTheory.gaussianReal (μ / c) (v / NNReal.mk (c ^ 2) ⋯)) P
-- Mathlib.Order.Category.DistLat
DistLat.hom_id : ∀ {X : DistLat}, DistLat.Hom.hom (CategoryTheory.CategoryStruct.id X) = LatticeHom.id ↑X
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_val : ∀ {M : Type u_3} [inst : AddCommMonoid M] (s : Finset M), s.val.sum = s.sum id
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.instRespectsIsoTrW : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C), P.trW.RespectsIso
-- Mathlib.Algebra.SkewMonoidAlgebra.Support
SkewMonoidAlgebra.support_neg : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommGroup k] (p : SkewMonoidAlgebra k G), (-p).support = p.support
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.AbsolutelyContinuous.smul_left : ∀ {α : Type u_1} {R : Type u_5} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : SMul R ENNReal]
  [inst_1 : IsScalarTower R ENNReal ENNReal], μ.AbsolutelyContinuous ν → ∀ (c : R), (c • μ).AbsolutelyContinuous ν
-- Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction
UpperHalfPlane.instProperSMul : ProperSMul (Matrix.SpecialLinearGroup (Fin 2) ℝ) UpperHalfPlane
-- Init.LawfulBEqTactics
DerivingHelpers.deriving_lawful_beq_helper_dep : ∀ {α : Type u_1} {x y : α} [inst : BEq α] [inst_1 : ReflBEq α] {t : (x == y) = true → Bool} {P : Prop},
  ((x == y) = true → x = y) → (∀ (h : x = y), t ⋯ = true → P) → (if h : (x == y) = true then t h else false) = true → P
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.isPrime_iff_of_isPrincipalIdealRing_of_noZeroDivisors : ∀ {α : Type u} [inst : CommSemiring α] [IsPrincipalIdealRing α] [NoZeroDivisors α] [Nontrivial α] {P : Ideal α},
  P.IsPrime ↔ P = ⊥ ∨ ∃ p, Prime p ∧ P = Ideal.span {p}
-- Mathlib.Topology.Category.CompactlyGenerated
CompactlyGenerated.mk.sizeOf_spec : ∀ (toTop : TopCat) [is_compactly_generated : UCompactlyGeneratedSpace ↑toTop],
  sizeOf { toTop := toTop, is_compactly_generated := is_compactly_generated } =
    1 + sizeOf toTop + sizeOf is_compactly_generated
-- Mathlib.Algebra.Ring.Subring.Defs
/-- A subring of a domain is a domain.  -/
Subring.instIsDomainSubtypeMem : ∀ {R : Type u_1} [inst : Ring R] [IsDomain R] (s : Subring R), IsDomain ↥s
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.isLocal_iff_isIso_map : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : G ⊣ F) [F.Full] [F.Faithful] {X Y : D} (f : X ⟶ Y),
  CategoryTheory.ObjectProperty.isLocal (fun x => x ∈ Set.range F.obj) f ↔ CategoryTheory.IsIso (G.map f)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.Nonempty.vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set α} {t : Set β}, s.Nonempty → t.Nonempty → (s +ᵥ t).Nonempty
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.sub_self : ∀ (a : Ordinal.{u_4}), a - a = 0
-- Init.Data.List.MinMaxOn
List.maxOn?.fun_cases_unfolding : ∀ {β : Type u_1} {α : Type u_2} [i : LE β] [inst : DecidableLE β] (f : α → β) (l : List α) (motive : Option α → Prop),
  motive (List.minOn? f l) → motive (List.maxOn? f l)
-- Mathlib.Data.WSeq.Defs
Stream'.WSeq.length_eq_map : ∀ {α : Type u} (s : Stream'.WSeq α), s.length = Computation.map List.length s.toList
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.mk.inj : ∀ {R : Type u_14} {S : Type u_15} {inst : Semiring R} {inst_1 : Semiring S} {σ : R →+* S} {σ' : S →+* R}
  {inst_2 : RingHomInvPair σ σ'} {inst_3 : RingHomInvPair σ' σ} {M : Type u_16} {M₂ : Type u_17}
  {inst_4 : AddCommMonoid M} {inst_5 : AddCommMonoid M₂} {inst_6 : Module R M} {inst_7 : Module S M₂}
  {toLinearMap : M →ₛₗ[σ] M₂} {invFun : M₂ → M}
  {left_inv : autoParam (Function.LeftInverse invFun toLinearMap.toFun) Equiv.left_inv._autoParam}
  {right_inv : autoParam (Function.RightInverse invFun toLinearMap.toFun) Equiv.right_inv._autoParam}
  {toLinearMap_1 : M →ₛₗ[σ] M₂} {invFun_1 : M₂ → M}
  {left_inv_1 : autoParam (Function.LeftInverse invFun_1 toLinearMap_1.toFun) Equiv.left_inv._autoParam}
  {right_inv_1 : autoParam (Function.RightInverse invFun_1 toLinearMap_1.toFun) Equiv.right_inv._autoParam},
  { toLinearMap := toLinearMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
      { toLinearMap := toLinearMap_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 } →
    toLinearMap = toLinearMap_1 ∧ invFun = invFun_1
-- Mathlib.Data.Real.ENatENNReal
ENat.map_coe_nnreal : ENat.map Nat.cast = ENat.toENNReal
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.OplaxTrans.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          (app : (a : B) → F.obj a ⟶ G.obj a) →
            (naturality :
                {a b : B} →
                  (f : a ⟶ b) →
                    CategoryTheory.CategoryStruct.comp (F.map f) (app b) ⟶
                      CategoryTheory.CategoryStruct.comp (app a) (G.map f)) →
              autoParam
                  (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
                    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (app b))
                        (naturality g) =
                      CategoryTheory.CategoryStruct.comp (naturality f)
                        (CategoryTheory.Bicategory.whiskerLeft (app a) (G.map₂ η)))
                  CategoryTheory.Lax.OplaxTrans.naturality_naturality._autoParam →
                autoParam
                    (∀ (a : B),
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (app a))
                          (naturality (CategoryTheory.CategoryStruct.id a)) =
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (app a)).hom
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (app a)).inv
                            (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapId a))))
                    CategoryTheory.Lax.OplaxTrans.naturality_id._autoParam →
                  autoParam
                      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
                        CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (app c))
                            (naturality (CategoryTheory.CategoryStruct.comp f g)) =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (app c)).hom
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.Bicategory.whiskerLeft (F.map f) (naturality g))
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.Bicategory.associator (F.map f) (app b) (G.map g)).inv
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.Bicategory.whiskerRight (naturality f) (G.map g))
                                  (CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.Bicategory.associator (app a) (G.map f) (G.map g)).hom
                                    (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapComp f g)))))))
                      CategoryTheory.Lax.OplaxTrans.naturality_comp._autoParam →
                    CategoryTheory.Lax.OplaxTrans F G
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoid.End.ext_iff : ∀ {M : Type u_4} [inst : AddZero M] {f g : AddMonoid.End M}, f = g ↔ ∀ (x : M), f x = g x
-- Mathlib.Data.Multiset.Defs
Multiset.subset_iff : ∀ {α : Type u_1} {s t : Multiset α}, s ⊆ t ↔ ∀ ⦃x : α⦄, x ∈ s → x ∈ t
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- A variant of `Matrix.det_neg` with scalar multiplication by `Units ℤ` instead of multiplication
by `R`.  -/
Matrix.det_neg_eq_smul : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : Matrix n n R),
  (-A).det = (-1) ^ Fintype.card n • A.det
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.instSMulCommClassSubtypeMemCenter_1 : ∀ {R : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : MulAction R M],
  SMulCommClass (↥(Subsemiring.center R)) R M
-- Mathlib.Topology.UniformSpace.Basic
uniformSpace_comap_id : ∀ {α : Type u_2}, UniformSpace.comap id = id
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Internal.Impl.any.eq_1 : ∀ {α : Type u} {β : α → Type v} (t : Std.DTreeMap.Internal.Impl α β) (p : (a : α) → β a → Bool),
  t.any p =
    (do
        let __s ←
          forIn t (none, ()) fun x __s =>
              match x with
              | ⟨a, b⟩ =>
                if p a b = true then pure (ForInStep.done (some true, ())) else pure (ForInStep.yield (none, ()))
        have __r : Option Bool × Unit := __s
        match __r.1 with
          | some r => pure r
          | none => pure false).run
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- For `neg ≫ neg = 𝟙` see `neg_comp_neg`.  -/
CategoryTheory.AddGrpObj.neg_neg : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : C) [inst_2 : CategoryTheory.AddGrpObj A],
  CategoryTheory.inv CategoryTheory.AddGrpObj.neg = CategoryTheory.AddGrpObj.neg
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.isClosed_C1 : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  IsClosed C → ∀ (ho : o < Ordinal.type fun x1 x2 => x1 < x2), IsClosed (Profinite.NobelingProof.C1 C ho)
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.neg : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_2} →
      {N : Type u_3} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommMonoid N] → [inst_3 : Module R M] → [inst_4 : Module R N] → Neg (TensorProduct R M N)
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symm_smul : ∀ {S : Type u_14} {R : Type u_15} {V : Type u_16} {W : Type u_17} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid V] [inst_3 : Module R V] [inst_4 : Module S V] [inst_5 : AddCommMonoid W]
  [inst_6 : Module R W] [inst_7 : Module S W] [inst_8 : SMulCommClass R S W] [inst_9 : SMul S R]
  [inst_10 : IsScalarTower S R V] [inst_11 : IsScalarTower S R W] [inst_12 : SMulCommClass R S V] (e : V ≃ₗ[R] W)
  (α : Sˣ), (α • e).symm = α⁻¹ • e.symm
-- Lean.Parser.Do
Lean.Parser.Term.do.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Mapping by the composite morphism `f ≫ g` is the same as mapping by `f` then by `g`.  -/
CategoryTheory.Under.mapComp_eq : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.Under.map (CategoryTheory.CategoryStruct.comp f g) =
    (CategoryTheory.Under.map g).comp (CategoryTheory.Under.map f)
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- `circumcenterWeightsWithCircumcenter` sums to 1.  -/
Affine.Simplex.sum_circumcenterWeightsWithCircumcenter : ∀ (n : ℕ), ∑ i, Affine.Simplex.circumcenterWeightsWithCircumcenter n i = 1
-- Lean.Message
Lean.MessageSeverity.error.sizeOf_spec : sizeOf Lean.MessageSeverity.error = 1
-- Mathlib.Order.Interval.Set.Image
Set.preimage_subtype_val_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {p : α → Prop} (a : { x // p x }), Subtype.val ⁻¹' Set.Ioi ↑a = Set.Ioi a
-- Mathlib.ModelTheory.Definability
/-- The identity function is `TermDefinable₁`  -/
Set.TermDefinable₁.id : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M], Set.TermDefinable₁ L id
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Coyoneda.ULiftCoyoneda.instFullOppositeFunctorTypeUliftCoyoneda : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C], CategoryTheory.uliftCoyoneda.{w, v₁, u₁}.Full
-- Mathlib.Order.ModularLattice
infIooOrderIsoIooSup_apply_coe : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : IsModularLattice α] (a b : α) (c : ↑(Set.Ioo (a ⊓ b) a)),
  ↑((infIooOrderIsoIooSup a b) c) = ↑c ⊔ b
-- Lean.Data.Lsp.Internal
/-- Used in the `$/lean/ileanHeaderSetupInfo` watchdog <- worker notifications.
Contains status information about `lake setup-file` and the direct imports of the file managed by
a worker.
 -/
Lean.Lsp.LeanILeanHeaderSetupInfoParams : Type
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.le_hittingBtwn : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n m : ι}, n ≤ m → ∀ (ω : Ω), n ≤ MeasureTheory.hittingBtwn u s n m ω
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum_sum_index : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] {ι₁ : Type u₁} [inst_1 : DecidableEq ι₁]
  {β₁ : ι₁ → Type v₁} [inst_2 : (i₁ : ι₁) → Zero (β₁ i₁)] [inst_3 : (i : ι₁) → (x : β₁ i) → Decidable (x ≠ 0)]
  [inst_4 : (i : ι) → AddCommMonoid (β i)] [inst_5 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_6 : AddCommMonoid γ]
  {f : Π₀ (i₁ : ι₁), β₁ i₁} {g : (i₁ : ι₁) → β₁ i₁ → Π₀ (i : ι), β i} {h : (i : ι) → β i → γ},
  (∀ (i : ι), h i 0 = 0) →
    (∀ (i : ι) (b₁ b₂ : β i), h i (b₁ + b₂) = h i b₁ + h i b₂) → (f.sum g).sum h = f.sum fun i b => (g i b).sum h
-- Mathlib.RingTheory.Congruence.Hom
RingCon.mapGen_apply_apply_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring N] {c : RingCon M} (f : M →+* N),
  RingCon.ker f ≤ c → Function.Surjective ⇑f → ∀ {x y : M}, (RingCon.mapGen ⇑f) (f x) (f y) ↔ c x y
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k a fallback : α},
  (m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback
-- Mathlib.Geometry.Manifold.ContMDiffMap
ContMDiffMap.ext : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {H' : Type u_5} [inst_6 : TopologicalSpace H'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_6} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {n : WithTop ℕ∞}
  {f g : ContMDiffMap I I' M M' n}, (∀ (x : M), f x = g x) → f = g
-- Lean.Elab.MutualInductive
/-- For handler use. The `inductive` command uses it for the resulting type for the constructor.  -/
Lean.Elab.Command.CtorView.type? : Lean.Elab.Command.CtorView → Option Lean.Syntax
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Summable.tendsto_atTop_zero : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {f : ℕ → G},
  Summable f → Filter.Tendsto f Filter.atTop (nhds 0)
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.iso_homₚ_inv_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (f : HP ⟶ HP') (i : ι) (X : TopCat),
  CategoryTheory.CategoryStruct.comp ((HP.iso i).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((f.homₚ i).app (TopPair.ofTopCat X)) ((HP'.iso i).inv.app X)) =
    (f.hom i).app X
-- Mathlib.Algebra.Ring.Action.Basic
MulSemiringAction.mk : {M : Type u} →
  {R : Type v} →
    [inst : Monoid M] →
      [inst_1 : Semiring R] →
        [toDistribMulAction : DistribMulAction M R] →
          (∀ (g : M), g • 1 = 1) → (∀ (g : M) (x y : R), g • (x * y) = g • x * g • y) → MulSemiringAction M R
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.ext : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S T : Subalgebra R A},
  (∀ (x : A), x ∈ S ↔ x ∈ T) → S = T
-- Mathlib.ModelTheory.Fraisse
/-- A class `K` has the amalgamation property when for any pair of embeddings of a structure `M` in
`K` into other structures in `K`, those two structures can be embedded into a fourth structure in
`K` such that the resulting square of embeddings commutes.  -/
FirstOrder.Language.Amalgamation : {L : FirstOrder.Language} → Set (CategoryTheory.Bundled L.Structure) → Prop
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nontrivial.mul_right : ∀ {α : Type u_2} [inst : Mul α] [IsRightCancelMul α] {s t : Set α}, s.Nontrivial → t.Nonempty → (s * t).Nontrivial
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.CoconeMorphism.mk.inj : ∀ {J : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} J} {C : Type u₃} {inst_1 : CategoryTheory.Category.{v₃, u₃} C}
  {F : CategoryTheory.Functor J C} {A B : CategoryTheory.Limits.Cocone F} {hom : A.pt ⟶ B.pt}
  {w :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (A.ι.app j) hom = B.ι.app j)
      CategoryTheory.Limits.CoconeMorphism.w._autoParam}
  {hom_1 : A.pt ⟶ B.pt}
  {w_1 :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (A.ι.app j) hom_1 = B.ι.app j)
      CategoryTheory.Limits.CoconeMorphism.w._autoParam},
  { hom := hom, w := w } = { hom := hom_1, w := w_1 } → hom = hom_1
-- Mathlib.Algebra.Module.GradedModule
/-- The piecewise multiplication from the `Mul` instance, as a bundled homomorphism.  -/
DirectSum.gsmulHom : {ιA : Type u_1} →
  {ιB : Type u_2} →
    (A : ιA → Type u_3) →
      (M : ιB → Type u_4) →
        [inst : AddMonoid ιA] →
          [inst_1 : VAdd ιA ιB] →
            [inst_2 : (i : ιA) → AddCommMonoid (A i)] →
              [inst_3 : (i : ιB) → AddCommMonoid (M i)] →
                [inst_4 : GradedMonoid.GMonoid A] →
                  [DirectSum.Gmodule A M] → {i : ιA} → {j : ιB} → A i →+ M j →+ M (i +ᵥ j)
-- Init.Data.String.Basic
String.Slice.Pos.ofSlice_endPos : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁}, String.Slice.Pos.ofSlice (s.slice p₀ p₁ h).endPos = p₁
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- Convergence along filters for `WithSeminorms`.

Variant with `Finset.sup`.  -/
WithSeminorms.tendsto_nhds' : ∀ {𝕜 : Type u_2} {E : Type u_6} {F : Type u_7} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] {p : SeminormFamily 𝕜 E ι},
  WithSeminorms p →
    ∀ (u : F → E) {f : Filter F} (y₀ : E),
      Filter.Tendsto u f (nhds y₀) ↔ ∀ (s : Finset ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in f, (s.sup p) (u x - y₀) < ε
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.add_zsmul : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G} (z : ℤ), a ≡ b [PMOD p] → a + z • p ≡ b [PMOD p]
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_one : ∀ {b : ℝ}, Real.logb b 1 = 0
-- Mathlib.MeasureTheory.Function.FactorsThrough
/-- If a function is measurable with respect to the σ-algebra generated by the
first coordinates, then it only depends on those first coordinates.  -/
Measurable.dependsOn_of_piLE : ∀ {Z : Type u_3} {ι : Type u_4} {X : ι → Type u_5} [inst : (i : ι) → MeasurableSpace (X i)] {f : ((i : ι) → X i) → Z}
  [inst_1 : Preorder ι] {i : ι} [inst_2 : MeasurableSpace Z] [MeasurableSingletonClass Z],
  Measurable f → DependsOn f (Set.Iic i)
-- Lean.DocString.Syntax
/-- An image, with alternate text and a URL.

The alternate text is a plain string, rather than Verso markup.

The image URL may either be a concrete URL (written in parentheses) or a named URL (written in
square brackets).
 -/
Lean.Doc.Syntax.image : Lean.ParserDescr
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∉ m₁ → (m₁ ∩ m₂).getKeyD k fallback = fallback
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.compl_eq_empty_iff : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α), sᶜ = ∅ ↔ s = Finset.univ
-- Mathlib.Algebra.Ring.Hom.Defs
/-- `f : α →+* β` has a trivial codomain iff `f 1 = 0`.  -/
RingHom.codomain_trivial_iff_map_one_eq_zero : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), 0 = 1 ↔ f 1 = 0
-- Mathlib.CategoryTheory.CommSq
/-- The upper left triangle commutes.  -/
CategoryTheory.CommSq.LiftStruct.fac_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} {sq : CategoryTheory.CommSq f i p g} (self : sq.LiftStruct),
  CategoryTheory.CategoryStruct.comp i self.l = f
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Expressions for 1-morphisms.  -/
Mathlib.Tactic.BicategoryLike.Mor₁ : Type
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.D₁_D₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁₂ i₁₂' i₁₂'' : I₁₂), CategoryTheory.CategoryStruct.comp (K.D₁ c₁₂ i₁₂ i₁₂') (K.D₁ c₁₂ i₁₂' i₁₂'') = 0
-- Lean.Meta.Tactic.Simp.Types
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.withSimpContext : {α : Type} → Lean.Meta.Simp.Context → Lean.MetaM α → Lean.MetaM α
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
/-- The fixed-point polynomial is identically zero iff `g` is scalar.  -/
Matrix.GeneralLinearGroup.fixpointPolynomial_eq_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] {g : GL (Fin 2) R},
  g.fixpointPolynomial = 0 ↔ ↑g ∈ Set.range ⇑(Matrix.scalar (Fin 2))
-- Std.Time.Zoned.Database.TZdb
Std.Time.Database.TZdb.TZSpec.filePath.sizeOf_spec : ∀ (p : String), sizeOf (Std.Time.Database.TZdb.TZSpec.filePath p) = 1 + sizeOf p
-- Mathlib.LinearAlgebra.Matrix.IsDiag
Matrix.isDiag_neg_iff : ∀ {α : Type u_1} {n : Type u_4} [inst : SubtractionMonoid α] {A : Matrix n n α}, (-A).IsDiag ↔ A.IsDiag