mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Decode
/-- Predicate for whether a byte can appear as the first byte of the UTF-8 encoding of a Unicode
scalar value.
 -/
UInt8.IsUTF8FirstByte : UInt8 → Prop
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.encode_lt_pair : ∀ (cf cg : Nat.Partrec.Code),
  Encodable.encode cf < Encodable.encode (cf.pair cg) ∧ Encodable.encode cg < Encodable.encode (cf.pair cg)
-- Mathlib.Tactic.Linter.Whitespace
/-- `CommandStart.endPos stx` returns the position up until the `whitespace` linter checks the
formatting.
This is every declaration until the type-specification, if there is one, or the value,
as well as all `variable` commands.
 -/
_private.Mathlib.Tactic.Linter.Whitespace.0.Mathlib.Linter.CommandStart.endPos : Lean.Syntax → Option String.Pos.Raw
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_diff_eq_size_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (∀ a ∈ t₁, a ∉ t₂) → (t₁ \ t₂).size = t₁.size
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_list_prod : ∀ {l : List ℝ}, (∀ x ∈ l, x ≠ 0) → Real.log l.prod = (List.map (fun x => Real.log x) l).sum
-- Mathlib.Topology.Order.IntermediateValue
/-- If a preconnected set contains endpoints of an interval, then it includes the whole interval.  -/
IsConnected.Icc_subset : ∀ {α : Type v} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {s : Set α},
  IsConnected s → ∀ {a b : α}, a ∈ s → b ∈ s → Set.Icc a b ⊆ s
-- Lean.Meta.Sym.Apply
Lean.Meta.Sym.ApplyResult.failed : Lean.Meta.Sym.ApplyResult
-- Mathlib.CategoryTheory.EssentialImage
/-- A functor `G : J ⥤ D` to the essential image of a fully faithful functor `F : C ⥤ D` does
factor through `essImage.liftFunctor G F hG`.  -/
CategoryTheory.Functor.essImage.liftFunctorCompIso : {J : Type u_1} →
  {C : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} J] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            (G : CategoryTheory.Functor J D) →
              (F : CategoryTheory.Functor C D) →
                [inst_3 : F.Full] →
                  [inst_4 : F.Faithful] →
                    (hG : ∀ (j : J), F.essImage (G.obj j)) →
                      (CategoryTheory.Functor.essImage.liftFunctor G F hG).comp F ≅ G
-- Mathlib.Data.List.Rotate
List.isRotated_singleton_iff' : ∀ {α : Type u} {l : List α} {x : α}, [x] ~r l ↔ [x] = l
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.map : ∀ {n : ℕ} {f : List.Vector ℕ n →. ℕ} {g : List.Vector ℕ (n + 1) → ℕ},
  Nat.Partrec' f → Nat.Partrec' ↑g → Nat.Partrec' fun v => Part.map (fun a => g (a ::ᵥ v)) (f v)
-- Mathlib.Algebra.Homology.Monoidal
HomologicalComplex.instHasGoodTensor₂₃OfHasGoodTensorTensor₂₃X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Preadditive C] {I : Type u_2} [inst_3 : AddMonoid I] {c : ComplexShape I}
  [inst_4 : c.TensorSigns] (K₁ K₂ K₃ : HomologicalComplex C c)
  [CategoryTheory.GradedObject.HasGoodTensorTensor₂₃ K₁.X K₂.X K₃.X], K₁.HasGoodTensor₂₃ K₂ K₃
