mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ModelCategory.Injective
/-- The weak equivalences in the category `CochainComplex.Plus C` of bounded
below cochain complexes are quasi-isomorphisms.  -/
CochainComplex.Plus.modelCategoryQuillen.instCategoryWithWeakEquivalences : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → HomotopicalAlgebra.CategoryWithWeakEquivalences (CochainComplex.Plus C)
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.ctor.inj : ∀ {a : Lean.Name} {a_1 : List Lean.Meta.Match.Example} {a_2 : Lean.Name} {a_3 : List Lean.Meta.Match.Example},
  Lean.Meta.Match.Example.ctor a a_1 = Lean.Meta.Match.Example.ctor a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_bot : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F), AddSubmonoid.map f ⊥ = ⊥
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Define a `NormalizedGCDMonoid` structure on a monoid just from the existence of a `gcd`.  -/
normalizedGCDMonoidOfExistsGCD : {α : Type u_1} →
  [inst : CommMonoidWithZero α] →
    [IsCancelMulZero α] →
      [NormalizationMonoid α] →
        [DecidableEq α] → (∀ (a b : α), ∃ c, ∀ (d : α), d ∣ a ∧ d ∣ b ↔ d ∣ c) → NormalizedGCDMonoid α
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.zero : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → {module_M : Module R M} → (p : Submodule R M) → Zero ↥p
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Predicate for a monoid object to be commutative.  -/
CategoryTheory.IsCommMonObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → (X : C) → [CategoryTheory.MonObj X] → Prop
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.valuation_eq_zero_iff : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] {x : R}, (ValuativeRel.valuation R) x = 0 ↔ x ≤ᵥ 0
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.inv_mem_units : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) {x : Mˣ}, x ∈ S.units → x⁻¹ ∈ S.units
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.involutiveInv.eq_1 : ∀ {G : Type u_2} [inst : Group G], Submonoid.involutiveInv = Function.Injective.involutiveInv SetLike.coe ⋯ ⋯
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
/-- A version of `cfcₙ_apply` in terms of `ContinuousMapZero.mkD`  -/
cfcₙ_apply_mkD : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (f : R → R) (a : A)
  (ha : autoParam (p a) _auto_173✝),
  cfcₙ f a = (cfcₙHom ha) (ContinuousMapZero.mkD ((quasispectrum R a).domRestrict f) 0)
