mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Piecewise
Set.pi_piecewise : ∀ {ι : Type u_8} {α : ι → Type u_9} (s s' : Set ι) (t t' : (i : ι) → Set (α i)) [inst : (x : ι) → Decidable (x ∈ s')],
  s.pi (s'.piecewise t t') = (s ∩ s').pi t ∩ (s \ s').pi t'
-- Std.Do.WP.SimpLemmas
Std.Do.WP.adapt_ExceptT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {ε ε' α : Type u} {x : ExceptT ε m α}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except ε' ps)} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (f : ε → ε'),
  (Std.Do.wp (ExceptT.adapt f x)).apply Q = (Std.Do.wp x).apply (Q.1, fun e => Q.2.1 (f e), Q.2.2)
-- Mathlib.Topology.Order.LiminfLimsup
Antitone.liminf_nhdsGT_eq_iSup₂ : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [DenselyOrdered α] [inst_4 : CompleteLattice β] {f : α → β} [NoMaxOrder α],
  Antitone f → ∀ (a : α), Filter.liminf f (nhdsWithin a (Set.Ioi a)) = ⨆ r, ⨆ (_ : r > a), f r
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.eqToHom_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X Y : CategoryTheory.Comma L R) (H : X = Y),
  (CategoryTheory.eqToHom H).right = CategoryTheory.eqToHom ⋯
-- Std.Async.System
Std.Async.System.GroupInfo.mk : String → Std.Async.System.GroupId → Array String → Std.Async.System.GroupInfo
-- Lean.Server.Utils
/-- Like `tee a | b` on Unix. See `chainOut`.  -/
Lean.IO.FS.Stream.chainLeft : IO.FS.Stream → IO.FS.Stream → optParam Bool false → IO.FS.Stream
-- Mathlib.Geometry.Manifold.VectorField.Pullback
VectorField.mpullbackWithin_neg_apply : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x : M}
  {V : (x : M') → TangentSpace I' x},
  VectorField.mpullbackWithin I I' f (-V) s x = -VectorField.mpullbackWithin I I' f V s x
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesOnBall.eventually_hasSum_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r → ∀ᶠ (y : E) in nhds x, HasSum (fun n => (p n) fun x_1 => y - x) (f y)
-- Mathlib.Data.Rel
SetRel.subset_iterate_comp : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α α} [R.IsRefl] {S : SetRel α β} {n : ℕ}, S ⊆ (fun x => R.comp x)^[n] S
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.«mrefinePat%_» : Lean.ParserDescr
-- Mathlib.RingTheory.PicardGroup
/-- In a total ring of fractions, if two ideals are inverse to each other in the Picard group,
the only possibility is that they are both the whole ring.  -/
Ideal.eq_top_of_mk_tensor_eq_one : ∀ {R : Type u_5} [inst : CommRing R] [IsFractionRing R R] (I J : Ideal R) [inst_2 : Module.Invertible R ↥I]
  [inst_3 : Module.Invertible R ↥J], CommRing.Pic.mk R (TensorProduct R ↥I ↥J) = 1 → I = ⊤ ∧ J = ⊤
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mk_intCast : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : IntCast R] (n : ℤ), SeparationQuotient.mk ↑n = ↑n
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjGenLinGroup.signDet_mk : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : Fact (Even (Fintype.card n))] [inst_4 : LinearOrder R] [inst_5 : IsStrictOrderedRing R] (g : GL n R),
  Matrix.ProjGenLinGroup.signDet (Matrix.ProjGenLinGroup.mk g) = (Units.map ↑signHom) (Matrix.GeneralLinearGroup.det g)
-- Lean.Elab.Match
/-- "Generalize" variables that depend on the discriminants.

