mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.comon : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → (self : CategoryTheory.Comon C) → CategoryTheory.ComonObj self.X
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.buildTable : (pat : String.Slice) → Vector ℕ pat.utf8ByteSize
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ActionToRep_map : ∀ (k : Type u) (G : Type v) [inst : Ring k] [inst_1 : Monoid G] {X Y : Action (ModuleCat k) G} (f : X ⟶ Y),
  (Rep.ActionToRep k G).map f = Rep.ofHom { toLinearMap := ModuleCat.Hom.hom f.hom, isIntertwining' := ⋯ }
-- Mathlib.CategoryTheory.GuitartExact.KanExtension
CategoryTheory.TwoSquare.hasPointwiseLeftKanExtension_iff : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} {D : Type u₅} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] [inst_4 : CategoryTheory.Category.{v₅, u₅} D]
  {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃} {R : CategoryTheory.Functor C₂ C₄}
  {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B) [w.GuitartExact] [B.EssSurj]
  (F : CategoryTheory.Functor C₂ D), L.HasPointwiseLeftKanExtension (T.comp F) ↔ R.HasPointwiseLeftKanExtension F
-- Mathlib.Order.Disjoint
/-- The sublattice of complemented elements.  -/
Complementeds : (α : Type u_2) → [inst : Lattice α] → [BoundedOrder α] → Type u_2
-- Mathlib.Topology.Inseparable
SeparationQuotient.comap_mk_nhdsSet : ∀ {X : Type u_1} [inst : TopologicalSpace X] {t : Set (SeparationQuotient X)},
  Filter.comap SeparationQuotient.mk (nhdsSet t) = nhdsSet (SeparationQuotient.mk ⁻¹' t)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.symm_neg : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : ContinuousNeg M], (ContinuousLinearEquiv.neg R).symm = ContinuousLinearEquiv.neg R
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.borelUpper_eq : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H) [inst_4 : Fintype ι] [IsDomain R]
  [CharZero R] [Module.IsTorsionFree R L],
  b.borelUpper = ⨆ n, ⨆ (_ : n ≠ 0), LieAlgebra.rootSpace H (∑ i, n i • ⇑(b.baseSupp i))
-- Init.Data.Float.Float
Float.repr : Float → ℕ → Std.Format
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_eq_of_equiv : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      (↑m₁).Equiv ↑m₂ →
        ∀ {k : α} [inst_4 : Inhabited β],
          Std.DHashMap.Internal.Raw₀.Const.get! m₁ k = Std.DHashMap.Internal.Raw₀.Const.get! m₂ k
-- Lean.Elab.Declaration
/-- Macro that expands a declaration with a complex name into an explicit `namespace` block.
Implementing this step as a macro means that reuse checking is handled by `elabCommand`.
  -/
Lean.Elab.Command.expandNamespacedDeclaration : Lean.Macro
-- Init.Data.Order.PackageFactories
Std.PreorderPackage.decidableLT : {α : Type u} → [self : Std.PreorderPackage α] → DecidableLT α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensLegend : Type
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.addSubgroup_strictAnti : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M],
  StrictAnti FiniteArchimedeanClass.addSubgroup
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_add_nsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℕ), toIocDiv hp a (b + m • p) = toIocDiv hp a b + ↑m
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- A function `f` is an absolute value if it is nonnegative, zero only at 0, additive, and
multiplicative.

See also the type `AbsoluteValue` which represents a bundled version of absolute values.
 -/
IsAbsoluteValue : {S : Type u_5} → [Semiring S] → [PartialOrder S] → {R : Type u_6} → [Semiring R] → (R → S) → Prop
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
/-- `ω n` is the number of distinct prime factors of `n`.  -/
ArithmeticFunction.cardDistinctFactors : ArithmeticFunction ℕ
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instReprOrdinal : Repr Std.Time.Nanosecond.Ordinal
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.coe_mkOfDistEq : ∀ {α : Type u_5} {β : Type u_6} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] (f : α → β)
  (h : ∃ r, r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y), ⇑(Dilation.mkOfDistEq f h) = f
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
/-- A flat surjective morphism of schemes is an epimorphism in the category of schemes.  -/
AlgebraicGeometry.Flat.epi_of_flat_of_surjective : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Flat f] [AlgebraicGeometry.Surjective f],
  CategoryTheory.Epi f
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_eq_some_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp],
  t.WF → ∀ {k : α}, t.contains k = true → t.get? k = some k
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
/-- The Möbius function on a product order. Based on lemma 2.1.13 of Incidence Algebras by Spiegel
and O'Donnell.  -/
IncidenceAlgebra.mu_prod_mu : ∀ (𝕜 : Type u_2) {α : Type u_5} {β : Type u_6} [inst : Ring 𝕜] [inst_1 : PartialOrder α] [inst_2 : PartialOrder β]
  [inst_3 : LocallyFiniteOrder α] [inst_4 : LocallyFiniteOrder β] [inst_5 : DecidableEq α] [inst_6 : DecidableEq β]
  [inst_7 : DecidableLE α] [inst_8 : DecidableLE β],
  (IncidenceAlgebra.mu 𝕜).prod (IncidenceAlgebra.mu 𝕜) = IncidenceAlgebra.mu 𝕜
