mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Prod
LinearMap.prodMap_zero : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} {M₄ : Type z} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄], LinearMap.prodMap 0 0 = 0
-- Init.Prelude
/-- The array of elements and separators, ordered like
`#[el1, sep1, el2, sep2, el3]`.  -/
Lean.Syntax.SepArray.elemsAndSeps : {sep : String} → Lean.Syntax.SepArray sep → Array Lean.Syntax
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.toSigmaCofork_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} {c : CategoryTheory.Limits.Cofan I.left}
  (hc : CategoryTheory.Limits.IsColimit c) {d : CategoryTheory.Limits.Cofan I.right}
  (hd : CategoryTheory.Limits.IsColimit d) (K : CategoryTheory.Limits.Multicofork I),
  (CategoryTheory.Limits.Multicofork.toSigmaCofork hc hd K).pt = K.pt
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.instPreservesFiniteLimitsObjFunctorExactFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : C ⥤ₑ D), CategoryTheory.Limits.PreservesFiniteLimits F.obj
-- Mathlib.Algebra.Module.Congruence.Defs
/-- A `SMulCon` is closed under scalar multiplication.  -/
ModuleCon.smul : ∀ {S : Type u_2} {M : Type u_3} [inst : Add M] [inst_1 : SMul S M] (self : ModuleCon S M) (s : S) {x y : M},
  self.toSetoid x y → self.toSetoid (s • x) (s • y)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.categoryStruct_id_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) {a b : B} (f : a ⟶ b),
  (CategoryTheory.CategoryStruct.id F).naturality f =
    CategoryTheory.Bicategory.leftUnitor (F.map f) ≪≫ (CategoryTheory.Bicategory.rightUnitor (F.map f)).symm
-- Mathlib.Order.Directed
Monotone.directed_ge : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [IsCodirectedOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Directed (fun x1 x2 => x2 ≤ x1) f
-- Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Mathlib.Tactic.Monoidal.naturality_leftUnitor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {p f pf : C}
  (η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj p f ≅ pf),
  CategoryTheory.MonoidalCategory.whiskerLeftIso p (CategoryTheory.MonoidalCategoryStruct.leftUnitor f) ≪≫ η_f =
    Mathlib.Tactic.Monoidal.normalizeIsoComp (CategoryTheory.MonoidalCategoryStruct.rightUnitor p) η_f
-- Mathlib.Algebra.Homology.Square
/-- The colimit cokernel cofork attached to a pushout square.  -/
CategoryTheory.Square.IsPushout.isColimitCokernelCofork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {sq : CategoryTheory.Square C} →
        [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct sq.X₂ sq.X₃] →
          sq.IsPushout → CategoryTheory.Limits.IsColimit sq.cokernelCofork
-- Mathlib.Data.List.DropRight
List.rdropWhile_idempotent : ∀ {α : Type u_1} (p : α → Bool) (l : List α), List.rdropWhile p (List.rdropWhile p l) = List.rdropWhile p l
-- Mathlib.CategoryTheory.Join.Opposites
_private.Mathlib.CategoryTheory.Join.Opposites.0.CategoryTheory.Join.opEquiv.match_5.splitter : (C : Type u_4) →
  (D : Type u_3) →
    [inst : CategoryTheory.Category.{u_2, u_4} C] →
      [inst_1 : CategoryTheory.Category.{u_1, u_3} D] →
        (motive : CategoryTheory.Join Dᵒᵖ Cᵒᵖ → Sort u_5) →
          (x : CategoryTheory.Join Dᵒᵖ Cᵒᵖ) →
            ((a : Dᵒᵖ) → motive (CategoryTheory.Join.left a)) →
              ((a : Cᵒᵖ) → motive (CategoryTheory.Join.right a)) → motive x
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.whisker_exchange_bimod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {X Y Z : CategoryTheory.Mon C} {M N : Bimod X Y} {P Q : Bimod Y Z} (f : M ⟶ N) (g : P ⟶ Q),
  CategoryTheory.CategoryStruct.comp (M.whiskerLeft g) (Bimod.whiskerRight f Q) =
    CategoryTheory.CategoryStruct.comp (Bimod.whiskerRight f P) (N.whiskerLeft g)
-- Mathlib.Analysis.InnerProductSpace.SingularValues
LinearMap.sq_singularValues_of_lt : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) {n : ℕ} (hn : Module.finrank 𝕜 E = n) {i : ℕ} (hi : i < n),
  T.singularValues i ^ 2 = ⋯.eigenvalues hn ⟨i, hi⟩