-- Mathlib.Data.Fintype.Basic
Fin.eq_iff_eq_zero_iff : ∀ (a b : Fin 2), a = b ↔ (a = 0 ↔ b = 0)
-- Init.Data.UInt.Lemmas
UInt64.toNat_ofNat_of_lt' : ∀ {n : ℕ}, n < UInt64.size → (UInt64.ofNat n).toNat = n
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
/-- The embedding from the existing vector space  -/
CliffordAlgebra.EquivEven.v : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → (Q : QuadraticForm R M) → M →ₗ[R] CliffordAlgebra (CliffordAlgebra.EquivEven.Q' Q)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLT!_eq_get!_getEntryLT? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k : α}
  [inst_1 : Inhabited ((a : α) × β a)],
  Std.DTreeMap.Internal.Impl.getEntryLT! k t = (Std.DTreeMap.Internal.Impl.getEntryLT? k t).get!
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- `G.IndepSetFreeOn s n` means that `G` has no `n`-independent sets contained in `s`.  -/
SimpleGraph.IndepSetFreeOn : {α : Type u_1} → SimpleGraph α → Set α → ℕ → Prop
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
/-- If `M → M'` is injective, then the set of associated primes of `M` is
contained in that of `M'`.  -/
associatedPrimes.subset_of_injective : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_3}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] {f : M →ₗ[R] M'},
  Function.Injective ⇑f → associatedPrimes R M ⊆ associatedPrimes R M'
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max!_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  t ≠ ∅ → ∀ {k : α}, (cmp t.max! k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_sub_Icc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => a - x) '' Set.Icc b c = Set.Icc (a - c) (a - b)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {f : α → β → Bool} {k : α},
  Std.ExtDHashMap.Const.get! (Std.ExtDHashMap.filter f m) k =
    ((Std.ExtDHashMap.Const.get? m k).pfilter fun x_2 h' => f (m.getKey k ⋯) x_2).get!
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Ioo.lt_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] (x : ↑(Set.Ioo 0 1)), ↑x < 1
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.mem_comap : ∀ {F : Type w} {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] {s : NonUnitalSubring S} {f : F} {x : R},
  x ∈ NonUnitalSubring.comap f s ↔ f x ∈ s
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
_private.Init.Data.Iterators.Lemmas.Combinators.FlatMap.0.Std.Iter.step_flatMapAfterM.match_5.eq_1 : ∀ {α₂ γ : Type u_1} {m : Type u_1 → Type u_2} (motive : Option (Std.IterM m γ) → Sort u_3)
  (h_1 : none = none → motive none) (h_2 : (it₂ : Std.IterM m γ) → none = some it₂ → motive (some it₂)),
  (match hit : none with
    | none => h_1 hit
    | some it₂ => h_2 it₂ hit) =
    h_1 ⋯
-- Mathlib.CategoryTheory.Limits.Connected
CategoryTheory.widePullbackShape_connected : ∀ (J : Type v₁), CategoryTheory.IsConnected (CategoryTheory.Limits.WidePullbackShape J)
-- Std.Http.Data.Status
Std.Http.Status.other.injEq : ∀ (status status_1 : Std.Http.CustomStatus),
  (Std.Http.Status.other status = Std.Http.Status.other status_1) = (status = status_1)
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.single_order_mul_powerSeriesPart : ∀ {R : Type u_1} [inst : Semiring R] (x : LaurentSeries R),
  (HahnSeries.single (HahnSeries.order x)) 1 * (HahnSeries.ofPowerSeries ℤ R) x.powerSeriesPart = x
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.instAdditiveRepCochainComplexModuleCatNatCochainsFunctor : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Group G], (groupCohomology.cochainsFunctor k G).Additive
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.mk.inj : ∀ {α : Type u} {β : Type v} {cmp : autoParam (α → α → Ordering) Std.ExtTreeMap._auto_1}
  {inner inner_1 : Std.ExtDTreeMap α (fun x => β) cmp}, { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.measurableSingletonClass_of_countablySeparated : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSpace.CountablySeparated α], MeasurableSingletonClass α
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.map_eq_zero : ∀ {σ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : DivisionSemiring R] [inst_1 : Semiring S] [Nontrivial S]
  (φ : MvPowerSeries σ R) (f : R →+* S), (MvPowerSeries.map f) φ = 0 ↔ φ = 0
