mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.expand_one : ∀ {R : Type u} [inst : CommSemiring R] (f : Polynomial R), (Polynomial.expand R 1) f = f
-- Mathlib.Topology.Algebra.MulAction
continuousVAdd_inf : ∀ {M : Type u_2} {X : Type u_3} [inst : TopologicalSpace M] [inst_1 : VAdd M X] {t₁ t₂ : TopologicalSpace X}
  [ContinuousVAdd M X] [ContinuousVAdd M X], ContinuousVAdd M X
-- Init.MetaTypes
Lean.Meta.Simp.ConfigCtx.mk.sizeOf_spec : ∀ (toConfig : Lean.Meta.Simp.Config), sizeOf { toConfig := toConfig } = 1 + sizeOf toConfig
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_enorm_rpow : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {q : ℝ} {μ : MeasureTheory.Measure α}
  [inst : ENorm ε] (f : α → ε),
  0 < q → MeasureTheory.eLpNorm (fun x => ‖f x‖ₑ ^ q) p μ = MeasureTheory.eLpNorm f (p * ENNReal.ofReal q) μ ^ q
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_valEmbedding_Ioi : ∀ {n : ℕ} (a : Fin n), Finset.map Fin.valEmbedding (Finset.Ioi a) = Finset.Ioo (↑a) n
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_union : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {k : α},
  Std.ExtDTreeMap.Const.get? (t₁.union t₂) k = (Std.ExtDTreeMap.Const.get? t₂ k).or (Std.ExtDTreeMap.Const.get? t₁ k)
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousWithinAt.div' : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Div G]
  [ContinuousDiv G] {f g : X → G} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → ContinuousWithinAt (f / g) s x
-- Aesop.Forward.Match
/-- Returns `true` if the match contains the given pattern substitution.  -/
Aesop.Match.containsPatSubst : Aesop.Substitution → Aesop.Match → Bool
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.quot_hom_ext : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {M₂ : Type u_3} [inst_3 : AddCommGroup M₂] [inst_4 : Module R M₂] (f g : M ⧸ p →ₗ[R] M₂),
  (∀ (x : M), f (Submodule.Quotient.mk x) = g (Submodule.Quotient.mk x)) → f = g
-- Mathlib.NumberTheory.DirichletCharacter.Orthogonality
DirichletCharacter.fintype : {R : Type u_1} → [inst : CommRing R] → [IsDomain R] → {n : ℕ} → Fintype (DirichletCharacter R n)
-- Lean.Data.Json.Printer
Lean.Json.renderString : String → optParam String "" → String
-- Mathlib.Algebra.Category.MonCat.Limits
AddCommMonCat.forget_createsLimits : CategoryTheory.CreatesLimits (CategoryTheory.forget AddMonCat)
-- Mathlib.Algebra.MvPolynomial.PDeriv
MvPolynomial.mkDerivation.congr_simp : ∀ {σ : Type u_1} (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (MvPolynomial σ R) A] [inst_4 : IsScalarTower R (MvPolynomial σ R) A] (f f_1 : σ → A),
  f = f_1 → MvPolynomial.mkDerivation R f = MvPolynomial.mkDerivation R f_1
-- Init.Data.BitVec.Lemmas
BitVec.cons_or_cons : ∀ {w : ℕ} (x y : BitVec w) (a b : Bool), BitVec.cons a x ||| BitVec.cons b y = BitVec.cons (a || b) (x ||| y)
-- Aesop.Tree.Data
Aesop.Goal.isActive : Aesop.Goal → BaseIO Bool
-- Mathlib.Topology.Sheaves.Abelian
TopCat.instAbelianPresheaf : {X : TopCat} →
  {C : Type v₁} →
    [inst : CategoryTheory.Category.{v₂, v₁} C] →
      [CategoryTheory.Abelian C] → CategoryTheory.Abelian (TopCat.Presheaf C X)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.mixedEmbeddingsOver.eq_1 : ∀ {K : Type u_3} (L : Type u_4) [inst : Field K] [inst_1 : Field L] (ψ : K →+* ℂ) [inst_2 : Algebra K L],
  NumberField.ComplexEmbedding.mixedEmbeddingsOver L ψ =
    {φ | NumberField.ComplexEmbedding.LiesOver φ ψ ∧ NumberField.ComplexEmbedding.IsMixed K φ}
