mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- If the `vectorSpan` of a finite affinely independent
family lies in a submodule with dimension one less than its
cardinality, it equals that submodule.  -/
AffineIndependent.vectorSpan_eq_of_le_of_card_eq_finrank_add_one : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] {p : ι → P},
  AffineIndependent k p →
    ∀ {sm : Submodule k V} [FiniteDimensional k ↥sm],
      vectorSpan k (Set.range p) ≤ sm → Fintype.card ι = Module.finrank k ↥sm + 1 → vectorSpan k (Set.range p) = sm
-- Init.Grind.AC
Lean.Grind.AC.diseq_simp_rhs_middle : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op}
  (lhs₁ rhs₁ head tail lhs₂ rhs₂ rhs₂' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_middle_cert lhs₁ rhs₁ head tail rhs₂ rhs₂' = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ ≠ Lean.Grind.AC.Seq.denote ctx rhs₂ →
        Lean.Grind.AC.Seq.denote ctx lhs₂ ≠ Lean.Grind.AC.Seq.denote ctx rhs₂'
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.map_φH : ∀ {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] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂}
  {h₁ : S₁.LeftHomologyData} {h₂ : S₂.LeftHomologyData} (ψ : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁ h₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : h₁.IsPreservedBy F]
  [inst_6 : h₂.IsPreservedBy F], (ψ.map F).φH = F.map ψ.φH
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.domDomCongrₗ_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {ι' : Type u_8} (S : Type u_12) [inst_5 : Semiring S]
  [inst_6 : Module S N] [inst_7 : SMulCommClass R S N] (σ : ι ≃ ι') (f : M [⋀^ι]→ₗ[R] N),
  (AlternatingMap.domDomCongrₗ S σ) f = AlternatingMap.domDomCongr σ f
-- Mathlib.LinearAlgebra.Complex.Module
realPart_nonneg_of_nonneg : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : PartialOrder A] [StarOrderedRing A]
  [inst_4 : Module ℂ A] [inst_5 : StarModule ℂ A] {a : A}, 0 ≤ a → 0 ≤ realPart a
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
/-- **Alias** of `Set.iUnion_smul_eq_ofPred_exists`. -/
Set.iUnion_smul_eq_setOf_exists : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {s : Set β}, ⋃ g, g • s = {a | ∃ g, g • a ∈ s}
-- Mathlib.Data.Matrix.Basis
/-- The center of `Matrix n n α` is equal to the image of the center of `α` under `scalar n`.  -/
Matrix.center_eq_scalar_image : ∀ {n : Type u_3} {α : Type u_7} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : Semiring α],
  Set.center (Matrix n n α) = ⇑(Matrix.scalar n) '' Set.center α