-- Mathlib.Logic.Unique
Unique.subtypeEq : {α : Sort u_1} → (y : α) → Unique { x // x = y }
-- Batteries.Linter.UnreachableTactic
/-- Search for tactic executions in the info tree and remove executed tactic syntaxes.  -/
Batteries.Linter.UnreachableTactic.eraseUsedTacticsList : Lean.PersistentArray Lean.Elab.InfoTree → Batteries.Linter.UnreachableTactic.M Unit
-- Mathlib.Algebra.Order.Round
round_sub_one : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (a : α),
  round (a - 1) = round a - 1
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.pi_symm : ∀ {ι : Type u_5} {αi : ι → Type u_6} {βi : ι → Type u_7} (ei : (i : ι) → PartialEquiv (αi i) (βi i)),
  (PartialEquiv.pi ei).symm = PartialEquiv.pi fun i => (ei i).symm
-- Mathlib.SetTheory.Ordinal.Notation
ONote.decidableTopBelow : DecidableRel ONote.TopBelow
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.ExSum.brecOn.eq : ∀ {u : Lean.Level} {α : Q(Type u)} {BaseType : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)}
  {motive_1 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExBase BaseType sα e → Sort u}
  {motive_2 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExProd BaseType sα e → Sort u}
  {motive_3 : (e : Q(«$α»)) → Mathlib.Tactic.Ring.Common.ExSum BaseType sα e → Sort u} {e : Q(«$α»)}
  (t : Mathlib.Tactic.Ring.Common.ExSum BaseType sα e)
  (F_1 : (e : Q(«$α»)) → (t : Mathlib.Tactic.Ring.Common.ExBase BaseType sα e) → t.below → motive_1 e t)
  (F_2 : (e : Q(«$α»)) → (t : Mathlib.Tactic.Ring.Common.ExProd BaseType sα e) → t.below → motive_2 e t)
  (F_3 : (e : Q(«$α»)) → (t : Mathlib.Tactic.Ring.Common.ExSum BaseType sα e) → t.below → motive_3 e t),
  t.brecOn F_1 F_2 F_3 = F_3 e t (Mathlib.Tactic.Ring.Common.ExSum.brecOn.go t F_1 F_2 F_3).2
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.exists_eigenvalues_eq : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n) {μ : 𝕜},
  Module.End.HasEigenvalue T μ → ∃ i, ↑(hT.eigenvalues hn i) = μ
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
/-- A functor `F : J ⥤ C` is eventually constant from `i : J` if
for any map `f : i ⟶ j`, the induced morphism `F.map f` is an isomorphism.
If `J` is filtered, this implies `F` has a colimit.  -/
CategoryTheory.Functor.IsEventuallyConstantFrom : {J : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] → CategoryTheory.Functor J C → J → Prop
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_le : ∀ {a b : UInt32}, a.toUInt64 ≤ b.toUInt64 ↔ a ≤ b
-- Mathlib.Data.Setoid.Basic
Setoid.sInf_equiv : ∀ {α : Type u_1} {S : Set (Setoid α)} {x y : α}, x ≈ y ↔ ∀ s ∈ S, s x y
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.lanAdjunction_counit_app : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasLeftKanExtension F]
  (G : CategoryTheory.Functor D H),
  (L.lanAdjunction H).counit.app G =
    (L.lan.obj (L.comp G)).descOfIsLeftKanExtension (L.lanUnit.app (L.comp G)) G
      (CategoryTheory.CategoryStruct.id (L.comp G))
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.instBEqAltParamInfo : BEq Lean.Meta.Match.AltParamInfo
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.val_add : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R) (x y : ↥s), ↑(x + y) = ↑x + ↑y
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.PollSources.requestBody : {α β : Type} → Std.Http.Server.Connection.PollSources✝ α β → Option Std.Http.Body.Stream
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.FunctorObjIndex.comm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)]
  (x : CategoryTheory.SmallObject.FunctorObjIndex f πX),
  CategoryTheory.CategoryStruct.comp (f x.i)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.Sigma.ι (CategoryTheory.SmallObject.functorObjTgtFamily f πX) x)
        (CategoryTheory.SmallObject.ρFunctorObj f πX)) =
    CategoryTheory.CategoryStruct.comp x.t (CategoryTheory.SmallObject.ιFunctorObj f πX)
-- Mathlib.FieldTheory.Laurent
RatFunc.laurent_algebraMap : ∀ {R : Type u} [inst : CommRing R] (r : R) (p : Polynomial R) [inst_1 : IsDomain R],
  (RatFunc.laurent r) ((algebraMap (Polynomial R) (RatFunc R)) p) =
    (algebraMap (Polynomial R) (RatFunc R)) ((Polynomial.taylor r) p)
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.basisFun_apply : ∀ (ι : Type u_1) (𝕜 : Type u_3) [inst : RCLike 𝕜] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i : ι),
  (EuclideanSpace.basisFun ι 𝕜) i = EuclideanSpace.single i 1
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_div_nonpos : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : LinearOrder G₀] {a : G₀} [PosMulMono G₀], 1 / a ≤ 0 ↔ a ≤ 0
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isSome_min?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.insert k).min?.isSome = true
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.of_ker_isNilpotent : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] (f : R →+* S) {I : Type u_3} [inst_2 : Fintype I]
  {e : I → R},
  (∀ x ∈ RingHom.ker f, IsNilpotent x) →
    (∀ (i : I), IsIdempotentElem (e i)) → CompleteOrthogonalIdempotents (⇑f ∘ e) → CompleteOrthogonalIdempotents e
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.cyclesIso₀_comp_H0π_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : groupHomology.H0 A ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupHomology.cyclesIso₀ A).hom
      (CategoryTheory.CategoryStruct.comp (groupHomology.H0π A) h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.π A 0) h
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- In the canonical isometric isomorphism between a Hilbert sum `E` of `G : ι → Type*` and
`lp G 2`, a finitely-supported vector in `lp G 2` is the image of the associated finite sum of
elements of `E`.  -/
IsHilbertSum.linearIsometryEquiv_apply_dfinsupp_sum_single : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {G : ι → Type u_4} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_5 : CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E}
  [inst_6 : DecidableEq ι] [inst_7 : (i : ι) → DecidableEq (G i)] (hV : IsHilbertSum 𝕜 G V) (W₀ : Π₀ (i : ι), G i),
  ↑(W₀.sum fun a b => hV.linearIsometryEquiv ((V a) b)) = ⇑W₀