-- Mathlib.RepresentationTheory.Induced
Representation.IndV.hom_ext : ∀ {k : Type u_1} {G : Type u_2} {H : Type u_3} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] (φ : G →* H)
  {A : Type u_4} {B : Type u_5} [inst_3 : AddCommGroup A] [inst_4 : Module k A] (ρ : Representation k G A)
  [inst_5 : AddCommGroup B] [inst_6 : Module k B] {f g : Representation.IndV φ ρ →ₗ[k] B},
  (∀ (h : H), f ∘ₗ Representation.IndV.mk φ ρ h = g ∘ₗ Representation.IndV.mk φ ρ h) → f = g
-- Mathlib.Data.Finset.Basic
Equiv.Finset.disjUnionEquiv_symm_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} (h : Disjoint s t) {i : α} (hi : i ∈ s)
  (hi' : i ∈ s.disjUnion t h), (Equiv.Finset.disjUnionEquiv s t h).symm ⟨i, hi'⟩ = Sum.inl ⟨i, hi⟩
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_int_le_one : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (z : ℤ), ‖↑z‖ ≤ 1
-- Init.Data.String.Defs
/-- Returns the length of the string `s`, assuming the string is comprised only of ASCII characters.

This is implemented as a synonym for `s.utf8ByteSize`, which takes constant time.
 -/
String.lengthAssumingAscii : String → ℕ
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.one.eq_1 : ∀ {α : Type u} [inst : One α], WithBot.one = { one := ↑1 }
-- Lean.Elab.PreDefinition.PartialFixpoint.Main
/-- Given two type-proof pairs for `monotone f` and `monotone g`, constructs a type-proof pair for `monotone fun x => ⟨f x, g x⟩`.
 -/
_private.Lean.Elab.PreDefinition.PartialFixpoint.Main.0.Lean.Elab.mkMonoPProd : Lean.Expr × Lean.Expr → Lean.Expr × Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Mathlib.Analysis.Calculus.MeanValue
/-- Over the reals or the complexes, a continuously differentiable function is strictly
differentiable.  -/
hasStrictFDerivAt_of_hasFDerivAt_of_continuousAt : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {G : Type u_4} [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G]
  {H : Type u_5} [inst_3 : NormedAddCommGroup H] [inst_4 : NormedSpace 𝕜 H] {f : G → H} {f' : G → G →L[𝕜] H} {x : G},
  (∀ᶠ (y : G) in nhds x, HasFDerivAt f (f' y) y) → ContinuousAt f' x → HasStrictFDerivAt f (f' x) x
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
/-- Given two differentiable maps into the same fibers of a Riemannian bundle,
their scalar product is differentiable.  -/
MDifferentiableOn.inner_bundle : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {B : Type u_3} [inst_3 : TopologicalSpace B]
  [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F]
  {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_8 : (x : B) → NormedAddCommGroup (E x)]
  [inst_9 : (x : B) → InnerProductSpace ℝ (E x)] [inst_10 : FiberBundle F E] [inst_11 : VectorBundle ℝ F E]
  {EM : Type u_6} [inst_12 : NormedAddCommGroup EM] [inst_13 : NormedSpace ℝ EM] {HM : Type u_7}
  [inst_14 : TopologicalSpace HM] {IM : ModelWithCorners ℝ EM HM} {M : Type u_8} [inst_15 : TopologicalSpace M]
  [inst_16 : ChartedSpace HM M] [h : IsContMDiffRiemannianBundle IB 1 F E] {b : M → B} {v w : (x : M) → E (b x)}
  {s : Set M},
  (MDiff[s] fun m => ⟨b m, v m⟩) → (MDiff[s] fun m => ⟨b m, w m⟩) → MDiff[s] fun b_1 => inner ℝ (v b_1) (w b_1)
-- Mathlib.Data.Finset.NAry
Finset.card_image₂_le : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] (f : α → β → γ) (s : Finset α) (t : Finset β),
  (Finset.image₂ f s t).card ≤ s.card * t.card
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instFromJsonDiagnosticWith.fromJson : {α : Type} → [Lean.FromJson α] → Lean.Json → Except String (Lean.Lsp.DiagnosticWith α)
-- Mathlib.Tactic.Sat.FromLRAT
Mathlib.Tactic.Sat.LRATStep.del.injEq : ∀ (ids ids_1 : Array ℕ), (Mathlib.Tactic.Sat.LRATStep.del ids = Mathlib.Tactic.Sat.LRATStep.del ids_1) = (ids = ids_1)
-- Mathlib.LinearAlgebra.Matrix.ZPow
Matrix.one_div_zpow : ∀ {n' : Type u_1} [inst : DecidableEq n'] [inst_1 : Fintype n'] {R : Type u_2} [inst_2 : CommRing R]
  {A : Matrix n' n' R} (n : ℤ), (1 / A) ^ n = 1 / A ^ n
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.of_pushout_inl_of_codescendsAlong : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P Q : CategoryTheory.MorphismProperty C} {Z X Y : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} [P.CodescendsAlong Q] [inst_2 : CategoryTheory.Limits.HasPushout f g],
  Q f → P (CategoryTheory.Limits.pushout.inl f g) → P g
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.not_indep : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCircuit C → ¬M.Indep C
-- Mathlib.Tactic.NormNum.GCD
Mathlib.Meta.NormNum.isNat_lcm : ∀ {x y nx ny z : ℕ},
  Mathlib.Meta.NormNum.IsNat x nx →
    Mathlib.Meta.NormNum.IsNat y ny → nx.lcm ny = z → Mathlib.Meta.NormNum.IsNat (x.lcm y) z
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.continuousOn_sub : ContinuousOn (fun p => p.1 - p.2) {p | p ≠ (⊤, ⊤)}
-- Mathlib.Data.Sym.Basic
/-- Inverse of `Sym_option_succ_equiv.decode`.  -/
SymOptionSuccEquiv.decode : {α : Type u_1} → {n : ℕ} → Sym (Option α) n ⊕ Sym α n.succ → Sym (Option α) n.succ
-- Mathlib.Analysis.Normed.Group.Continuity
Inseparable.norm_eq_norm' : ∀ {E : Type u_4} [inst : SeminormedGroup E] {u v : E}, Inseparable u v → ‖u‖ = ‖v‖
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.isIso_toSpecΓ : ∀ (R : CommRingCat), CategoryTheory.IsIso (AlgebraicGeometry.toSpecΓ R)
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.ofHom_comp : ∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : S →+* T),
  CommRingCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom f) (CommRingCat.ofHom g)
-- Mathlib.Algebra.Order.Floor.Ring
Int.sub_floor_div_mul_lt : ∀ {k : Type u_4} [inst : Field k] [inst_1 : LinearOrder k] [IsOrderedRing k] [inst_3 : FloorRing k] {b : k} (a : k),
  0 < b → a - ↑⌊a / b⌋ * b < b
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_intCast_nonneg : ∀ (n : ℤ), 0 ≤ Real.log ↑n
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLE?.go.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option ((a : α) × β a)),
  Std.DTreeMap.Internal.Impl.getEntryLE?.go k best Std.DTreeMap.Internal.Impl.leaf = best
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- Expressions for 2-isomorphisms.  -/
Mathlib.Tactic.BicategoryLike.Mor₂Iso : Type
-- Mathlib.Data.Complex.Basic
Complex.ofReal_injective : Function.Injective Complex.ofReal
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
/-- **Andrásfai-Erdős-Sós** theorem

If `G` is a `Kᵣ₊₁`-free graph with `n` vertices and `(3 * r - 4) * n / (3 * r - 1) < G.minDegree`
then `G` is `r + 1`-colorable, e.g. if `G` is `K₃`-free and `2 * n / 5 < G.minDegree` then `G`
is `2`-colorable.
 -/
SimpleGraph.colorable_of_cliqueFree_lt_minDegree : ∀ {α : Type u_1} {G : SimpleGraph α} {r : ℕ} [inst : Fintype α] [inst_1 : DecidableRel G.Adj],
  G.CliqueFree (r + 1) → (3 * r - 4) * Fintype.card α / (3 * r - 1) < G.minDegree → G.Colorable r
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.toExpr : Lean.Compiler.LCNF.LitValue → Lean.Expr
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
/-- For a `P : AffineTargetMorphismProperty`, `targetAffineLocally P` holds for
`f : X ⟶ Y` whenever `P` holds for the restriction of `f` on every affine open subset of `Y`.  -/
AlgebraicGeometry.targetAffineLocally : AlgebraicGeometry.AffineTargetMorphismProperty → CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme
-- Init.Prelude
/-- Creates a `UInt16` from a `BitVec 16`. This function is overridden with a native implementation.
 -/
UInt16.ofBitVec : BitVec 16 → UInt16
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.δ_eq_zero_of_isIso₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
  CategoryTheory.IsIso f →
    ∀ (n₀ n₁ : ℤ) (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.δ_eq_zero_of_isIso₁._auto_1),
      X.δ f g n₀ n₁ hn₁ = 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.apply_eq_true_of_containsKey_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {f : (a : α) → β a → Bool}
  {l : List ((a : α) × β a)} {k : α} (hl : Std.Internal.List.DistinctKeys l)
  (h : Std.Internal.List.containsKey k (List.filter (fun p => f p.fst p.snd) l) = true),
  f k (Std.Internal.List.getValueCast k l ⋯) = true
-- Mathlib.Algebra.Group.Equiv.Opposite
MulOpposite.opAddEquiv_symm_apply : ∀ {α : Type u_2} [inst : Add α], ⇑MulOpposite.opAddEquiv.symm = MulOpposite.unop
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instTrivialStar : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddMonoid β]
  [inst_3 : StarAddMonoid β] [inst_4 : ContinuousStar β] [TrivialStar β],
  TrivialStar (CompactlySupportedContinuousMap α β)