Remarks and limitations:
- We currently do not generalize let-decls.
- We abort generalization if the new `matchType` is type incorrect.
- Only discriminants that are free variables are considered during specialization.
- We "generalize" by adding new discriminants and pattern variables. We do not "clear" the generalized variables,
  but they become inaccessible since they are shadowed by the patterns variables. We assume this is ok since
  this is the exact behavior users would get if they had written it by hand. Recall there is no `clear` in term mode.
 -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.generalize : Array Lean.Elab.Term.Discr →
  Lean.Expr → Array Lean.Elab.Term.TermMatchAltView → Option Bool → Lean.Elab.TermElabM Lean.Elab.Term.GeneralizeResult
-- Mathlib.Order.Category.CompleteLat
/-- The underlying lattice.  -/
CompleteLat.carrier : CompleteLat → Type u_1
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.nthHom.eq_1 : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} (f : (k : ℕ) → R →+* ZMod (p ^ k)) (r : R) (n : ℕ),
  PadicInt.nthHom f r n = ↑((f n) r).val
-- Mathlib.Data.Finsupp.Single
Finsupp.single_eq_of_ne' : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a a' : α} {b : M}, a ≠ a' → (fun₀ | a => b) a' = 0
-- Init.System.IO
/-- The child process's standard input handle, if it was configured as `IO.Process.Stdio.piped`, or
`()` otherwise.
 -/
IO.Process.Child.stdin : {cfg : IO.Process.StdioConfig} → IO.Process.Child cfg → cfg.stdin.toHandleType
-- Mathlib.CategoryTheory.Limits.VanKampen
/-- Pullbacks distribute over universal coproducts on the left: This is the isomorphism
`∐ (B ×[S] Xᵢ) ≅ B ×[S] (∐ Xᵢ)`.  -/
CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_isPullback_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_3} {S B : C} {X : ι → C}
  {a : CategoryTheory.Limits.Cofan X},
  CategoryTheory.IsUniversalColimit a →
    ∀ (f : (i : ι) → X i ⟶ S) (u : a.pt ⟶ S) (v : B ⟶ S) {P : ι → C} (q₁ : (i : ι) → P i ⟶ B)
      (q₂ : (i : ι) → P i ⟶ X i),
      (∀ (i : ι), CategoryTheory.IsPullback (q₁ i) (q₂ i) v (f i)) →
        ∀ {Z : C} {p₁ : Z ⟶ B} {p₂ : Z ⟶ a.pt},
          CategoryTheory.IsPullback p₁ p₂ v u →
            ∀ (d : CategoryTheory.Limits.Cofan P) (e : d.pt ≅ Z),
              autoParam (∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i)
                  CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_isPullback_left._auto_1 →
                autoParam
                    (∀ (i : ι),
                      CategoryTheory.CategoryStruct.comp (d.inj i) (CategoryTheory.CategoryStruct.comp e.hom p₁) = q₁ i)
                    CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_isPullback_left._auto_3 →
                  autoParam
                      (∀ (i : ι),
                        CategoryTheory.CategoryStruct.comp (d.inj i) (CategoryTheory.CategoryStruct.comp e.hom p₂) =
                          CategoryTheory.CategoryStruct.comp (q₂ i) (a.inj i))
                      CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_isPullback_left._auto_5 →
                    Nonempty (CategoryTheory.Limits.IsColimit d)
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.inv_mul_toLeftFun_mem : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {S : Set G} (hS : Subgroup.IsComplement S ↑H) (g : G),
  g⁻¹ * ↑(hS.toLeftFun g) ∈ H
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivWithinAt.differentiableWithinAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x → DifferentiableWithinAt 𝕜 f s x
-- Mathlib.CategoryTheory.Bicategory.Product
CategoryTheory.Bicategory.prod_whiskerRight_snd : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {a b c : B × C} {f g : a ⟶ b} (θ : f ⟶ g) (g_1 : b ⟶ c),
  (CategoryTheory.Bicategory.whiskerRight θ g_1).2 = CategoryTheory.Bicategory.whiskerRight θ.2 g_1.2
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get_eq_get! : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {a : α} [inst_3 : Inhabited (β a)] {h : m.contains a = true}, m.get a h = m.get! a
-- Mathlib.Data.Setoid.Basic
/-- There is a Galois insertion of equivalence relations on α into binary relations
on α, with equivalence closure the lower adjoint.  -/
Setoid.gi : {α : Type u_1} → GaloisInsertion Relation.EqvGen.setoid (@Setoid.r α)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_insertIfNew_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insertIfNew k v).contains k = true
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.lift_symm_apply : ∀ (R : Type u) {X : Type v} [inst : CommRing R] {L : Type w} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (F : FreeLieAlgebra R X →ₗ⁅R⁆ L), (FreeLieAlgebra.lift R).symm F = ⇑F ∘ FreeLieAlgebra.of R
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.orbitEquivQuotientStabilizer_symm_apply : ∀ (G : Type u) {X : Type v} [inst : AddGroup G] [inst_1 : AddAction G X] (b : X) (g : G),
  ↑((AddAction.orbitEquivQuotientStabilizer G b).symm ↑g) = g +ᵥ b