-- Mathlib.Data.Part
Part.mem_toOption : ∀ {α : Type u_1} {o : Part α} [inst : Decidable o.Dom] {a : α}, a ∈ o.toOption ↔ a ∈ o
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toMeasure_apply : ∀ {α : Type u_1} [inst : MeasurableSpace α] (p : PMF α) {s : Set α},
  MeasurableSet s → p.toMeasure s = ∑' (x : α), s.indicator (⇑p) x
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.eq_generate : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → l = Filter.generate {U | ∃ i, p i ∧ s i = U}
-- Lean.Meta.LitValues
/-- Return `some n` if `e` is a raw natural number or an `OfNat.ofNat`-application encoding `n`.  -/
Lean.Meta.getNatValue? : Lean.Expr → Lean.MetaM (Option ℕ)
-- Mathlib.NumberTheory.Bertrand
/-- An upper bound on the central binomial coefficient used in the proof of Bertrand's postulate.
The bound splits the prime factors of `centralBinom n` into those
1. At most `sqrt (2 * n)`, which contribute at most `2 * n` for each such prime.
2. Between `sqrt (2 * n)` and `2 * n / 3`, which contribute at most `4^(2 * n / 3)` in total.
3. Between `2 * n / 3` and `n`, which do not exist.
4. Between `n` and `2 * n`, which would not exist in the case where Bertrand's postulate is false.
5. Above `2 * n`, which do not exist.
 -/
centralBinom_le_of_no_bertrand_prime : ∀ (n : ℕ),
  2 < n → (∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p) → n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.AbelMode.noConfusionType : Sort v✝ → Mathlib.Tactic.Abel.AbelMode → Mathlib.Tactic.Abel.AbelMode → Sort v✝
-- Batteries.Lean.LawfulMonadLift
_private.Batteries.Lean.LawfulMonadLift.0.EST.bind.match_1.eq_1 : ∀ {ε σ α : Type} (motive : EST.Out ε σ α → Sort u_1) (a : α) (s : Void σ)
  (h_1 : (a : α) → (s : Void σ) → motive (EST.Out.ok a s)) (h_2 : (e : ε) → (s : Void σ) → motive (EST.Out.error e s)),
  (match EST.Out.ok a s with
    | EST.Out.ok a s => h_1 a s
    | EST.Out.error e s => h_2 e s) =
    h_1 a s
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
AlgebraicGeometry.ValuativeCriterion.eq : AlgebraicGeometry.ValuativeCriterion =
  AlgebraicGeometry.ValuativeCriterion.Existence ⊓ AlgebraicGeometry.ValuativeCriterion.Uniqueness
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_eq_getD_getKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {a fallback : α}, t.getKeyD a fallback = (t.getKey? a).getD fallback
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions
_private.Mathlib.Analysis.InnerProductSpace.Harmonic.Constructions.0.analyticAt_harmonicAt_log_normSq : ∀ {z : ℂ} {g : ℂ → ℂ},
  AnalyticAt ℂ g z → g z ≠ 0 → g z ∈ Complex.slitPlane → InnerProductSpace.HarmonicAt (Real.log ∘ ⇑Complex.normSq ∘ g) z
-- Mathlib.Algebra.Algebra.Subalgebra.Pointwise
Subalgebra.mul_toSubmodule_le : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S T : Subalgebra R A), Subalgebra.toSubmodule S * Subalgebra.toSubmodule T ≤ Subalgebra.toSubmodule (S ⊔ T)
-- Mathlib.Order.Hom.Lattice
InfHom.instSemilatticeInf : {α : Type u_2} → {β : Type u_3} → [inst : Min α] → [inst_1 : SemilatticeInf β] → SemilatticeInf (InfHom α β)
-- Mathlib.Order.OmegaCompletePartialOrder
/-- **Alias** of the forward direction of `OmegaCompletePartialOrder.ωScottContinuous_iff_monotone_map_ωSup`.

---