-- Mathlib.Data.EReal.Operations
EReal.sub_add_cancel_left : ∀ {a : EReal} {b : ℝ}, ↑b - (↑b + a) = -a
-- Mathlib.RingTheory.Extension.ExtendScalars
Algebra.Extension.Hom.ofAlgHom.congr_simp : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u_1} {S' : Type u_2} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S'] (f f_1 : P.Ring →ₐ[R] P'.Ring) (e_f : f = f_1)
  (H :
    (IsScalarTower.toAlgHom R P'.Ring S').comp f =
      (IsScalarTower.toAlgHom R S S').comp (IsScalarTower.toAlgHom R P.Ring S)),
  Algebra.Extension.Hom.ofAlgHom f H = Algebra.Extension.Hom.ofAlgHom f_1 ⋯
-- Mathlib.Algebra.Ring.CompTypeclasses
RingHomInvPair.toRingEquiv_symm_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] (σ : R₁ →+* R₂) (σ' : R₂ →+* R₁)
  [inst_2 : RingHomInvPair σ σ'] (a : R₂), (RingHomInvPair.toRingEquiv σ σ').symm a = σ' a
-- Init.Prelude
/-- Retrieve the immediate info from the Syntax node.  -/
Lean.Syntax.getInfo? : Lean.Syntax → Option Lean.SourceInfo
-- Mathlib.Order.Filter.Extr
IsMaxOn.max : ∀ {α : Type u} {β : Type v} [inst : LinearOrder β] {f g : α → β} {a : α} {s : Set α},
  IsMaxOn f s a → IsMaxOn g s a → IsMaxOn (fun x => max (f x) (g x)) s a
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
_private.Std.Tactic.BVDecide.LRAT.Internal.Clause.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder.match_1.eq_1 : ∀ (motive : Option Bool → Sort u_1) (val' : Bool) (h_1 : (val' : Bool) → motive (some val'))
  (h_2 : (x : Option Bool) → motive x),
  (match some val' with
    | some val' => h_1 val'
    | x => h_2 x) =
    h_1 val'
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.singleton_last : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i : ι} (x : M i) (hne_one : x ≠ 1),
  (Monoid.CoprodI.NeWord.singleton x hne_one).last = x
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.naturality_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (self : CategoryTheory.Oplax.StrongTrans F G) (a : B),
  CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.id a)).hom
      (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapId a)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (self.app a))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.app a)).hom
        (CategoryTheory.Bicategory.rightUnitor (self.app a)).inv)