-- Lean.Data.PersistentArray
Lean.PersistentArray.Stats.depth : Lean.PersistentArray.Stats → ℕ
-- Mathlib.Algebra.Ring.Parity
Nat.Odd.of_mul_left : ∀ {m n : ℕ}, Odd (m * n) → Odd m
-- Mathlib.Topology.Order.Compact
/-- `Set.Ioc a b` is only compact if it is empty.  -/
isCompact_Ioc_iff : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [DenselyOrdered α] {a b : α},
  IsCompact (Set.Ioc a b) ↔ b ≤ a
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Limits.pullback.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f f_1 : X ⟶ Z) (e_f : f = f_1) (g g_1 : Y ⟶ Z)
  (e_g : g = g_1) [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.Limits.pullback f g = CategoryTheory.Limits.pullback f_1 g_1
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- Lifting universe and morphism levels preserves wide pushout diagrams.  -/
CategoryTheory.Limits.WidePushoutShape.uliftEquivalence : {J : Type w} →
  CategoryTheory.ULiftHom (ULift.{w', w} (CategoryTheory.Limits.WidePushoutShape J)) ≌
    CategoryTheory.Limits.WidePushoutShape (ULift.{w', w} J)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_obj_iso_hom_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  (J : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) (X_1 : X),
  ((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).functor.obj J).iso.hom.app X_1 = (J.obj X_1).iso.hom
-- Std.Sat.CNF.RelabelFin
_private.Std.Sat.CNF.RelabelFin.0.Std.Sat.CNF.numLiterals.match_1.eq_1 : ∀ (motive : Option ℕ → 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.RingTheory.FreeCommRing
FreeCommRing.isSupported_sub : ∀ {α : Type u} {x y : FreeCommRing α} {s : Set α}, x.IsSupported s → y.IsSupported s → (x - y).IsSupported s
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.FiniteRangeSetoid.equiv_zero_iff_hasFiniteRange : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [IsNoetherianRing K] {u : V →ₗ[K] V₂}, u ≈ 0 ↔ u.HasFiniteRange
-- Mathlib.CategoryTheory.Comma.Over.StrictInitial
CategoryTheory.MorphismProperty.underEquivOfIsTerminal_inverse : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P Q : CategoryTheory.MorphismProperty C)
  [inst_1 : P.ContainsIdentities] [inst_2 : Q.IsMultiplicative] [inst_3 : Q.RespectsIso]
  [inst_4 : CategoryTheory.Limits.HasStrictTerminalObjects C] (X : C) (h : CategoryTheory.Limits.IsTerminal X),
  (CategoryTheory.MorphismProperty.underEquivOfIsTerminal.{w, v_1, u_1} P Q X h).inverse =
    CategoryTheory.Functor.fromPUnit (CategoryTheory.MorphismProperty.Under.mk Q (CategoryTheory.CategoryStruct.id X) ⋯)
-- Mathlib.Algebra.BigOperators.Finprod
finprod_eq_finsetProd_of_mulSupport_subset : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (f : α → M) {s : Finset α},
  Function.mulSupport f ⊆ ↑s → ∏ᶠ (i : α), f i = ∏ i ∈ s, f i
-- Mathlib.Algebra.Module.LinearMap.End
/-- The canonical (semi)ring isomorphism from `R` to `Module.End Rᵐᵒᵖ R` induced by the left
multiplication.  -/
RingEquiv.moduleEndSelfOp : (R : Type u_1) → [inst : Semiring R] → R ≃+* Module.End Rᵐᵒᵖ R
-- Mathlib.Algebra.MvPolynomial.CommRing
/-- Subtracting `monomial d c - monomial d' c` from `p`, where `c = coeff d p` and `d ≠ d'`,
removes `d` from the support.  -/
MvPolynomial.notMem_support_sub_monomial_sub_monomial : ∀ {R : Type u} {σ : Type u_1} [inst : CommRing R] (p : MvPolynomial σ R) (d d' : σ →₀ ℕ) (c : R),
  d ≠ d' → MvPolynomial.coeff d p = c → d ∉ (p - ((MvPolynomial.monomial d) c - (MvPolynomial.monomial d') c)).support
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.filterMapTR.go.match_3.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : List α → Array β → Sort u_3) →
      (x : List α) →
        (x_1 : Array β) →
          ((acc : Array β) → motive [] acc) →
            ((a : α) → (as : List α) → (acc : Array β) → motive (a :: as) acc) → motive x x_1
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.whiskerRight : ∀ {C : Type u} {Y Z : CategoryTheory.FreeMonoidalCategory C} (f f' : Y.Hom Z)
  (X : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.HomEquiv f f' →
    CategoryTheory.FreeMonoidalCategory.HomEquiv (f.whiskerRight X) (f'.whiskerRight X)
-- Mathlib.RingTheory.Polynomial.Dickson
_private.Mathlib.RingTheory.Polynomial.Dickson.0.Polynomial.C_half_mul_two_eq_one : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Invertible 2], Polynomial.C ⅟2 * 2 = 1
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.Poly.isZero : Lean.Grind.CommRing.Poly → Bool
-- Lean.DocString.Types
/-- An item in either an ordered or unordered list.  -/
Lean.Doc.ListItem : Type u → Type u
-- Std.Tactic.BVDecide.Normalize.Canonicalize
Std.Tactic.BVDecide.Normalize.Bool.ne_to_beq : ∀ (a b : Bool), (a ≠ b) = ((!a == b) = true)
-- Mathlib.Data.Num.Basic
PosNum.bit0.injEq : ∀ (a a_1 : PosNum), (a.bit0 = a_1.bit0) = (a = a_1)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.elabInline.withSpace : String → String
-- Std.Data.Internal.List.Associative
Std.Internal.List.constModifyKey_eq_modifyKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k : α} {f : β → β} {l : List ((_ : α) × β)},
  Std.Internal.List.Const.modifyKey k f l = Std.Internal.List.modifyKey k f l
-- Mathlib.Data.ENNReal.Operations
ENNReal.iSup_add_iSup_of_monotone : ∀ {ι : Type u_3} [inst : Preorder ι] [IsDirectedOrder ι] {f g : ι → ENNReal},
  Monotone f → Monotone g → iSup f + iSup g = ⨆ a, f a + g a
-- Mathlib.Algebra.Group.Equiv.Basic
/-- A family of additive equivalences `Π j, (Ms j ≃+ Ns j)`
generates an additive equivalence between `Π j, Ms j` and `Π j, Ns j`.

This is the `AddEquiv` version of `Equiv.piCongrRight`, and the dependent version of
`AddEquiv.arrowCongr`.  -/
AddEquiv.piCongrRight : {η : Type u_16} →
  {Ms : η → Type u_17} →
    {Ns : η → Type u_18} →
      [inst : (j : η) → Add (Ms j)] →
        [inst_1 : (j : η) → Add (Ns j)] → ((j : η) → Ms j ≃+ Ns j) → ((j : η) → Ms j) ≃+ ((j : η) → Ns j)
-- Mathlib.Data.Nat.Cast.Commute
Nat.cast_add_comm : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] (m n : ℕ), ↑m + ↑n = ↑n + ↑m
-- Std.Internal.Do.Order.Basic
/-- Entailment between functions is pointwise.  -/
Lean.Order.le_iff_forall_le : ∀ {σ α : Type u} [inst : Lean.Order.PartialOrder α] {f g : σ → α},
  Lean.Order.PartialOrder.rel f g ↔ ∀ (s : σ), Lean.Order.PartialOrder.rel (f s) (g s)
-- Mathlib.RingTheory.Unramified.Basic
Algebra.FormallyUnramified.localization_map : ∀ {R : Type u_1} {S : Type u_2} {Rₘ : Type u_3} {Sₘ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : CommRing Rₘ] [inst_3 : CommRing Sₘ] (M : Submonoid R) [inst_4 : Algebra R S] [inst_5 : Algebra R Sₘ]
  [inst_6 : Algebra S Sₘ] [inst_7 : Algebra R Rₘ] [inst_8 : Algebra Rₘ Sₘ] [IsScalarTower R Rₘ Sₘ]
  [IsScalarTower R S Sₘ] [IsLocalization (Submonoid.map (algebraMap R S) M) Sₘ] [Algebra.FormallyUnramified R S],
  Algebra.FormallyUnramified Rₘ Sₘ
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.isOpen_iff_dist : ∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)]
  (s : Set ((n : ℕ) → E n)), IsOpen s ↔ ∀ x ∈ s, ∃ ε > 0, ∀ (y : (n : ℕ) → E n), dist x y < ε → y ∈ s
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rci.length_iter : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [inst_3 : Std.Rxi.HasSize α] [Std.Rxi.LawfulHasSize α] {r : Std.Rci α},
  r.iter.length = r.size
