mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.HahnSeries.Multiplication
Finset.antidiagonal.congr_simp : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedCancelAddMonoid α]
  {s s_1 : Set α} (e_s : s = s_1) {t t_1 : Set α} (e_t : t = t_1) (hs : s.IsPWO) (ht : t.IsPWO) (a a_1 : α),
  a = a_1 → Finset.antidiagonal hs ht a = Finset.antidiagonal ⋯ ⋯ a_1
-- Mathlib.Topology.CompactOpen
ContinuousMap.continuous_const' : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Continuous (ContinuousMap.const X)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.gcd_eq_sup : ∀ {A : Type u_2} [inst : CommRing A] [inst_1 : IsDedekindDomain A] (I J : Ideal A), gcd I J = I ⊔ J
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- **Alias** of `sq_nonneg`. -/
pow_two_nonneg : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [PosMulMono R] [AddLeftMono R] (a : R),
  0 ≤ a ^ 2
-- Mathlib.RingTheory.Localization.Away.Basic
selfZPow_add : ∀ {R : Type u_1} [inst : CommSemiring R] (x : R) (B : Type u_2) [inst_1 : CommSemiring B] [inst_2 : Algebra R B]
  [inst_3 : IsLocalization.Away x B] {n m : ℤ}, selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m
-- Mathlib.ModelTheory.ElementarySubstructures
FirstOrder.Language.ElementarySubstructure.instInhabited : {L : FirstOrder.Language} → {M : Type u_1} → [inst : L.Structure M] → Inhabited (L.ElementarySubstructure M)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.colimitsOfShape_isoClosure : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], P.isoClosure.colimitsOfShape J = P.colimitsOfShape J
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- A non-unital subsemiring of a `NonUnitalSemiring` is a `NonUnitalSemiring`.  -/
NonUnitalSubsemiringClass.toNonUnitalSemiring : {S : Type v} →
  (s : S) →
    {R : Type u_1} →
      [inst : NonUnitalSemiring R] → [inst_1 : SetLike S R] → [NonUnitalSubsemiringClass S R] → NonUnitalSemiring ↥s
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.hasZeroObject_unop : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject Cᵒᵖ],
  CategoryTheory.Limits.HasZeroObject C
-- Mathlib.Order.Filter.Extr
isMinFilter_dual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMinFilter (⇑OrderDual.toDual ∘ f) l a ↔ IsMaxFilter f l a
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.id_apply : ∀ (R : CommRingCat) (r : ↑R), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id R)) r = r
-- Init.Grind.Interactive
/-- Show active local theorems and their anchors for heuristic instantiation.  -/
Lean.Parser.Tactic.Grind.showLocalThms : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
AlgebraicGeometry.Scheme.irreducibleComponentι.eq_1 : ∀ (X : AlgebraicGeometry.Scheme) (Z : Set ↥X) (hZ : Z ∈ irreducibleComponents ↥X)
  [inst : AlgebraicGeometry.IsNoetherian X],
  X.irreducibleComponentι Z hZ = (X.irreducibleComponentIdeal Z hZ).subschemeι
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_right_self_sup : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R} [I.IsTwoSided], I * J ⊔ I = I
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.coe_det_isEmpty : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] [IsEmpty n],
  Matrix.det = Function.const (Matrix n n R) 1
-- Mathlib.RingTheory.Valuation.Basic
/-- The `Valuation` associated to an `AddValuation` (useful if the latter is constructed using
`AddValuation.of`).  -/
AddValuation.toValuation : {R : Type u_3} →
  {Γ₀ : Type u_4} →
    [inst : Ring R] →
      [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] → AddValuation R Γ₀ ≃ Valuation R (Multiplicative Γ₀ᵒᵈ)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_refl_left : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} (g' : α → F') (l : Filter α), (fun x => f' x - f' x) =o[l] g'
