mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.zip.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} (aig : Std.Sat.AIG α) (idx : ℕ) (s : aig.RefVec idx)
  (hidx : idx ≤ len) (lhs rhs : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [inst_3 : Std.Sat.AIG.RefVec.LawfulZipOperator α f],
  Std.Sat.AIG.RefVec.zip.go aig idx s hidx lhs rhs f =
    if hidx : idx < len then
      let res := f aig { lhs := lhs.get idx hidx, rhs := rhs.get idx hidx };
      let aig_1 := res.aig;
      have newRef := res.ref;
      have this := ⋯;
      have s := s.cast this;
      have s := s.push newRef;
      Std.Sat.AIG.RefVec.zip.go aig_1 (idx + 1) s ⋯ (lhs.cast this) (rhs.cast this) f
    else
      have this := ⋯;
      { aig := aig, vec := this ▸ s }
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.mk : {β : Type u_4} → Filter (Finset β) → SummationFilter β
-- Lean.Meta.Tactic.Grind.LawfulEqCmp
/-- If `op` implements `LawfulEqCmp`, then returns the proof term for
`∀ a b, op a b = .eq → a = b`
 -/
Lean.Meta.Grind.getLawfulEqCmpThm? : Lean.Expr → Lean.Meta.Grind.GrindM (Option Lean.Expr)
-- Mathlib.Order.Partition.Equipartition
Set.Subsingleton.isEquipartition : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {P : Finpartition s}, (↑P.parts).Subsingleton → P.IsEquipartition
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Fanin.ofRaw : ℕ → Std.Sat.AIG.Fanin
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.coe_mul : ∀ {R : Type u_1} {A : Type u_6} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : DecidableEq ι] [inst_4 : AddMonoid ι] {𝒜 : ι → Submodule R A} [inst_5 : GradedAlgebra 𝒜] (f g : 𝒜 →ₐᵍ[R] 𝒜),
  ⇑(f * g) = ⇑f ∘ ⇑g
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.head_terminates_of_mem : ∀ {α : Type u} {s : Stream'.WSeq α} {a : α}, a ∈ s → s.head.Terminates
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.periodicPts_subset_range : ∀ {α : Type u_1} {f : α → α}, Function.periodicPts f ⊆ Set.range f
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
/-- If two sequences have the same head and applying `op` reduces their distance, then
it also reduces the distance of their tails.  -/
Tactic.ComputeAsymptotics.Seq.dist_const_tail_cons_tail_le : ∀ {α : Type u_1} {op : Stream'.Seq α → Stream'.Seq α} {hd : α} {x y : Stream'.Seq α},
  dist (op (Stream'.Seq.cons hd x)) (op (Stream'.Seq.cons hd y)) ≤
      dist (Stream'.Seq.cons hd x) (Stream'.Seq.cons hd y) →
    dist (op (Stream'.Seq.cons hd x)).tail (op (Stream'.Seq.cons hd y)).tail ≤ dist x y
-- Mathlib.Analysis.Calculus.Conformal.InnerProduct
conformalFactorAt_pos : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : InnerProductSpace ℝ F] {f : E → F} {x : E} (h : ConformalAt f x),
  0 < conformalFactorAt h
-- Mathlib.GroupTheory.Submonoid.Center
AddSubmonoid.center_toAddSubsemigroup : ∀ (M : Type u_1) [inst : AddZeroClass M], (AddSubmonoid.center M).toAddSubsemigroup = AddSubsemigroup.center M
-- Mathlib.Order.Sublocale
Sublocale.carrier.instCompleteLattice : {X : Type u_1} → [inst : Order.Frame X] → {S : Sublocale X} → CompleteLattice ↥S
-- Init.Data.Array.Find
Array.findIdx?_eq_none_iff : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, Array.findIdx? p xs = none ↔ ∀ x ∈ xs, p x = false
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.get!_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {m : Std.DHashMap.Raw α β}
  (h : m.WF) {a : α} [inst_3 : Inhabited (β a)], m.get! a = Std.DHashMap.Internal.Raw₀.get! ⟨m, ⋯⟩ a
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
OpenPartialHomeomorph.interior_extend_target_subset_interior_range : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H}, interior (f.extend I).target ⊆ interior (Set.range ↑I)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.affineSpan_faceOpposite_le : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  affineSpan k (Set.range (s.faceOpposite i).points) ≤ affineSpan k (Set.range s.points)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_union_of_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₂ → k ∈ m₁ ∪ m₂
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.inter_neg : ∀ {α : Type u_2} [inst : Neg α] {s t : Set α}, -(s ∩ t) = -s ∩ -t
-- Lean.Environment
/-- Optional function that, given state before and after realization and newly added constants,
replays this change onto a state from another (derived) environment. This function is used only
when making changes to an extension inside a `realizeConst` call, in which case it must be
present.
 -/