-- Mathlib.Data.LawfulXor.Equiv
Equiv.xor_zero : ∀ {α : Type u_1} [inst : XorOp α] [inst_1 : Zero α] [inst_2 : LawfulXor α], Equiv.xor 0 = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.yonedaEquiv_symm_app_id : ∀ {X : SSet} {n : ℕ} (x : X.obj (Opposite.op { len := n })),
  (CategoryTheory.ConcreteCategory.hom ((SSet.yonedaEquiv.symm x).app (Opposite.op { len := n })))
      (SSet.yonedaEquiv (CategoryTheory.CategoryStruct.id (SSet.stdSimplex.obj { len := n }))) =
    x
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- Topological sum of `term`s.  -/
ZetaAsymptotics.termTSum : ℝ → ℝ
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.hasCoproducts_of_finite_and_filtered : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteCoproducts C]
  [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w, v, u} C], CategoryTheory.Limits.HasCoproducts C
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardSliceSearcher.matchesAt_iff_getElem : ∀ {pat s : String.Slice} {pos : s.Pos},
  pat.isEmpty = false →
    (String.Slice.Pattern.Model.MatchesAt pat pos ↔
      ∃ (h : pos.offset.byteIdx + pat.copy.toByteArray.size ≤ s.copy.toByteArray.size),
        ∀ (j : ℕ) (hj : j < pat.copy.toByteArray.size),
          pat.copy.toByteArray[j] = s.copy.toByteArray[pos.offset.byteIdx + j])
-- Lean.Parser.Basic
/-- Match an arbitrary Parser and return the consumed String in a `Syntax.atom`.  -/
Lean.Parser.rawFn : Lean.Parser.ParserFn → optParam Bool false → Lean.Parser.ParserFn
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.whiskerLeft_curry_ihom_ev_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A X : C) {Y : C}
  [inst_2 : CategoryTheory.Closed A] (g : CategoryTheory.MonoidalCategoryStruct.tensorObj A Y ⟶ X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalClosed.curry g))
      ((CategoryTheory.ihom.ev A).app X) =
    g
