mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Immersion
/-- A choice of chart on the domain `M` of an immersion `f` at `x`:
w.r.t. this chart and the data `h.codChart` and `h.equiv`,
`f` will look like an inclusion `u ↦ (u, 0)` in these extended charts.
The particular chart is arbitrary, but this choice matches the witnesses given by
`h.codChart` and `h.codChart`.  -/
Manifold.IsImmersionAtOfComplement.domChart : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {E'' : Type u} →
        {F : Type u_5} →
          [inst_1 : NormedAddCommGroup E] →
            [inst_2 : NormedSpace 𝕜 E] →
              [inst_3 : NormedAddCommGroup E''] →
                [inst_4 : NormedSpace 𝕜 E''] →
                  [inst_5 : NormedAddCommGroup F] →
                    [inst_6 : NormedSpace 𝕜 F] →
                      {H : Type u_7} →
                        [inst_7 : TopologicalSpace H] →
                          {G : Type u_9} →
                            [inst_8 : TopologicalSpace G] →
                              {I : ModelWithCorners 𝕜 E H} →
                                {J : ModelWithCorners 𝕜 E'' G} →
                                  {M : Type u_11} →
                                    [inst_9 : TopologicalSpace M] →
                                      [inst_10 : ChartedSpace H M] →
                                        {N : Type u_13} →
                                          [inst_11 : TopologicalSpace N] →
                                            [inst_12 : ChartedSpace G N] →
                                              {n : WithTop ℕ∞} →
                                                {f : M → N} →
                                                  {x : M} →
                                                    Manifold.IsImmersionAtOfComplement F I J n f x →
                                                      OpenPartialHomeomorph M H
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.laplacianCLM_eq_sum : ∀ {ι : Type u_1} {E : Type u_6} {V₁ : Type u_8} {V₂ : Type u_9} {V₃ : Type u_10} [inst : LineDeriv E V₁ V₂]
  [inst_1 : LineDeriv E V₂ V₃] [inst_2 : AddCommGroup V₁] [inst_3 : AddCommGroup V₂] [inst_4 : AddCommGroup V₃]
  [inst_5 : NormedAddCommGroup E] [inst_6 : InnerProductSpace ℝ E] [inst_7 : FiniteDimensional ℝ E]
  [inst_8 : Module ℝ V₁] [inst_9 : Module ℝ V₂] [inst_10 : Module ℝ V₃] [inst_11 : TopologicalSpace V₁]
  [inst_12 : TopologicalSpace V₂] [inst_13 : TopologicalSpace V₃] [inst_14 : IsTopologicalAddGroup V₃]
  [inst_15 : LineDerivAdd E V₁ V₂] [inst_16 : LineDerivSMul ℝ E V₁ V₂] [inst_17 : ContinuousLineDeriv E V₁ V₂]
  [inst_18 : LineDerivAdd E V₂ V₃] [inst_19 : LineDerivSMul ℝ E V₂ V₃] [inst_20 : ContinuousLineDeriv E V₂ V₃]
  [LineDerivLeftSMul ℝ E V₁ V₂] [LineDerivLeftSMul ℝ E V₂ V₃] [inst_23 : Fintype ι] (v : OrthonormalBasis ι ℝ E)
  (f : V₁), (LineDeriv.laplacianCLM ℝ E V₁) f = ∑ i, LineDeriv.lineDerivOp (v i) (LineDeriv.lineDerivOp (v i) f)
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- The closure of a bounded set is bounded.  -/
Bornology.IsVonNBounded.closure : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [T1Space E] [RegularSpace E] [ContinuousConstSMul 𝕜 E] {a : Set E},
  Bornology.IsVonNBounded 𝕜 a → Bornology.IsVonNBounded 𝕜 (closure a)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.c₆_of_isCharThreeJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF],
  W.c₆ = -64 * W.a₂ ^ 3 - 864 * W.a₆
