mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.disjoint_iff_mul_eq_one : ∀ {G : Type u_1} [inst : Group G] {H₁ H₂ : Subgroup G},
  Disjoint H₁ H₂ ↔ ∀ {x y : G}, x ∈ H₁ → y ∈ H₂ → x * y = 1 → x = 1 ∧ y = 1
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.Hom.mk.sizeOf_spec : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R} [inst_1 : SizeOf R] (hom' : ↑M →ₗ[R] ↑N),
  sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_le_size_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, m.size ≤ (m.insert k v).size
-- Std.Internal.Do.WP.Frame
Std.Internal.Do.WP.Frames.mk : ∀ {Prog : Type u} {Value : Type v} {Pred : Type w} {EPred : Type z} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] {R : Type t}
  {op : R → Pred → Pred} {x : Prog} {F : R},
  (∀ (Q : Value → Pred) (E : EPred),
      Lean.Order.PartialOrder.rel (op F (Std.Internal.Do.wp x Q E)) (Std.Internal.Do.wp x (fun a => op F (Q a)) E)) →
    Std.Internal.Do.WP.Frames op x F
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsCondKernelCDF.toKernel_Iic : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {x : MeasurableSpace β} {f : α × β → StieltjesFunction ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β}
  {hf : ProbabilityTheory.IsCondKernelCDF f κ ν} (p : α × β) (x_1 : ℝ),
  ((ProbabilityTheory.IsCondKernelCDF.toKernel f hf) p) (Set.Iic x_1) = ENNReal.ofReal (↑(f p) x_1)
-- Mathlib.Analysis.Complex.Basic
Complex.instNormedField : NormedField ℂ
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.neg : ∀ {α : Type u_1} {M : Type u_3} [inst : SubtractionMonoid M] {f : α → M},
  Function.HasFiniteSupport f → Function.HasFiniteSupport (-f)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
IsSemilinearSet.sInter : ∀ {M : Type u_1} [inst : AddCommMonoid M] [AddMonoid.FG M] {S : Set (Set M)},
  S.Finite → (∀ s ∈ S, IsSemilinearSet s) → IsSemilinearSet (⋂₀ S)
-- Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
/-- The canonical isomorphism between
`w.costructuredArrowRightwards Y₁ ⋙ w'.costructuredArrowRightwards (B₁.obj Y₁)` and
`(w ≫ₕ w').costructuredArrowRightwards Y₁`.  -/
CategoryTheory.TwoSquare.GuitartExact.costructuredArrowRightwardsComp : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {D₁ : Type u_4} →
        {D₂ : Type u_5} →
          {D₃ : Type u_6} →
            [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
              [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁] →
                    [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] →
                      [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] →
                        {V₁ : CategoryTheory.Functor C₁ D₁} →
                          {T₁ : CategoryTheory.Functor C₁ C₂} →
                            {B₁ : CategoryTheory.Functor D₁ D₂} →
                              {V₂ : CategoryTheory.Functor C₂ D₂} →
                                (w : CategoryTheory.TwoSquare T₁ V₁ V₂ B₁) →
                                  {T₂ : CategoryTheory.Functor C₂ C₃} →
                                    {B₂ : CategoryTheory.Functor D₂ D₃} →
                                      {V₃ : CategoryTheory.Functor C₃ D₃} →
                                        (w' : CategoryTheory.TwoSquare T₂ V₂ V₃ B₂) →
                                          (Y₁ : D₁) →
                                            (w.costructuredArrowRightwards Y₁).comp
                                                (w'.costructuredArrowRightwards (B₁.obj Y₁)) ≅
                                              (w.hComp w').costructuredArrowRightwards Y₁
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.get!_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], k ∈ t₂ → (t₁ \ t₂).get! k = default
-- Std.Http.Data.URI.Encoding
/-- The underlying byte array containing the percent-encoded query data.
 -/
Std.Http.URI.EncodedQueryString.toByteArray : {r : UInt8 → Bool} → Std.Http.URI.EncodedQueryString r → ByteArray
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.natCast : {α : Type u} → [NatCast α] → NatCast (WithTop α)
-- Init.Meta.Defs
/-- Creates a round-trippable string name component if possible, otherwise returns `none`.
Names that are valid identifiers are not escaped, and otherwise, if they do not contain `»`, they are escaped.
- If `force` is `true`, then even valid identifiers are escaped.
 -/
_private.Init.Meta.Defs.0.Lean.Name.Internal.Meta.escapePart : String → optParam Bool false → Option String
-- Mathlib.FieldTheory.Finite.Basic
/-- The cardinality of a field is at most `n` times the cardinality of the image of a degree `n`
polynomial  -/
FiniteField.card_image_polynomial_eval : ∀ {R : Type u_2} [inst : CommRing R] [IsDomain R] [inst_2 : DecidableEq R] [inst_3 : Fintype R] {p : Polynomial R},
  0 < p.degree → Fintype.card R ≤ p.natDegree * (Finset.image (fun x => Polynomial.eval x p) Finset.univ).card
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Multiplying the second vector passed to `oangle` by a real multiplies the sign of the angle by
the sign of the real.  -/
Orientation.oangle_sign_smul_right : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V) (r : ℝ), (o.oangle x (r • y)).sign = SignType.sign r * (o.oangle x y).sign
-- Mathlib.SetTheory.Cardinal.Pigeonhole
/-- The infinite pigeonhole principle  -/
Cardinal.infinite_pigeonhole : ∀ {β α : Type u} (f : β → α),
  Cardinal.aleph0 ≤ Cardinal.mk β →
    Cardinal.mk α < (Cardinal.mk β).ord.cof → ∃ a, Cardinal.mk ↑(f ⁻¹' {a}) = Cardinal.mk β
-- Lean.Parser.Term
Lean.Parser.Term.structInst.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_modify : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β),
  (↑m).WF → ∀ {k : α} {f : β → β}, (↑(Std.DHashMap.Internal.Raw₀.Const.modify m k f)).size = (↑m).size
-- Mathlib.NumberTheory.LSeries.ZMod
ZMod.completedLFunction_def_even : ∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ},
  Function.Even Φ →
    ∀ (s : ℂ),
      ZMod.completedLFunction Φ s = ↑N ^ (-s) * ∑ j, Φ j * HurwitzZeta.completedHurwitzZetaEven (ZMod.toAddCircle j) s
-- Mathlib.Algebra.Lie.EngelSubalgebra
LieSubalgebra.mem_engel_iff : ∀ (R : Type u_1) {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (x y : L),
  y ∈ LieSubalgebra.engel R x ↔ ∃ n, ((LieAlgebra.ad R L) x ^ n) y = 0
-- Lean.Data.Name
Lean.Name.isAnonymous : Lean.Name → Bool
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- A trail doesn't go through any leaf vertex, except possibly at its endpoints.  -/
SimpleGraph.Walk.IsTrail.not_mem_support_of_subsingleton_neighborSet : ∀ {V : Type u} {G : SimpleGraph V} {u v x : V} {w : G.Walk u v},
  w.IsTrail → x ≠ u → x ≠ v → (G.neighborSet x).Subsingleton → x ∉ w.support
-- Mathlib.NumberTheory.Dioph
Poly.coe_neg : ∀ {α : Type u_1} (f : Poly α), ⇑(-f) = -⇑f
-- Mathlib.Topology.List
List.Vector.instTopologicalSpace : {α : Type u_1} → [TopologicalSpace α] → (n : ℕ) → TopologicalSpace (List.Vector α n)
-- Mathlib.Data.Rat.Cast.Defs
map_ratCast : ∀ {F : Type u_1} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : DivisionRing α]
  [inst_2 : DivisionRing β] [RingHomClass F α β] (f : F) (q : ℚ), f ↑q = ↑q
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.toLocalizationMap_toMonoidHom : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S],
  (IsLocalization.toLocalizationMap M S).toMonoidHom = ↑(MonoidWithZeroHom.ofClass (algebraMap R S))
-- Mathlib.Order.DirSupClosed
dirSupInacc_Iic : ∀ {α : Type u_1} [inst : Preorder α] (a : α), DirSupInacc (Set.Iic a)
-- Mathlib.Analysis.Distribution.TemperedDistribution
SchwartzMap.toTemperedDistributionCLM.congr_simp : ∀ (E : Type u_3) (F : Type u_4) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] [inst_6 : SecondCountableTopology E]
  (μ μ_1 : MeasureTheory.Measure E) (e_μ : μ = μ_1) [hμ : μ.HasTemperateGrowth],
  SchwartzMap.toTemperedDistributionCLM E F μ = SchwartzMap.toTemperedDistributionCLM E F μ_1