-- Mathlib.Data.PNat.Defs
PNat.strongInductionOn.eq_def : ∀ {p : ℕ+ → Sort u_1} (n : ℕ+) (x : (k : ℕ+) → ((m : ℕ+) → m < k → p m) → p k),
  n.strongInductionOn x =
    have IH := x;
    IH n fun a x => a.strongInductionOn IH
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.primeSpectrum_asIdeal_range_eq : ∀ {R : Type u_1} [inst : CommRing R] [IsArtinianRing R],
  Set.range PrimeSpectrum.asIdeal = Set.range MaximalSpectrum.asIdeal
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_insertListIfNewUnit : ∀ {α : Type u} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α},
  Std.Internal.List.containsKey k (Std.Internal.List.insertListIfNewUnit l toInsert) =
    (Std.Internal.List.containsKey k l || toInsert.contains k)
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.mk.injEq : ∀ {M : Type u_10} {N : Type u_11} [inst : AddZero M] [inst_1 : AddZero N] (toZeroHom : ZeroHom M N)
  (map_add' : ∀ (x y : M), toZeroHom.toFun (x + y) = toZeroHom.toFun x + toZeroHom.toFun y) (toZeroHom_1 : ZeroHom M N)
  (map_add'_1 : ∀ (x y : M), toZeroHom_1.toFun (x + y) = toZeroHom_1.toFun x + toZeroHom_1.toFun y),
  ({ toZeroHom := toZeroHom, map_add' := map_add' } = { toZeroHom := toZeroHom_1, map_add' := map_add'_1 }) =
    (toZeroHom = toZeroHom_1)
-- Lean.Elab.PreDefinition.WF.Fix
/-- Creates a subgoal for a recursive call, as an unsolved `MVar`. The goal is cleaned up, and
the current syntax reference is stored in the `MVar`’s type as a `RecApp` marker, for
use by `solveDecreasingGoals` below.
 -/
_private.Lean.Elab.PreDefinition.WF.Fix.0.Lean.Elab.WF.mkDecreasingProof : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Order.PiLex
Pi.toColex_update_lt_self_iff : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] {x : (i : ι) → β i} {i : ι} {a : β i}
  [inst_1 : (i : ι) → PartialOrder (β i)] [WellFoundedGT ι], toColex (Function.update x i a) < toColex x ↔ a < x i
-- Mathlib.Order.CompleteLattice.Defs
lt_biInf_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLinearOrder α] {a : α} {s : Set β} {f : β → α},
  ⨅ i ∈ s, f i < a ↔ ∃ i ∈ s, f i < a
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_add : ∀ (b : ℕ), 1 < b → ∀ (x y : ℕ), x < b → x ≠ 0 ∨ y ≠ 0 → b.digits (x + b * y) = x :: b.digits y
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
LocallyConstant.comapₗ.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {Z : Type u_6} (R : Type u_7)
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid Z] [inst_4 : Module R Z] (f : C(X, Y)),
  LocallyConstant.comapₗ R f = { toFun := LocallyConstant.comap f, map_add' := ⋯, map_smul' := ⋯ }
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.ap.inj : ∀ {x : Lean.IR.VarId} {ys : Array Lean.IR.Arg} {x_1 : Lean.IR.VarId} {ys_1 : Array Lean.IR.Arg},
  Lean.IR.Expr.ap x ys = Lean.IR.Expr.ap x_1 ys_1 → x = x_1 ∧ ys = ys_1
-- Init.Grind.Module.Basic
/-- Addition is commutative.  -/
Lean.Grind.AddCommMonoid.add_comm : ∀ {M : Type u} [self : Lean.Grind.AddCommMonoid M] (a b : M), a + b = b + a
-- Mathlib.Data.ENat.Basic
ENat.map_natCast_mul : ∀ {R : Type u_2} [inst : NonAssocSemiring R] [inst_1 : DecidableEq R] [CharZero R] (a b : ℕ∞),
  ENat.map Nat.cast (a * b) = ENat.map Nat.cast a * ENat.map Nat.cast b