-- Init.Data.Array.Count
Array.one_le_count_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {xs : Array α}, 1 ≤ Array.count a xs ↔ a ∈ xs
-- Mathlib.Order.WithBot
WithBot.le_unbot_iff : ∀ {α : Type u_1} {a : α} [inst : LE α] {x : WithBot α} (hx : x ≠ ⊥), a ≤ x.unbot hx ↔ ↑a ≤ x
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.σ_neg : ∀ (g : GL (Fin 2) ℝ), UpperHalfPlane.σ (-g) = UpperHalfPlane.σ g
-- Batteries.Data.List.Perm
_private.Batteries.Data.List.Perm.0.cond.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.isPath_dropLast : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.IsCycle → p.dropLast.IsPath
-- Mathlib.RingTheory.Polynomial.Nilpotent
Polynomial.isNilpotent_pow_X_mul_C_of_isNilpotent : ∀ {R : Type u_1} {r : R} [inst : Semiring R] (n : ℕ), IsNilpotent r → IsNilpotent (Polynomial.X ^ n * Polynomial.C r)
-- Mathlib.CategoryTheory.Filtered.Final
CategoryTheory.exists_eq_of_isCofiltered_costructuredArrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {d : D} [CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow F d)]
  {c₁ c₂ : C} (s₁ : F.obj c₁ ⟶ d) (s₂ : F.obj c₂ ⟶ d),
  ∃ c t₁ t₂, CategoryTheory.CategoryStruct.comp (F.map t₁) s₁ = CategoryTheory.CategoryStruct.comp (F.map t₂) s₂
-- Mathlib.RingTheory.RingHom.Flat
RingHom.Flat.containsIdentities : RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => RingHom.Flat
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.ext_iff : ∀ {n : ℕ} {x y : OrderedFinpartition n}, x = y ↔ x.length = y.length ∧ x.partSize ≍ y.partSize ∧ x.emb ≍ y.emb
-- Lean.Setup
/-- Available for execution during elaboration.  -/
Lean.IRPhases.comptime : Lean.IRPhases
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
RightDerivMeasurableAux.D.eq_1 : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : ℝ → F) (K : Set F),
  RightDerivMeasurableAux.D f K =
    ⋂ e,
      ⋃ n,
        ⋂ p, ⋂ (_ : p ≥ n), ⋂ q, ⋂ (_ : q ≥ n), RightDerivMeasurableAux.B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e)
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.mk : ∀ {R : Type u} {Γ₀ : Type v} [inst : CommRing R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O R],
  Function.Injective ⇑(algebraMap O R) →
    (∀ (x : O), v ((algebraMap O R) x) ≤ 1) → (∀ ⦃r : R⦄, v r ≤ 1 → ∃ x, (algebraMap O R) x = r) → v.Integers O
-- Mathlib.RepresentationTheory.Homological.Resolution
HomotopyEquiv.trans.eq_1 : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : HomotopyEquiv C D) (g : HomotopyEquiv D E),
  f.trans g =
    { hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, inv := CategoryTheory.CategoryStruct.comp g.inv f.inv,
      homotopyHomInvId :=
        ⋯.mpr (⋯.mp (((g.homotopyHomInvId.compRightId f.inv).compLeft f.hom).trans f.homotopyHomInvId)),
      homotopyInvHomId :=
        ⋯.mpr (⋯.mp (((f.homotopyInvHomId.compRightId g.hom).compLeft g.inv).trans g.homotopyInvHomId)) }
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
CategoryTheory.Functor.instPreservesZeroMorphismsFlipOfObj : ∀ {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] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms E] (F : CategoryTheory.Functor C (CategoryTheory.Functor D E))
  [∀ (X : C), (F.obj X).PreservesZeroMorphisms], F.flip.PreservesZeroMorphisms
-- Init.Data.List.Lemmas
List.getElem_length_sub_one_eq_getLast : ∀ {α : Type u_1} {l : List α} (h : l.length - 1 < l.length), l[l.length - 1] = l.getLast ⋯
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.toTopCat_map_apply : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y Z : ContinuousGeneratedByCat X} (f : Y ⟶ Z)
  (y : Topology.WithGeneratedByTopology X ↑Y),
  (CategoryTheory.ConcreteCategory.hom ((ContinuousGeneratedByCat.toTopCat X).map f)) y =
    Topology.WithGeneratedByTopology.equiv.symm
      ((CategoryTheory.ConcreteCategory.hom f) (Topology.WithGeneratedByTopology.equiv y))
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
/-- A non-cyclic additive group is non-trivial.  -/
Nontrivial.of_not_isAddCyclic : ∀ {α : Type u_1} [inst : AddGroup α], ¬IsAddCyclic α → Nontrivial α
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of `AddMonoidAlgebra.coeff_mul_antidiag`. -/
AddMonoidAlgebra.mul_apply_antidiagonal : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Add M] (x y : AddMonoidAlgebra R M) (m : M)
  (s : Finset (M × M)), (∀ {p : M × M}, p ∈ s ↔ p.1 + p.2 = m) → (x * y).coeff m = ∑ p ∈ s, x.coeff p.1 * y.coeff p.2
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.instWeakEquivalenceUnopOfOpposite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  {X Y : Cᵒᵖ} (f : X ⟶ Y) [HomotopicalAlgebra.WeakEquivalence f], HomotopicalAlgebra.WeakEquivalence f.unop
-- Mathlib.CategoryTheory.Shift.ShiftSequence
/-- Given an isomorphism `π ⋙ H ≅ F`, where `π` is a functor which commutes
with the shift by `M` and `H` is equipped with a shift sequence,
then this is the shift sequence for `F` induced by composition.  -/
CategoryTheory.Functor.ShiftSequence.leftComp : {C : Type u_1} →
  {D : Type u_2} →
    {A : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} A] →
            {F : CategoryTheory.Functor C A} →
              {π : CategoryTheory.Functor C D} →
                {H : CategoryTheory.Functor D A} →
                  (π.comp H ≅ F) →
                    (M : Type u_4) →
                      [inst_3 : AddMonoid M] →
                        [inst_4 : CategoryTheory.HasShift C M] →
                          [inst_5 : CategoryTheory.HasShift D M] →
                            [π.CommShift M] → [H.ShiftSequence M] → F.ShiftSequence M