Lean.EnvExtension.replay? : {σ : Type} → Lean.EnvExtension σ → Option (Lean.ReplayFn σ)
-- Init.Data.UInt.Lemmas
UInt32.toUSize_ofNat : ∀ {n : ℕ}, n < 4294967296 → (OfNat.ofNat n).toUSize = OfNat.ofNat n
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- The function `f ↦ cfc f a` is Lipschitz with constant 1 with respect to
supremum metric (on `R →ᵤ[{s}] R`) on those functions which are continuous on a set `s` containing
the spectrum.  -/
lipschitzOnWith_cfc_fun_of_subset : ∀ {R : Type u_2} {A : Type u_3} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A]
  [inst_7 : MetricSpace A] [inst_8 : Algebra R A] [inst_9 : IsometricContinuousFunctionalCalculus R A p] (a : A)
  {s : Set R},
  spectrum R a ⊆ s →
    LipschitzOnWith 1 (fun f => cfc ((UniformOnFun.toFun {s}) f) a) {f | ContinuousOn ((UniformOnFun.toFun {s}) f) s}
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.instIsIPCFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C]
  [inst_2 : CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C] [CategoryTheory.Limits.IsIPC C]
  {D : Type u₁} [inst_4 : CategoryTheory.Category.{v₁, u₁} D], CategoryTheory.Limits.IsIPC (CategoryTheory.Functor D C)
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.fpowerSeriesBilinear_apply_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (f : E →L[𝕜] F →L[𝕜] G) (x : E × F),
  f.fpowerSeriesBilinear x 0 = ContinuousMultilinearMap.uncurry0 𝕜 (E × F) ((f x.1) x.2)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.instAddGroup : {α : Type u_1} →
  {γ : Type u_3} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} →
        [inst_1 : TopologicalSpace γ] → [inst_2 : AddGroup γ] → [IsTopologicalAddGroup γ] → AddGroup (α →ₘ[μ] γ)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- `R'` as an algebra over `TrivSqZeroExt R' M`. Not an instance since it creates a different