-- Mathlib.Data.ENNReal.Basic
ENNReal.instNontrivial : Nontrivial ENNReal
-- Mathlib.Order.Heyting.Hom
BiheytingHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β]
  [inst_2 : BiheytingAlgebra γ] [inst_3 : BiheytingAlgebra δ] (f : BiheytingHom γ δ) (g : BiheytingHom β γ)
  (h : BiheytingHom α β), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Analysis.Distribution.TestFunction
TestFunctionClass.toDFunLike : {B : Type u_6} →
  {E : outParam (Type u_7)} →
    {inst : NormedAddCommGroup E} →
      {inst_1 : NormedSpace ℝ E} →
        {Ω : outParam (TopologicalSpace.Opens E)} →
          {F : outParam (Type u_8)} →
            {inst_2 : NormedAddCommGroup F} →
              {inst_3 : NormedSpace ℝ F} →
                {n : outParam ℕ∞} → [self : TestFunctionClass B Ω F n] → DFunLike B E fun x => F
-- Mathlib.Combinatorics.HalesJewett
Combinatorics.Subspace.apply_def : ∀ {η : Type u_5} {α : Type u_6} {ι : Type u_7} (l : Combinatorics.Subspace η α ι) (x : η → α) (i : ι),
  ↑l x i = Sum.elim id x (l.idxFun i)