-- Mathlib.Analysis.Calculus.ContDiff.RCLike
/-- If `f` is `C¹`, it is locally Lipschitz.  -/
ContDiff.locallyLipschitz : ∀ {𝕂 : Type u_1} [inst : RCLike 𝕂] {E' : Type u_2} [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedSpace 𝕂 E']
  {F' : Type u_3} [inst_3 : NormedAddCommGroup F'] [inst_4 : NormedSpace 𝕂 F'] {f : E' → F'},
  ContDiff 𝕂 1 f → LocallyLipschitz f
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.tensor.inj : ∀ {C : Type u} {a : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C} {a_1 : C}
  {a_2 : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C} {a_3 : C},
  a.tensor a_1 = a_2.tensor a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExSum.add.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {a b : Q(«$α»)}
  (a_1 : Mathlib.Tactic.Ring.Common.ExProd BaseType sα a) (a_2 : Mathlib.Tactic.Ring.Common.ExSum BaseType sα b)
  (a_3 : Mathlib.Tactic.Ring.Common.ExProd BaseType sα a) (a_4 : Mathlib.Tactic.Ring.Common.ExSum BaseType sα b),
  (Mathlib.Tactic.Ring.Common.ExSum.add a_1 a_2 = Mathlib.Tactic.Ring.Common.ExSum.add a_3 a_4) =
    (a_1 = a_3 ∧ a_2 = a_4)
-- Mathlib.Analysis.Calculus.DSlope
continuousAt_dslope_of_ne : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a b : 𝕜}, b ≠ a → (ContinuousAt (dslope f a) b ↔ ContinuousAt f b)
-- Mathlib.Topology.Constructions.SumProd
ContinuousAt.prodMap : ∀ {X : Type u} {Y : Type v} {W : Type u_1} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace W] {f : X → Z} {g : Y → W} {p : X × Y},
  ContinuousAt f p.1 → ContinuousAt g p.2 → ContinuousAt (Prod.map f g) p
-- Init.Data.String.PosRaw
String.Pos.Raw.lt_iff : ∀ {i₁ i₂ : String.Pos.Raw}, i₁ < i₂ ↔ i₁.byteIdx < i₂.byteIdx
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.cone_π : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  [inst_1 : CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }],
  (CategoryTheory.Limits.Pi.cone X).π =
    CategoryTheory.Discrete.natTrans fun x => CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) x.as
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.conv_eq_conts_a_div_conts_b : ∀ {K : Type u_1} {g : GenContFract K} {n : ℕ} [inst : DivisionRing K], g.convs n = (g.conts n).a / (g.conts n).b
-- Mathlib.FieldTheory.AbsoluteGaloisGroup
/-- `absoluteGaloisGroup` is a topological space with the Krull topology.  -/
Field.instTopologicalSpaceAbsoluteGaloisGroup : (K : Type u_1) → [inst : Field K] → TopologicalSpace (Field.absoluteGaloisGroup K)
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.tensorUnit_carrier : ∀ {R : Type u} [inst : CommRing R], ↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat R)) = R
-- Mathlib.GroupTheory.OrderOfElement
finEquivZMultiples.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {x : G} (hx : IsOfFinAddOrder x),
  finEquivZMultiples hx = (finEquivMultiples hx).trans (Equiv.setCongr ⋯)
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.LimitOfShape.ofLE_toLimitPresentation : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {X : C} (h : P.LimitOfShape J X) {Q : CategoryTheory.ObjectProperty C}
  (hPQ : P ≤ Q), (h.ofLE hPQ).toLimitPresentation = h.toLimitPresentation
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- A partially applied version of `Matrix.row_apply`  -/
Matrix.row_apply' : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α) (i : m), A.row i = A i
-- Mathlib.Data.ENNReal.BigOperators
ENNReal.prod_div_distrib : ∀ {ι : Type u_1} {f g : ι → ENNReal} {s : Finset ι},
  ((↑s).Pairwise fun i j => g i ≠ 0 ∨ g j ≠ ⊤) → ∏ i ∈ s, f i / g i = (∏ i ∈ s, f i) / ∏ i ∈ s, g i
