mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.fac : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ) (i₀' i₀ i₁ i₂ i₃ i₃' : ι)
  (hi₀' : i₀' = data.i₀ r' pq' ⋯) (hi₀ : i₀ = data.i₀ r pq' ⋯) (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq')
  (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.fac._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.fac._auto_3),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.Fork.ι
        (CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kf X data r r' hrr' hr pq' pq'' i₀' i₀ i₁
          i₂ i₃ hi₀' hi₀ hi₁ hi₂ hi₃ n₀ n₁ n₂ hn₁' ⋯ ⋯))
      (CategoryTheory.Limits.Cofork.π
        (CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.cc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃
          i₃' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯)) =
    CategoryTheory.CategoryStruct.comp (X.mapFourδ₄Toδ₃' i₀' i₁ i₂ i₃ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯)
      (X.mapFourδ₁Toδ₀' i₀' i₀ i₁ i₂ i₃' ⋯ ⋯ ⋯ ⋯ n₀ n₁ n₂ ⋯ ⋯)
-- Mathlib.NumberTheory.Niven
/-- `tan(q * π)` for `q : ℚ` is algebraic over `ℤ`, using the complex `tan` function.  -/
Complex.isAlgebraic_tan_rat_mul_pi : ∀ (q : ℚ), IsAlgebraic ℤ (Complex.tan (↑q * ↑Real.pi))
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.subterminals_to_monoOver_terminal_comp_forget : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasTerminal C],
  (CategoryTheory.subterminalsEquivMonoOverTerminal C).functor.comp
      ((CategoryTheory.MonoOver.forget (⊤_ C)).comp (CategoryTheory.Over.forget (⊤_ C))) =
    CategoryTheory.subterminalInclusion C
-- Mathlib.Analysis.Calculus.Deriv.Basic
Filter.EventuallyEq.hasDerivWithinAt_iff_of_mem : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f₁ : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  f₁ =ᶠ[nhdsWithin x s] f → x ∈ s → (HasDerivWithinAt f₁ f' s x ↔ HasDerivWithinAt f f' s x)
-- Mathlib.Topology.Algebra.Monoid
Submonoid.top_closure_mul_self_subset : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [SeparatelyContinuousMul M] (s : Submonoid M),
  closure ↑s * closure ↑s ⊆ closure ↑s
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_addNat_Ioi_addNat : ∀ {n : ℕ} (m : ℕ) (i : Fin n), (fun x => x.addNat m) ⁻¹' Set.Ioi (i.addNat m) = Set.Ioi i
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.rotateR : ∀ {α : Type u_1} [inst : Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α},
  Ordnode.Valid' o₁ l ↑x →
    Ordnode.Valid' (↑x) r o₂ →
      ¬l.size + r.size ≤ 1 →
        Ordnode.delta * r.size < l.size →
          2 * l.size ≤ 9 * r.size + 5 ∨ l.size ≤ 3 → Ordnode.Valid' o₁ (l.rotateR x r) o₂
-- Mathlib.Data.Nat.Nth
Nat.count_eq_zero : ∀ {p : ℕ → Prop} [inst : DecidablePred p], (∃ n, p n) → ∀ {n : ℕ}, Nat.count p n = 0 ↔ n ≤ Nat.nth p 0
-- Mathlib.Algebra.Group.Submonoid.Membership
Nat.addSubmonoidClosure_one : AddSubmonoid.closure {1} = ⊤
-- Mathlib.AlgebraicGeometry.Scheme
/-- `f ⁻¹ᵁ U` is notation for `(Opens.map f.base).obj U`, the preimage of an open set `U` under `f`.
The preferred name in lemmas is `preimage` and it should be treated as an infix.  -/
AlgebraicGeometry.«term_⁻¹ᵁ_» : Lean.TrailingParserDescr
-- Mathlib.Topology.ContinuousMap.LocallyConstant
/-- The inclusion of locally-constant functions into continuous functions as an algebra map.  -/
LocallyConstant.toContinuousMapAlgHom : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (R : Type u_3) →
          [inst_2 : CommSemiring R] →
            [inst_3 : Semiring Y] →
              [inst_4 : Algebra R Y] → [inst_5 : IsTopologicalSemiring Y] → LocallyConstant X Y →ₐ[R] C(X, Y)
-- Init.Data.Int.Order
Int.le_of_sub_nonpos : ∀ {a b : ℤ}, a - b ≤ 0 → a ≤ b
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.subsingleton_of_subsingleton : ∀ {R : Type u_6} {M : Type u_8} {M' : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (S : Submonoid R) (g : M →ₗ[R] M') [IsLocalizedModule S g]
  [Subsingleton M], Subsingleton M'
-- Mathlib.RingTheory.PowerSeries.Inverse
/-- `firstUnitCoeff` is the non-zero coefficient whose index is `f.order`, seen as a unit of the
field. It is obtained using `divided_by_X_pow_order`, defined in `PowerSeries.Order`.  -/
PowerSeries.firstUnitCoeff : {k : Type u_2} → [inst : Field k] → {f : PowerSeries k} → f ≠ 0 → kˣ
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.CMExtension.eq_maximalRealSubfield : ∀ (K : Type u_2) [inst : Field K] [inst_1 : CharZero K] [Algebra.IsIntegral ℚ K] [NumberField.IsTotallyComplex K]
  (E : Subfield K) [NumberField.IsTotallyReal ↥E] [Algebra.IsQuadraticExtension (↥E) K],
  E = NumberField.maximalRealSubfield K
-- Mathlib.Order.Fin.Finset
Fin.orderIsoPair_one : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableEq α] (a b : α) (hab : a < b),
  ↑((Fin.orderIsoPair a b hab) 1) = b
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
MeasureTheory.Measure.toSphereBallBound.eq_1 : ∀ (n : ℕ) (ε : ℝ),
  MeasureTheory.Measure.toSphereBallBound n ε = if n ≠ 0 ∧ 0 < ε then ↑n * (min ε.toNNReal 2 / 4) ^ n else 1
-- Mathlib.RingTheory.Ideal.Operations
Ideal.prod_eq_iInf_of_pairwise_isCoprime : ∀ {R : Type u} {ι : Type u_1} [inst : CommSemiring R] {s : Finset ι} {J : ι → Ideal R},
  (↑s).Pairwise (Function.onFun IsCoprime J) → ∏ i ∈ s, J i = ⨅ i ∈ s, J i
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_Ico_add_right_sub_eq : ∀ {α : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] {f : α → M} [inst_1 : AddCommMonoid α]
  [inst_2 : PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α] [inst_5 : LocallyFiniteOrder α]
  [inst_6 : Sub α] [OrderedSub α] (a b c : α), ∑ x ∈ Finset.Ico (a + c) (b + c), f (x - c) = ∑ x ∈ Finset.Ico a b, f x
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.reverse_of : ∀ {α : Type u_1} (a : α), (FreeMonoid.of a).reverse = FreeMonoid.of a
-- Mathlib.Algebra.GroupWithZero.Units.Fintype
Fintype.card_units : ∀ (α : Type u_1) [inst : GroupWithZero α] [inst_1 : Fintype α] [inst_2 : DecidableEq α],
  Fintype.card αˣ = Fintype.card α - 1
-- Mathlib.Analysis.Normed.Ring.Basic
ULift.nonUnitalSeminormedRing : {α : Type u_2} → [NonUnitalSeminormedRing α] → NonUnitalSeminormedRing (ULift.{u_5, u_2} α)
-- Mathlib.Data.Complex.Basic
Complex.re_ofScientific : ∀ (m : ℕ) (s : Bool) (e : ℕ), Complex.re (OfScientific.ofScientific m s e) = OfScientific.ofScientific m s e
-- Mathlib.Topology.Order.OrderClosed
Dense.exists_le : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] [NoMinOrder α] {s : Set α},
  Dense s → ∀ (x : α), ∃ y ∈ s, y ≤ x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {a : α} {c : ℕ},
  (Std.DHashMap.Raw.emptyWithCapacity c).contains a = false
