mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_norm_tendsto_zero : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2),
  Filter.Tendsto (fun i => ‖(Polynomial.aeval (↑(newton_cau_seq✝ hnorm) i)) F‖) Filter.atTop (nhds 0)
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The direction of the affine span of a subset of a family indexed
by a `Fintype` is finite-dimensional.  -/
finiteDimensional_direction_affineSpan_image_of_finite : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [Finite ι] (p : ι → P) (s : Set ι),
  FiniteDimensional k ↥(affineSpan k (p '' s)).direction
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instSubNegAddMonoidOfAddOpposite : {M : Type u_1} → [SubNegMonoid Mᵃᵒᵖ] → SubNegMonoid Mᵈᵃᵃ
-- Lean.Meta.Offset
_private.Lean.Meta.Offset.0.Lean.Meta.withInstantiatedMVars : {α : Type} → Lean.Expr → (Lean.Expr → OptionT Lean.MetaM α) → OptionT Lean.MetaM α
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
SemilinearIsometryClass.norm_map : ∀ {𝓕 : Type u_11} {R : outParam (Type u_12)} {R₂ : outParam (Type u_13)} {inst : Semiring R} {inst_1 : Semiring R₂}
  {σ₁₂ : outParam (R →+* R₂)} {E : outParam (Type u_14)} {E₂ : outParam (Type u_15)} {inst_2 : SeminormedAddCommGroup E}
  {inst_3 : SeminormedAddCommGroup E₂} {inst_4 : Module R E} {inst_5 : Module R₂ E₂} {inst_6 : FunLike 𝓕 E E₂}
  [self : SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) (x : E), ‖f x‖ = ‖x‖
-- Init.Data.BitVec.Bitblast
BitVec.msb_neg_umod_neg_of_msb_true_of_msb_true : ∀ {w : ℕ} {x y : BitVec w}, x.msb = true → y.msb = true → (-x % -y).msb = false
-- Mathlib.Analysis.Normed.Module.Basic
NormedSpace.toModule : {𝕜 : Type u_6} →
  {E : Type u_7} → {inst : NormedField 𝕜} → {inst_1 : SeminormedAddCommGroup E} → [self : NormedSpace 𝕜 E] → Module 𝕜 E
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.neg_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : Neg γ] [inst_4 : ContinuousNeg γ] (f : C(β, γ)) (g : C(α, β)),
  (-f).comp g = -f.comp g
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_mul_C : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (f : PowerSeries R) (r : R),
  (PowerSeries.trunc n) (f * PowerSeries.C r) = (PowerSeries.trunc n) f * Polynomial.C r
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_ofNat : ∀ (n x i : ℕ), (BitVec.ofNat n x).getLsbD i = (decide (i < n) && x.testBit i)
-- Mathlib.Data.Holor
/-- The tensor product of two holors.  -/
Holor.mul : {α : Type} → {ds₁ ds₂ : List ℕ} → [Mul α] → Holor α ds₁ → Holor α ds₂ → Holor α (ds₁ ++ ds₂)
-- Mathlib.Topology.ExtremallyDisconnected
/-- The sigma-type of extremally disconnected spaces is extremally disconnected.  -/
instExtremallyDisconnected : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)]
  [h₀ : ∀ (i : ι), ExtremallyDisconnected (X i)], ExtremallyDisconnected ((i : ι) × X i)
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_add_left : ∀ {α : Type u} [inst : Ring α] (x y : α), Ideal.span {x, y + x} = Ideal.span {x, y}
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getElem!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁[k]! = t₂[k]!
-- Init.Data.UInt.Lemmas
UInt32.le_of_eq : ∀ {a b : UInt32}, a = b → a ≤ b
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.hasFPowerSeriesAt : ∀ {𝕜 : 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 →L[𝕜] F)
  (x : E), HasFPowerSeriesAt (⇑f) (f.fpowerSeries x) x
-- Mathlib.Analysis.RCLike.Extend
/-- **Alias** of `Module.Dual.extendRCLike`.

---

Extend `fr : Dual ℝ F` to `Dual 𝕜 F` in a way that will also be continuous and have its norm
(as a continuous linear map) equal to `‖fr‖` when `fr` is itself continuous on a normed space.  -/
LinearMap.extendTo𝕜 : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {F : Type u_2} →
      [inst_1 : AddCommGroup F] →
        [inst_2 : Module ℝ F] → [inst_3 : Module 𝕜 F] → [IsScalarTower ℝ 𝕜 F] → Module.Dual ℝ F → Module.Dual 𝕜 F