-- Init.Data.Vector.Nat
Vector.sum_pos_iff_exists_pos_nat : ∀ {n : ℕ} {xs : Vector ℕ n}, 0 < xs.sum ↔ ∃ x ∈ xs, 0 < x
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.nonpos_iff : ∀ {α : Type u_2} [inst : Zero α] {f : Filter α}, f.NeBot → (f ≤ 0 ↔ f = 0)
-- Lean.Elab.AssertExists
Lean.Elab.Command.instHashableAssertExists : Hashable Lean.Elab.Command.AssertExists
-- Mathlib.Order.Filter.Ultrafilter.Basic
Ultrafilter.eq_pure_of_finite_mem : ∀ {α : Type u} {f : Ultrafilter α} {s : Set α}, s.Finite → s ∈ f → ∃ x ∈ s, f = pure x
-- Mathlib.Tactic.Widget.CommDiag
/-- Triangle with `homs = [f,g,h]` and `objs = [A,B,C]`
```
A f B
  h g
    C
```
 -/
Mathlib.Tactic.Widget.subTriangle : String
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.algEquiv_comp_algebraMap_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {Rₘ : Type u_4} (Sₙ : Type u_5) (Rₘ' : Type u_6) (Sₙ' : Type u_7) [inst_3 : CommSemiring Rₘ]
  [inst_4 : CommSemiring Sₙ] [inst_5 : CommSemiring Rₘ'] [inst_6 : CommSemiring Sₙ'] [inst_7 : Algebra R Rₘ]
  [inst_8 : Algebra S Sₙ] [inst_9 : Algebra R Rₘ'] [inst_10 : Algebra S Sₙ'] [inst_11 : Algebra R Sₙ]
  [inst_12 : Algebra Rₘ Sₙ] [inst_13 : Algebra Rₘ' Sₙ'] [inst_14 : Algebra R Sₙ'] (N : Submonoid S)
  [inst_15 : IsLocalization M Rₘ] [inst_16 : IsLocalization N Sₙ] [inst_17 : IsLocalization M Rₘ']
  [inst_18 : IsLocalization N Sₙ'] [IsScalarTower R Rₘ Sₙ] [IsScalarTower R S Sₙ] [IsScalarTower R Rₘ' Sₙ']
  [IsScalarTower R S Sₙ'] (x : Rₘ),
  ((↑(IsLocalization.algEquiv N Sₙ Sₙ')).comp (algebraMap Rₘ Sₙ)) x =
    ((algebraMap Rₘ' Sₙ').comp ↑(IsLocalization.algEquiv M Rₘ Rₘ')) x
-- Mathlib.LinearAlgebra.Matrix.PosDef
/-- For an invertible matrix `U`, `U * x * star U` is positive semi-definite iff `x` is.
This works on any ⋆-ring with a partial order.

See `IsUnit.star_right_conjugate_nonneg_iff` for a similar statement for star-ordered rings.  -/
Matrix.IsUnit.posSemidef_star_right_conjugate_iff : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [inst_3 : Fintype n]
  [inst_4 : DecidableEq n] {U x : Matrix n n R}, IsUnit U → ((U * x * star U).PosSemidef ↔ x.PosSemidef)
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddModObj.vadd_eq_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (M : C)
  [inst_2 : CategoryTheory.AddMonObj M], CategoryTheory.AddModObj.vadd = CategoryTheory.AddMonObj.add
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- The multiplication on the left in an algebra is a linear map.

Note that this only assumes `SMulCommClass R A A`, so that it also works for `R := Aᵐᵒᵖ`.

When `A` is unital and associative, this is the same as `DistribSMul.toLinearMap R A a`  -/
LinearMap.mulLeft : (R : Type u_14) →
  {A : Type u_15} →
    [inst : Semiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] → [inst_2 : Module R A] → [SMulCommClass R A A] → A → A →ₗ[R] A
-- Mathlib.GroupTheory.Index
/-- Relative version of `AddSubgroup.index_dvd_two_iff`.  -/
AddSubgroup.relIndex_dvd_two_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G}, H.relIndex K ∣ 2 ↔ ∃ a ∈ K, ∀ b ∈ K, b + a ∈ H ∨ b ∈ H
-- Mathlib.Data.Complex.Basic
Complex.ofReal_pow : ∀ (r : ℝ) (n : ℕ), ↑(r ^ n) = ↑r ^ n
-- Lean.Parser.Do
Lean.Parser.Term.doMatch.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Hom.mk.injEq : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {l : a ⟶ b} {r : b ⟶ a}
  (adj : CategoryTheory.Bicategory.Adjunction l r) (l_1 : a ⟶ b) (r_1 : b ⟶ a)
  (adj_1 : CategoryTheory.Bicategory.Adjunction l_1 r_1),
  ({ l := l, r := r, adj := adj } = { l := l_1, r := r_1, adj := adj_1 }) = (l = l_1 ∧ r = r_1 ∧ adj ≍ adj_1)
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.ThinSkeleton.map_comp_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] [Quiver.IsThin C] (F : CategoryTheory.Functor E D)
  (G : CategoryTheory.Functor D C),
  CategoryTheory.ThinSkeleton.map (F.comp G) =
    (CategoryTheory.ThinSkeleton.map F).comp (CategoryTheory.ThinSkeleton.map G)
-- Mathlib.FieldTheory.Extension
/-- `σ : L →ₐ[F] K` is an extendible lift ("extendible pair" in [Isaacs1980]) if for every
intermediate field `M` that is finite-dimensional over `L`, `σ` extends to some `M →ₐ[F] K`.
In our definition we only require `M` to be finitely generated over `L`, which is equivalent
if the ambient field `E` is algebraic over `F` (which is the case in our main application).
We also allow the domain of the extension to be an intermediate field that properly contains `M`,
since one can always restrict the domain to `M`.  -/
IntermediateField.Lifts.IsExtendible : {F : Type u_1} →
  {E : Type u_2} →
    {K : Type u_3} →
      [inst : Field F] →
        [inst_1 : Field E] →
          [inst_2 : Field K] → [inst_3 : Algebra F E] → [inst_4 : Algebra F K] → IntermediateField.Lifts F E K → Prop
-- Mathlib.CategoryTheory.Adjunction.Mates
/-- Suppose we have a square of functors (where the top and bottom are adjunctions `L₁ ⊣ R₁`
and `L₂ ⊣ R₂` respectively).

```
      C ↔ D
    G ↓   ↓ H
      E ↔ F
```

Then we have a bijection between natural transformations `G ⋙ L₂ ⟶ L₁ ⋙ H` and
`R₁ ⋙ G ⟶ H ⋙ R₂`. This can be seen as a bijection of the 2-cells:

```
         L₁                  R₁
      C --→ D             C ←-- D
    G ↓  ↗  ↓ H         G ↓  ↘  ↓ H
      E --→ F             E ←-- F
         L₂                  R₂
```

Note that if one of the transformations is an iso, it does not imply the other is an iso.
 -/
CategoryTheory.mateEquiv : {C : Type u₁} →
  {D : Type u₂} →
    {E : Type u₃} →
      {F : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} F] →
                {G : CategoryTheory.Functor C E} →
                  {H : CategoryTheory.Functor D F} →
                    {L₁ : CategoryTheory.Functor C D} →
                      {R₁ : CategoryTheory.Functor D C} →
                        {L₂ : CategoryTheory.Functor E F} →
                          {R₂ : CategoryTheory.Functor F E} →
                            (L₁ ⊣ R₁) →
                              (L₂ ⊣ R₂) → CategoryTheory.TwoSquare G L₁ L₂ H ≃ CategoryTheory.TwoSquare R₁ H G R₂
-- Init.Data.String.Lemmas.Iter
_private.Init.Data.String.Lemmas.Iter.0.Std.Iter.intercalateString_eq.match_1_4.eq_2 : ∀ (motive : Option String → String → Sort u_1) (str sl : String) (h_1 : (sl : String) → motive none sl)
  (h_2 : (str sl : String) → motive (some str) sl),
  (match some str, sl with
    | none, sl => h_1 sl
    | some str, sl => h_2 str sl) =
    h_2 str sl
-- Mathlib.NumberTheory.Real.Irrational
/-- A transcendental real number is irrational.  -/
Transcendental.irrational : ∀ {r : ℝ}, Transcendental ℚ r → Irrational r
-- Init.Data.Nat.Basic
Nat.zero_lt_one : 0 < 1
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGE.congr_simp : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k k_1 : α) (e_k : k = k_1)
  (t t_1 : Std.DTreeMap.Internal.Impl α fun x => β) (e_t : t = t_1) (ho : t.Ordered)
  (he : ∃ a ∈ t, (compare a k).isGE = true),
  Std.DTreeMap.Internal.Impl.Const.getEntryGE k t ho he = Std.DTreeMap.Internal.Impl.Const.getEntryGE k_1 t_1 ⋯ ⋯
-- Init.Data.Range.Polymorphic.SInt
Int64.instRxoHasSize : Std.Rxo.HasSize Int64
-- Init.Data.SInt.Lemmas
Int16.eq_iff_toBitVec_eq : ∀ {a b : Int16}, a = b ↔ a.toBitVec = b.toBitVec
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.ObjectProperty.fullSubcategoryCongr_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P P' : CategoryTheory.ObjectProperty C} (h : P = P'),
  (CategoryTheory.ObjectProperty.fullSubcategoryCongr h).inverse = CategoryTheory.ObjectProperty.ιOfLE ⋯
-- Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology
CategoryTheory.extensiveTopology.mem_sieves_iff_contains_colimit_cofan : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.FinitaryPreExtensive C] {X : C}
  (S : CategoryTheory.Sieve X),
  S ∈ (CategoryTheory.extensiveTopology C) X ↔
    ∃ α,
      ∃ (_ : Finite α),
        ∃ Y π,
          Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk X π)) ∧ ∀ (a : α), S.arrows (π a)
-- Std.Time.Date.ValidDate
Std.Time.instTransOrdValidDate : ∀ {leap : Bool}, Std.TransOrd (Std.Time.ValidDate leap)
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.add_posSemidef : ∀ {m : Type u_1} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [AddLeftMono R]
  {A B : Matrix m m R}, A.PosDef → B.PosSemidef → (A + B).PosDef
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.truncTotal_subst_eq_truncTotal_truncTotal_subst : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} {f : MvPowerSeries σ R} [inst_3 : Finite τ] {k : ℕ}
  [inst_4 : Finite σ],
  (∀ (i : σ), MvPowerSeries.constantCoeff (a i) = 0) →
    (MvPowerSeries.truncTotal k) (MvPowerSeries.subst a f) =
      (MvPowerSeries.truncTotal k) (MvPowerSeries.subst a ↑((MvPowerSeries.truncTotal k) f))