-- Mathlib.Data.PFunctor.Univariate.M
/-- The head of the trees are equal  -/
PFunctor.M.IsBisimulation.head : ∀ {F : PFunctor.{uA, uB}} {R : F.M → F.M → Prop},
  PFunctor.M.IsBisimulation R →
    ∀ {a a' : F.A} {f : F.B a → F.M} {f' : F.B a' → F.M}, R (PFunctor.M.mk ⟨a, f⟩) (PFunctor.M.mk ⟨a', f'⟩) → a = a'
-- Lean.Parser.Extra
Lean.Parser.mkAntiquotSplice.parenthesizer : Lean.SyntaxNodeKind →
  Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
FirstOrder.Field.genericMonicPoly.eq_1 : ∀ (n : ℕ),
  FirstOrder.Field.genericMonicPoly n =
    FreeCommRing.of (Fin.last n) ^ n + ∑ i, FreeCommRing.of i.castSucc * FreeCommRing.of (Fin.last n) ^ ↑i
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.constInsertManyIfNewUnit : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {ρ : Type u_1} [inst : ForIn Id ρ α] {l : ρ}
  {t : Std.DTreeMap.Raw α (fun x => Unit) cmp}, t.WF → (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l).WF
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- An alias for endowing a ring with a preorder defined as the valuative relation.  -/
ValuativeRel.WithPreorder : Type u_1 → Type u_1
-- Plausible.Gen
/-- Get access to the size parameter of the `Gen` monad.  -/
Plausible.Gen.getSize : Plausible.Gen ℕ
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instSemilatticeInfOpenSubgroup : {G : Type u_1} → [inst : Group G] → [inst_1 : TopologicalSpace G] → SemilatticeInf (OpenSubgroup G)
-- Mathlib.Order.Filter.Bases.Basic
Filter.IsAntitoneBasis.toIsBasis : ∀ {α : Type u_1} {ι'' : Type u_6} [inst : Preorder ι''] {s'' : ι'' → Set α},
  Filter.IsAntitoneBasis s'' → Filter.IsBasis (fun x => True) s''
-- Mathlib.RingTheory.Extension.Generators
/-- Given families of generators `X ⊆ T`, there is a map `R[X] → S[X]`.  -/
Algebra.Generators.toExtendScalars : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            {T : Type u_7} →
              [inst_3 : CommRing T] →
                [inst_4 : Algebra R T] →
                  [inst_5 : Algebra S T] →
                    [inst_6 : IsScalarTower R S T] →
                      (P : Algebra.Generators R T ι) → P.Hom (Algebra.Generators.extendScalars S P)
-- Mathlib.Algebra.Homology.CochainComplexPlus
/-- The inclusion of the full subcategory of bounded below cochain complexes.  -/
CochainComplex.Plus.ι : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      CategoryTheory.Functor (CochainComplex.Plus C) (CochainComplex C ℤ)
-- Mathlib.Algebra.Group.End
/-- **Alias** of `AddAut.add_apply`. -/
AddAut.mul_apply : ∀ (M : Type u_2) [inst : Add M] (e₁ e₂ : AddAut M) (m : M), (e₁ + e₂) m = e₁ (e₂ m)
-- Mathlib.Data.Multiset.Filter
Multiset.monotone_filter_right : ∀ {α : Type u_1} (s : Multiset α) ⦃p q : α → Prop⦄ [inst : DecidablePred p] [inst_1 : DecidablePred q],
  (∀ (b : α), p b → q b) → Multiset.filter p s ≤ Multiset.filter q s
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.commGroup.eq_1 : ∀ {𝕜 : 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] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : CommGroup G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : LieGroup I' n G], ContMDiffMap.commGroup = { toGroup := ContMDiffMap.group, mul_comm := ⋯ }
-- Mathlib.Logic.Relation
Relation.iff_comp : ∀ {α : Type u_1} {r : Prop → α → Prop}, Relation.Comp (fun x1 x2 => x1 ↔ x2) r = r
-- Init.Data.Bool
Bool.cond_neg : ∀ {α : Sort u_1} {b : Bool} {a a' : α}, b = false → (bif b then a else a') = a'
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.limitConePtAux.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteGrp.{max v u}),
  ProfiniteGrp.limitConePtAux F =
    { carrier := {x | ∀ ⦃i j : J⦄ (π : i ⟶ j), (ProfiniteGrp.Hom.hom (F.map π)) (x i) = x j}, mul_mem' := ⋯,
      one_mem' := ⋯, inv_mem' := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.RelStruct.ofEq_map : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} (h : f = g) (i : Fin (n + 1)),
  (SSet.PtSimplex.RelStruct.ofEq h i).map = CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.σ i) f.map
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasFDerivWithinAt.comp_hasDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : 𝕜 → F}
  {f' : F} (x : 𝕜) {l : F → E} {l' : F →L[𝕜] E} {t : Set F},
  HasFDerivWithinAt l l' t (f x) → HasDerivAt f f' x → (∀ᶠ (x' : 𝕜) in nhds x, f x' ∈ t) → HasDerivAt (l ∘ f) (l' f') x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.PushoutCocone.pasteVert.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {Y₃ Y₂ Y₁ X₃ : C} {g₂ : Y₃ ⟶ Y₂} {g₁ : Y₂ ⟶ Y₁} {i₃ : Y₃ ⟶ X₃}
  (t₁ : CategoryTheory.Limits.PushoutCocone g₂ i₃) {i₂ : Y₂ ⟶ t₁.pt}
  (t₂ t₂_1 : CategoryTheory.Limits.PushoutCocone g₁ i₂),
  t₂ = t₂_1 → ∀ (hi₂ : i₂ = t₁.inl), t₁.pasteVert t₂ hi₂ = t₁.pasteVert t₂_1 hi₂
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.mk_hom : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F), (CategoryTheory.Functor.RightExtension.mk F' α).hom = α
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_mem_coeffsIn : ∀ {R : Type u_2} {S : Type u_3} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Module R S]
  {M : Submodule R S} {x : S}, MvPolynomial.C x ∈ MvPolynomial.coeffsIn σ M ↔ x ∈ M