-- Mathlib.Control.Traversable.Basic
/-- A traversable functor commutes with all applicative functors.  -/
sequence : {t : Type u → Type u} → {α : Type u} → {f : Type u → Type u} → [Applicative f] → [Traversable t] → t (f α) → f (t α)
-- Mathlib.Topology.Category.LightProfinite.Sequence
_private.Mathlib.Topology.Category.LightProfinite.Sequence.0.LightProfinite.natUnionInftyEmbedding.match_1.eq_1 : ∀ (motive : OnePoint ℕ → Sort u_1) (h_1 : Unit → motive none) (h_2 : (n : ℕ) → motive (some n)),
  (match none with
    | none => h_1 ()
    | some n => h_2 n) =
    h_1 ()
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
WeakDual.CharacterSpace.instIsEmpty : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : NonUnitalNonAssocSemiring A] [inst_5 : TopologicalSpace A]
  [inst_6 : Module 𝕜 A] [Subsingleton A], IsEmpty ↑(WeakDual.characterSpace 𝕜 A)
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.map_lift : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  (self : F.WellOrderInductionData) (j : J) (hj : Order.IsSuccLimit j) (x : ↑(⋯.functor.op.comp F).sections) (i : J)
  (hi : i < j),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) (self.lift j hj x) =
    ↑x (Opposite.op ⟨i, hi⟩)
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rxc.Iterator.Monadic.step.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (next : α) (h_1 : Unit → motive none)
  (h_2 : (next : α) → motive (some next)),
  (match some next with
    | none => h_1 ()
    | some next => h_2 next) =
    h_2 next
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_lt_add_of_lt_of_le : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddLeftMono α] [AddRightStrictMono α] {a b c d : α},
  a < b → c ≤ d → a + c < b + d
-- Mathlib.Algebra.Free
/-- Recursor for free semigroup using `of` and `*`.  -/
FreeSemigroup.recOnMul : {α : Type u} →
  {C : FreeSemigroup α → Sort l} →
    (x : FreeSemigroup α) →
      ((x : α) → C (FreeSemigroup.of x)) →
        ((x : α) → (y : FreeSemigroup α) → C (FreeSemigroup.of x) → C y → C (FreeSemigroup.of x * y)) → C x
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.unit_eq_unit_of_mem_ofUnits : ∀ {M : Type u_1} [inst : Monoid M] (S : Subgroup Mˣ) {x : M} (h₁ : IsUnit x) (h₂ : x ∈ S.ofUnits),
  h₁.unit = S.unit_of_mem_ofUnits h₂
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fromEdgeSet_edgeSet : ∀ {V : Type u} (G : SimpleGraph V), SimpleGraph.fromEdgeSet G.edgeSet = G
-- Mathlib.CategoryTheory.Monad.Monadicity
/-- To show `G` is a monadic right adjoint, we can show it preserves and reflects `G`-split
coequalizers, and `D` has them.
 -/
CategoryTheory.Monad.monadicOfHasPreservesReflectsGSplitCoequalizers : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {G : CategoryTheory.Functor D C} →
          {F : CategoryTheory.Functor C D} →
            (F ⊣ G) →
              [CategoryTheory.Monad.HasCoequalizerOfIsSplitPair G] →
                [CategoryTheory.Monad.PreservesColimitOfIsSplitPair G] →
                  [CategoryTheory.Monad.ReflectsColimitOfIsSplitPair G] → CategoryTheory.MonadicRightAdjoint G
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.HasMultiplicativeReduction.not_hasGoodReduction : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] {W : WeierstrassCurve K},
  WeierstrassCurve.HasMultiplicativeReduction R W → ¬WeierstrassCurve.HasGoodReduction R W
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.comp.congr_simp : ∀ {X Y Z : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} (f f_1 : SSet.RelativeMorphism A B φ),
  f = f_1 →
    ∀ {C : Z.Subcomplex} {ψ : B.toSSet ⟶ C.toSSet} (f' f'_1 : SSet.RelativeMorphism B C ψ),
      f' = f'_1 →
        ∀ {φψ : A.toSSet ⟶ C.toSSet} (fac : CategoryTheory.CategoryStruct.comp φ ψ = φψ),
          f.comp f' fac = f_1.comp f'_1 fac
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.mapL_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] {A : Type u_6} {B : Type u_7}
  [inst_9 : NormedAddCommGroup A] [inst_10 : InnerProductSpace 𝕜 A] [inst_11 : NormedAddCommGroup B]
  [inst_12 : InnerProductSpace 𝕜 B] (f₁ : E →L[𝕜] F) (f₂ : A →L[𝕜] E) (g₁ : G →L[𝕜] H) (g₂ : B →L[𝕜] G),
  TensorProduct.mapL (f₁ ∘SL f₂) (g₁ ∘SL g₂) = TensorProduct.mapL f₁ g₁ ∘SL TensorProduct.mapL f₂ g₂
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.ext_iff : ∀ {q : ℕ} {x y : LucasLehmer.X q}, x = y ↔ x.1 = y.1 ∧ x.2 = y.2
-- Mathlib.Order.UpperLower.Relative
RelUpperSet.isRelUpperSet : ∀ {α : Type u_1} {P : α → Prop} [inst : LE α] (u : RelUpperSet P), IsRelUpperSet (↑u) P
-- Lean.Server.CodeActions.Basic
Lean.Server.codeActionProviderExt : Lean.SimplePersistentEnvExtension Lean.Name Lean.NameSet
-- Mathlib.CategoryTheory.Limits.Cones
/-- If `F : J ⥤ C` then `F.cones` is the functor assigning to an object `X : C` the
type of natural transformations from the constant functor with value `X` to `F`.
An object representing this functor is a limit of `F`.
 -/