`Algebra (TrivSqZeroExt R' M) (TrivSqZeroExt R' M)` instance from `TrivSqZeroExt.algebra'`.  -/
TrivSqZeroExt.algebraBase : (R' : Type u) →
  (M : Type v) →
    [inst : CommSemiring R'] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R' M] →
          [inst_3 : Module R'ᵐᵒᵖ M] → [inst_4 : IsCentralScalar R' M] → Algebra (TrivSqZeroExt R' M) R'
-- Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
/-- Given an `n`-th primitive root of unity `ζ`, we have that two conjugates of `ζ - 1`
are associated.  -/
IsPrimitiveRoot.associated_map_sub_one_map_sub_one : ∀ {A : Type u_1} {ζ : A} [inst : CommRing A] [IsDomain A] {R : Type u_3} [inst_2 : CommRing R] [inst_3 : Algebra R A]
  {n : ℕ} [NeZero n], IsPrimitiveRoot ζ n → ∀ (σ τ : A ≃ₐ[R] A), Associated (σ (ζ - 1)) (τ (ζ - 1))
-- Init.MetaTypes
Lean.Meta.EtaStructMode.noConfusionType : Sort v✝ → Lean.Meta.EtaStructMode → Lean.Meta.EtaStructMode → Sort v✝
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
/-- The small affine étale site: The category of affine schemes étale over `S`, whose objects are
commutative rings `R` with an étale structure morphism `Spec R ⟶ S`.  -/
AlgebraicGeometry.Scheme.AffineEtale : AlgebraicGeometry.Scheme → Type (u + 1)
-- Lean.Attributes
Lean.instInhabitedTagAttribute : Inhabited Lean.TagAttribute
-- Mathlib.LinearAlgebra.Multilinear.Finsupp
MultilinearMap.freeFinsuppEquiv_apply : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {κ : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : Fintype ι]
  [inst_2 : CommSemiring R] [inst_3 : DecidableEq R] [inst_4 : DecidableEq ι'] [inst_5 : (i : ι) → Fintype (κ i)]
  [inst_6 : (i : ι) → DecidableEq (κ i)] [inst_7 : Fintype ι'] (f : ((i : ι) → κ i) × ι' →₀ R) (x : (i : ι) → κ i →₀ R),
  (MultilinearMap.freeFinsuppEquiv f) x = ∑ p, f p • fun₀ | p.2 => ∏ i, (x i) (p.1 i)
-- Mathlib.CategoryTheory.Yoneda
/-- If `C` is a category with `[Category.{max w v₁} C]`, this is the isomorphism
`uliftCoyoneda.{w} (C := C) ≅ coyoneda`.  -/
CategoryTheory.uliftCoyonedaIsoCoyoneda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{max w v₁, u₁} C] →
    CategoryTheory.uliftCoyoneda.{w, max v₁ w, u₁} ≅ CategoryTheory.coyoneda
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {a : α}, t.isEmpty = true → Std.DTreeMap.Const.get! t a = default
-- Mathlib.Algebra.Group.End
Equiv.Perm.permGroup : {α : Type u_4} → Group (Equiv.Perm α)
-- Mathlib.Algebra.Category.Grp.Limits
/-- The category of groups has all limits.  -/
GrpCat.hasLimitsOfSize : ∀ [UnivLE.{v, u}], CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} GrpCat
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.Strand.mk.inj : ∀ {hPos : ℕ} {startPoint endPoint : Mathlib.Tactic.Widget.StringDiagram.Node}
  {atom₁ : Mathlib.Tactic.BicategoryLike.Atom₁} {hPos_1 : ℕ}
  {startPoint_1 endPoint_1 : Mathlib.Tactic.Widget.StringDiagram.Node} {atom₁_1 : Mathlib.Tactic.BicategoryLike.Atom₁},
  { hPos := hPos, startPoint := startPoint, endPoint := endPoint, atom₁ := atom₁ } =
      { hPos := hPos_1, startPoint := startPoint_1, endPoint := endPoint_1, atom₁ := atom₁_1 } →
    hPos = hPos_1 ∧ startPoint = startPoint_1 ∧ endPoint = endPoint_1 ∧ atom₁ = atom₁_1
-- Mathlib.RingTheory.Ideal.Maps
Ideal.comap_radical : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : FunLike F R S]
  [rc : RingHomClass F R S] (f : F) (K : Ideal S), Ideal.comap f K.radical = (Ideal.comap f K).radical
-- Init.Data.Dyadic.Basic
Int.trailingZeros.aux.eq_1 : ∀ (i : ℤ) (hi : i ≠ 0) (acc k_2 : ℕ) (x_1 : k_2 + 1 ≠ 0) (hk_2 : i.natAbs ≤ k_2 + 1),
  Int.trailingZeros.aux k_2.succ i hi hk_2 acc =
    if h : i % 2 = 0 then Int.trailingZeros.aux k_2 (i / 2) ⋯ ⋯ (acc + 1) else acc
-- Mathlib.RepresentationTheory.Invariants
/-- The average of all elements of the group `G`, considered as an element of `k[G]`.  -/
GroupAlgebra.average : (k : Type u_1) →
  (G : Type u_2) →
    [inst : CommSemiring k] → [Group G] → [inst_2 : Fintype G] → [Invertible ↑(Fintype.card G)] → MonoidAlgebra k G
-- Std.Do.WP.Sound
Std.Do.instWPSoundExceptTExceptPureOfLawfulMonad : ∀ {m : Type u_1 → Type u_2} {ε : Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Do.WP m Std.Do.PostShape.pure]
  [Std.Do.WPSound m Std.Do.PostShape.pure],
  Std.Do.WPSound (ExceptT ε m) (Std.Do.PostShape.except ε Std.Do.PostShape.pure)