-- Init.Data.Rat.Basic
/-- The numerator of the rational number is an integer.  -/
Rat.num : ℚ → ℤ
-- Mathlib.Order.Sublattice
Sublattice.sup_mem : ∀ {α : Type u_2} [inst : Lattice α] {L : Sublattice α} {a b : α}, a ∈ L → b ∈ L → a ⊔ b ∈ L
-- Mathlib.Geometry.Euclidean.Incenter
/-- An excenter of a triangle is either the incenter or the excenter opposite one of three
enumerated different vertices. This is intended for when it is known a point is an excenter and
it is to be proved which excenter it is by elimination of the other cases.  -/
Affine.Triangle.excenter_eq_incenter_or_excenter_singleton_of_ne : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (t : Affine.Triangle ℝ P) (signs : Finset (Fin 3)) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        Affine.Simplex.excenter t signs = Affine.Simplex.incenter t ∨
          Affine.Simplex.excenter t signs = Affine.Simplex.excenter t {i₁} ∨
            Affine.Simplex.excenter t signs = Affine.Simplex.excenter t {i₂} ∨
              Affine.Simplex.excenter t signs = Affine.Simplex.excenter t {i₃}
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_mod_of_dvd : ∀ (a b : UInt64), b.toNat ∣ 65536 → (a % b).toUInt16 = a.toUInt16 % b.toUInt16
-- Batteries.Data.List.Lemmas
List.cons_diff_of_mem : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l₂ : List α},
  a ∈ l₂ → ∀ (l₁ : List α), (a :: l₁).diff l₂ = l₁.diff (l₂.erase a)
-- Mathlib.GroupTheory.Submonoid.Inverses
IsAddUnit.addSubmonoid.coe_neg : ∀ {M : Type u_1} [inst : AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)), ↑(-x) = ↑(-IsAddUnit.addUnit ⋯)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.maxKey? = some km → t.contains km = true
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.opEquiv.match_13.splitter : (C : Type u_1) →
  (motive : CategoryTheory.WithTerminal Cᵒᵖ → Sort u_2) →
    (x : CategoryTheory.WithTerminal Cᵒᵖ) →
      ((x : Cᵒᵖ) → motive (CategoryTheory.WithTerminal.of x)) →
        (Unit → motive CategoryTheory.WithTerminal.star) → motive x
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.mul_add_right_right_iff : ∀ {R : Type u} [inst : CommRing R] {x y z : R}, IsCoprime x (z * x + y) ↔ IsCoprime x y
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The unitary elements of continuous linear maps on a Hilbert space coincide with the linear
isometric equivalences on that Hilbert space.  -/
Unitary.linearIsometryEquiv : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {H : Type u_5} →
      [inst_1 : NormedAddCommGroup H] →
        [inst_2 : InnerProductSpace 𝕜 H] → [inst_3 : CompleteSpace H] → ↥(unitary (H →L[𝕜] H)) ≃* (H ≃ₗᵢ[𝕜] H)
-- Mathlib.Analysis.RCLike.Basic
RCLike.normSq_sub : ∀ {K : Type u_1} [inst : RCLike K] (z w : K),
  RCLike.normSq (z - w) = RCLike.normSq z + RCLike.normSq w - 2 * RCLike.re (z * (starRingEnd K) w)
-- Mathlib.Control.Bitraversable.Instances
instLawfulBitraversableProd : LawfulBitraversable Prod
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → ∀ {h : k' ∈ Std.ExtTreeMap.ofList l cmp}, (Std.ExtTreeMap.ofList l cmp)[k'] = v
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z},
  autoParam (CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g i)
      CategoryTheory.CommSq.w._autoParam →
    CategoryTheory.CommSq f g h i
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Transitivity of multiplication-preserving isomorphisms  -/
MulEquiv.trans : {M : Type u_4} →
  {N : Type u_5} → {P : Type u_6} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : Mul P] → M ≃* N → N ≃* P → M ≃* P