-- Mathlib.Analysis.Meromorphic.Basic
/-- Eta-expanded form of `MeromorphicAt.zpow` -/
MeromorphicAt.fun_zpow : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {f : 𝕜 → 𝕜'}, MeromorphicAt f x → ∀ (n : ℤ), MeromorphicAt (fun i => f i ^ n) x
-- Mathlib.Analysis.Analytic.IsolatedZeros
AnalyticAt.eventually_eq_or_eventually_ne : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜},
  AnalyticAt 𝕜 f z₀ →
    AnalyticAt 𝕜 g z₀ → (∀ᶠ (z : 𝕜) in nhds z₀, f z = g z) ∨ ∀ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z ≠ g z
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.mem_top : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {x : A}, x ∈ ⊤
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.Hom.mk.sizeOf_spec : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  {R R' : Φ.RightResolution X₂} [inst_2 : SizeOf C₁] [inst_3 : SizeOf C₂]
  [inst_4 : ⦃X Y : C₁⦄ → (x : X ⟶ Y) → SizeOf (W₁ x)] [inst_5 : ⦃X Y : C₂⦄ → (x : X ⟶ Y) → SizeOf (W₂ x)]
  (f : R.X₁ ⟶ R'.X₁)
  (comm :
    autoParam (CategoryTheory.CategoryStruct.comp R.w (Φ.functor.map f) = R'.w)
      CategoryTheory.LocalizerMorphism.RightResolution.Hom.comm._autoParam),
  sizeOf { f := f, comm := comm } = 1 + sizeOf f + sizeOf comm
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- The `EvalConfigItemHandlerKind.wildcard` handler for this trie position's key.  -/
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.wildcard? : Lean.Elab.ConfigEval.HandlerTrie✝ → Option Lean.Elab.ConfigEval.EvalConfigItemHandler
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₃ : Lean.Expr → Lean.Expr → Aesop.EqualUpToIds.ExprsEqualUpToIdsM Bool
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.isEmpty_alter_eq_isEmpty_erase : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β},
  m.WF →
    (Std.DHashMap.Raw.Const.alter m k f).isEmpty = ((m.erase k).isEmpty && (f (Std.DHashMap.Raw.Const.get? m k)).isNone)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.zsmul_eq_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SubtractionMonoid α] {s : Finset α} {n : ℤ}, n • s = ∅ ↔ s = ∅ ∧ n ≠ 0
-- Mathlib.Topology.Compactness.SigmaCompact
/-- The minimal `n` such that `x ∈ K n`.  -/
CompactExhaustion.find : {X : Type u_1} → [inst : TopologicalSpace X] → CompactExhaustion X → X → ℕ
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofTermInfo.inj : ∀ {i i_1 : Lean.Elab.TermInfo}, Lean.Elab.Info.ofTermInfo i = Lean.Elab.Info.ofTermInfo i_1 → i = i_1
-- Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic
_private.Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic.0.ProbabilityTheory.HasIndepIncrements.indepFun_sub_sub.match_1_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (x : ℕ) → motive x),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | x => h_3 x) =
    h_1 ()
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.toFinsupp_comp_toFreeAbelianGroup : ∀ {X : Type u_1}, FreeAbelianGroup.toFinsupp.comp Finsupp.toFreeAbelianGroup = AddMonoidHom.id (X →₀ ℤ)
-- Mathlib.Algebra.Module.LinearMap.Index
_private.Mathlib.Algebra.Module.LinearMap.Index.0.LinearMap.index.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommGroup M] [inst_1 : AddCommGroup N] {R : Type u_3} [inst_2 : Ring R]
  [inst_3 : Module R M] [inst_4 : Module R N] (f : M →ₗ[R] N),
  f.index = ↑(Module.finrank R ↥f.ker) - ↑(Module.finrank R (N ⧸ f.range))
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.presheafIso_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ ℱ' : CategoryTheory.Sheaf K A} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) (X : Dᵒᵖ),
  (CategoryTheory.Functor.IsCoverDense.presheafIso i).hom.app X =
    CategoryTheory.yoneda.preimage ((CategoryTheory.Functor.IsCoverDense.sheafYonedaHom i.hom).app X)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_map_of_isNormal : ∀ {f : Ordinal.{u_1} → Ordinal.{u_1}}, Order.IsNormal f → ∀ {a : Ordinal.{u_1}}, Order.IsSuccLimit a → (f a).cof = a.cof
-- Std.Time.DateTime.PlainDateTime
/-- Subtracts `Month.Offset` from a `PlainDateTime`, it clips the day to the last valid day of that month.
 -/