-- Std.Http.Data.URI.Basic
/-- User information (username and optional password).
 -/
Std.Http.URI.Builder.userInfo : Std.Http.URI.Builder → Option Std.Http.URI.UserInfo
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.mulEquivHaarChar_eq_one_of_compactSpace : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalGroup G] [inst_5 : LocallyCompactSpace G] [CompactSpace G] (φ : G ≃ₜ* G),
  MeasureTheory.mulEquivHaarChar φ = 1
-- Mathlib.Algebra.Order.BigOperators.Group.List
/-- If `l₁` is a sublist of `l₂` and all elements of `l₂` are nonnegative,
then `l₁.sum ≤ l₂.sum`.
One can prove a stronger version assuming `∀ a ∈ l₂.diff l₁, 0 ≤ a` instead of `∀ a ∈ l₂, 0 ≤ a`
but this lemma is not yet in `mathlib`.  -/
List.Sublist.sum_le_sum : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddRightMono M] [AddLeftMono M] {l₁ l₂ : List M},
  l₁.Sublist l₂ → (∀ a ∈ l₂, 0 ≤ a) → l₁.sum ≤ l₂.sum
-- Std.Time.Format.Basic
/-- A specification on how to format a data or parse some string.
 -/
Std.Time.GenericFormat : Std.Time.Awareness → Type
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.mk : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} [inst_1 : Fintype I] {e : I → R},
  OrthogonalIdempotents e → ∑ i, e i = 1 → CompleteOrthogonalIdempotents e
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.map_normalClosure : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (s : Set G) (f : G →+ N),
  Function.Surjective ⇑f → AddSubgroup.map f (AddSubgroup.normalClosure s) = AddSubgroup.normalClosure (⇑f '' s)