-- Std.Time.Zoned.TimeZone
/-- Converts an `Offset` to a string in ISO 8601 format. The `colon` parameter determines if the hour
and minute components are separated by a colon (e.g., "+01:00" or "+0100").
 -/
Std.Time.TimeZone.Offset.toIsoString : Std.Time.TimeZone.Offset → Bool → String
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.instInhabitedProofInstArgInfo.default : Lean.Meta.Sym.ProofInstArgInfo
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.subtypeVal_submodule_iConvexComb : ∀ {F : Type u_1} {R : Type u_2} {M : Type u_3} {I : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : SetLike F M]
  [inst_6 : AddSubmonoidClass F M] [inst_7 : SMulMemClass F R M] [inst_8 : Convexity.ConvexSpace R M]
  [inst_9 : Convexity.IsModuleConvexSpace R M] (S : F) (w : Convexity.StdSimplex R I) (f : I → ↥S),
  ↑(Convexity.iConvexComb w f) = Convexity.iConvexComb w fun i => ↑(f i)
-- Mathlib.RingTheory.Flat.Equalizer
/-- If `M` is `R`-flat, the canonical map `M ⊗[R] eq(f, g) →ₗ[S] eq (𝟙 ⊗ f, 𝟙 ⊗ g)` is an
isomorphism.  -/
LinearMap.tensorEqLocusEquiv : {R : Type u_1} →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          (M : Type u_3) →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] →
                  [inst_6 : IsScalarTower R S M] →
                    {N : Type u_4} →
                      {P : Type u_5} →
                        [inst_7 : AddCommGroup N] →
                          [inst_8 : AddCommGroup P] →
                            [inst_9 : Module R N] →
                              [inst_10 : Module R P] →
                                (f g : N →ₗ[R] P) →
                                  [Module.Flat R M] →
                                    TensorProduct R M ↥(f.eqLocus g) ≃ₗ[S]
                                      ↥(((TensorProduct.AlgebraTensorModule.lTensor S M) f).eqLocus
                                          ((TensorProduct.AlgebraTensorModule.lTensor S M) g))
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.distribLattice : {V : Type u} → DistribLattice (SimpleGraph V)
-- Mathlib.Data.Int.Log
Int.zpow_log_le_self : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  {b : ℕ} {r : R}, 1 < b → 0 < r → ↑b ^ Int.log b r ≤ r
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.isoClosure_strictLimitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J], (P.strictLimitsOfShape J).isoClosure = P.limitsOfShape J
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
/-- Given `φ : a ≅ b` and `f : R ⟶ S`, such that `φ.hom` lifts `f`, then `φ.inv` lifts the
inverse of `f` given by `isoOfIsoLift`.  -/
CategoryTheory.IsHomLift.inv_lift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ≅ b) [inst_2 : p.IsHomLift f φ.hom],
  p.IsHomLift (CategoryTheory.IsHomLift.isoOfIsoLift p f φ).inv φ.inv
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {km : α}, t.max? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Combinatorics.SimpleGraph.Star
SimpleGraph.connected_starGraph : ∀ {V : Type u_1} (r : V), (SimpleGraph.starGraph r).Connected
-- Mathlib.Tactic.Tauto
/-- Matches propositions where we want to apply the `constructor` tactic
in the core loop of `tauto`.  -/
Mathlib.Tactic.Tauto.coreConstructorMatcher : Q(Prop) → Lean.MetaM Bool
-- Mathlib.Data.Int.SuccPred
/-- **Alias** of the reverse direction of `Int.natCast_covBy`. -/
CovBy.intCast : ∀ {a b : ℕ}, a ⋖ b → ↑a ⋖ ↑b
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.ProjRestricts_coe : ∀ {I : Type u} (C : Set (I → Bool)) {J K : I → Prop} [inst : (i : I) → Decidable (J i)]
  [inst_1 : (i : I) → Decidable (K i)] (h : ∀ (i : I), J i → K i) (a : ↑(Profinite.NobelingProof.π C K)) (a_1 : I),
  ↑(Profinite.NobelingProof.ProjRestricts C h a) a_1 = Profinite.NobelingProof.Proj J (↑a) a_1