-- Init.Data.BitVec.Lemmas
BitVec.slt_eq_ult : ∀ {w : ℕ} {x y : BitVec w}, x.slt y = (x.msb != y.msb ^^ x.ult y)
-- Mathlib.CategoryTheory.Core
CategoryTheory.Core.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : CategoryTheory.Core C} {f g : X ⟶ Y},
  f.iso.hom = g.iso.hom → f = g
-- Lean.Meta.Tactic.Simp.Rewrite
/-- Try to unfold ground term in the ground/symbolic evaluator.
 -/
Lean.Meta.Simp.simpGround : Lean.Meta.Simp.Simproc
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.IterM.DefaultConsumers.forIn'_eq_match_step.match_1.eq_1 : ∀ {β : Type u_3} {γ : Type u_1} {init : γ} (PlausibleForInStep : β → γ → ForInStep γ → Prop) (out : β)
  (motive : Subtype (PlausibleForInStep out init) → Sort u_2) (c : γ)
  (property : PlausibleForInStep out init (ForInStep.yield c))
  (h_1 : (c : γ) → (property : PlausibleForInStep out init (ForInStep.yield c)) → motive ⟨ForInStep.yield c, property⟩)
  (h_2 : (c : γ) → (property : PlausibleForInStep out init (ForInStep.done c)) → motive ⟨ForInStep.done c, property⟩),
  (match ⟨ForInStep.yield c, property⟩ with
    | ⟨ForInStep.yield c, property⟩ => h_1 c property
    | ⟨ForInStep.done c, property⟩ => h_2 c property) =
    h_1 c property
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- Elements of the left subgroup lie in `Δ`.  -/
IsHeckeTriple.mem_of_mem_left : ∀ {G : Type u_1} [inst : Group G] {Δ : Submonoid G} {H₁ : Subgroup G} (H₂ : Subgroup G) [IsHeckeTriple Δ H₁ H₂] {x : G},
  x ∈ H₁ → x ∈ Δ
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
/-- **Alias** of the reverse direction of `Subalgebra.bot_eq_top_iff_finrank_eq_one`. -/
Subalgebra.bot_eq_top_of_finrank_eq_one : ∀ {F : Type u_1} {E : Type u_2} [inst : CommRing F] [StrongRankCondition F] [inst_2 : Ring E] [inst_3 : Algebra F E]
  [Nontrivial E] [Module.Free F E], Module.finrank F E = 1 → ⊥ = ⊤
-- Mathlib.Data.Seq.Defs
Stream'.Seq.head_eq_none : ∀ {α : Type u} {s : Stream'.Seq α}, s.head = none → s = Stream'.Seq.nil
-- Mathlib.Topology.Separation.SeparatedNhds
/-- `HasSeparatingCover`s can be useful witnesses for `SeparatedNhds`.  -/
HasSeparatingCover : {X : Type u_1} → [TopologicalSpace X] → Set X → Set X → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- The cone obtained from `IsPullback fst snd f g` is a limit cone.
 -/
CategoryTheory.IsPullback.isLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P X Y Z : C} →
      {fst : P ⟶ X} →
        {snd : P ⟶ Y} →
          {f : X ⟶ Z} → {g : Y ⟶ Z} → (h : CategoryTheory.IsPullback fst snd f g) → CategoryTheory.Limits.IsLimit h.cone
-- Lean.Meta.Tactic.Grind.Types
/-- Argument `arg : type` of an application `app` in `SplitInfo`.  -/
Lean.Meta.Grind.SplitArg : Type
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.congr_mono : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {x : M} {s t : Set M},
  MDiffAt[s] f x → (∀ x ∈ t, f₁ x = f x) → f₁ x = f x → t ⊆ s → MDiffAt[t] f₁ x