-- Mathlib.Analysis.Seminorm
Seminorm.smul_ball_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {p : Seminorm 𝕜 E} {k : 𝕜} {r : ℝ}, k ≠ 0 → k • p.ball 0 r = p.ball 0 (‖k‖ * r)
-- Mathlib.Topology.Instances.EReal.Lemmas
_private.Mathlib.Topology.Instances.EReal.Lemmas.0.EReal.continuousAt_mul_top_pos : ∀ {a : ℝ}, 0 < a → ContinuousAt (fun p => p.1 * p.2) (⊤, ↑a)
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebra_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat))
  {ι : Type t} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) {X_1 Y : ↑(F.obj { as := Opposite.op S }).obj} (g : X_1 ⟶ Y)
  (i : ι), ((F.toDescentDataAsCoalgebra f).map g).hom i = (F.map (f i).op.toLoc).l.toFunctor.map g
-- Init.Data.List.Nat.InsertIdx
List.insertIdx_eraseIdx : ∀ {α : Type u} {a : α} {i : ℕ} {as : List α} {j : ℕ},
  i < as.length →
    (as.eraseIdx i).insertIdx j a =
      if i ≤ j then (as.insertIdx (j + 1) a).eraseIdx i else (as.insertIdx j a).eraseIdx (i + 1)