-- Mathlib.Data.ZMod.Basic
ZMod.cast_add' : ∀ {n : ℕ} {R : Type u_1} [inst : Ring R] [CharP R n] (a b : ZMod n), (a + b).cast = a.cast + b.cast
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃_obj_obj_map_app_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7)
  [inst_6 : CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  (F₂ : CategoryTheory.Functor C₂ D₂) {X Y : CategoryTheory.Functor C₃ D₃} (τ₃ : X ⟶ Y)
  (F : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X_1 : C₁) (X_2 : C₂)
  (c : C₃),
  (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).obj F₂).map τ₃).app F).app X_1).app X_2).app c =
    ((F.obj (F₁.obj X_1)).obj (F₂.obj X_2)).map (τ₃.app c)
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.Tree.term.inj : ∀ {ref : Lean.Syntax} {infoTrees : Lean.PersistentArray Lean.Elab.InfoTree} {val : Lean.Expr} {ref_1 : Lean.Syntax}
  {infoTrees_1 : Lean.PersistentArray Lean.Elab.InfoTree} {val_1 : Lean.Expr},
  FBinopElab.Tree.term✝ ref infoTrees val = FBinopElab.Tree.term✝ ref_1 infoTrees_1 val_1 →
    ref = ref_1 ∧ infoTrees = infoTrees_1 ∧ val = val_1