-- Mathlib.FieldTheory.Fixed
FixedPoints.minpoly.irreducible : ∀ (G : Type u) [inst : Group G] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction G F] [inst_3 : Fintype G]
  (x : F), Irreducible (FixedPoints.minpoly G F x)
-- Batteries.Lean.AttributeExtra
Lean.instInhabitedParametricAttributeExtra.default : {α : Type} → Lean.ParametricAttributeExtra α
-- Mathlib.Analysis.Complex.Asymptotics
Complex.isLittleO_ofReal_right : ∀ {α : Type u_1} {E : Type u_2} [inst : Norm E] {l : Filter α} {f : α → E} {g : α → ℝ},
  (f =o[l] fun x => ↑(g x)) ↔ f =o[l] g
-- Mathlib.LinearAlgebra.Basis.SMul
Module.Basis.coe_smul : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {G : Type u_5} [inst_3 : Group G] [inst_4 : DistribMulAction G M] [inst_5 : SMulCommClass G R M] (g : G)
  (b : Module.Basis ι R M), ⇑(g • b) = g • ⇑b
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_set_subset_iff_subset_inv_smul_set : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] {A B : Set β} {a : α}, a • A ⊆ B ↔ A ⊆ a⁻¹ • B
-- Mathlib.CategoryTheory.ObjectProperty.Ind
/-- `X` satisfies `ind P` if `X` is a filtered colimit of `Xᵢ` for `Xᵢ` in `P`.  -/
CategoryTheory.ObjectProperty.ind : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C → CategoryTheory.ObjectProperty C
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.range_faceOpposite_reindex : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {m n : ℕ} [inst_4 : NeZero m] [inst_5 : NeZero n] (s : Affine.Simplex k P m)
  (e : Fin (m + 1) ≃ Fin (n + 1)) (i : Fin (n + 1)),
  Set.range ((s.reindex e).faceOpposite i).points = Set.range (s.faceOpposite (e.symm i)).points
