mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasKernel S.g]
  [inst_3 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)],
  (CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernelOfHasCokernel S).H =
    CategoryTheory.Limits.cokernel (CategoryTheory.Limits.kernel.lift S.g S.f ⋯)
-- Init.Data.Option.Basic
Option.bind_none : ∀ {α : Type u_1} {β : Type u_2} (f : α → Option β), none.bind f = none
-- Mathlib.Algebra.Group.Equiv.Opposite
AddHom.toOpposite.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N)
  (hf : ∀ (x y : M), AddCommute (f x) (f y)), f.toOpposite hf = { toFun := AddOpposite.op ∘ ⇑f, map_add' := ⋯ }
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.lieQuotientLieRingModule : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              [inst_4 : LieRingModule L M] →
                (N : LieSubmodule R L M) → [inst_5 : LieAlgebra R L] → [LieModule R L M] → LieRingModule L (M ⧸ N)
-- Mathlib.Order.Sublocale
Sublocale.sInf_mem : ∀ {X : Type u_1} [inst : Order.Frame X] {S : Sublocale X} {s : Set X}, s ⊆ ↑S → sInf s ∈ S
-- Mathlib.FieldTheory.Normal.Closure
IntermediateField.normalClosureOperator_apply : ∀ (F : Type u_1) (L : Type u_3) [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L] [inst_3 : Normal F L]
  (K : IntermediateField F L),
  (IntermediateField.normalClosureOperator F L) K = IntermediateField.normalClosure F (↥K) L
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_algebraMap_nnreal : ∀ {A : Type u_2} [inst : Ring A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Algebra ℝ A]
  [inst_4 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_5 : PartialOrder A] [inst_6 : StarOrderedRing A]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] [StarModule ℝ A] (x : NNReal),
  CFC.abs ((algebraMap NNReal A) x) = (algebraMap NNReal A) x