-- Init.Data.List.Sublist
List.dropWhile_sublist : ∀ {α : Type u_1} {l : List α} (p : α → Bool), (List.dropWhile p l).Sublist l
-- Mathlib.RingTheory.Congruence.Hom
RingCon.comapQuotientEquivRange_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : Ring M] [inst_1 : Ring N] (c : RingCon M) (f : N →+* M) {d : RingCon N}
  (hcd : d = c.comap f) (x : N), (c.comapQuotientEquivRange f hcd) ↑x = ⟨↑(f x), ⋯⟩
-- Mathlib.Data.List.Destutter
_private.Mathlib.Data.List.Destutter.0.List.destutter.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : (h : α) → (l : List α) → motive (h :: l)) (h_2 : Unit → motive []),
  (match [] with
    | h :: l => h_1 h l
    | [] => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PushoutCocone.mk_ι_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} {W : C} (inl : Y ⟶ W)
  (inr : Z ⟶ W) (eq : CategoryTheory.CategoryStruct.comp f inl = CategoryTheory.CategoryStruct.comp g inr),
  (CategoryTheory.Limits.PushoutCocone.mk inl inr eq).ι.app CategoryTheory.Limits.WalkingSpan.right = inr
-- Mathlib.Algebra.Group.End
MulAutMultiplicative_apply_symm_apply : ∀ (G : Type u_3) [inst : AddGroup G] (a : Multiplicative G ≃* Multiplicative G) (a_1 : G),
  (AddEquiv.symm ((MulAutMultiplicative G) a)) a_1 = Multiplicative.toAdd (a.symm (Multiplicative.ofAdd a_1))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List (α × β)} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
      k ∈ List.map Prod.fst l → (Std.ExtTreeMap.ofList l cmp).getKeyD k' fallback = k