Std.Time.PlainDateTime.subMonthsClip : Std.Time.PlainDateTime → Std.Time.Month.Offset → Std.Time.PlainDateTime
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation.Rels.add : {R : Type u} → {ι : Type u_4} → {M : Type u_5} → (ι → M) → ι → M → M → exteriorPower.presentation.Rels R ι M
-- Mathlib.Topology.CompactOpen
ContinuousMap.homeoFnOfDiscrete_symm_apply : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : DiscreteTopology X]
  (f : X → Y), ⇑(ContinuousMap.homeoFnOfDiscrete.symm f) = f
-- Mathlib.LinearAlgebra.Matrix.PosDef
/-- A matrix `M : Matrix n n R` is positive definite if it is Hermitian
and `xᴴMx` is greater than zero for all nonzero `x`.  -/
Matrix.PosDef : {n : Type u_2} → {R : Type u_3} → [inst : Ring R] → [PartialOrder R] → [StarRing R] → Matrix n n R → Prop
-- Lean.Environment
Lean.Kernel.Exception.funExpected : Lean.Kernel.Environment → Lean.LocalContext → Lean.Expr → Lean.Kernel.Exception
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
/-- An auxiliary submodule used to store the half-applied values of `f`.
This is the span of elements `f'` such that `∃ x m₂, ∀ m₁, f' m₁ = f m₁ m₂ * x`.  -/
_private.Mathlib.LinearAlgebra.CliffordAlgebra.Even.0.CliffordAlgebra.even.lift.S : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {Q : QuadraticForm R M} →
            {A : Type u_3} →
              [inst_3 : Ring A] → [inst_4 : Algebra R A] → CliffordAlgebra.EvenHom Q A → Submodule R (M →ₗ[R] A)
-- Lean.Exception
Lean.Exception.error.injEq : ∀ (ref : Lean.Syntax) (msg : Lean.MessageData) (ref_1 : Lean.Syntax) (msg_1 : Lean.MessageData),
  (Lean.Exception.error ref msg = Lean.Exception.error ref_1 msg_1) = (ref = ref_1 ∧ msg = msg_1)
-- Mathlib.NumberTheory.Padics.PadicNumbers
/-- `Padic.valuation` lifts the `p`-adic valuation on rationals to `ℚ_[p]`.  -/
Padic.valuation : {p : ℕ} → [hp : Fact (Nat.Prime p)] → ℚ_[p] → ℤ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k : α} {fallback : β},
  (Std.TreeMap.filter f t).getD k fallback = (t[k]?.pfilter fun x h' => f (t.getKey k ⋯) x).getD fallback
-- Std.Internal.Do.WP.Basic
_private.Std.Internal.Do.WP.Basic.0.EStateM.bind.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (a : α) (s : σ)
  (h_1 : (a : α) → (s : σ) → motive (EStateM.Result.ok a s))
  (h_2 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)),
  (match EStateM.Result.ok a s with
    | EStateM.Result.ok a s => h_1 a s
    | EStateM.Result.error e s => h_2 e s) =
    h_1 a s
-- Mathlib.RingTheory.KrullDimension.Zero
ringKrullDimZero_iff_ringKrullDim_eq_zero : ∀ {R : Type u_1} [inst : CommSemiring R] [Nontrivial R], Ring.KrullDimLE 0 R ↔ ringKrullDim R = 0
-- Mathlib.Geometry.RingedSpace.SheafedSpace
/-- The trivial `unit`-valued sheaf on any topological space.  -/
AlgebraicGeometry.SheafedSpace.unit : TopCat → AlgebraicGeometry.SheafedSpace (CategoryTheory.Discrete Unit)
-- Mathlib.Order.Filter.Finite
Filter.mem_biInf_principal : ∀ {α : Type u} {ι : Type u_2} {p : ι → Prop} {s : ι → Set α} {t : Set α},
  t ∈ ⨅ i, ⨅ (_ : p i), Filter.principal (s i) ↔ ∃ I, I.Finite ∧ (∀ i ∈ I, p i) ∧ ⋂ i ∈ I, s i ⊆ t