-- Batteries.Data.List.Count
List.injective_idxToSigmaCount : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : ReflBEq α] {xs : List α}, Function.Injective xs.idxToSigmaCount
-- Init.Data.Vector.Zip
Vector.zipWith_append : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n m : ℕ} {f : α → β → γ} {as : Vector α n} {as' : Vector α m}
  {bs : Vector β n} {bs' : Vector β m},
  Vector.zipWith f (as ++ as') (bs ++ bs') = Vector.zipWith f as bs ++ Vector.zipWith f as' bs'
-- Mathlib.LinearAlgebra.Ray
/-- Scaling by a positive unit is a no-op.  -/
Module.Ray.units_smul_of_pos : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (u : Rˣ), 0 < ↑u → ∀ (v : Module.Ray R M), u • v = v
-- Mathlib.Data.List.Sublists
List.sublists_cons_perm_append : ∀ {α : Type u} (a : α) (l : List α), (a :: l).sublists.Perm (l.sublists ++ List.map (List.cons a) l.sublists)
-- Mathlib.Data.Rat.Star
NNRat.addSubmonoid_closure_range_mul_self : AddSubmonoid.closure (Set.range fun x => x * x) = ⊤
-- Init.Data.Iterators.Basic
Std.IterM.IsPlausibleIndirectSuccessorOf.brecOn : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] {a : Std.IterM m β}
  {motive : (a_1 : Std.IterM m β) → a.IsPlausibleIndirectSuccessorOf a_1 → Prop} {a_1 : Std.IterM m β}
  (t : a.IsPlausibleIndirectSuccessorOf a_1),
  (∀ (a_2 : Std.IterM m β) (t : a.IsPlausibleIndirectSuccessorOf a_2),
      Std.IterM.IsPlausibleIndirectSuccessorOf.below t → motive a_2 t) →
    motive a_1 t
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.isMulCocycle₂_of_mem_cocycles₂ : ∀ {G M : Type} [inst : Group G] [inst_1 : CommGroup M] [inst_2 : MulDistribMulAction G M],
  ∀ f ∈ groupCohomology.cocycles₂ (Rep.ofMulDistribMulAction G M), groupCohomology.IsMulCocycle₂ (⇑Additive.toMul ∘ f)
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- This relies on `default ℕ = 0`.  -/
List.tail_sum : ∀ (L : List ℕ), L.tail.sum = L.sum - L.headI
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.all_toList : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {p : (a : α) → β a → Bool},
  (m.toList.all fun x => p x.fst x.snd) = m.all p
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.exact_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S₁ S₂ : CategoryTheory.ComposableArrows C n} (e : S₁ ≅ S₂), S₁.Exact → S₂.Exact
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_image_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Set α), IsPiSystem (Set.Iic '' s)
-- Mathlib.Data.Tree.Basic
BinaryTree.instInhabited : {α : Type u} → Inhabited (BinaryTree α)
-- Mathlib.Algebra.Order.SuccPred
Order.covBy_iff_sub_one_eq : ∀ {α : Type u_1} {x y : α} [inst : PartialOrder α] [inst_1 : Sub α] [inst_2 : One α] [PredSubOrder α] [NoMinOrder α],
  x ⋖ y ↔ y - 1 = x
-- Mathlib.RingTheory.PowerSeries.Order
/-- The order of the product of two formal power series over an integral domain
is the sum of their orders.  -/
PowerSeries.order_mul : ∀ {R : Type u_1} [inst : Semiring R] [NoZeroDivisors R] (φ ψ : PowerSeries R), (φ * ψ).order = φ.order + ψ.order
-- Mathlib.Logic.Small.Set
small_union : ∀ {α : Type u1} (s t : Set α) [Small.{u, u1} ↑s] [Small.{u, u1} ↑t], Small.{u, u1} ↑(s ∪ t)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.ofMulEquivOfDom_eq : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {T : Submonoid P} {k : P ≃* M}
  (H : Submonoid.map k.toMonoidHom T = S), (f.ofMulEquivOfDom H).toMonoidHom = f.toMonoidHom.comp k.toMonoidHom
-- Mathlib.Order.Basic
Prod.instLE_mathlib : {α : Type u_2} → {β : Type u_3} → [LE α] → [LE β] → LE (α × β)
-- Mathlib.Analysis.Analytic.Order
/-- The set where an analytic function has infinite order is clopen in its domain of analyticity.  -/
AnalyticOnNhd.isClopen_setOfPred_analyticOrderAt_eq_top : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E}, AnalyticOnNhd 𝕜 f U → IsClopen {u | analyticOrderAt f ↑u = ⊤}
-- Init.Data.Int.DivMod.Lemmas
Int.tdiv_one : ∀ (a : ℤ), a.tdiv 1 = a
-- Mathlib.NumberTheory.RamificationInertia.Galois
Ideal.ramificationIdxIn_mul_ramificationIdxIn : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {p : Ideal A}
  (P : Ideal B) [hPp : P.IsPrime] [hp : P.LiesOver p] (G : Type u_3) [inst_3 : Group G] [Finite G]
  [inst_5 : MulSemiringAction G B] [IsGaloisGroup G A B] (C : Type u_4) [inst_7 : CommRing C] [inst_8 : Algebra A C]
  [inst_9 : Algebra B C] [Nonempty ↑(P.primesOver C)] [IsScalarTower A B C] (GAC : Type u_5) [inst_12 : Group GAC]
  [Finite GAC] [inst_14 : MulSemiringAction GAC C] [IsGaloisGroup GAC A C] (GBC : Type u_6) [inst_16 : Group GBC]
  [Finite GBC] [inst_18 : MulSemiringAction GBC C] [IsGaloisGroup GBC B C] [Module.Flat B C],
  p.ramificationIdxIn B * P.ramificationIdxIn C = p.ramificationIdxIn C
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.le_sliceTo_iff : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h : q ≤ p₀},
  p ≤ p₀.sliceTo q h ↔ String.Slice.Pos.ofSliceTo p ≤ q
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] [inst_1 : SupSet β] (f : α → β)
  (hf : ∀ (s : Set α), f (sSup s) = sSup (f '' s)), ⇑{ toFun := f, map_sSup' := hf } = f
-- Mathlib.Algebra.Category.Grp.Limits
/-- If `J` is `u`-small, the forgetful functor from `CommGrpCat.{u}` preserves limits of
shape `J`.  -/
CommGrpCat.forget_preservesLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget CommGrpCat)
-- Mathlib.Geometry.Diffeology.Basic
Diffeology.IsContDiffCompatible.mk : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] [inst_1 : NormedSpace ℝ X] [inst_2 : DiffeologicalSpace X],
  (∀ {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X}, Diffeology.IsPlot p ↔ ContDiff ℝ (↑⊤) p) →
    Diffeology.IsContDiffCompatible X
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- A `R`-algebra homomorphism from `A[M]` is uniquely defined by its
values on the functions `single m 1` and `single 1 a`.