-- Mathlib.Topology.FiberBundle.Trivialization
/-- See Note [custom simps projection]  -/
Bundle.Trivialization.Simps.symm_apply : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          [inst_2 : TopologicalSpace Z] → (proj : Z → B) → Bundle.Trivialization F proj → B × F → Z
-- Mathlib.Algebra.Module.ULift
ULift.mulAction : {R : Type u} → {M : Type v} → [inst : Monoid R] → [MulAction R M] → MulAction (ULift.{u_1, u} R) M
-- Mathlib.CategoryTheory.ObjectProperty.Equivalence
CategoryTheory.ObjectProperty.topEquivalence_counitIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.ObjectProperty.topEquivalence C).counitIso =
    CategoryTheory.Iso.refl ((⊤.lift (CategoryTheory.Functor.id C) ⋯).comp ⊤.ι)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.mem_fixingSubgroup_insert_iff : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {a : α} {s : Set α} {m : M},
  m ∈ fixingSubgroup M (insert a s) ↔ m • a = a ∧ m ∈ fixingSubgroup M s
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.coe_zero : ∀ {α : Type u_1} {_m : MeasurableSpace α}, ⇑0 = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Y : C}
  {φ φ' : Y ⟶ h.pullback},
  CategoryTheory.CategoryStruct.comp φ h.p₁ = CategoryTheory.CategoryStruct.comp φ' h.p₁ →
    CategoryTheory.CategoryStruct.comp φ h.p₂ = CategoryTheory.CategoryStruct.comp φ' h.p₂ →
      CategoryTheory.CategoryStruct.comp φ h.p₃ = CategoryTheory.CategoryStruct.comp φ' h.p₃ → φ = φ'
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.intCast_mul_eq_zsmul : ∀ (x : ℝ) (n : ℤ), ↑(↑n * x) = n • ↑x
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max?_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (∀ (k' : α), t.max? = some k' → (cmp k' k).isLE = true) ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Order.Bounded
Set.unbounded_gt_of_forall_exists_ge : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α], (∀ (a : α), ∃ b ∈ s, b ≤ a) → Set.Unbounded (fun x1 x2 => x1 > x2) s
-- Mathlib.RingTheory.Idempotents
OrthogonalIdempotents.isIdempotentElem_sum : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} {e : I → R},
  OrthogonalIdempotents e → ∀ {s : Finset I}, IsIdempotentElem (∑ i ∈ s, e i)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.id_whiskerRight : ∀ {B : Type u} [self : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  CategoryTheory.Bicategory.whiskerRight (CategoryTheory.CategoryStruct.id f) g =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Data.PFun
PFun.mem_core : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) (s : Set β), x ∈ f.core s ↔ ∀ y ∈ f x, y ∈ s
-- Mathlib.Data.Num.Lemmas
PosNum.bit.eq_1 : ∀ (b : Bool), PosNum.bit b = bif b then PosNum.bit1 else PosNum.bit0
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- If `ι` is finite, the disjoint union of the prime spectra of the `R i` is homeomorphic
to the prime spectrum of the product.  -/
PrimeSpectrum.sigmaToPiHomeo : {ι : Type u_3} →
  (R : ι → Type u_4) →
    [inst : (i : ι) → CommRing (R i)] → [Finite ι] → (i : ι) × PrimeSpectrum (R i) ≃ₜ PrimeSpectrum ((i : ι) → R i)
-- Mathlib.Data.Multiset.UnionInter
Multiset.nodup_add : ∀ {α : Type u_1} {s t : Multiset α}, (s + t).Nodup ↔ s.Nodup ∧ t.Nodup ∧ Disjoint s t
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- The `a₆` coefficient of a Weierstrass curve.  -/
WeierstrassCurve.a₆ : {R : Type u} → WeierstrassCurve R → R
-- Mathlib.Tactic.Linter.ValidatePRTitle
/-- Basic parser for PR titles: given a title `kind(scope): main title` or `kind: title`,
extracts the `kind`, `scope` and `main title` components.  -/
_private.Mathlib.Tactic.Linter.ValidatePRTitle.0.prTitle : Std.Internal.Parsec.String.Parser (String × Option String × String)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
Seminorm.isBounded_sup : ∀ {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι : Type u_9} {ι' : Type u_10} [inst : SeminormedRing 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : SeminormedRing 𝕜₂] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂] {p : ι → Seminorm 𝕜 E}
  {q : ι' → Seminorm 𝕜₂ F} {f : E →ₛₗ[σ₁₂] F},
  Seminorm.IsBounded p q f → ∀ (s' : Finset ι'), ∃ C s, (s'.sup q).comp f ≤ C • s.sup p
-- Mathlib.Tactic.FunProp.Decl
/-- Turn tactic syntax into a discharger function.  -/
Mathlib.Meta.FunProp.tacticToDischarge : Lean.TSyntax `tactic → Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.ModelTheory.ElementaryMaps
FirstOrder.Language.ElementaryEmbedding.map_fun : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] [inst_1 : L.Structure N]
  (φ : L.ElementaryEmbedding M N) {n : ℕ} (f : L.Functions n) (x : Fin n → M),
  φ (FirstOrder.Language.Structure.funMap f x) = FirstOrder.Language.Structure.funMap f (⇑φ ∘ x)
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.isOpen_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] (F : Ctop.Realizer α) {s : Set α},
  IsOpen s ↔ ∀ a ∈ s, ∃ b, a ∈ F.F.f b ∧ F.F.f b ⊆ s
-- Lean.Meta.Match.Match
/-- Predicate for testing whether we need to expand `Int` value patterns into constructors.
There are two cases:
- We have constructor patterns. Example:
```
| 0, ...
| Int.toVal p, ...
...
```
- We don't have the `else`-case (i.e., inaccessible pattern). This can happen
when the non-value cases are unreachable.
 -/
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.isIntValueTransition : Lean.Meta.Match.Problem → Lean.MetaM Bool
-- Init.Data.ToString.Basic
instToStringSum : {α : Type u} → {β : Type v} → [ToString α] → [ToString β] → ToString (α ⊕ β)
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShiftCore.shift_app_assoc : ∀ {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₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] {a : A},
  CategoryTheory.NatTrans.CommShiftCore τ a →
    ∀ (X : C) {Z : D} (h : (CategoryTheory.shiftFunctor D a).obj (F₂.obj X) ⟶ Z),
      CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (τ.app X)) h =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F₁ a).inv.app X)
          (CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X))
            (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F₂ a).hom.app X) h))
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_lt_of_lt_log : ∀ {x y z : ℝ}, 0 < y → Real.log x < z * Real.log y → x < y ^ z
-- Init.Data.String.Lemmas.Pattern.Split.Pred
String.Slice.toList_splitToSubslice_prop : ∀ {s : String.Slice} {p : Char → Prop} [inst : DecidablePred p],
  List.map (String.Slice.copy ∘ String.Slice.Subslice.toSlice) (s.splitToSubslice p).toList =
    List.map String.ofList (List.splitOnP (fun b => decide (p b)) s.copy.toList)
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation.map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} {x : CategoryTheory.Presieve.FamilyOfElements P R} {t : P.obj (Opposite.op X)}
  (f : P ⟶ Q),
  x.IsAmalgamation t → (x.map f).IsAmalgamation ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op X))) t)
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.evariance_zero_measure : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ}, ProbabilityTheory.evariance X 0 = 0
-- Mathlib.Data.Set.Function
Function.Injective.injOn_range : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ},
  Function.Injective (g ∘ f) → Set.InjOn g (Set.range f)
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
DirichletCharacter.rootNumber.eq_1 : ∀ {N : ℕ} [inst : NeZero N] (χ : DirichletCharacter ℂ N),
  χ.rootNumber = (gaussSum χ ZMod.stdAddChar / Complex.I ^ if χ.Even then 0 else 1) / ↑N ^ (1 / 2)
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.exists_mul_lt_apply_of_lt_opNNNorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  (f : E →SL[σ₁₂] F) {r : NNReal}, r < ‖f‖₊ → ∃ x, r * ‖x‖₊ < ‖f x‖₊
-- Mathlib.Order.Copy
OrderBot.copy.congr_simp : ∀ {α : Type u} {h h' : LE α} (c c_1 : OrderBot α) (e_c : c = c_1) (bot bot_1 : α) (e_bot : bot = bot_1)
  (eq_bot : bot = ⊥) (le_eq : ∀ (x y : α), x ≤ y ↔ x ≤ y), c.copy bot eq_bot le_eq = c_1.copy bot_1 ⋯ le_eq
-- Mathlib.Data.Fin.Tuple.Basic
Fin.find_eq_dite : ∀ {n : ℕ} {p : Fin (n + 1) → Prop} [inst : DecidablePred p] (h : ∃ i, p i),
  Fin.find p h = if h0 : p 0 then 0 else (Fin.find (fun k => p k.succ) ⋯).succ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_of_contains_union!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α},
        Std.DTreeMap.Internal.Impl.contains k (m₁.union! m₂) = true →
          Std.DTreeMap.Internal.Impl.contains k m₁ = false → Std.DTreeMap.Internal.Impl.contains k m₂ = true
-- Aesop.Index.Basic
/-- Pattern substitutions for this rule that were found in the goal. `none`
iff the rule doesn't have a pattern. The array contains no duplicates.  -/
Aesop.IndexMatchResult.patternSubsts? : {α : Type} → Aesop.IndexMatchResult α → Option (Array Aesop.Substitution)
-- Init.Data.List.Lemmas
List.mem_singleton_self : ∀ {α : Type u_1} (a : α), a ∈ [a]
-- Init.Data.Array.Lemmas
Array.size_leftpad : ∀ {α : Type u_1} {n : ℕ} {a : α} {xs : Array α}, (Array.leftpad n a xs).size = max n xs.size
-- Mathlib.LinearAlgebra.BilinearForm.DualLattice
/-- The natural paring of `B.dualSubmodule N` and `N`.  -/
LinearMap.BilinForm.dualSubmoduleToDual : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : Field S] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Algebra R S] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] →
                  [inst_6 : IsScalarTower R S M] →
                    (B : LinearMap.BilinForm S M) →
                      [IsDomain R] →
                        [Module.IsTorsionFree R S] → (N : Submodule R M) → ↥(B.dualSubmodule N) →ₗ[R] Module.Dual R ↥N
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.mkOrCached.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.BinaryInput),
  aig.mkOrCached input =
    { aig := (aig.mkGateCached (input.invert true true)).aig,
      ref := (aig.mkGateCached (input.invert true true)).ref.not }
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
/-- Part 4 of the induction structure applied to `Statement R₀ R n`. See the docstring of
`induction_structure`.  -/
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.induction_aux : ∀ {R₀ : Type u_1} [inst : CommRing R₀] {n : ℕ} (R : Type u_6) [inst_1 : CommRing R] [inst_2 : Algebra R₀ R] (c : R)
  (i : Fin n) (e : ChevalleyThm.PolynomialC.InductionObj✝ R n),
  c = (ChevalleyThm.PolynomialC.InductionObj.val✝ e i).leadingCoeff →
    c ≠ 0 →
      ChevalleyThm.PolynomialC.InductionObj.Statement✝ R₀ (Localization.Away c) n
          {
            val :=
              Polynomial.C (IsLocalization.Away.invSelf c) •
                ⇑(Polynomial.mapRingHom (algebraMap R (Localization.Away c))) ∘
                  ChevalleyThm.PolynomialC.InductionObj.val✝ e } →
        ChevalleyThm.PolynomialC.InductionObj.Statement✝ R₀ (R ⧸ Ideal.span {c}) n
            {
              val :=
                ⇑(Polynomial.mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘
                  ChevalleyThm.PolynomialC.InductionObj.val✝ e } →
          ChevalleyThm.PolynomialC.InductionObj.Statement✝ R₀ R n e
-- Mathlib.Order.SupIndep
iSupIndep_pair : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] {t : ι → α} {i j : ι},
  i ≠ j → (∀ (k : ι), k = i ∨ k = j) → (iSupIndep t ↔ Disjoint (t i) (t j))
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
norm_iteratedFDerivWithin_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E}, ‖iteratedFDerivWithin 𝕜 0 f s x‖ = ‖f x‖
-- Mathlib.Topology.Algebra.IsUniformGroup.Constructions
isUniformGroup_iInf : ∀ {G : Type u_1} [inst : Group G] {ι : Sort u_4} {us' : ι → UniformSpace G},
  (∀ (i : ι), IsUniformGroup G) → IsUniformGroup G
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsMulIndecomposable.pairwise_baseOf_div_notMem : ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S] [inst_2 : InvolutiveInv ι]
  [inst_3 : CommGroup S] [IsOrderedMonoid S] (v : ι → G),
  (∀ (i : ι), v i⁻¹ = (v i)⁻¹) →
    ∀ (f : G →* S),
      (∀ (i : ι), f (v i) ≠ 1) → (IsMulIndecomposable.baseOf v f).Pairwise fun i j => v i / v j ∉ Set.range v
-- Mathlib.Topology.Connected.PathConnected
JoinedIn.joined : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {F : Set X}, JoinedIn F x y → Joined x y
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.KernelFork.map_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.KernelFork f) (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms], CategoryTheory.Limits.Fork.ι (c.map G) = G.map (CategoryTheory.Limits.Fork.ι c)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_pow : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (x : R) [inst : CommRing R] (n : ℕ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support_symmDiff_support_subset_support_add : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (p q : MvPolynomial σ R),
  symmDiff p.support q.support ⊆ (p + q).support
-- Mathlib.Algebra.Category.Grp.EpiMono
GrpCat.SurjectiveOfEpiAuxs.h.eq_1 : ∀ {A B : GrpCat} (f : A ⟶ B),
  GrpCat.SurjectiveOfEpiAuxs.h f =
    {
      toFun := fun β =>
        ((Equiv.symm (GrpCat.SurjectiveOfEpiAuxs.tau f)).trans ((GrpCat.SurjectiveOfEpiAuxs.g f) β)).trans
          (GrpCat.SurjectiveOfEpiAuxs.tau f),
      map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.diff : ∀ {α : Type u_1} {m : MeasurableSpace α} {s₁ s₂ : Set α}, MeasurableSet s₁ → MeasurableSet s₂ → MeasurableSet (s₁ \ s₂)
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.isLittleO_logb_id_atTop : ∀ {b : ℝ}, Real.logb b =o[Filter.atTop] id
-- Mathlib.Data.List.Chain
/-- Given a chain from `a` to `b`, and a predicate true at `b`, if `r x y → p y → p x` then
the predicate is true at `a`.
That is, we can propagate the predicate all the way up the chain.
 -/
List.IsChain.backwards_cons_induction_head : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α),
  List.IsChain r (a :: l) → (a :: l).getLast ⋯ = b → (∀ ⦃x y : α⦄, r x y → p y → p x) → p b → p a
-- Mathlib.Data.Multiset.Filter
Multiset.le_filter : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {s t : Multiset α},
  s ≤ Multiset.filter p t ↔ s ≤ t ∧ ∀ a ∈ s, p a
-- Init.WFComputable
WellFounded.fix_eq_fixC : @WellFounded.fix = @WellFounded.fixC
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartRing.leibniz_mul_right' : ∀ {A : Type u_1} {L : Type u_2} {inst : CommRing A} {inst_1 : LieRing L} {inst_2 : Module A L}
  {inst_3 : LieRingModule L A} [self : LieRinehartRing A L] (x : L) (a b : A), ⁅x, a * b⁆ = a • ⁅x, b⁆ + ⁅x, a⁆ * b
-- Init.Data.Nat.ToString
_private.Init.Data.Nat.ToString.0.Nat.toDigitsCore_eq_of_lt_fuel : ∀ {b n fuel₁ fuel₂ : ℕ} {cs : List Char},
  1 < b → n < fuel₁ → n < fuel₂ → b.toDigitsCore fuel₁ n cs = b.toDigitsCore fuel₂ n cs
-- Batteries.Control.AlternativeMonad
LawfulAlternativeLift.mk : ∀ {m : semiOutParam (Type u → Type v)} {n : Type u → Type w} [inst : Alternative m] [inst_1 : Alternative n]
  [inst_2 : MonadLift m n],
  (∀ {α : Type u}, monadLift failure = failure) →
    (∀ {α : Type u} (x y : m α), monadLift (x <|> y) = (monadLift x <|> monadLift y)) → LawfulAlternativeLift m n
-- Mathlib.FieldTheory.PolynomialGaloisGroup
/-- For a separable polynomial, its Galois group has cardinality
equal to the dimension of its splitting field over `F`.  -/
Polynomial.Gal.card_of_separable : ∀ {F : Type u_1} [inst : Field F] {p : Polynomial F}, p.Separable → Nat.card p.Gal = Module.finrank F p.SplittingField
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.IsStarNormal.ker_adjoint_eq_ker : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E} [inst_3 : CompleteSpace E], IsStarNormal T → (↑(ContinuousLinearMap.adjoint T)).ker = (↑T).ker