-- Init.Data.BitVec.Lemmas
BitVec.getMsb?.eq_1 : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), x.getMsb? i = if h : i < w then some (x.getMsb ⟨i, h⟩) else none
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- **Alias** of `FunLike.coe_add`. -/
ContDiffMapSupportedIn.coe_add : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [IsAddApply F α β] (f g : F), ⇑(f + g) = ⇑f + ⇑g
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.MkSimpContextResult.ctx : Lean.Elab.Tactic.MkSimpContextResult → Lean.Meta.Simp.Context
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.coe_zero : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero β], ⇑0 = 0
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.faithfulSMul : ∀ {R' : Type u_1} {α : Type u_2} [inst : NonAssocSemiring R'] [inst_1 : SMul R' α] [FaithfulSMul R' α]
  (S : Subsemiring R'), FaithfulSMul (↥S) α
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.isClosedEmbedding : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.IsClosedImmersion f],
  Topology.IsClosedEmbedding ⇑f
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiffAddMonoidMorphism.mk.sizeOf_spec : ∀ {𝕜 : 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] {H' : Type u_5} [inst_4 : TopologicalSpace H']
  {E' : Type u_6} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] {I : ModelWithCorners 𝕜 E H}
  {I' : ModelWithCorners 𝕜 E' H'} {n : WithTop ℕ∞} {G : Type u_8} [inst_7 : TopologicalSpace G]
  [inst_8 : ChartedSpace H G] [inst_9 : AddMonoid G] {G' : Type u_9} [inst_10 : TopologicalSpace G']
  [inst_11 : ChartedSpace H' G'] [inst_12 : AddMonoid G'] [inst_13 : SizeOf 𝕜] [inst_14 : SizeOf H] [inst_15 : SizeOf E]
  [inst_16 : SizeOf H'] [inst_17 : SizeOf E'] [inst_18 : SizeOf G] [inst_19 : SizeOf G'] (toAddMonoidHom : G →+ G')
  (contMDiff_toFun : ContMDiff I I' n (↑toAddMonoidHom).toFun),
  sizeOf { toAddMonoidHom := toAddMonoidHom, contMDiff_toFun := contMDiff_toFun } = 1 + sizeOf toAddMonoidHom
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_erase_eq_iff_not_compare_eq_minKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {he : (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty = false},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.minKey he = t.minKey ⋯ ↔ ¬compare k (t.minKey ⋯) = Ordering.eq
-- Mathlib.Order.ULift
ULift.instCompl : {α : Type u} → [Compl α] → Compl (ULift.{v, u} α)
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haarMeasure_self : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] {K₀ : TopologicalSpace.PositiveCompacts G},
  (MeasureTheory.Measure.haarMeasure K₀) ↑K₀ = 1
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.instEquivLike : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {ρ : ContRepresentation R G V} → {σ : ContRepresentation R G W} → EquivLike (ρ.Equiv σ) V W
-- Mathlib.Algebra.Homology.SpectralObject.Differentials
CategoryTheory.Abelian.SpectralObject.Ψ_opcyclesMap : ∀ {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 l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k),
  CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂ →
    ∀ (f₂₃ : j ⟶ l) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ : ℤ)
      (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.Ψ_opcyclesMap._auto_1),
      CategoryTheory.CategoryStruct.comp (X.Ψ f₁ f₂ f₃ n₀ n₁ hn₁)
          (X.opcyclesMap f₁ f₂ f₁ f₂₃ (CategoryTheory.ComposableArrows.threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃) n₁) =
        0
-- Mathlib.Data.List.ToFinsupp
List.toFinsupp_eq_sum_mapIdx_single : ∀ {R : Type u_2} [inst : AddMonoid R] (l : List R) [inst_1 : DecidablePred fun x => l.getD x 0 ≠ 0],
  l.toFinsupp = (List.mapIdx (fun n r => fun₀ | n => r) l).sum
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_stalkMap_toSpec_assoc : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) (x : ↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toTopCat)
  {Z : CommRingCat} (h : ((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).presheaf.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).inv
      (CategoryTheory.CategoryStruct.comp
        ((AlgebraicGeometry.Spec.locallyRingedSpaceObj
                (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).presheaf.germ
          ⊤ ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).base) x) ⋯)
        (CategoryTheory.CategoryStruct.comp
          (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f) x)
          h)) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ 𝒜 f)
      (CategoryTheory.CategoryStruct.comp
        (((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).presheaf.Γgerm x) h)
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.neg.sizeOf_spec : ∀ (a : Int.Internal.Linear.Expr), sizeOf a.neg = 1 + sizeOf a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.coe_map_Δ' : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [inst_1 : W.IsElliptic] {A : Type v} [inst_2 : CommRing A]
  (f : R →+* A), ↑(W.map f).Δ' = f ↑W.Δ'
-- Mathlib.Combinatorics.Additive.CovBySMul
CovByVAdd.subset_right : ∀ {M : Type u_1} {X : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M X] {K : ℝ} {A B₁ B₂ : Set X},
  B₁ ⊆ B₂ → CovByVAdd M K A B₁ → CovByVAdd M K A B₂
-- Mathlib.Order.WellFoundedSet
Set.wellFoundedOn_range : ∀ {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {f : β → α},
  (Set.range f).WellFoundedOn r ↔ WellFounded (Function.onFun r f)
-- Lean.Data.JsonRpc
Lean.JsonRpc.Notification.mk : {α : Type u} → String → α → Lean.JsonRpc.Notification α
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_lt_of_countable_range : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : PartialOrder ι] {τ : Ω → WithTop ι}
  {f : MeasureTheory.Filtration ι m},
  MeasureTheory.IsStoppingTime f τ → (Set.range τ).Countable → ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_coeff_cert.eq_1 : ∀ (p p' : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.eq_coeff_cert p p' k = (p.beq' (p'.mul_k k)).and' (decide (k > 0))
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.isoFinYoneda.eq_1 : ∀ (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [inst : CategoryTheory.Limits.PreservesFiniteProducts F],
  LightCondensed.isoFinYoneda F =
    CategoryTheory.NatIso.ofComponents
      (fun X => LightCondensed.isoFinYonedaComponents F (FintypeCat.toLightProfinite.obj (Opposite.unop X))) ⋯
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.sum_coeff_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (f : MonoidAlgebra R M), f.coeff.sum MonoidAlgebra.single = f
-- Mathlib.Data.Int.Cast.Lemmas
Int.cast_inj : ∀ {α : Type u_3} [inst : AddGroupWithOne α] [CharZero α] {m n : ℤ}, ↑m = ↑n ↔ m = n
-- Init.Data.BitVec.Bitblast
/-- The remainder is strictly less than the denominator.  -/
BitVec.DivModState.Lawful.hrLtDivisor : ∀ {w : ℕ} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w},
  BitVec.DivModState.Lawful args qr → qr.r.toNat < args.d.toNat
-- Mathlib.Algebra.Category.Grp.Basic
/-- The underlying type.  -/
AddCommGrpCat.carrier : AddCommGrpCat → Type u
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.stVar.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} (v : σ) (l : List (Γ k)) (f : σ → Γ k),
  Turing.TM2to1.stVar v l (Turing.TM2to1.StAct.push f) = v