See note [partially-applied ext lemmas]. Note that the first assumption isn't written as an
equality of `AddMonoidHom`s because `of` doesn't multiplicativise.  -/
AddMonoidAlgebra.algHom_ext : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : AddMonoid M]
  ⦃φ₁ φ₂ : AddMonoidAlgebra A M →ₐ[R] B⦄,
  (∀ (m : M), φ₁ (AddMonoidAlgebra.single m 1) = φ₂ (AddMonoidAlgebra.single m 1)) →
    φ₁.comp AddMonoidAlgebra.singleZeroAlgHom = φ₂.comp AddMonoidAlgebra.singleZeroAlgHom → φ₁ = φ₂
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.coconesEquiv_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  (G : CategoryTheory.Functor D E),
  (CategoryTheory.Functor.Final.coconesEquiv F G).inverse = CategoryTheory.Limits.Cocone.whiskering F
-- Mathlib.MeasureTheory.Measure.PreVariation
/-- The `Measure X` built from a σ-subadditive function.  -/
MeasureTheory.preVariation : {X : Type u_1} →
  [inst : MeasurableSpace X] →
    (f : Set X → ENNReal) → MeasureTheory.IsSigmaSubadditiveSetFun f → f ∅ = 0 → MeasureTheory.Measure X
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- The conjugation action by elements of the spin group keeps vectors as vectors.  -/
pinGroup.conjAct_smul_ι_mem_range_ι : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ},
  ↑x ∈ pinGroup Q →
    ∀ [Invertible 2] (y : M), ConjAct.toConjAct x • (CliffordAlgebra.ι Q) y ∈ (CliffordAlgebra.ι Q).range
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.addSemigroup.eq_1 : ∀ {𝕜 : 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] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : AddSemigroup G] [inst_10 : TopologicalSpace G]
  [inst_11 : ChartedSpace H' G] [inst_12 : ContMDiffAdd I' n G],
  ContMDiffMap.addSemigroup = Function.Injective.addSemigroup DFunLike.coe ⋯ ⋯
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toSpanSingletonLE_apply : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : SMulCommClass R S M] [inst_6 : TopologicalSpace M]
  [inst_7 : ContinuousAdd M] [inst_8 : ContinuousConstSMul S M] [inst_9 : TopologicalSpace R]
  [inst_10 : ContinuousSMul R M], ⇑(ContinuousLinearMap.toSpanSingletonLE R S M) = ContinuousLinearMap.toSpanSingleton R
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.lift_comp : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)),
  (f.lift hg).comp f.toMonoidHom = g
-- Mathlib.MeasureTheory.Measure.Hausdorff
/-- An outer measure constructed using `OuterMeasure.mkMetric'` is a metric outer measure.  -/
MeasureTheory.OuterMeasure.mkMetric'_isMetric : ∀ {X : Type u_2} [inst : EMetricSpace X] (m : Set X → ENNReal), (MeasureTheory.OuterMeasure.mkMetric' m).IsMetric
-- Std.Data.DHashMap.Basic
Std.DHashMap.instInhabited : {α : Type u} → {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Inhabited (Std.DHashMap α β)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `BitVec.ofInt`.  -/
BitVec.reduceOfInt : Lean.Meta.Simp.DSimproc