-- Batteries.Data.List.Pairwise
List.pairwise_pwFilter : ∀ {α : Type u_1} {R : α → α → Prop} [inst : DecidableRel R] (l : List α), List.Pairwise R (List.pwFilter R l)
-- Mathlib.GroupTheory.MonoidLocalization.Away
Localization.Away.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] (x : M), Localization.Away x = Localization (Submonoid.powers x)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.toCocycles_comp_isoCocycles₁_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : (Fin 0 → G) → ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.isoCocycles₁ A).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.toCocycles A 0 1)) x) =
    (groupCohomology.shortComplexH1 A).moduleCatToCycles
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₀ A).hom) x)
-- Mathlib.Analysis.Normed.Group.Completeness
Metric.exists_subseq_summable_dist_of_cauchySeq : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] (u : ℕ → α),
  CauchySeq u → ∃ f, StrictMono f ∧ Summable fun i => dist (u (f (i + 1))) (u (f i))
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid.left : ∀ {α : Type u_1} [inst : Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α},
  (Ordnode.node s l x r).Valid → l.Valid
-- Init.Data.SInt.Bitwise
ISize.or_assoc : ∀ (a b c : ISize), a ||| b ||| c = a ||| (b ||| c)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.not_equiv_of_Z_eq_zero_right : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R}, P 2 ≠ 0 → Q 2 = 0 → ¬P ≈ Q
-- Mathlib.Algebra.Module.Congruence.Defs
ModuleCon.mk.injEq : ∀ {S : Type u_2} {M : Type u_3} [inst : Add M] [inst_1 : SMul S M] (toAddCon : AddCon M)
  (smul : ∀ (s : S) {x y : M}, toAddCon.toSetoid x y → toAddCon.toSetoid (s • x) (s • y)) (toAddCon_1 : AddCon M)
  (smul_1 : ∀ (s : S) {x y : M}, toAddCon_1.toSetoid x y → toAddCon_1.toSetoid (s • x) (s • y)),
  ({ toAddCon := toAddCon, smul := smul } = { toAddCon := toAddCon_1, smul := smul_1 }) = (toAddCon = toAddCon_1)
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- If `v` is an irreducible ideal of `R`, `w` is an irreducible ideal of `S` lying over `v`, and
`I` is an ideal of `R`, then the multiplicity of `w` in `I.map (algebraMap R S)` is given by
the multiplicity of `v` in `I` multiplied by the ramification index of `w` over `v`.  -/
Ideal.IsDedekindDomain.emultiplicity_map_eq_ramificationIdx'_mul : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDedekindDomain S]
  [IsDedekindDomain R] [FaithfulSMul R S] {v : Ideal R} {w : Ideal S} {I : Ideal R},
  I ≠ ⊥ →
    Irreducible v →
      Irreducible w →
        w ≠ ⊥ →
          ∀ [w.LiesOver v], emultiplicity w (Ideal.map (algebraMap R S) I) = ↑(v.ramificationIdx' w) * emultiplicity v I
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.unone.congr_simp : ∀ {α : Type u} {x x_1 : WithOne α} (e_x : x = x_1) (a : x ≠ 1), WithOne.unone a = WithOne.unone ⋯
-- Init.Data.List.Nat.Sum
List.sum_eq_foldl_nat : ∀ {xs : List ℕ}, xs.sum = List.foldl (fun x1 x2 => x1 + x2) 0 xs
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitInfo.getGenerationCore : Lean.Meta.Grind.Goal → Lean.Meta.Grind.SplitInfo → ℕ
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_add_right' : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocDiv hp (a + p) b = toIocDiv hp a b - 1
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.ker_projectionOnto`. -/
Submodule.linearProjOfIsCompl_ker : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q), (p.projectionOnto q h).ker = q
-- Mathlib.Data.Nat.Cast.Basic
Nat.coe_castAddMonoidHom : ∀ {α : Type u_1} [inst : AddMonoidWithOne α], ⇑(Nat.castAddMonoidHom α) = Nat.cast
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getKeyGED_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k fallback : α},
          Std.DTreeMap.Internal.Impl.getKeyGED k t₁ fallback = Std.DTreeMap.Internal.Impl.getKeyGED k t₂ fallback
-- Init.Data.String.Lemmas.Slice
String.Slice.front.eq_1 : ∀ (s : String.Slice), s.front = s.front?.getD default
-- Mathlib.CategoryTheory.IsoCat
/-- A functor which is an isomorphism of categories is full.  -/
CategoryTheory.Functor.IsIso.full : ∀ {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} {F : CategoryTheory.Functor C D} [self : F.IsIso], F.Full
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.coeff_pderiv : ∀ {R : Type u} {σ : Type v} [inst : CommSemiring R] {i : σ} (p : MvPolynomial σ R) (m : σ →₀ ℕ),
  MvPolynomial.coeff m ((MvPolynomial.pderiv i) p) = MvPolynomial.coeff (m + fun₀ | i => 1) p * (↑(m i) + 1)
-- Mathlib.NumberTheory.ModularForms.SlashActions
ModularForm.SLAction : SlashAction ℤ (Matrix.SpecialLinearGroup (Fin 2) ℤ) (UpperHalfPlane → ℂ)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.mem_basicOpen : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (f : ↑(X.presheaf.obj (Opposite.op U))) (x : ↥X) (hx : x ∈ U),
  x ∈ X.basicOpen f ↔ IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.mapNeighborSet_coe : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G') (v : V) (w : ↑(G.neighborSet v)),
  ↑(f.mapNeighborSet v w) = f ↑w
-- Mathlib.Analysis.Normed.MulAction
Pi.instNormSMulClass : ∀ {α : Type u_1} [inst : SeminormedRing α] {ι : Type u_3} {β : ι → Type u_4} [inst_1 : Fintype ι]
  [inst_2 : (i : ι) → SeminormedAddGroup (β i)] [inst_3 : (i : ι) → SMul α (β i)] [∀ (i : ι), NormSMulClass α (β i)],
  NormSMulClass α ((i : ι) → β i)
-- Mathlib.Analysis.Normed.Algebra.UnitizationL1
WithLp.unitization_isometry_inr : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NonUnitalNormedRing A] [inst_2 : NormedSpace 𝕜 A],
  Isometry fun x => WithLp.toLp 1 ↑x
-- Mathlib.Algebra.Lie.Prod
/-- The map `(x, y) ↦ (y, x)` as a Lie equivalence.  -/
LieEquiv.prodComm : (R : Type u_1) →
  (L₁ : Type u_2) →
    (L₂ : Type u_3) →
      [inst : CommRing R] →
        [inst_1 : LieRing L₁] →
          [inst_2 : LieAlgebra R L₁] → [inst_3 : LieRing L₂] → [inst_4 : LieAlgebra R L₂] → (L₁ × L₂) ≃ₗ⁅R⁆ L₂ × L₁
-- Mathlib.Logic.Relation
Relation.EqvGen.transGen_le_eqvGen : ∀ {α : Type u_1} (r : α → α → Prop), Relation.TransGen r ≤ Relation.EqvGen r
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.coe_toMultiplicative_ker : ∀ {A : Type u_8} {A' : Type u_9} [inst : AddGroup A] [inst_1 : AddZeroClass A'] (f : A →+ A'),
  (AddMonoidHom.toMultiplicative f).ker = AddSubgroup.toSubgroup f.ker
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_eq_some_get!_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {a : α}
  [inst_1 : Inhabited (β a)], m.contains a = true → m.get? a = some (m.get! a)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Decl.size : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Decl pu → ℕ
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.lcm_dvd_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α} {a : α}, s.lcm f ∣ a ↔ ∀ b ∈ s, f b ∣ a
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.rid_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (m : M)
  (r : R), (TensorProduct.rid R M) (m ⊗ₜ[R] r) = r • m
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- Promote `HahnEmbedding.Partial.extendFun` to a new `HahnEmbedding.Partial`.  -/
HahnEmbedding.Partial.extend : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      {R : Type u_3} →
                        [inst_9 : AddCommGroup R] →
                          [inst_10 : LinearOrder R] →
                            [inst_11 : Module K R] →
                              {seed : HahnEmbedding.Seed K M R} →
                                (f : HahnEmbedding.Partial seed) →
                                  [IsOrderedAddMonoid R] →
                                    [Archimedean R] → {x : M} → x ∉ (↑f).domain → HahnEmbedding.Partial seed
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- This will be a special case of `LinearMap.toMatrix_id_eq_basis_toMatrix`.  -/
LinearMap.toMatrix_id : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁),
  (LinearMap.toMatrix v₁ v₁) LinearMap.id = 1
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- A coreflective functor is fully faithful.  -/
CategoryTheory.Functor.fullyFaithfulOfCoreflective : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (j : CategoryTheory.Functor C D) → [CategoryTheory.Coreflective j] → j.FullyFaithful
-- Mathlib.Combinatorics.SimpleGraph.Metric
/-- Supergraphs have smaller or equal distances to their subgraphs.  -/
SimpleGraph.Reachable.dist_anti : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} {G' : SimpleGraph V}, G ≤ G' → G.Reachable u v → G'.dist u v ≤ G.dist u v
-- Std.Time.Date.Unit.Week
Std.Time.Week.instAddOffset : Add Std.Time.Week.Offset
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.mem_comap : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] [inst_6 : Semiring B] [inst_7 : StarRing B]
  [inst_8 : Algebra R B] [inst_9 : StarModule R B] (S : StarSubalgebra R B) (f : A →⋆ₐ[R] B) (x : A),
  x ∈ StarSubalgebra.comap f S ↔ f x ∈ S
-- Mathlib.Topology.Defs.Basic
Continuous.mk : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  (∀ (s : Set Y), IsOpen s → IsOpen (f ⁻¹' s)) → Continuous f
-- Mathlib.Tactic.TacticAnalysis
/-- Run tactic code, capturing InfoTrees for extracting "Try this:" suggestions.

Returns both the resulting goals and the InfoTrees produced during tactic execution.
Use `collectTryThisSuggestions` from `Mathlib.Lean.Elab.InfoTree` to extract suggestions.  -/
Mathlib.TacticAnalysis.TacticNode.runTacticCodeCapturingInfoTree : Mathlib.TacticAnalysis.TacticNode →
  Lean.MVarId →
    Lean.Syntax → Lean.Elab.Command.CommandElabM (List Lean.MVarId × Lean.PersistentArray Lean.Elab.InfoTree)