-- Std.Http.Data.URI.Basic
/-- Adds an already-encoded key-value pair to the query string.
 -/
Std.Http.URI.Query.insertEncoded : Std.Http.URI.Query → Std.Http.URI.EncodedQueryParam → Option Std.Http.URI.EncodedQueryParam → Std.Http.URI.Query
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.instQuasiIsoIntι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)],
  QuasiIso (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.ι✝ f n₀)
-- Mathlib.Data.Set.Function
Set.MapsTo.insert : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β},
  Set.MapsTo f s t → ∀ (x : α), Set.MapsTo f (insert x s) (insert (f x) t)
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₂_app_app_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (x x_1 x_2 : C),
  (((CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₂ C).app x).app x_1).app x_2 =
    (CategoryTheory.MonoidalCategoryStruct.associator x_1 x x_2).hom
-- Mathlib.FieldTheory.Normal.Closure
IntermediateField.normal_iff_normalClosure_eq : ∀ {F : Type u_1} {L : Type u_3} [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L] [Normal F L]
  {K : IntermediateField F L}, Normal F ↥K ↔ IntermediateField.normalClosure F (↥K) L = K
-- Init.Core
ByteArray.mk.inj : ∀ {data data_1 : Array UInt8}, { data := data } = { data := data_1 } → data = data_1
-- Mathlib.Analysis.Calculus.Gradient.Basic
DifferentiableWithinAt.hasGradientWithinAt : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {x : F} {s : Set F},
  DifferentiableWithinAt 𝕜 f s x → HasGradientWithinAt f (gradientWithin f s x) s x
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isNat_intCast : ∀ {R : Type u_1} [inst : Ring R] (n : ℤ) (m : ℕ), Mathlib.Meta.NormNum.IsNat n m → Mathlib.Meta.NormNum.IsNat (↑n) m
-- Mathlib.GroupTheory.Descent
/-- If `M` is an additive monoid and `n : ℕ`, `h : M → ℝ` satisfy
* for all `x : M`, `h (n • x) ≥ b * h x - c₀`,
* for all `B : ℝ`, there are only finitely many `x : M` such that `h x ≤ B`,

where `1 < b` and `c₀` are real numbers, then the set of elements of finite order in `M`
is finite.  -/
AddMonoid.finite_set_isOfFiniteOrder_of_descent : ∀ {M : Type u_1} [inst : AddMonoid M] {n : ℕ} {h : M → ℝ} {b c₀ : ℝ},
  1 < b → (∀ (x : M), b * h x - c₀ ≤ h (n • x)) → ∀ [Northcott h], Finite ↑{x | IsOfFinAddOrder x}
-- Mathlib.Geometry.Manifold.Instances.Icc
/-- The inclusion map from of a closed segment to `ℝ` is smooth in the manifold sense.  -/
contMDiff_subtypeVal_Icc : ∀ {x y : ℝ} [h : Fact (x < y)] {n : WithTop ℕ∞},
  ContMDiff (modelWithCornersEuclideanHalfSpace 1) (modelWithCornersSelf ℝ ℝ) n fun z => ↑z
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- Two finite measures on a Borel space are equal if they agree on all closed-open intervals.  If
`α` is a conditionally complete linear order with no top element,
`MeasureTheory.Measure.ext_of_Ico` is an extensionality lemma with weaker assumptions on `μ` and
`ν`.  -/
MeasureTheory.Measure.ext_of_Ico_finite : ∀ {α : Type u_5} [inst : TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α]
  [inst_2 : LinearOrder α] [OrderTopology α] [BorelSpace α] (μ ν : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure μ],
  μ Set.univ = ν Set.univ → (∀ ⦃a b : α⦄, a < b → μ (Set.Ico a b) = ν (Set.Ico a b)) → μ = ν