-- Init.Data.List.Scan.Lemmas
List.scanr_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → β} {g : γ → α} (b : β) (l : List γ),
  List.scanr f b (List.map g l) = List.scanr (fun x acc => f (g x) acc) b l
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.nonempty_of_hausdorffEDist_ne_top`.

---

If a set is at finite Hausdorff edistance of a nonempty set, it is nonempty.  -/
EMetric.nonempty_of_hausdorffEdist_ne_top : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α}, s.Nonempty → Metric.hausdorffEDist s t ≠ ⊤ → t.Nonempty
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.analyticAt_cuspFunction_zero : ∀ {h : ℝ} {f : UpperHalfPlane → ℂ},
  0 < h →
    Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑h →
      MDiff f → UpperHalfPlane.IsBoundedAtImInfty f → AnalyticAt ℂ (UpperHalfPlane.cuspFunction h f) 0
-- Mathlib.Data.PNat.Defs
PNat.one_coe : ↑1 = 1
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) {Z : ModuleCat k}
  (h : ModuleCat.of k ↥(groupCohomology.cocycles₂ A) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.toCocycles A 1 2)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.isoCocycles₂ A).hom h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₁ A).hom
      (CategoryTheory.CategoryStruct.comp (groupCohomology.shortComplexH2 A).moduleCatLeftHomologyData.f' h)
-- Mathlib.CategoryTheory.Sites.SubcanonicalOver
CategoryTheory.GrothendieckTopology.subcanonical_over : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  [J.Subcanonical] (X : C), (J.over X).Subcanonical
-- Init.Data.Iterators.Producers.Monadic.List
_private.Init.Data.Iterators.Producers.Monadic.List.0.Std.Iterators.Types.ListIterator.instIterator.match_3.eq_2 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterM m α → Sort u_3) (x : α) (xs : List α)
  (h_1 : Unit → motive { internalState := { list := [] } })
  (h_2 : (x : α) → (xs : List α) → motive { internalState := { list := x :: xs } }),
  (match { internalState := { list := x :: xs } } with
    | { internalState := { list := [] } } => h_1 ()
    | { internalState := { list := x :: xs } } => h_2 x xs) =
    h_2 x xs
-- Mathlib.Control.Traversable.Instances
instLawfulTraversableOption : LawfulTraversable Option
-- Mathlib.Algebra.Lie.Basic
/-- A Lie module may be pulled back along a morphism of Lie algebras.  -/
LieModule.compLieHom : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} (M : Type w₁) [inst : CommRing R] [inst_1 : LieRing L₁]
  [inst_2 : LieAlgebra R L₁] [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] [inst_5 : AddCommGroup M]
  [inst_6 : LieRingModule L₂ M] (f : L₁ →ₗ⁅R⁆ L₂) [inst_7 : Module R M] [LieModule R L₂ M], LieModule R L₁ M
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.coe_toAlgHom : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  (f : 𝒜 →ₐᵍ[R] ℬ), ⇑↑f = ⇑f
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  CategoryTheory.CategoryStruct.comp hU.isoSpec.inv U.ι = hU.fromSpec
-- Init.Data.BitVec.Lemmas
BitVec.sub_right_inj : ∀ {w : ℕ} {x y : BitVec w} (z : BitVec w), z - x = z - y ↔ x = y
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toList_rcc_eq_add : ∀ {m n : ℤ} {i : ℕ}, i < (n + 1 - m).toNat → (m...=n).toList[i]! = m + ↑i
-- Mathlib.Data.NNReal.Star
instStarRingNNReal : StarRing NNReal
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.of_commute : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {m : M} [inst_1 : MulOneClass M],
  (∀ (m' : M), Commute m m') → ∀ (f : MonoidAlgebra R M), Commute ((MonoidAlgebra.of R M) m) f
-- Mathlib.FieldTheory.Galois.Infinite
InfiniteGalois.fixingSubgroup_fixedField : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] (H : ClosedSubgroup Gal(K/k))
  [IsGalois k K], (IntermediateField.fixedField ↑H).fixingSubgroup = ↑H
-- Mathlib.Tactic.ExtractGoal
/-- Configuration for `extract_goal` for which variables from the context to include.  -/
Mathlib.Tactic.ExtractGoal.config : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] [inst_1 : CategoryTheory.Abelian A]
  (X : CategoryTheory.SimplicialObject A),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.inclusionOfMooreComplexMap X) AlgebraicTopology.DoldKan.PInfty =
    AlgebraicTopology.inclusionOfMooreComplexMap X
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- If a sum of a `Finset` of size at most 1 has a given
value, so do the terms in that sum.  -/
Finset.eq_of_card_le_one_of_sum_eq : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] {s : Finset ι},
  s.card ≤ 1 → ∀ {f : ι → M} {b : M}, ∑ x ∈ s, f x = b → ∀ x ∈ s, f x = b
-- Aesop.RuleSet
Aesop.instInhabitedGlobalRuleSet.default : Aesop.GlobalRuleSet
-- Mathlib.RingTheory.Bialgebra.Equiv
/-- `BialgEquivClass F R A B` asserts `F` is a type of bundled bialgebra equivalences
from `A` to `B`.  -/
BialgEquivClass : (F : Type u_1) →
  (R : outParam (Type u_2)) →
    (A : outParam (Type u_3)) →
      (B : outParam (Type u_4)) →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] → [CoalgebraStruct R A] → [CoalgebraStruct R B] → [EquivLike F A B] → Prop
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.IsReduced.nodup_rightInvSeq : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {ω : List B},
  cs.IsReduced ω → (cs.rightInvSeq ω).Nodup
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.trans_isThetaTVS : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [inst_7 : AddCommGroup G] [inst_8 : TopologicalSpace G]
  [inst_9 : Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} {k : α → G}, f =O[𝕜; l] g → g =Θ[𝕜; l] k → f =O[𝕜; l] k
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainTermGoalParams.toTextDocumentPositionParams : Lean.Lsp.PlainTermGoalParams → Lean.Lsp.TextDocumentPositionParams
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.Truncated.Hom.tr_comp : ∀ {n : ℕ} {a b c : SimplexCategory} (f : a ⟶ b) (g : b ⟶ c)
  (ha : autoParam (a.len ≤ n) SimplexCategory.Truncated.Hom.tr_comp._auto_1)
  (hb : autoParam (b.len ≤ n) SimplexCategory.Truncated.Hom.tr_comp._auto_3)
  (hc : autoParam (c.len ≤ n) SimplexCategory.Truncated.Hom.tr_comp._auto_5),
  SimplexCategory.Truncated.Hom.tr (CategoryTheory.CategoryStruct.comp f g) ha hc =
    CategoryTheory.CategoryStruct.comp (SimplexCategory.Truncated.Hom.tr f ha hb)
      (SimplexCategory.Truncated.Hom.tr g hb hc)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.dropEndWhile_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String},
  s.toSlice.dropEndWhile pat = s.dropEndWhile pat
-- Mathlib.Tactic.ClickSuggestions.Unfold
/-- Render the unfolds of `e` as given by `filteredUnfolds`, with buttons at each suggestion
for pasting the rewrite tactic. Return `none` when there are no unfolds.  -/
Mathlib.Tactic.ClickSuggestions.suggestUnfold : Lean.Expr →
  Mathlib.Tactic.ClickSuggestions.RwKind → Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM (Option ProofWidgets.Html)
-- Mathlib.RingTheory.WittVector.Domain
/-- `WittVector.verschiebung` translates the entries of a Witt vector upward, inserting 0s in the gaps.
`WittVector.shift` does the opposite, removing the first entries.
This is mainly useful as an auxiliary construction for `WittVector.verschiebung_nonzero`.
 -/
WittVector.shift : {p : ℕ} → {R : Type u_1} → WittVector p R → ℕ → WittVector p R
-- Mathlib.Topology.Algebra.Monoid
eventuallyEq_sum : ∀ {ι : Type u_1} {X : Type u_6} {M : Type u_7} [inst : AddCommMonoid M] {s : Finset ι} {l : Filter X} {f g : ι → X → M},
  (∀ i ∈ s, f i =ᶠ[l] g i) → ∑ i ∈ s, f i =ᶠ[l] ∑ i ∈ s, g i
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationDomain.radical_neg : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizationMonoid R] [inst_2 : UniqueFactorizationMonoid R] {a : R},
  UniqueFactorizationMonoid.radical (-a) = UniqueFactorizationMonoid.radical a
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_eq_empty_of_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b ≤ a → Set.Ico a b = ∅
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.liftAction : Lean.Meta.Grind.Action → Lean.Elab.Tactic.Grind.GrindTacticM Unit
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] (f : A →ₚ[ℂ] ℂ) [inst_2 : StarOrderedRing A]
  {a : A} {b : f.PreGNS}, (f.gnsNonUnitalStarAlgHom a) ↑b = ↑((f.leftMulMapPreGNS a) b)
-- Mathlib.CategoryTheory.Monoidal.Braided.Reflection
/-- Given a reflective functor `R : C ⥤ D` with a monoidal left adjoint, such that `D` is symmetric
monoidal closed, then `C` is monoidal closed.
 -/
CategoryTheory.Monoidal.Reflective.monoidalClosed : {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] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          [CategoryTheory.SymmetricCategory D] →
            [CategoryTheory.MonoidalClosed D] →
              [inst_5 : CategoryTheory.MonoidalCategory C] →
                {L : CategoryTheory.Functor D C} →
                  [L.Monoidal] →
                    {R : CategoryTheory.Functor C D} →
                      [R.Faithful] → [R.Full] → (L ⊣ R) → CategoryTheory.MonoidalClosed C
-- Mathlib.Combinatorics.Matroid.Map
Matroid.map_isBasis_iff : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} {I X : Set α} (f : α → β) (hf : Set.InjOn f M.E),
  I ⊆ M.E → X ⊆ M.E → ((M.map f hf).IsBasis (f '' I) (f '' X) ↔ M.IsBasis I X)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
addEquivOfAddOrderOfEq.eq_1 : ∀ {G : Type u_2} {G' : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup G'] {g : G}
  (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {g' : G'} (hg' : ∀ (x : G'), x ∈ AddSubgroup.zmultiples g')
  (h : addOrderOf g = addOrderOf g'),
  addEquivOfAddOrderOfEq hg hg' h =
    (addMonoidHomOfForallMemZMultiples hg ⋯).toAddEquiv (addMonoidHomOfForallMemZMultiples hg' ⋯) ⋯ ⋯
-- Mathlib.Data.Set.Insert
Set.singleton_inter_nonempty : ∀ {α : Type u_1} {s : Set α} {a : α}, ({a} ∩ s).Nonempty ↔ a ∈ s
-- Mathlib.Analysis.Analytic.Linear
_private.Mathlib.Analysis.Analytic.Linear.0.ContinuousLinearMap.fpowerSeries.match_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.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addY_of_X_eq' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P →
    W'.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → W'.addY P Q * (P 2 * Q 2) ^ 3 = -(P 1 * Q 2 - Q 1 * P 2) ^ 3 * (P 2 * Q 2) ^ 2
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxLeftLinear.μₗ_associativity_inv : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'] [inst_6 : F.LaxLeftLinear C] (c c' : C) (d : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c
        (CategoryTheory.Functor.LaxLeftLinear.μₗ F c' d))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxLeftLinear.μₗ F c
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c' d))
        (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).inv)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' (F.obj d)).inv
      (CategoryTheory.Functor.LaxLeftLinear.μₗ F (CategoryTheory.MonoidalCategoryStruct.tensorObj c c') d)
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.State.modified : Lean.Meta.SimpAll.State → Bool
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
_private.Mathlib.Probability.Kernel.IonescuTulcea.Traj.0.Iic_pi_eq : ∀ {X : ℕ → Type u_1} {a b : ℕ}, a = b → ((i : ↥(Finset.Iic a)) → X ↑i) = ((i : ↥(Finset.Iic b)) → X ↑i)
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Functor.instIsCardinalAccessibleComp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (κ : Cardinal.{w}) [inst_2 : Fact κ.IsRegular] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [F.IsCardinalAccessible κ]
  [G.IsCardinalAccessible κ], (F.comp G).IsCardinalAccessible κ
-- Mathlib.Order.Partition.Finpartition
/-- A `Finpartition` constructor in `Subtype Pr` for `Pr : Set X → Prop` such that `Pr` is closed
under intersection and union and `Pr ⊥` holds from a `P : Finpartition s` with explicit assumptions
that `Pr s` and `Pr p` for each part `p`.  -/
Finpartition.toSubtype : {α : Type u_1} →
  [inst : Lattice α] →
    [inst_1 : OrderBot α] →
      {s : α} →
        (P : Finpartition s) →
          {Pr : α → Prop} →
            (Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)) →
              (Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)) →
                (Prbot : Pr ⊥) → (hs : Pr s) → (∀ p ∈ P.parts, Pr p) → Finpartition ⟨s, hs⟩
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_emptyWithCapacity : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {a fallback : α} {c : ℕ},
  (Std.HashMap.Raw.emptyWithCapacity c).getKeyD a fallback = fallback
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.range_eq_range_of_surjective : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) (e : X ⟶ Y) [AlgebraicGeometry.Surjective e],
  CategoryTheory.CategoryStruct.comp e g = f → Set.range ⇑f = Set.range ⇑g
-- Mathlib.Order.Interval.Set.Basic
Set.Ioi_eq_empty_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Ioi a = ∅ ↔ IsMax a
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map₂Congr.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B}
  {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V)
  {F' : CategoryTheory.Functor C A} {G' : CategoryTheory.Functor D B} (e₁ : F ≅ F') (e₂ : G ≅ G')
  (α' : F'.comp U ⟶ S.comp G') (β' : G'.obj T ⟶ V)
  (hα :
    CategoryTheory.CategoryStruct.comp α (S.whiskerLeft e₂.hom) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight e₁.hom U) α')
  (hβ : β = CategoryTheory.CategoryStruct.comp (e₂.hom.app T) β'),
  CategoryTheory.CostructuredArrow.map₂Congr α β e₁ e₂ α' β' hα hβ =
    CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.CostructuredArrow.isoMk (e₁.app X.left) ⋯) ⋯
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.copy.eq_1 : ∀ {X : Type u_1} [inst : MetricSpace X] (D : Delone.DeloneSet X) (carrier : Set X)
  (packingRadius coveringRadius : NNReal) (h_carrier : carrier = D.carrier)
  (h_packing : packingRadius = D.packingRadius) (h_covering : coveringRadius = D.coveringRadius),
  D.copy carrier packingRadius coveringRadius h_carrier h_packing h_covering =
    { carrier := carrier, packingRadius := packingRadius, packingRadius_pos := ⋯, isSeparated_packingRadius := ⋯,
      coveringRadius := coveringRadius, coveringRadius_pos := ⋯, isCover_coveringRadius := ⋯ }
-- Mathlib.Data.Set.Lattice
Set.sInter_range : ∀ {β : Type u_2} {ι : Sort u_5} (f : ι → Set β), ⋂₀ Set.range f = ⋂ x, f x
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivWithinAt.clm_comp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {x : 𝕜} {s : Set 𝕜}
  {G : Type u_2} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {c : 𝕜 → F →L[𝕜] G} {c' : F →L[𝕜] G}
  {d : 𝕜 → E →L[𝕜] F} {d' : E →L[𝕜] F},
  HasDerivWithinAt c c' s x →
    HasDerivWithinAt d d' s x → HasDerivWithinAt (fun y => c y ∘SL d y) (c' ∘SL d x + c x ∘SL d') s x
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.hom_zero : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] {M₁ M₂ : TopModuleCat R}, TopModuleCat.Hom.hom 0 = 0
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndependent.pair_add_smul_add_smul_iff : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M} {S : Type u_6}
  [inst_3 : CommRing S] [IsDomain S] [inst_5 : Module S R] [inst_6 : Module S M] [SMulCommClass S R M]
  [IsScalarTower S R M] [Module.IsTorsionFree S R] (a b c d : S) [Nontrivial R],
  LinearIndependent R ![a • x + b • y, c • x + d • y] ↔ LinearIndependent R ![x, y] ∧ a * d ≠ b * c
-- Lean.Server.Requests
Lean.Server.LspResponse.response : {α : Type} → Lean.Server.LspResponse α → α