CategoryTheory.Functor.cones : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        CategoryTheory.Functor J C → CategoryTheory.Functor Cᵒᵖ (Type (max u₁ v₃))
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_zpow : ∀ {β : Type u_8} [inst : DivisionCommMonoid β] {r : ℤ} {l : List β}, l.prod ^ r = (List.map (fun x => x ^ r) l).prod
-- Std.Data.DTreeMap.Internal.Lemmas
/-- This is a restatement of `mem_of_mem_insertIfNew!` that is written to exactly match the
proof obligation in the statement of `get_insertIfNew!`.  -/
Std.DTreeMap.Internal.Impl.mem_of_mem_insertIfNew!' : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k a : α} {v : β k},
      a ∈ Std.DTreeMap.Internal.Impl.insertIfNew! k v t → ¬(compare k a = Ordering.eq ∧ k ∉ t) → a ∈ t
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- The proposition that a sequence indexed by `ℤ` is an elliptic net.  -/
IsEllipticNet : {R : Type u_1} → [CommRing R] → (ℤ → R) → Prop
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.length_mono : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R) {s₁ s₂ : Set R},
  s₁ ⊆ s₂ → f.length s₁ ≤ f.length s₂
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
/-- Morphisms `n ⟶ m` in `SemiSimplexCategory` identify to order embeddings
`Fin (n.len + 1) ↪o Fin (m.len + 1)`.  -/
SemiSimplexCategory.homEquiv : {n m : SemiSimplexCategory} → (n ⟶ m) ≃ (Fin (n.len + 1) ↪o Fin (m.len + 1))
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.fullSubcategory_whiskerLeft_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {P : CategoryTheory.ObjectProperty C} [inst_2 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete PEmpty.{1})]
  [inst_3 : P.IsClosedUnderLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)]
  (X x x_1 : P.FullSubcategory) (f : x ⟶ x_1),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f).hom =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.obj f.hom
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.map : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M}
  {x y : M} {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N],
  x ≡ y [SMOD U] → ∀ (f : M →ₗ[R] N), f x ≡ f y [SMOD Submodule.map f U]
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.mem_split_iff : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {i : ι} {x : ℝ},
  J ∈ BoxIntegral.Prepartition.split I i x ↔ ↑J = I.splitLower i x ∨ ↑J = I.splitUpper i x
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.postcompCLM_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {F' : Type u_5} [inst_6 : NormedAddCommGroup F']
  [inst_7 : NormedSpace ℝ F'] [inst_8 : NormedSpace 𝕜 F'] {n : ℕ∞} [inst_9 : Algebra ℝ 𝕜]
  [inst_10 : IsScalarTower ℝ 𝕜 F] [inst_11 : IsScalarTower ℝ 𝕜 F'] (T : F →L[𝕜] F') (f : TestFunction Ω F n),
  ⇑((TestFunction.postcompCLM T) f) = ⇑T ∘ ⇑f