-- Mathlib.RingTheory.PowerSeries.Exp
PowerSeries.coeff_exp : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℚ A] (n : ℕ),
  (PowerSeries.coeff n) (PowerSeries.exp A) = (algebraMap ℚ A) (1 / ↑n.factorial)
-- Mathlib.RingTheory.TensorProduct.Free
Algebra.TensorProduct.basisAux.eq_1 : ∀ {R : Type u_1} (A : Type u_2) {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (b : Module.Basis ι R M),
  Algebra.TensorProduct.basisAux A b =
    (TensorProduct.congr (Finsupp.uniqueLinearEquiv R A ()).symm b.repr).trans
      ((finsuppTensorFinsupp R R A R PUnit.{1} ι).trans
        (Finsupp.lcongr (Equiv.uniqueProd ι PUnit.{1}) (TensorProduct.rid R A)))
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.monodromyPerm.congr_simp : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) (x : X), cov.monodromyPerm x = cov.monodromyPerm x
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- The naive presentation of a quotient `R[Xᵢ] ⧸ (vⱼ)`.
If the definitional equality of the section matters, it can be explicitly provided.
 -/
Algebra.Presentation.naive : {R : Type u} →
  {ι : Type w} →
    {σ : Type t} →
      [inst : CommRing R] →
        {v : ι → MvPolynomial σ R} →
          (s : optParam (MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R) (Function.surjInv ⋯)) →
            autoParam
                (∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)),
                  (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x)
                Algebra.Presentation.naive._auto_1 →
              Algebra.Presentation R (MvPolynomial σ R ⧸ Ideal.span (Set.range v)) σ ι
-- Mathlib.Data.Set.Equitable
Finset.equitableOn_iff_le_le_add_one : ∀ {α : Type u_1} {s : Finset α} {f : α → ℕ},
  (↑s).EquitableOn f ↔ ∀ a ∈ s, (∑ i ∈ s, f i) / s.card ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / s.card + 1
-- Mathlib.CategoryTheory.Equivalence
/-- If `C` is equivalent to `D`, then `C ⥤ E` is equivalent to `D ⥤ E`.  -/
CategoryTheory.Equivalence.congrLeft : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (C ≌ D) → (CategoryTheory.Functor C E ≌ CategoryTheory.Functor D E)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {fallback : β k}, k ∉ t₂ → (t₁ ∩ t₂).getD k fallback = fallback
-- Mathlib.Algebra.Ring.Center
Set.neg_mem_center : ∀ {M : Type u_1} [inst : NonUnitalNonAssocRing M] {a : M}, a ∈ Set.center M → -a ∈ Set.center M
-- Mathlib.NumberTheory.SumTwoSquares
/-- If `-1` is a square modulo the natural number `n`, then `n` is a sum of two squares.  -/
Nat.eq_sq_add_sq_of_isSquare_mod_neg_one : ∀ {n : ℕ}, IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.mem_support_of_mem_noncommProd_support : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Fintype β] {s : Finset α} {f : α → Equiv.Perm β}
  {comm : (↑s).Pairwise (Function.onFun Commute f)} {x : β},
  x ∈ (s.noncommProd f comm).support → ∃ a ∈ s, x ∈ (f a).support
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.aestronglyMeasurable_uIoc_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : LinearOrder α] [TopologicalSpace.PseudoMetrizableSpace β] {f : α → β} {a b : α},
  MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b)) ↔
    MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.Ioc a b)) ∧
      MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.Ioc b a))
-- Mathlib.GroupTheory.Complement
AddSubgroup.not_isComplement_empty_left : ∀ {G : Type u_1} [inst : AddGroup G] {T : Set G}, ¬AddSubgroup.IsComplement ∅ T
-- Mathlib.SetTheory.Ordinal.Arithmetic
/-- `Ordinal.pred` and `Order.succ` form a Galois insertion.  -/
Ordinal.pred_succ_gi : GaloisInsertion Ordinal.pred Order.succ
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- the condition that there exists a homology data whose `left.H` field is zero  -/
CategoryTheory.ShortComplex.Exact.condition : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C}, S.Exact → ∃ h, CategoryTheory.Limits.IsZero h.left.H
-- Mathlib.Analysis.Complex.Basic
_private.Mathlib.Analysis.Complex.Basic.0.RCLike.termNorm_sqC : Lean.ParserDescr
-- Init.Data.Int.DivMod.Lemmas
Int.mul_fdiv_mul_of_pos_left : ∀ (a : ℤ) {b : ℤ} (c : ℤ), 0 < b → (a * b).fdiv (c * b) = a.fdiv c
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rxo.Iterator.pairwise_toList_upwardEnumerableLt : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxo.IsAlwaysFinite α]
  (it : Std.Iter α), List.Pairwise (fun a b => Std.PRange.UpwardEnumerable.LT a b) it.toList