-- Mathlib.CategoryTheory.Functor.KanExtension.Dense
CategoryTheory.Functor.isDense_iff_fullyFaithful_restrictedULiftYoneda : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Full],
  F.IsDense ↔ Nonempty (CategoryTheory.Presheaf.restrictedULiftYoneda F).FullyFaithful
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.snd_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β], ⇑ContinuousMap.snd = Prod.snd
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat_rat : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ}
  [ProbabilityTheory.IsFiniteKernel κ] (hf : ProbabilityTheory.IsRatCondKernelCDF f κ ν) (a : α) (q : ℚ) {s : Set β},
  MeasurableSet s →
    ∫⁻ (b : β) in s, ENNReal.ofReal (↑(ProbabilityTheory.stieltjesOfMeasurableRat f ⋯ (a, b)) ↑q) ∂ν a =
      (κ a) (s ×ˢ Set.Iic ↑q)
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.map_comap_le : ∀ {α : Type u_1} {β : Type u_3} (f : α → β) (m : MeasureTheory.OuterMeasure β),
  (MeasureTheory.OuterMeasure.map f) ((MeasureTheory.OuterMeasure.comap f) m) ≤ m
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_sub' : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f g : α → G},
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ → ∫ (a : α), (f - g) a ∂μ = ∫ (a : α), f a ∂μ - ∫ (a : α), g a ∂μ
-- Mathlib.Combinatorics.Matroid.Rank.ENat
/-- If `I` is a finite independent subset of `X` for which `M.eRk X ≤ M.eRk I`,
then `I` is a `Basis'` for `X`.  -/
Matroid.Indep.isBasis'_of_eRk_ge : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.Indep I → I.Finite → I ⊆ X → M.eRk X ≤ M.eRk I → M.IsBasis' I X
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rcc_ne_empty_iff : ∀ {m n : ℕ}, (m...=n).toArray ≠ #[] ↔ m ≤ n
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.lim_const : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] [inst_5 : CauSeq.IsComplete β abv] (x : β),
  (CauSeq.const abv x).lim = x
-- Init.Data.String.Basic
String.Slice.Pos.lt_next : ∀ {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.endPos}, pos < pos.next h
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_inj : ∀ {x y : ℝ}, -1 ≤ x → x ≤ 1 → -1 ≤ y → y ≤ 1 → (Real.arccos x = Real.arccos y ↔ x = y)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_eq' : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} [inst_1 : TopologicalSpace ι] [OrderTopology ι] [FirstCountableTopology ι]
  (hτ : MeasureTheory.IsStoppingTime f τ) (i : ι), MeasurableSet {ω | τ ω = ↑i}
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianReal_of_var_ne_zero : ∀ (μ : ℝ) {v : NNReal},
  v ≠ 0 → ProbabilityTheory.gaussianReal μ v = MeasureTheory.volume.withDensity (ProbabilityTheory.gaussianPDF μ v)
-- Mathlib.Algebra.Homology.QuasiIso
quasiIsoAt_comp : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L)
  (φ' : L ⟶ M) (i : ι) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [inst_4 : M.HasHomology i]
  [hφ : QuasiIsoAt φ i] [hφ' : QuasiIsoAt φ' i], QuasiIsoAt (CategoryTheory.CategoryStruct.comp φ φ') i
-- Mathlib.GroupTheory.Subgroup.Saturated
/-- **Alias** of `Submonoid.PowSaturated`.

---

A submonoid `H` of `G` is *saturated* if for all `n : ℕ` and `g : G` with `g^n ∈ H` we have
`n = 0` or `g ∈ H`. We use the name `PowSaturated` to distinguish from `Submonoid.MulSaturated`.  -/
Subgroup.Saturated : {G : Type u_1} → [inst : Monoid G] → Submonoid G → Prop
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.dual_symm_apply_toOrderHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : BoundedOrder α] [inst_2 : Preorder β]
  [inst_3 : BoundedOrder β] (f : BoundedOrderHom αᵒᵈ βᵒᵈ),
  (BoundedOrderHom.dual.symm f).toOrderHom = OrderHom.dual.symm f.toOrderHom
-- Mathlib.LinearAlgebra.Projection
LinearMap.IsIdempotentElem.comp_eq_left_iff : ∀ {S : Type u_5} [inst : Semiring S] {M : Type u_7} [inst_1 : AddCommGroup M] [inst_2 : Module S M] {q : M →ₗ[S] M},
  IsIdempotentElem q →
    ∀ {E : Type u_8} [inst_3 : AddCommGroup E] [inst_4 : Module S E] (p : M →ₗ[S] E), p ∘ₗ q = p ↔ q.ker ≤ p.ker
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `sub_le_self_iff`. -/
sub_le_self : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] (a : α) {b : α}, 0 ≤ b → a - b ≤ a
-- Mathlib.Order.SuccPred.Basic
WithBot.instPredOrder.eq_1 : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : (a : α) → Decidable (Order.pred a = a)],
  WithBot.instPredOrder =
    {
      pred := fun x =>
        match x with
        | none => ⊥
        | some a => if Order.pred a = a then ⊥ else ↑(Order.pred a),
      pred_le := ⋯, min_of_le_pred := ⋯, le_pred_of_lt := ⋯ }
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.AddConvolutionExistsAt.add_distrib : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [inst : AddMonoid M]
  [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : AddCommMonoid F]
  [inst_5 : Module S E] [inst_6 : Module S E'] [inst_7 : Module S F] [inst_8 : TopologicalSpace F] [T2Space F]
  [ContinuousAdd F] {f f' : M → E} {g : M → E'} {x : M} (L : E →ₗ[S] E' →ₗ[S] F),
  DiscreteConvolution.AddConvolutionExistsAt L f g x →
    DiscreteConvolution.AddConvolutionExistsAt L f' g x →
      DiscreteConvolution.addConvolution L (f + f') g x =
        DiscreteConvolution.addConvolution L f g x + DiscreteConvolution.addConvolution L f' g x
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.gcd_ndunion : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] [inst_2 : DecidableEq α]
  (s₁ s₂ : Multiset α), (s₁.ndunion s₂).gcd = gcd s₁.gcd s₂.gcd
-- Mathlib.Computability.MyhillNerode
Language.eq_1 : ∀ (α : Type u_4), Language α = Set (List α)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_whiskerLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C)
  {Z Z' : C} (f : Z ⟶ Z'),
  CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y f))
        (CategoryTheory.MonoidalCategoryStruct.associator X Y Z').inv)
-- Mathlib.LinearAlgebra.TensorProduct.Basis
Module.Basis.tensorProduct_apply : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [inst : CommSemiring R]
  [inst_1 : Semiring S] [inst_2 : Algebra R S] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M]
  [inst_6 : IsScalarTower R S M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] (b : Module.Basis ι S M)
  (c : Module.Basis κ R N) (i : ι) (j : κ), (b.tensorProduct c) (i, j) = b i ⊗ₜ[R] c j