-- Init.Data.SInt.Lemmas
instLawfulCommIdentityInt16HMulOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 * x2) 1
-- Mathlib.Analysis.Normed.Group.Defs
enorm_eq_nnnorm : ∀ {E : Type u_8} [inst : NNNorm E] (x : E), ‖x‖ₑ = ↑‖x‖₊
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.normalizer_le_normalizer_sup_normal : ∀ {G : Type u_2} [inst : AddGroup G] {H K : AddSubgroup G} [hK : K.Normal],
  AddSubgroup.normalizer ↑H ≤ AddSubgroup.normalizer ↑(H ⊔ K)
-- Mathlib.Combinatorics.Additive.Energy
Finset.addEnergy_eq_zero_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Add α] {s t : Finset α}, s.addEnergy t = 0 ↔ s = ∅ ∨ t = ∅
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.processLevel : Lean.Level → Lean.Level → Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.lift_comp_inr : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddMonoid P]
  (f : M →+ P) (g : N →+ P), (AddMonoid.Coprod.lift f g).comp AddMonoid.Coprod.inr = g
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.isAcyclic_bot : ∀ {V : Type u_1}, ⊥.IsAcyclic
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.nextn : ∀ {l r : List Char} {it : String.Legacy.Iterator},
  String.Legacy.Iterator.ValidFor l r it →
    ∀ n ≤ r.length, String.Legacy.Iterator.ValidFor ((List.take n r).reverse ++ l) (List.drop n r) (it.nextn n)
-- Mathlib.Algebra.Order.Nonneg.Ring
Nonneg.isOrderedAddMonoid : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedAddMonoid α],
  IsOrderedAddMonoid { x // 0 ≤ x }
-- Mathlib.FieldTheory.Minpoly.MinpolyDiv
eval_minpolyDiv_of_aeval_eq_zero : ∀ {R : Type u_2} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S} [IsDomain S]
  [inst_4 : DecidableEq S] {y : S},
  (Polynomial.aeval y) (minpoly R x) = 0 →
    Polynomial.eval y (minpolyDiv R x) = if x = y then (Polynomial.aeval x) (Polynomial.derivative (minpoly R x)) else 0
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.insertMany_ind : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {ρ : Type w} [inst : ForIn Id ρ ((a : α) × β a)]
  [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {motive : Std.ExtDHashMap α β → Prop} (m : Std.ExtDHashMap α β)
  (l : ρ),
  motive m → (∀ (m : Std.ExtDHashMap α β) (a : α) (b : β a), motive m → motive (m.insert a b)) → motive (m.insertMany l)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.induction_on : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Monoid M] {motive : MonoidAlgebra R M → Prop}
  (x : MonoidAlgebra R M),
  (∀ (m : M), motive ((MonoidAlgebra.of R M) m)) →
    (∀ (x y : MonoidAlgebra R M), motive x → motive y → motive (x + y)) →
      (∀ (r : R) (x : MonoidAlgebra R M), motive x → motive (r • x)) → motive x