-- Mathlib.Topology.Order.LeftRightNhds
/-- A set is a neighborhood of `a` within `(a, +∞)` if and only if it contains an interval `(a, u)`
with `a < u`.  -/
mem_nhdsGT_iff_exists_Ioo_subset : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMaxOrder α] {a : α}
  {s : Set α}, s ∈ nhdsWithin a (Set.Ioi a) ↔ ∃ u ∈ Set.Ioi a, Set.Ioo a u ⊆ s
-- Init.Data.Array.Count
Array.countP_mono_left : ∀ {α : Type u_1} {p q : α → Bool} {xs : Array α},
  (∀ x ∈ xs, p x = true → q x = true) → Array.countP p xs ≤ Array.countP q xs
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.classifyWeekdayNumberText : ℕ → Option (Std.Time.Number ⊕ Std.Time.Text)
-- Mathlib.CategoryTheory.Abelian.Refinements
CategoryTheory.ShortComplex.mono_homologyMap_iff_up_to_refinements : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂),
  CategoryTheory.Mono (CategoryTheory.ShortComplex.homologyMap φ) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
      CategoryTheory.CategoryStruct.comp x₂ S₁.g = 0 →
        ∀ (y₁ : A ⟶ S₂.X₁),
          CategoryTheory.CategoryStruct.comp x₂ φ.τ₂ = CategoryTheory.CategoryStruct.comp y₁ S₂.f →
            ∃ A' π,
              ∃ (_ : CategoryTheory.Epi π),
                ∃ x₁, CategoryTheory.CategoryStruct.comp π x₂ = CategoryTheory.CategoryStruct.comp x₁ S₁.f
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.containsThenInsert_snd : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t.containsThenInsert k).2 = t.insert k
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.nat_lt_lift_iff : ∀ {n : ℕ} {a : Cardinal.{u}}, ↑n < Cardinal.lift.{v, u} a ↔ ↑n < a
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.δ_eq_δAux : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ) (x : ↥Q.ker)
  (hx : Algebra.Extension.Cotangent.mk x ∈ Q.toExtension.cotangentComplex.ker),
  (Algebra.Generators.H1Cotangent.δ Q P) ⟨Algebra.Extension.Cotangent.mk x, hx⟩ =
    (Algebra.Generators.H1Cotangent.δAux R Q) ↑x
-- Std.Data.Iterators.Lemmas.Producers.Monadic.List
Std.Types.ListIterator.stepAsHetT_iterM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} [LawfulMonad m] {l : List β},
  (l.iterM m).stepAsHetT =
    match l with
    | [] => pure Std.IterStep.done
    | x :: xs => pure (Std.IterStep.yield (xs.iterM m) x)
-- Init.Data.String.Lemmas.Iterate
String.Slice.chars.eq_1 : ∀ (s : String.Slice),
  s.chars =
    Std.Iter.map
      (fun x =>
        match x with
        | ⟨pos, h⟩ => pos.get h)
      s.positions
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H1AddEquivOfIsTrivial_single : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial] (g : G) (a : ↑A),
  (groupHomology.H1AddEquivOfIsTrivial A)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.H1π A))
        ((CategoryTheory.ConcreteCategory.hom (groupHomology.cycles₁IsoOfIsTrivial A).inv) fun₀ | g => a)) =
    Additive.ofMul (Abelianization.of g) ⊗ₜ[ℤ] a
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
NonarchimedeanAddGroup.mk : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [toIsTopologicalAddGroup : IsTopologicalAddGroup G],
  (∀ U ∈ nhds 0, ∃ V, ↑V ⊆ U) → NonarchimedeanAddGroup G
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_diff_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₁ \ m₂ ↔ k ∈ m₁ ∧ k ∉ m₂
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- An `n`-independent set in a graph is a set of `n` vertices which are pairwise nonadjacent.  -/
SimpleGraph.IsNIndepSet : {α : Type u_1} → SimpleGraph α → ℕ → Finset α → Prop
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.finiteAt_nhdsWithin : ∀ {α : Type u_1} [inst : TopologicalSpace α] {_m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α)
  [MeasureTheory.IsLocallyFiniteMeasure μ] (x : α) (s : Set α), μ.FiniteAtFilter (nhdsWithin x s)