-- Mathlib.NumberTheory.JacobiSum.Basic
_private.Mathlib.NumberTheory.JacobiSum.Basic.0.MulChar.exists_apply_sub_one_eq_mul_sub_one : ∀ {F : Type u_1} {R : Type u_2} [inst : Field F] [inst_1 : CommRing R] [IsDomain R] [Finite F] {n : ℕ} [NeZero n]
  {χ : MulChar F R} {μ : R}, χ ^ n = 1 → IsPrimitiveRoot μ n → ∀ {x : F}, x ≠ 0 → ∃ z ∈ ℤ[μ], χ x - 1 = z * (μ - 1)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- Composition of `StrictlyUnitaryLaxFunctor` is strictly right unitary  -/
CategoryTheory.StrictlyUnitaryLaxFunctor.comp_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.StrictlyUnitaryLaxFunctor B C), F.comp (CategoryTheory.StrictlyUnitaryLaxFunctor.id C) = F
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instPreorder : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → [Preorder β] → Preorder (l.Germ β)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
ProfiniteGrp.toLimit_injective : ∀ (P : ProfiniteGrp.{u}), Function.Injective ⇑(ProfiniteGrp.Hom.hom P.toLimit)
-- Mathlib.Topology.Sets.VietorisTopology
/-- When `Set` is equipped with the Vietoris topology, taking the image under a continuous map is
continuous.  -/
Continuous.image_vietoris : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Continuous f → Continuous fun x => f '' x
-- Mathlib.Data.Countable.Basic
uncountable_iff_isEmpty_embedding : ∀ {α : Sort u}, Uncountable α ↔ IsEmpty (α ↪ ℕ)
-- Mathlib.Data.Set.Basic
/-- Extract a witness from `s.Nonempty`. This function might be used instead of case analysis
on the argument. Note that it makes a proof depend on the `Classical.choice` axiom.  -/
Set.Nonempty.some : {α : Type u} → {s : Set α} → s.Nonempty → α
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- A finite-dimensional space is nontrivial if it has positive `finrank`.  -/
Module.nontrivial_of_finrank_pos : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R],
  0 < Module.finrank R M → Nontrivial M
-- Mathlib.Analysis.Normed.Affine.Isometry
/-- `AffineEquiv.ofEq` as an `AffineIsometryEquiv`.  -/
AffineIsometryEquiv.ofEq : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {P : Type u_10} →
      [inst : NormedField 𝕜] →
        [inst_1 : SeminormedAddCommGroup V] →
          [inst_2 : NormedSpace 𝕜 V] →
            [inst_3 : PseudoMetricSpace P] →
              [inst_4 : NormedAddTorsor V P] →
                (s₁ s₂ : AffineSubspace 𝕜 P) →
                  [inst_5 : Nonempty ↥s₁] → [inst_6 : Nonempty ↥s₂] → s₁ = s₂ → ↥s₁ ≃ᵃⁱ[𝕜] ↥s₂