-- Mathlib.RepresentationTheory.Invariants
Representation.instIsTrivialSubtypeMemSubgroupSubmoduleInvariantsCompLinearMapIdSubtypeToInvariants : ∀ {k : Type u_1} {G : Type u_2} [inst : CommRing k] [inst_1 : Group G] {V : Type u_5} [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (S : Subgroup G) [inst_4 : S.Normal],
  Representation.IsTrivial (MonoidHom.comp (ρ.toInvariants S) S.subtype)
-- Mathlib.Analysis.Seminorm
Seminorm.restrictScalars_closedBall : ∀ (𝕜 : Type u_3) {E : Type u_7} {𝕜' : Type u_12} [inst : NormedField 𝕜] [inst_1 : SeminormedRing 𝕜']
  [inst_2 : SMul 𝕜 𝕜'] [inst_3 : NormSMulClass 𝕜 𝕜'] [inst_4 : NormOneClass 𝕜'] [inst_5 : AddCommGroup E]
  [inst_6 : Module 𝕜' E] [inst_7 : SMul 𝕜 E] [inst_8 : IsScalarTower 𝕜 𝕜' E] (p : Seminorm 𝕜' E),
  (Seminorm.restrictScalars 𝕜 p).closedBall = p.closedBall
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.addOrderOf_coe_rat : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)] {q : ℚ},
  addOrderOf ↑(↑q * p) = q.den
-- Mathlib.Tactic.NormNum.Result
/-- Constructs a `Result` out of a raw rat cast.
Assumes `e` is a raw rat cast expression denoting `n`.  -/
Mathlib.Meta.NormNum.Result.ofRawRat : {u : Lean.Level} →
  {α : Q(Type u)} → ℚ → (e : Q(«$α»)) → optParam (Option Lean.Expr) none → Mathlib.Meta.NormNum.Result e
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip.0.Std.IterM.step_intermediateZip.match_3.eq_1 : ∀ {α₁ β₁ : Type u_1} {m : Type u_1 → Type u_2} [inst : Std.Iterator α₁ m β₁]
  (motive : Option { out // ∃ it, it.IsPlausibleOutput out } → Sort u_3) (h_1 : Unit → motive none)
  (h_2 : (out₁ : { out // ∃ it, it.IsPlausibleOutput out }) → motive (some out₁)),
  (match none with
    | none => h_1 ()
    | some out₁ => h_2 out₁) =
    h_1 ()
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.trans_toLinearEquiv : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : AddCommMonoid C] [inst_4 : Module R A] [inst_5 : Module R B]
  [inst_6 : Module R C] [inst_7 : CoalgebraStruct R A] [inst_8 : CoalgebraStruct R B] [inst_9 : CoalgebraStruct R C]
  {e₁₂ : A ≃ₗc[R] B} {e₂₃ : B ≃ₗc[R] C}, (e₁₂.trans e₂₃).toLinearEquiv = e₁₂.toLinearEquiv ≪≫ₗ e₂₃.toLinearEquiv
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
/-- For a spectral object indexed by a preorder, this is the map
`E^{n₁}(i₀ ≤ i₂ ≤ i₃ ≤ i₄) ⟶ E^{n₁}(i₁ ≤ i₂ ≤ i₃ ≤ i₄)`.  -/
CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀' : {C : Type u_1} →
  {ι' : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        [inst_2 : Preorder ι'] →
          (X' : CategoryTheory.Abelian.SpectralObject C ι') →
            (i₀ i₁ i₂ i₃ i₄ : ι') →
              (hi₀₁ : i₀ ≤ i₁) →
                (hi₁₂ : i₁ ≤ i₂) →
                  (hi₂₃ : i₂ ≤ i₃) →
                    (hi₃₄ : i₃ ≤ i₄) →
                      (n₀ n₁ n₂ : ℤ) →
                        (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'._auto_1) →
                          (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'._auto_3) →
                            X'.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE hi₂₃) (CategoryTheory.homOfLE hi₃₄)
                                n₀ n₁ n₂ hn₁ hn₂ ⟶
                              X'.E (CategoryTheory.homOfLE hi₁₂) (CategoryTheory.homOfLE hi₂₃)
                                (CategoryTheory.homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.GroupTheory.GroupExtension.Basic
AddGroupExtension.Section.add_add_add_neg_mem_range_inl : ∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  {S : AddGroupExtension N E G} (σ : S.Section) (g₁ g₂ : G), σ g₁ + σ g₂ + -σ (g₁ + g₂) ∈ S.inl.range
-- Mathlib.RingTheory.Ideal.Maps
Ideal.coe_piOrderIso_symm_apply : ∀ {ι : Type u_4} {R : ι → Type u_5} [inst : (i : ι) → Semiring (R i)] [inst_1 : Finite ι] (a : (i : ι) → Ideal (R i)),
  ↑((RelIso.symm Ideal.piOrderIso) a) = {r | ∀ (i : ι), r i ∈ a i}
-- Init.Data.Array.Subarray
/-- Checks whether all of the elements in a subarray satisfy a Boolean predicate.

The elements are tested starting at the lowest index and moving up. The search terminates as soon as
an element that does not satisfy the predicate is found.
 -/
Subarray.all : {α : Type u} → (α → Bool) → Subarray α → Bool
-- Mathlib.Analysis.Asymptotics.LinearGrowth
LinearGrowth.linearGrowthInf_zero : LinearGrowth.linearGrowthInf 0 = 0
-- Mathlib.Algebra.Group.Finsupp
Finsupp.single_add : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (a : ι) (b₁ b₂ : M),
  (fun₀ | a => b₁ + b₂) = (fun₀ | a => b₁) + fun₀ | a => b₂
-- Mathlib.LinearAlgebra.Complex.Module
selfAdjoint.realPart_coe : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  {x : ↥(selfAdjoint A)}, realPart ↑x = x
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.smul_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (k : R)
  (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂),
  (k • z₁).comp z₂ h = k • z₁.comp z₂ h
-- Mathlib.Analysis.Normed.Operator.Conformal
IsConformalMap.smul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : NormedField R] [inst_1 : SeminormedAddCommGroup M]
  [inst_2 : SeminormedAddCommGroup N] [inst_3 : NormedSpace R M] [inst_4 : NormedSpace R N] {f : M →L[R] N},
  IsConformalMap f → ∀ {c : R}, c ≠ 0 → IsConformalMap (c • f)
-- Mathlib.Algebra.Ring.CentroidHom
/-- `id` as a `CentroidHom`.  -/
CentroidHom.id : (α : Type u_5) → [inst : NonUnitalNonAssocSemiring α] → CentroidHom α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_insert : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  (↑m).WF → ∀ {k a : α} {v : β k}, (m.insert k v).getKey! a = if (k == a) = true then k else m.getKey! a
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.freeVarFinset.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u'} [inst : DecidableEq α] (x : ℕ) (t₁ t₂ : L.Term (α ⊕ Fin x)),
  (FirstOrder.Language.BoundedFormula.equal t₁ t₂).freeVarFinset = t₁.varFinsetLeft ∪ t₂.varFinsetLeft
-- Init.Data.Nat.Dvd
Nat.dvd_zero : ∀ (a : ℕ), a ∣ 0
-- Init.Data.Order.Lemmas
Std.le_refl : ∀ {α : Type u} [inst : LE α] [Std.Refl fun x1 x2 => x1 ≤ x2] (a : α), a ≤ a
-- Mathlib.Data.Fin.SuccPred
Fin.one_succAbove_zero : ∀ {n : ℕ}, Fin.succAbove 1 0 = 0
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.instCompatibleSMulRat : ∀ {R : Type u_8} {M : Type u_9} {N : Type u_10} [inst : CommSemiring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Module R M] [inst_4 : Module R N] [inst_5 : Module ℚ M] [inst_6 : Module ℚ N],
  TensorProduct.CompatibleSMul R ℚ M N
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_map : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  [inst : Std.TransOrd α] [inst_1 : Std.LawfulEqOrd α] {f : (a : α) → β a → γ a} {k : α} (h : t.WF)
  {h' : k ∈ Std.DTreeMap.Internal.Impl.map f t}, (Std.DTreeMap.Internal.Impl.map f t).get k h' = f k (t.get k ⋯)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.or_and_distrib_left : ∀ (x y z : ℕ), x ||| y &&& z = (x ||| y) &&& (x ||| z)
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- To check that a function is `n` times continuously differentiable, it suffices to check that its
first `n` derivatives are differentiable. This is slightly too strong as the condition we
require on the `n`-th derivative is differentiability instead of continuity, but it has the
advantage of avoiding the discussion of continuity in the proof (and for `n = ∞` this is optimal).
 -/
contDiffOn_of_differentiableOn_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {n : ℕ∞},
  (∀ (m : ℕ), ↑m ≤ n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s) → ContDiffOn 𝕜 (↑n) f s
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.counitApp.congr_simp : ∀ {P : TopCat → Prop} [inst : ∀ (S : CompHausLike P) (p : ↑S.toTop → Prop), CompHausLike.HasProp P (Subtype p)]
  [inst_1 : CompHausLike.HasProp P PUnit.{u + 1}] [inst_2 : CompHausLike.HasExplicitFiniteCoproducts P]
  (Y : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w)))
  [inst_3 : CategoryTheory.Limits.PreservesFiniteProducts Y],
  CompHausLike.LocallyConstant.counitApp Y = CompHausLike.LocallyConstant.counitApp Y
-- Lean.Elab.DocString
/-- Runs a documentation elaborator in a declaration's context, discarding changes made to the
environment.
 -/
Lean.Doc.DocM.exec : {α : Type} →
  Lean.Name →
    Lean.Syntax →
      Lean.Doc.DocM α →
        optParam Lean.Doc.SuggestionMode Lean.Doc.SuggestionMode.interactive →
          Lean.Elab.TermElabM (α × Array Lean.Doc.DeferredCheck)
-- Mathlib.Algebra.Order.Hom.Basic
/-- `GroupSeminormClass F α` states that `F` is a type of `β`-valued seminorms on the group `α`.

You should extend this class when you extend `GroupSeminorm`.  -/
GroupSeminormClass : (F : Type u_7) →
  (α : outParam (Type u_8)) →
    (β : outParam (Type u_9)) → [Group α] → [AddCommMonoid β] → [PartialOrder β] → [FunLike F α β] → Prop
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentChange.delete : Lean.Lsp.DeleteFile → Lean.Lsp.DocumentChange
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.mk'.sizeOf_spec : ∀ {X : SSet} {A : X.Subcomplex} (toN : X.N) (notMem : toN.simplex ∉ A.obj (Opposite.op { len := toN.dim })),
  sizeOf { toN := toN, notMem := notMem } = 1 + sizeOf toN
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_add_natCast' : ∀ {y : ℝ} {n : ℕ}, y + ↑n ≠ 0 → ∀ (x : NNReal), x ^ (y + ↑n) = x ^ y * x ^ n
-- Mathlib.NumberTheory.Transcendental.Liouville.Residual
/-- **Alias** of `setOfPred_liouville_eq_irrational_inter_iInter_iUnion`. -/
setOf_liouville_eq_irrational_inter_iInter_iUnion : {x | Liouville x} = {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), Metric.ball (↑a / ↑b) (1 / ↑b ^ n)
-- Mathlib.Data.EReal.Basic
EReal.coe_ne_one : ∀ {x : ℝ}, ↑x ≠ 1 ↔ x ≠ 1
-- Lean.Data.Lsp.Workspace
Lean.Lsp.DidChangeWatchedFilesRegistrationOptions.mk.sizeOf_spec : ∀ (watchers : Array Lean.Lsp.FileSystemWatcher), sizeOf { watchers := watchers } = 1 + sizeOf watchers
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m.contains a = false → Std.DHashMap.Raw.Const.get? m a = none
-- Mathlib.Data.List.MinMax
List.maximum_eq_bot : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLT α] {l : List α}, l.maximum = ⊥ ↔ l = []
-- Init.Data.Array.Lemmas
Array.foldr_assoc : ∀ {α : Type u_1} {op : α → α → α} [ha : Std.Associative op] {xs : Array α} {a₁ a₂ : α},
  Array.foldr op (op a₁ a₂) xs = op (Array.foldr op a₁ xs) a₂
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
returning `none` if no such pair exists.
 -/
Std.TreeMap.Raw.getEntryLT? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → Option (α × β)
-- Init.Grind.Interactive
/-- `intro x₁ ... xₙ` introduces binders and internalizes them into the E-graph.
Only available in `sym =>` mode.
`intro` with no arguments introduces one binder with an inaccessible name.
Use `intro (internalize := false)` or `intro~` to skip internalization.  -/
Lean.Parser.Tactic.Grind.symIntro : Lean.ParserDescr