-- Mathlib.Algebra.Group.Action.Sum
Sum.instVAddCommClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} {β : Type u_4} [inst : VAdd M α] [inst_1 : VAdd M β] [inst_2 : VAdd N α]
  [inst_3 : VAdd N β] [VAddCommClass M N α] [VAddCommClass M N β], VAddCommClass M N (α ⊕ β)
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.coe_refl : ∀ {A : Type u_2} [inst : Mul A] [inst_1 : Star A], ⇑(StarMulEquiv.refl A) = id
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.le_of_le_of_eq : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {f g h : CauSeq α abs},
  f ≤ g → g ≈ h → f ≤ h
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.inv_top : ∀ {G : Type u_2} [inst : Group G], ⊤⁻¹ = ⊤
-- Mathlib.Data.ENNReal.Inv
ENNReal.half_le_self : ∀ {a : ENNReal}, a / 2 ≤ a
-- Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Unitary.mulRight_one : ∀ {R : Type u_1} {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : CStarRing A] [inst_3 : Ring R]
  [inst_4 : Module R A] [inst_5 : IsScalarTower R A A], Unitary.mulRight R 1 = LinearIsometryEquiv.refl R A
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.closure_sUnion : ∀ {R : Type u} [inst : NonAssocRing R] (s : Set (Set R)), Subring.closure (⋃₀ s) = ⨆ t ∈ s, Subring.closure t
-- Mathlib.CategoryTheory.Preadditive.Projective.Resolution
CategoryTheory.ProjectiveResolution.cokernelCofork.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} (P : CategoryTheory.ProjectiveResolution Z),
  P.cokernelCofork = CategoryTheory.Limits.CokernelCofork.ofπ (P.π.f 0) ⋯
-- Mathlib.Algebra.Ring.Equiv
/-- An equivalence between two (non-unital non-associative semi)rings that preserves the
algebraic structure.  -/
RingEquiv : (R : Type u_7) → (S : Type u_8) → [Mul R] → [Mul S] → [Add R] → [Add S] → Type (max u_7 u_8)
-- Mathlib.Algebra.CubicDiscriminant
Cubic.ne_zero_of_c_ne_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.c ≠ 0 → P.toPoly ≠ 0
-- Mathlib.Analysis.Normed.Group.Quotient
Submodule.Quotient.normedSpace : {M : Type u_1} →
  [inst : SeminormedAddCommGroup M] →
    {R : Type u_3} →
      [inst_1 : Ring R] →
        [inst_2 : Module R M] →
          (S : Submodule R M) →
            (𝕜 : Type u_4) →
              [inst_3 : NormedField 𝕜] →
                [inst_4 : NormedSpace 𝕜 M] → [inst_5 : SMul 𝕜 R] → [IsScalarTower 𝕜 R M] → NormedSpace 𝕜 (M ⧸ S)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.aecover_Ioo_of_Icc : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [OrderClosedTopology α] [OpensMeasurableSpace α] {a b : ι → α}
  {A B : α},
  Filter.Tendsto a l (nhds A) →
    Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Ioo A B)) l fun i => Set.Icc (a i) (b i)
-- Mathlib.Data.Set.Lattice
Set.iInter_iInter_eq_or_left : ∀ {α : Type u_1} {β : Type u_2} {b : β} {p : β → Prop} {s : (x : β) → x = b ∨ p x → Set α},
  ⋂ x, ⋂ (h : x = b ∨ p x), s x h = s b ⋯ ∩ ⋂ x, ⋂ (h : p x), s x ⋯
-- Mathlib.Algebra.Category.Grp.Colimits
AddCommGrpCat.Colimits.quotUliftToQuot_ι : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat)
  [inst_1 : DecidableEq J] (j : J) (x : ↑((F.comp AddCommGrpCat.uliftFunctor).obj j)),
  (AddCommGrpCat.Colimits.quotUliftToQuot F) ((AddCommGrpCat.Colimits.Quot.ι (F.comp AddCommGrpCat.uliftFunctor) j) x) =
    (AddCommGrpCat.Colimits.Quot.ι F j) x.down