-- Mathlib.Order.Category.LinOrd
LinOrd.dualEquiv_functor : LinOrd.dualEquiv.functor = LinOrd.dual
-- Mathlib.LinearAlgebra.Prod
/-- The second projection of a product is a linear map.  -/
LinearMap.snd : (R : Type u) →
  (M : Type v) →
    (M₂ : Type w) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid M₂] → [inst_3 : Module R M] → [inst_4 : Module R M₂] → M × M₂ →ₗ[R] M₂
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitSource.ematch.injEq : ∀ (origin origin_1 : Lean.Meta.Grind.Origin),
  (Lean.Meta.Grind.SplitSource.ematch origin = Lean.Meta.Grind.SplitSource.ematch origin_1) = (origin = origin_1)
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.rewritePre : optParam Bool false → Lean.Meta.Simp.Simproc
-- Mathlib.Data.ULift
ULift.instUnique : {α : Type u} → [Unique α] → Unique (ULift.{u_1, u} α)
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Special case of `fderivWithin_const_smul_of_invertible` over a division semiring: any constant
is allowed.

TODO: This would work for scalars in a `GroupWithZero` if we had a `DistribMulActionWithZero`
typeclass.  -/
fderivWithin_const_smul_field : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E} {R : Type u_4} [inst_5 : DivisionSemiring R] [inst_6 : Module R F] [inst_7 : SMulCommClass 𝕜 R F]
  [inst_8 : ContinuousConstSMul R F] (c : R),
  UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (c • f) s x = c • fderivWithin 𝕜 f s x