-- Lean.ReducibilityAttrs
Lean.instInhabitedReducibilityStatus : Inhabited Lean.ReducibilityStatus
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.entryAtIdxD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {i : ℕ}
  {fallback : (a : α) × β a}, t₁.Equiv t₂ → t₁.entryAtIdxD i fallback = t₂.entryAtIdxD i fallback
-- Mathlib.Condensed.Functors
instFullCompHausCondensedTypeCompHausToCondensed' : compHausToCondensed'.Full
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph.eq_2 : SimpleGraph.cycleGraph 1 = ⊥
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.derivCLM_apply_apply : ∀ {F : Type u_4} [inst : AddCommGroup F] [inst_1 : Module ℂ F] [inst_2 : TopologicalSpace F]
  [inst_3 : IsTopologicalAddGroup F] [inst_4 : ContinuousConstSMul ℂ F] (f : TemperedDistribution ℝ F)
  (g : SchwartzMap ℝ ℂ), ((TemperedDistribution.derivCLM F) f) g = f (-(SchwartzMap.derivCLM ℂ ℂ) g)
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.Cell.getEntry?_empty : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.OrientedOrd α] [Std.LawfulEqOrd α] {k : α},
  Std.DTreeMap.Internal.Cell.empty.getEntry? = none
-- Init.MetaTypes
/-- If true (default: false), extract lets from subterms that are proofs.
Top-level lets are always extracted.  -/
Lean.Meta.ExtractLetsConfig.proofs : Lean.Meta.ExtractLetsConfig → Bool
-- Mathlib.Topology.Algebra.Polynomial
Polynomial.continuous : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : TopologicalSpace R] [IsTopologicalSemiring R] (p : Polynomial R),
  Continuous fun x => Polynomial.eval x p
-- Mathlib.AlgebraicGeometry.Normalization
/-- The normalization of `Y` in a coproduct is isomorphic to the coproduct of the normalizations in
each of the components.  -/
AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso : {X Y : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    [inst : AlgebraicGeometry.QuasiCompact f] →
      [inst_1 : AlgebraicGeometry.QuasiSeparated f] →
        {U V : AlgebraicGeometry.Scheme} →
          {iU : U ⟶ X} →
            {iV : V ⟶ X} →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV) →
                [inst_2 : AlgebraicGeometry.QuasiCompact iU] →
                  [inst_3 : AlgebraicGeometry.QuasiSeparated iU] →
                    [inst_4 : AlgebraicGeometry.QuasiCompact iV] →
                      [inst_5 : AlgebraicGeometry.QuasiSeparated iV] →
                        AlgebraicGeometry.Scheme.Hom.normalization (CategoryTheory.CategoryStruct.comp iU f) ⨿
                            AlgebraicGeometry.Scheme.Hom.normalization (CategoryTheory.CategoryStruct.comp iV f) ≅
                          AlgebraicGeometry.Scheme.Hom.normalization f
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- If `r` is not a unit, then `e.mulShift r` is not primitive.  -/
AddChar.not_isPrimitive_mulShift : ∀ {R : Type u} [inst : CommRing R] {R' : Type v} [inst_1 : CommMonoid R'] [Finite R] (e : AddChar R R') {r : R},
  ¬IsUnit r → ¬(e.mulShift r).IsPrimitive
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getD t.min! fallback = t.min!
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst.sizeOf_spec : ∀ (k₁ k₂ : ℤ) (c₁ : Lean.Meta.Grind.Arith.Linear.EqCnstr) (c₂ : Lean.Meta.Grind.Arith.Linear.DiseqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst k₁ k₂ c₁ c₂) =
    1 + sizeOf k₁ + sizeOf k₂ + sizeOf c₁ + sizeOf c₂
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScott.isOpen_iff_Iic_compl_or_univ : ∀ {α : Type u_1} [inst : CompleteLinearOrder α] [inst_1 : TopologicalSpace α] [Topology.IsScott α Set.univ] (U : Set α),
  IsOpen U ↔ U = Set.univ ∨ ∃ a, (Set.Iic a)ᶜ = U
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousInv.continuous_inv : ∀ {G : Type u} {inst : TopologicalSpace G} {inst_1 : Inv G} [self : ContinuousInv G], Continuous fun a => a⁻¹