-- Batteries.Data.Fin.Fold
Fin.dfoldrM_loop : ∀ {m : Type u_1 → Type u_2} {n : ℕ} {α : Fin (n + 1 + 1) → Type u_1} {i : ℕ} {h : i + 1 < n + 1 + 1} [inst : Monad m]
  [LawfulMonad m] (f : (i : Fin (n + 1)) → α i.succ → m (α i.castSucc)) (x : α ⟨i + 1, h⟩),
  Fin.dfoldrM.loop (n + 1) α f (i + 1) h x = Fin.dfoldrM.loop n (α ∘ Fin.succ) (fun x => f x.succ) i ⋯ x >>= f 0
-- Mathlib.Algebra.DirectSum.Idempotents
DirectSum.idempotent.eq_1 : ∀ {R : Type u_1} {I : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq I] (V : I → Ideal R)
  [inst_2 : DirectSum.Decomposition V] (i : I), DirectSum.idempotent V i = ↑(((DirectSum.decompose V) 1) i)
-- Mathlib.Data.Matrix.Mul
smul_dotProduct : ∀ {m : Type u_2} {R : Type u_7} {α : Type v} [inst : Fintype m] [inst_1 : Mul α] [inst_2 : AddCommMonoid α]
  [inst_3 : DistribSMul R α] [IsScalarTower R α α] (x : R) (v w : m → α), x • v ⬝ᵥ w = x • (v ⬝ᵥ w)
-- Mathlib.Order.Cover
WithTop.covBy_top_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : WithTop α}, a ⋖ ⊤ ↔ ∃ b, IsMax b ∧ a = ↑b
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
MDifferentiableAt.clm_precomp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {F₃ : Type u_16} [inst_10 : NormedAddCommGroup F₃] [inst_11 : NormedSpace 𝕜 F₃] {f : M → F₁ →L[𝕜] F₂} {x : M},
  MDiffAt f x → (MDiffAt fun y => ContinuousLinearMap.precomp F₃ (f y)) x
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.pentagon_hom_inv_inv_inv_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z Z_1 : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) Z ⟶
      Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W
          (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
              Z).inv
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom
          Z)
        h)
-- Mathlib.Data.FunLike.Group
FunLike.rightCancelSemigroup.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : RightCancelSemigroup β]
  [inst_3 : IsMulApply F α β], FunLike.rightCancelSemigroup = Function.Injective.rightCancelSemigroup (fun f => ⇑f) ⋯ ⋯
-- Mathlib.Topology.ExtendFrom
/-- If `f` converges to some `y` as `x` tends to `x₀` within `A`,
then `f` tends to `extendFrom A f x` as `x` tends to `x₀`.  -/
tendsto_extendFrom : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {A : Set X} {f : X → Y}
  {x : X},
  (∃ y, Filter.Tendsto f (nhdsWithin x A) (nhds y)) → Filter.Tendsto f (nhdsWithin x A) (nhds (extendFrom A f x))
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instPowNat : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : LinearOrderedCommGroupWithZero Γ₀] → [inst_1 : Ring R] → (v : Valuation R Γ₀) → Pow (WithVal v) ℕ
-- Mathlib.Order.SymmDiff
symmDiff_sdiff_inf : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), symmDiff a b \ (a ⊓ b) = symmDiff a b
-- Init.Data.Int.Order
Int.eq_neg_natAbs_of_nonpos : ∀ {a : ℤ}, a ≤ 0 → a = -↑a.natAbs
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isRevMatch_iff_slice : ∀ {pat : String} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsRevMatch pat pos ↔ String.Slice.Pattern.Model.IsRevMatch pat.toSlice pos
-- Mathlib.MeasureTheory.Function.EssSup
ENNReal.essSup_restrict_eq_of_support_subset : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f : α → ENNReal},
  Function.support f ⊆ s → essSup f (μ.restrict s) = essSup f μ
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.getD_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α]
  {k fallback : α}, m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.getD k fallback = m₂.getD k fallback
-- Mathlib.Topology.Order.LiminfLimsup
/-- If a filter is converging, its limsup coincides with its limit.  -/
limsInf_eq_of_le_nhds : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  {f : Filter α} {a : α} [f.NeBot], f ≤ nhds a → f.limsInf = a
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.refl_h₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂), (CategoryTheory.ShortComplex.Homotopy.refl φ).h₂ = 0
-- Mathlib.Tactic.CategoryTheory.Bicategory.Normalize
Mathlib.Tactic.Bicategory.instMonadNormalExprBicategoryM : Mathlib.Tactic.BicategoryLike.MonadNormalExpr Mathlib.Tactic.Bicategory.BicategoryM