-- Mathlib.RingTheory.DedekindDomain.PID
/-- A Dedekind domain is a PID if its set of primes is finite.  -/
IsPrincipalIdealRing.of_finite_primes : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R], {I | I.IsPrime}.Finite → IsPrincipalIdealRing R
-- Init.Data.UInt.Lemmas
UInt16.sub_left_inj : ∀ {a b : UInt16} (c : UInt16), a - c = b - c ↔ a = b
-- Mathlib.AlgebraicGeometry.Group.Affine
AlgebraicGeometry.instGrpObjSpecAsOverSpec : {R A : CommRingCat} →
  [inst : HopfAlgebra ↑R ↑A] → CategoryTheory.GrpObj ((AlgebraicGeometry.Spec A).asOver (AlgebraicGeometry.Spec R))
-- Mathlib.Order.Interval.Finset.Defs
Finset.coe_Iio : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (a : α), ↑(Finset.Iio a) = Set.Iio a
-- Lean.Parser.Term
Lean.Parser.Term.whereFinally.formatter : Lean.PrettyPrinter.Formatter
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.find?_toArray_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} {v : β},
      Array.find? (fun x => cmp x.1 k == Ordering.eq) t.toArray = some (k', v) ↔ t.getKey? k = some k' ∧ t[k]? = some v
-- Mathlib.Algebra.Ring.InjSurj
/-- Pullback a `CommSemiring` instance along an injective function.  -/
Function.Injective.commSemiring : {R : Type u_1} →
  {S : Type u_2} →
    (f : S → R) →
      Function.Injective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : One S] →
                [inst_4 : SMul ℕ S] →
                  [inst_5 : Pow S ℕ] →
                    [inst_6 : NatCast S] →
                      [inst_7 : CommSemiring R] →
                        f 0 = 0 →
                          f 1 = 1 →
                            (∀ (x y : S), f (x + y) = f x + f y) →
                              (∀ (x y : S), f (x * y) = f x * f y) →
                                (∀ (n : ℕ) (x : S), f (n • x) = n • f x) →
                                  (∀ (x : S) (n : ℕ), f (x ^ n) = f x ^ n) → (∀ (n : ℕ), f ↑n = ↑n) → CommSemiring S