-- Std.Http.Internal.Char
/-- Checks if a byte is a valid character in a URI userinfo component according to RFC 3986.
`userinfo = *( unreserved/ sub-delims / ":" )`

Note: It avoids the pct-encoded of the original grammar because it is used with `Encoding.lean`
that provides it.
 -/
Std.Http.Internal.Char.isUserInfoChar : UInt8 → Bool
-- Mathlib.Topology.Instances.NNReal.Lemmas
ENNReal.iSup₂_pow_of_ne_zero : ∀ {ι : Sort u_1} {κ : ι → Sort u_2} (f : (i : ι) → κ i → ENNReal) {n : ℕ},
  n ≠ 0 → (⨆ i, ⨆ j, f i j) ^ n = ⨆ i, ⨆ j, f i j ^ n
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RicSliceData.treeMap : {α : Type u} →
  {β : Type v} → [inst : Ord α] → Std.DTreeMap.Internal.Const.RicSliceData α β → Std.DTreeMap.Internal.Impl α fun x => β
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrixₛₗ₂'_apply : ∀ {R : Type u_1} {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_10} {n : Type u_11}
  {m : Type u_12} [inst : CommSemiring R] [inst_1 : AddCommMonoid N₂] [inst_2 : Module R N₂] [inst_3 : Semiring R₁]
  [inst_4 : Semiring R₂] [inst_5 : Semiring S₁] [inst_6 : Semiring S₂] [inst_7 : Module S₁ N₂] [inst_8 : Module S₂ N₂]
  [inst_9 : SMulCommClass S₁ R N₂] [inst_10 : SMulCommClass S₂ R N₂] [inst_11 : SMulCommClass S₂ S₁ N₂] (σ₁ : R₁ →+* S₁)
  (σ₂ : R₂ →+* S₂) [inst_12 : Fintype n] [inst_13 : Fintype m] [inst_14 : DecidableEq n] [inst_15 : DecidableEq m]
  (B : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) (i : n) (j : m),
  (LinearMap.toMatrixₛₗ₂' R) B i j = (B (Pi.single i 1)) (Pi.single j 1)
-- Mathlib.Topology.Algebra.Monoid
/-- **Alias** of `continuous_const_add`. -/
continuous_add_left : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M] (m : M),
  Continuous fun x => m + x
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit
SSet.functorN_map : ∀ (X : SSet) {X_1 Y : X.N} (f : X_1 ⟶ Y), X.functorN.map f = SSet.Subcomplex.toSSetFunctor.map (⋯.functor.map f)
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
instBracketGroupLieAlgebra.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Group G],
  instBracketGroupLieAlgebra =
    { bracket := fun v w => VectorField.mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1 }
-- Lean.Data.Iterators.Producers.PersistentHashMap
/-- Returns a finite iterator over the key-value pairs of the given `PersistentHashMap`.
The iteration order is unspecified.

**Termination properties:**

* `Finite` instance: always
* `Productive` instance: always
 -/
Lean.PersistentHashMap.iter : {α : Type u_1} → {β : Type u_2} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PersistentHashMap α β → Std.Iter (α × β)
-- Mathlib.LinearAlgebra.Prod
LinearEquiv.coe_prodCongr : ∀ {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₄] {module_M : Module R M}
  {module_M₂ : Module R M₂} {module_M₃ : Module R M₃} {module_M₄ : Module R M₄} (e₁ : M ≃ₗ[R] M₂) (e₂ : M₃ ≃ₗ[R] M₄),
  ↑(e₁.prodCongr e₂) = (↑e₁).prodMap ↑e₂
-- Mathlib.Data.Finset.Lattice.Fold
Finset.codisjoint_inf_left : ∀ {α : Type u_2} {ι : Type u_5} [inst : DistribLattice α] [inst_1 : OrderTop α] {s : Finset ι} {f : ι → α} {a : α},
  Codisjoint (s.inf f) a ↔ ∀ ⦃i : ι⦄, i ∈ s → Codisjoint (f i) a
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.endsWith_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String},
  s.toSlice.endsWith pat = s.endsWith pat