-- Mathlib.Topology.Defs.Filter
/-- If `f` is a filter, then `Filter.lim f` is a limit of the filter, if it exists.  -/
Filter.lim : {X : Type u_1} → [TopologicalSpace X] → [Nonempty X] → Filter X → X
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
/-- `LinearMap.fst` as an isometry, when the second space has the zero quadratic form.  -/
QuadraticMap.Isometry.fst : {R : Type u_2} →
  {M₁ : Type u_3} →
    (M₂ : Type u_4) →
      {P : Type u_7} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid P] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] → [inst_6 : Module R P] → (Q₁ : QuadraticMap R M₁ P) → Q₁.prod 0 →qᵢ Q₁
-- Mathlib.Combinatorics.Colex
Finset.lt_geomSum_of_mem : ∀ {s : Finset ℕ} {n a : ℕ}, 2 ≤ n → a ∈ s → a < ∑ i ∈ s, n ^ i
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isSeparator_coprod_of_isSeparator_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] (G H : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct G H],
  CategoryTheory.IsSeparator H → CategoryTheory.IsSeparator (G ⨿ H)
-- Init.Prelude
HAppend.mk : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → (α → β → γ) → HAppend α β γ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β}, a ∈ t.insertIfNew k v ↔ cmp k a = Ordering.eq ∨ a ∈ t
-- Lean.Meta.Tactic.Simp.Main
/-- Simplify the given goal target (aka type). Return `none` if the goal was closed. Return `some mvarId'` otherwise,
where `mvarId'` is the simplified new goal.  -/
Lean.Meta.simpTarget : Lean.MVarId →
  Lean.Meta.Simp.Context →
    optParam Lean.Meta.Simp.SimprocsArray #[] →
      optParam (Option Lean.Meta.Simp.Discharge) none →
        optParam Bool true → optParam Lean.Meta.Simp.Stats { } → Lean.MetaM (Option Lean.MVarId × Lean.Meta.Simp.Stats)
-- Mathlib.Tactic.Linter.TextBased
/-- The underlying `StyleError`  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.ErrorContext.error : Mathlib.Linter.TextBased.ErrorContext✝ → Mathlib.Linter.TextBased.StyleError✝
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
/-- Performing a simplicial insertion in a list is the same as composition on the right by the
corresponding degeneracy operator.  -/
SimplexCategoryGenRel.standardσ_simplicialInsert : ∀ {m : ℕ} (L : List ℕ),
  SimplexCategoryGenRel.IsAdmissible (m + 1) L →
    ∀ j < m + 1,
      ∀ (m₁ : ℕ) (hm₁ : m + L.length + 1 = m₁),
        SimplexCategoryGenRel.standardσ (SimplexCategoryGenRel.simplicialInsert j L) ⋯ =
          CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.standardσ L ⋯)
            (SimplexCategoryGenRel.σ (Fin.ofNat (m + 1) j))
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_unitOfList_le : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  (Std.ExtDTreeMap.Const.unitOfList l cmp).size ≤ l.length
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Scalar multiplication by any element send `0` to `0`.  -/
MulActionWithZero.smul_zero : ∀ {M₀ : Type u_2} {A : Type u_7} {inst : MonoidWithZero M₀} {inst_1 : Zero A} [self : MulActionWithZero M₀ A] (r : M₀),
  r • 0 = 0
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
ContinuousLinearMap.add_compLp : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {𝕜 : Type u_6} {𝕜' : Type u_7}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' F] {σ : 𝕜 →+* 𝕜'} [inst_6 : RingHomIsometric σ] (L L' : E →SL[σ] F)
  (f : ↥(MeasureTheory.Lp E p μ)), (L + L').compLp f = L.compLp f + L'.compLp f
-- Mathlib.Algebra.Lie.Abelian
LieModule.mem_ker : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (x : L),
  x ∈ LieModule.ker R L M ↔ ∀ (m : M), ⁅x, m⁆ = 0
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.mem_zero : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {x : M}, x ∈ 0 ↔ x = 0
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.toList.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Batteries.AssocList α β → Sort u_3) →
      (x : Batteries.AssocList α β) →
        (Unit → motive Batteries.AssocList.nil) →
          ((a : α) → (b : β) → (es : Batteries.AssocList α β) → motive (Batteries.AssocList.cons a b es)) → motive x
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instSMulCommClass_2 : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_3} {M : Type u_5} [inst_1 : TopologicalSpace M]
  [inst_2 : SMul R M] [inst_3 : ContinuousConstSMul R M] [inst_4 : Mul M] [inst_5 : ContinuousMul M]
  [SMulCommClass M R M], SMulCommClass C(α, M) R C(α, M)
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
fn_max_add_fn_min : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : AddCommSemigroup β] (f : α → β) (a b : α),
  f (max a b) + f (min a b) = f a + f b
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.wfImp_modifyₘ : ∀ {α : Type u} {β : Type v} {m : Std.DHashMap.Internal.Raw₀ α fun x => β} [inst : BEq α] [EquivBEq α]
  [inst_2 : Hashable α] [LawfulHashable α],
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : β → β}, Std.DHashMap.Internal.Raw.WFImp ↑(Std.DHashMap.Internal.Raw₀.Const.modifyₘ m a f)
-- Std.Async.System
Std.Async.System.instOrdGroupId.ord : Std.Async.System.GroupId → Std.Async.System.GroupId → Ordering
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Precoverage.ZeroHypercover.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  (toPreZeroHypercover toPreZeroHypercover_1 : CategoryTheory.PreZeroHypercover S)
  (e_toPreZeroHypercover : toPreZeroHypercover = toPreZeroHypercover_1)
  (mem₀ : toPreZeroHypercover.presieve₀ ∈ J.coverings S),
  { toPreZeroHypercover := toPreZeroHypercover, mem₀ := mem₀ } =
    { toPreZeroHypercover := toPreZeroHypercover_1, mem₀ := ⋯ }
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.map_ideal : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) {U V : ↑X.affineOpens} (h : U ≤ V),
  Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE h).op)) (I.ideal V) = I.ideal U