-- Init.NotationExtra
unexpandMkArray6 : Lean.PrettyPrinter.Unexpander
-- Mathlib.Topology.Algebra.Group.Basic
/-- Conjugation by a fixed element is continuous when `add` is continuous.  -/
IsTopologicalAddGroup.continuous_addConj : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Neg G] [inst_2 : Add G] [SeparatelyContinuousAdd G] (g : G),
  Continuous fun h => g + h + -g
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.isDPMorphism_iff : ∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  (hI : DividedPowers I) (hJ : DividedPowers J) (f : A →+* B),
  hI.IsDPMorphism hJ f ↔ Ideal.map f I ≤ J ∧ ∀ (n : ℕ), n ≠ 0 → ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Ioo_castSucc : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (a b : Fin n),
  ∏ i ∈ Finset.Ioo a.castSucc b.castSucc, f i = ∏ i ∈ Finset.Ioo a b, f i.castSucc
-- Aesop.Options.Internal
Aesop.Options'.mk.inj : ∀ {toOptions : Aesop.Options} {generateScript : Bool} {forwardMaxDepth? : Option ℕ} {toOptions_1 : Aesop.Options}
  {generateScript_1 : Bool} {forwardMaxDepth?_1 : Option ℕ},
  { toOptions := toOptions, generateScript := generateScript, forwardMaxDepth? := forwardMaxDepth? } =
      { toOptions := toOptions_1, generateScript := generateScript_1, forwardMaxDepth? := forwardMaxDepth?_1 } →
    toOptions = toOptions_1 ∧ generateScript = generateScript_1 ∧ forwardMaxDepth? = forwardMaxDepth?_1
-- Mathlib.Data.Countable.Defs
/-- A type `α` is countable if there exists an injective map `α → ℕ`.  -/
Countable.exists_injective_nat' : ∀ {α : Sort u} [self : Countable α], ∃ f, Function.Injective f
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- On morphisms with affine target, being a closed immersion is precisely having affine source
and being surjective on global sections.  -/
AlgebraicGeometry.IsClosedImmersion.hasAffineProperty : AlgebraicGeometry.HasAffineProperty @AlgebraicGeometry.IsClosedImmersion fun X x f [AlgebraicGeometry.IsAffine x] =>
  AlgebraicGeometry.IsAffine X ∧
    Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appTop f))
-- Mathlib.Computability.StateTransition
/-- A "proof" of the fact that `f` eventually reaches `b` in at most `m` steps when repeatedly
evaluated on `a`, remembering the number of steps it takes.  -/
StateTransition.EvalsToInTime : {σ : Type u_1} → (σ → Option σ) → σ → Option σ → ℕ → Type
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.startsWith_char_iff_exists_append : ∀ {c : Char} {s : String}, s.startsWith c = true ↔ ∃ t, s = String.singleton c ++ t
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.isOrtho_comm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E}, U ⟂ V ↔ V ⟂ U
-- Mathlib.Order.Preorder.Chain
IsChain.image_of_map_rel : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (f : α → β),
  (∀ (x y : α), r x y → s (f x) (f y)) → ∀ {c : Set α}, IsChain r c → IsChain s (f '' c)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.cancelDen.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr) (val : ℤ) (x n : Lean.Grind.Linarith.Var),
  sizeOf (Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.cancelDen c val x n) =
    1 + sizeOf c + sizeOf val + sizeOf x + sizeOf n
-- Mathlib.Algebra.Group.Invertible.Defs
mul_invOf_cancel_left' : ∀ {α : Type u} [inst : Monoid α] (a b : α) {x : Invertible a}, a * (⅟a * b) = b
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
MvPolynomial.universalFactorizationMap.congr_simp : ∀ (R : Type u_1) [inst : CommRing R] (n m k : ℕ) (hn : n = m + k),
  MvPolynomial.universalFactorizationMap R n m k hn = MvPolynomial.universalFactorizationMap R n m k hn
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- An alternate constructor for strictly unitary lax functors that does not
require the `mapId` fields, and that adapts the `map₂_leftUnitor` and
`map₂_rightUnitor` to the fact that the functor is strictly unitary.  -/
CategoryTheory.StrictlyUnitaryLaxFunctor.mk' : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.StrictlyUnitaryLaxFunctorCore B C → CategoryTheory.StrictlyUnitaryLaxFunctor B C
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mem_map : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N}
  {S : L.Substructure M} {y : N}, y ∈ FirstOrder.Language.Substructure.map f S ↔ ∃ x ∈ S, f x = y