`ωScottContinuous f` asserts that `f` is both monotone and distributes over ωSup.  -/
OmegaCompletePartialOrder.ωScottContinuous.monotone_map_ωSup : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β] {f : α → β},
  OmegaCompletePartialOrder.ωScottContinuous f →
    ∃ (hf : Monotone f),
      ∀ (c : OmegaCompletePartialOrder.Chain α),
        f (OmegaCompletePartialOrder.ωSup c) = OmegaCompletePartialOrder.ωSup (c.map { toFun := f, monotone' := hf })
-- Mathlib.RingTheory.Idempotents
/-- Orthogonal idempotents lift along nil ideals.  -/
exists_isIdempotentElem_mul_eq_zero_of_ker_isNilpotent : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S),
  (∀ x ∈ RingHom.ker f, IsNilpotent x) →
    ∀ e₁ ∈ f.range,
      IsIdempotentElem e₁ →
        ∀ (e₂ : R),
          IsIdempotentElem e₂ →
            e₁ * f e₂ = 0 → f e₂ * e₁ = 0 → ∃ e', IsIdempotentElem e' ∧ f e' = e₁ ∧ e' * e₂ = 0 ∧ e₂ * e' = 0
-- Mathlib.Condensed.Light.Basic
LightCondensed.hom_ext_iff : ∀ {C : Type w} [inst : CategoryTheory.Category.{v, w} C] {X Y : LightCondensed C} {f g : X ⟶ Y},
  f = g ↔ ∀ (S : LightProfiniteᵒᵖ), f.hom.app S = g.hom.app S
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.tendsto_approx_atTop : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P) (x : X),
  Filter.Tendsto (fun n => Urysohns.CU.approx n c x) Filter.atTop (nhds (c.lim x))
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instBraidedMonMapMon.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : CategoryTheory.SymmetricCategory C]
  [inst_5 : CategoryTheory.SymmetricCategory D] [inst_6 : F.Braided],
  CategoryTheory.Functor.instBraidedMonMapMon = { toMonoidal := F.instMonoidalMonMapMon, braided := ⋯ }
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
cbiSup_eq_of_forall_not : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderSup α] {p : ι → Prop} {f : (i : ι) → p i → α},
  (∀ (i : ι), ¬p i) → ⨆ i, ⨆ (h : p i), f i h = sSup ∅
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.coxeterWeightIn_eq_four_iff_not_linearIndependent : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  {i j : ι} [Finite ι] [CharZero R] [IsDomain R] [Module.IsTorsionFree R M] [inst_9 : CommRing S]
  [inst_10 : Algebra S R] [FaithfulSMul S R] [inst_12 : P.IsValuedIn S],
  P.coxeterWeightIn S i j = 4 ↔ ¬LinearIndependent R ![P.root i, P.root j]
-- Mathlib.Algebra.Vertex.VertexOperator
VertexOperator.ncoeff_eq_zero_of_lt_order : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (A : VertexOperator R V) (n : ℤ) (x : V),
  -n - 1 < ((HahnModule.of R).symm (A x)).order → (VertexOperator.ncoeff A n) x = 0
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the right whiskering `η ▷ h` with `η : f ⟶ g`.  -/
Mathlib.Tactic.BicategoryLike.Mor₂.whiskerRight : Lean.Expr →
  Option Mathlib.Tactic.BicategoryLike.IsoLift →
    Mathlib.Tactic.BicategoryLike.Mor₁ →
      Mathlib.Tactic.BicategoryLike.Mor₁ →
        Mathlib.Tactic.BicategoryLike.Mor₂ → Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂
-- Mathlib.RingTheory.Ideal.Quotient.PowTransition
Submodule.eq_factor_of_eq_factor_succ : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : ℕ → Submodule R M}
  (hp : Antitone p) (x : (n : ℕ) → M ⧸ p n),
  (∀ (m : ℕ), x m = (Submodule.factor ⋯) (x (m + 1))) → ∀ {m n : ℕ} (g : m ≤ n), x m = (Submodule.factor ⋯) (x n)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.mapIso_inv_π : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.mapIso p).inv (CategoryTheory.Limits.Pi.π f b) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π g b) (p b).inv
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapIso_hom : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (e : G ≃* H) (e' : ↑A ≃ₗ[k] ↑B) (he : ∀ (g : G), ↑e' ∘ₗ A.ρ g = B.ρ (e g) ∘ₗ ↑e') (n : ℕ),
  (groupHomology.mapIso e e' he n).hom =
    groupHomology.map (↑e) (Rep.ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }) n
-- Mathlib.Analysis.RCLike.Basic
/-- The imaginary part in an `RCLike` field, as a linear map.  -/
RCLike.imLm : {K : Type u_1} → [inst : RCLike K] → K →ₗ[ℝ] ℝ