-- Mathlib.GroupTheory.Divisible
RootableBy.root_cancel : ∀ {A : Type u_1} {α : Type u_2} {inst : Monoid A} {inst_1 : Pow A α} {inst_2 : Zero α} [self : RootableBy A α] {n : α}
  (a : A), n ≠ 0 → RootableBy.root a n ^ n = a
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
/-- For a reflexive module `M`, an equivalence `N ≃ₗ[R] Dual R M` naturally yields an equivalence
`M ≃ₗ[R] Dual R N`. Such equivalences are known as perfect pairings.  -/
LinearEquiv.flip : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommGroup N] →
              [inst_4 : Module R N] → [Module.IsReflexive R M] → (N ≃ₗ[R] Module.Dual R M) → M ≃ₗ[R] Module.Dual R N
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.monomial_eq_monomial_iff : ∀ {R : Type u_1} [inst : Semiring R] {m n : ℕ} {a b : R},
  (SkewPolynomial.monomial m) a = (SkewPolynomial.monomial n) b ↔ m = n ∧ a = b ∨ a = 0 ∧ b = 0
-- Mathlib.Order.Monotone.Basic
StrictMonoOn.injOn : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictMonoOn f s → Set.InjOn f s
-- Mathlib.Analysis.Normed.Module.Ray
/-- Two nonzero vectors `x y` in a real normed space are on the same ray if and only if the unit
vectors `‖x‖⁻¹ • x` and `‖y‖⁻¹ • y` are equal.  -/
sameRay_iff_inv_norm_smul_eq_of_ne : ∀ {F : Type u_2} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {x y : F},
  x ≠ 0 → y ≠ 0 → (SameRay ℝ x y ↔ ‖x‖⁻¹ • x = ‖y‖⁻¹ • y)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.Proj.map_id : ∀ {A σ : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜],
  AlgebraicGeometry.Proj.map (GradedRingHom.id 𝒜) ⋯ = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Proj 𝒜)
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
Filter.principal_isMeasurablyGenerated_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α}, (Filter.principal s).IsMeasurablyGenerated ↔ MeasurableSet s
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT : ∀ (N : Type u_2) [inst : Add N] [IsLeftCancelAdd N] [inst_2 : PartialOrder N] [AddLeftReflectLT N], AddLeftReflectLE N
-- Init.Data.Sum.Lemmas
Sum.getLeft?_swap : ∀ {α : Type u_1} {β : Type u_2} (x : α ⊕ β), x.swap.getLeft? = x.getRight?
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.instMonoIntι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n₁ : ℤ) [CategoryTheory.Mono f],
  CategoryTheory.Mono (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁.ι✝ f n₁)
-- Mathlib.Algebra.Order.Nonneg.Lattice
Nonneg.instDenselyOrdered : ∀ {α : Type u_1} [inst : Preorder α] [DenselyOrdered α] {a : α}, DenselyOrdered { x // a ≤ x }
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
/-- Summation over a finite set of terms in Presburger arithmetic.

It is defined via choice, so the result only makes sense when the structure satisfies
commutativity (see `realize_sum`).  -/
FirstOrder.Language.presburger.sum : {α : Type u_1} →
  {β : Type u_2} → Finset β → (β → FirstOrder.Language.presburger.Term α) → FirstOrder.Language.presburger.Term α
-- Lean.Parser.Term
Lean.Parser.Term.waitIfContainsMVar.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- The function `Complex.cosh` is complex analytic.  -/
Complex.analyticOn_cosh : ∀ {s : Set ℂ}, AnalyticOn ℂ Complex.cosh s
-- Mathlib.Data.Num.Lemmas
Num.bit.eq_1 : ∀ (b : Bool), Num.bit b = bif b then Num.bit1 else Num.bit0
-- Init.Data.Option.Attach
Option.attach_map_val : ∀ {α : Type u_1} {β : Type u_2} (o : Option α) (f : α → β), Option.map (fun i => f ↑i) o.attach = Option.map f o
-- Init.Core
iff_true_left : ∀ {a b : Prop}, a → ((a ↔ b) ↔ b)