-- Init.Data.Nat.Bitwise.Lemmas
Nat.bitwise_div_two_pow : ∀ {f : Bool → Bool → Bool} {x y n : ℕ},
  autoParam (f false false = false) Nat.bitwise_div_two_pow._auto_9 →
    Nat.bitwise f x y / 2 ^ n = Nat.bitwise f (x / 2 ^ n) (y / 2 ^ n)
-- Mathlib.RingTheory.MvPowerSeries.GaussNorm
MvPowerSeries.gaussNorm_le_mul : ∀ {R : Type u_1} {σ : Type u_2} (v : R → ℝ) (c : σ → ℝ) [inst : Ring R] [inst_1 : DecidableEq σ]
  (f g : MvPowerSeries σ R),
  (∀ (a b : R), v (a * b) = v a * v b) →
    IsNonarchimedean v →
      (∀ (a : R), v a = v (-a)) →
        MvPowerSeries.HasGaussNorm v c (f * g) →
          (∃ i j,
              MvPowerSeries.AchievesGaussNorm v c f i ∧
                MvPowerSeries.AchievesGaussNorm v c g j ∧
                  ∀ p ∈ Finset.HasAntidiagonal.antidiagonal (i + j),
                    p ≠ (i, j) →
                      v ((MvPowerSeries.coeff p.1) f * (MvPowerSeries.coeff p.2) g) <
                        v ((MvPowerSeries.coeff i) f) * v ((MvPowerSeries.coeff j) g)) →
            MvPowerSeries.gaussNorm v c f * MvPowerSeries.gaussNorm v c g ≤ MvPowerSeries.gaussNorm v c (f * g)
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.pow_ne_top_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MonoidWithZero α] [inst_2 : NoZeroDivisors α] [inst_3 : Nontrivial α]
  {x : WithTop α} {n : ℕ}, x ^ n ≠ ⊤ ↔ x ≠ ⊤ ∨ n = 0
-- Mathlib.Algebra.GradedMonoid
GradedMonoid.GMonoid.gnpowRec_succ : ∀ {ι : Type u_1} {A : ι → Type u_2} [inst : AddMonoid ι] [inst_1 : GradedMonoid.GMul A] [inst_2 : GradedMonoid.GOne A]
  (n : ℕ) (a : GradedMonoid A),
  GradedMonoid.mk (n.succ • a.fst) (GradedMonoid.GMonoid.gnpowRec n.succ a.snd) =
    ⟨n • a.fst, GradedMonoid.GMonoid.gnpowRec n a.snd⟩ * a
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {he : t.isEmpty = false} {km : α},
  t.max he = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Data.TwoPointing
TwoPointing.bool_snd : TwoPointing.bool.toProd.2 = true
-- Init.Data.Int.DivMod.Lemmas
Int.add_mul_fmod_self_left : ∀ (a b c : ℤ), (a + b * c).fmod b = a.fmod b