-- Mathlib.Analysis.Normed.Module.RCLike.Real
interior_closedBall : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] (x : E) {r : ℝ},
  r ≠ 0 → interior (Metric.closedBall x r) = Metric.ball x r
-- Mathlib.Order.Category.CompleteLat
CompleteLat.dual_map : ∀ {x x_1 : CompleteLat} (a : CompleteLatticeHom ↑x ↑x_1), CompleteLat.dual.map a = CompleteLatticeHom.dual a
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get_get? : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {k : α} {h' : (m.get? k).isSome = true}, (m.get? k).get h' = m.get k ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.mapArrowLeft_left : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {f₁ f₁' : CategoryTheory.Arrow C₁}
  {f₃ : CategoryTheory.Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁'.hom f₃.hom)
  (sq : f₁' ⟶ f₁), (sq₁₃.mapArrowLeft sq₁₃' sq).left = (G.map (CategoryTheory.Arrow.Hom.right sq).op).app f₃.left
-- Mathlib.Topology.Constructions.SumProd
/-- If `Sum.elim f g` is an embedding, then so is `f`.  -/
Topology.IsEmbedding.sumElim_left : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z} {g : Y → Z}, Topology.IsEmbedding (Sum.elim f g) → Topology.IsEmbedding f
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.D₃.eq_1 : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : 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_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄] (j j' : ι₄),
  HomologicalComplex.mapBifunctor₁₂.D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' =
    HomologicalComplex.mapBifunctor.D₂ (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ j j'
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.containsThenInsert!_snd_eq_containsThenInsert_snd : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (t : Std.DTreeMap.Internal.Impl α β) (htb : t.Balanced) (a : α)
  (b : β a),
  (Std.DTreeMap.Internal.Impl.containsThenInsert! a b t).2 =
    (Std.DTreeMap.Internal.Impl.containsThenInsert a b t htb).2.impl
-- Mathlib.FieldTheory.SeparableDegree
IntermediateField.finSepDegree_bot : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E], Field.finSepDegree F ↥⊥ = 1
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.instInhabitedAuxLemmas : Inhabited Lean.Meta.AuxLemmas
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.instIsPartialOrderQ : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] [inst_1 : LE α] [inst_2 : Std.IsPartialOrder α]
  [inst_3 : Lean.Grind.OrderedAdd α], Std.IsPartialOrder (Lean.Grind.IntModule.OfNatModule.Q α)