mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Lsp.Basic
Lean.Lsp.instBEqLocation.beq : Lean.Lsp.Location → Lean.Lsp.Location → Bool
-- Mathlib.Analysis.Convex.Between
wbtw_iff_right_eq_or_left_mem_image_Ici : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {x y z : P},
  Wbtw R x y z ↔ z = y ∨ x ∈ ⇑(AffineMap.lineMap z y) '' Set.Ici 1
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instNeg : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [Neg Y] → Neg (LocallyConstant X Y)
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- An arbitrarily chosen section  -/
AddGroupExtension.surjInvRightHom : {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
-- Mathlib.Data.List.Infix
List.mem_tails : ∀ {α : Type u_1} (s t : List α), s ∈ t.tails ↔ s <:+ t
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.Groupoid.invEquivalence_inverse_obj : ∀ (C : Type u) [inst : CategoryTheory.Groupoid C] (self : Cᵒᵖ),
  (CategoryTheory.Groupoid.invEquivalence C).inverse.obj self = Opposite.unop self
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁_inverse_obj_left : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {L L' : CategoryTheory.Functor C D} (iso₁ : L ≅ L') (F : CategoryTheory.Functor C H)
  (X :
    CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L')),
  ((CategoryTheory.Functor.leftExtensionEquivalenceOfIso₁ iso₁ F).inverse.obj X).left = X.left
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsTrivialOn.eq_one : ∀ {Γ₀ : Type u_4} {inst : LinearOrderedCommMonoidWithZero Γ₀} {B : Type u_7} {A : Type u_8} {inst_1 : CommSemiring A}
  {inst_2 : Ring B} {inst_3 : Algebra A B} {v : Valuation B Γ₀} [self : Valuation.IsTrivialOn A v] (a : A),
  a ≠ 0 → v ((algebraMap A B) a) = 1
-- Mathlib.MeasureTheory.Group.Arithmetic
AddSubmonoid.instMeasurableConstVAdd : ∀ {M : Type u_2} {α : Type u_3} [inst : MeasurableSpace α] [inst_1 : AddMonoid M] [inst_2 : AddAction M α]
  [MeasurableConstVAdd M α] (s : AddSubmonoid M), MeasurableConstVAdd (↥s) α
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.Path.reverse.eq_def : ∀ {V : Type u_2} [inst : Quiver V] [inst_1 : Quiver.HasReverse V] {a : V} (x : V) (x_1 : Quiver.Path a x),
  x_1.reverse =
    match x, x_1 with
    | .(a), Quiver.Path.nil => Quiver.Path.nil
    | x, p.cons e => (Quiver.reverse e).toPath.comp p.reverse
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.foldM_filterMapWithPostcondition : ∀ {α β γ δ : Type w} {n : Type w → Type w''} {o : Type w → Type w'''} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : Monad o] [LawfulMonad n] [LawfulMonad o]
  [inst_6 : Std.IteratorLoop α Id n] [inst_7 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id n]
  [Std.LawfulIteratorLoop α Id o] [inst_10 : MonadLiftT n o] [LawfulMonadLiftT n o]
  {f : β → Std.Iterators.PostconditionT n (Option γ)} {g : δ → γ → o δ} {init : δ} {it : Std.Iter β},
  Std.IterM.foldM g init (Std.Iter.filterMapWithPostcondition f it) =
    Std.Iter.foldM
      (fun d b => do
        let __x ← liftM (f b).run
        match __x with
          | some c => g d c
          | x => pure d)
      init it
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.map_eq_map_iff : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {H K : Subgroup G},
  Subgroup.map f H = Subgroup.map f K ↔ H ⊔ f.ker = K ⊔ f.ker
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.id_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (p q : ℤ) (hpq : p + 1 = q),
  CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v p q hpq)
        ((CochainComplex.mappingCone.inl φ).v q p ⋯) +
      CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v p p ⋯)
        ((CochainComplex.mappingCone.inr φ).f p) =
    CategoryTheory.CategoryStruct.id ((CochainComplex.mappingCone φ).X p)
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.hV1 : {k : Type u} →
  {G : Type v} →
    [inst : Ring k] → [inst_1 : TopologicalSpace k] → [inst_2 : Monoid G] → (self : TopRep k G) → AddCommGroup ↑self
-- Lean.Data.Lsp.Ipc
/-- Waits for the worker to emit all diagnostic notifications for the current document version and
returns the accumulated diagnostics, if any.

Incoming notifications are merged using `mergePublishDiagnosticsParams`.

We used to return all notifications but with debouncing in the server, this would not be
deterministic anymore as what messages are dropped depends on wall-clock timing.
  -/
Lean.Lsp.Ipc.collectDiagnostics : optParam Lean.JsonRpc.RequestID 0 →
  Lean.Lsp.DocumentUri → ℕ → Lean.Lsp.Ipc.IpcM (Option (Lean.JsonRpc.Notification Lean.Lsp.PublishDiagnosticsParams))
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.constCompPiIsoConst_hom_app : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] {I : α → Type u_1}
  [inst_2 : (i : α) → CategoryTheory.Category.{v_1, u_1} (I i)] (X : α → C) (X_1 : (i : α) → I i),
  (CategoryTheory.Limits.Pi.constCompPiIsoConst X).hom.app X_1 = CategoryTheory.CategoryStruct.id (∏ᶜ fun i => X i)
-- Lean.DocString.Types
Lean.Doc.Block.dl.injEq : ∀ {i : Type u} {b : Type v} (items items_1 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))),
  (Lean.Doc.Block.dl items = Lean.Doc.Block.dl items_1) = (items = items_1)
-- Init.Data.Order.Ord
Array.instLawfulEqCmpCompareLex : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.LawfulEqCmp cmp], Std.LawfulEqCmp (Array.compareLex cmp)
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.emptyWithCapacity.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (capacity : ℕ),
  Std.DHashMap.emptyWithCapacity capacity = { inner := Std.DHashMap.Raw.emptyWithCapacity capacity, wf := ⋯ }
-- Lean.Meta.Tactic.Simp.SimpTheorems
_private.Lean.Meta.Tactic.Simp.SimpTheorems.0.Lean.Meta.isRflTheoremCore : Bool → Lean.Name → Lean.CoreM Bool
-- Mathlib.Data.Multiset.FinsetOps
Multiset.disjoint_ndinsert_right : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s t : Multiset α},
  Disjoint s (Multiset.ndinsert a t) ↔ a ∉ s ∧ Disjoint s t
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.restrict_eq_zero_iff : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.FiniteMeasure Ω) (A : Set Ω), μ.restrict A = 0 ↔ μ A = 0
-- Mathlib.Data.Matrix.Basic
LinearMap.entryLinearMap_comp_mapMatrix : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type u_11} {β : Type u_12} [inst : Semiring R]
  [inst_1 : Semiring S] {σᵣₛ : R →+* S} [inst_2 : AddCommMonoid α] [inst_3 : AddCommMonoid β] [inst_4 : Module R α]
  [inst_5 : Module S β] (f : α →ₛₗ[σᵣₛ] β) (i : m) (j : n),
  Matrix.entryLinearMap S β i j ∘ₛₗ f.mapMatrix = f ∘ₛₗ Matrix.entryLinearMap R α i j
-- Mathlib.CategoryTheory.Subterminal
CategoryTheory.subterminalsEquivMonoOverTerminal_functor_obj_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasTerminal C]
  (X : CategoryTheory.Subterminals C),
  ((CategoryTheory.subterminalsEquivMonoOverTerminal C).functor.obj X).obj =
    CategoryTheory.Over.mk (CategoryTheory.Limits.terminal.from X.obj)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min_eq_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {he : t.isEmpty = false}, t.min he = t.min!
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
smul_ball : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {c : 𝕜}, c ≠ 0 → ∀ (x : E) (r : ℝ), c • Metric.ball x r = Metric.ball (c • x) (‖c‖ * r)
-- Lean.ToLevel
Lean.ToLevel.mk : Lean.Level → (∀ (x : Sort u), True) → Lean.ToLevel
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.Ioo_subset_uIoo : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioo a b ⊆ Set.uIoo a b
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_lt_one : ∀ {x : ENNReal} {z : ℝ}, x < 1 → 0 < z → x ^ z < 1
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_eq_some_get!_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {a : α}, t.contains a = true → t.get? a = some (t.get! a)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
ChartedSpace.LiftPropWithinAt.mk : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {f : M → M'}
  {s : Set M} {x : M},
  ContinuousWithinAt f s x →
    P (↑(chartAt H' (f x)) ∘ f ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) →
      ChartedSpace.LiftPropWithinAt P f s x
-- Mathlib.Topology.UniformSpace.UniformApproximation
/-- If `Fₙ` tends locally uniformly to `f`, and `gₙ` tends to `x`, then `Fₙ gₙ` tends to `f x`.  -/
TendstoLocallyUniformly.tendsto_comp : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {F : ι → α → β}
  {f : α → β} {x : α} {p : Filter ι} {g : ι → α},
  TendstoLocallyUniformly F f p →
    ContinuousAt f x → Filter.Tendsto g p (nhds x) → Filter.Tendsto (fun n => F n (g n)) p (nhds (f x))
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.surjOn : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), Set.SurjOn (↑e) e.source e.target
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin_finTwoProd : ∀ {R : Type u_1} [inst : CommSemiring R] (a b c d : R),
  (Matrix.toLin (Module.Basis.finTwoProd R) (Module.Basis.finTwoProd R)) !![a, b; c, d] =
    (a • LinearMap.fst R R R + b • LinearMap.snd R R R).prod (c • LinearMap.fst R R R + d • LinearMap.snd R R R)
-- Mathlib.Algebra.Ring.GeomSum
/-- Value of a geometric sum over the naturals. Note: see `geom_sum_mul_add` for a formulation
that avoids division and subtraction.  -/
Nat.geomSum_eq : ∀ {m : ℕ}, 2 ≤ m → ∀ (n : ℕ), ∑ k ∈ Finset.range n, m ^ k = (m ^ n - 1) / (m - 1)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnCommRing.injEq : ∀ (e : Lean.Expr) (p : Int.Internal.Linear.Poly) (re : Lean.Meta.Grind.Arith.CommRing.RingExpr)
  (rp : Lean.Grind.CommRing.Poly) (p' : Int.Internal.Linear.Poly) (e_1 : Lean.Expr) (p_1 : Int.Internal.Linear.Poly)
  (re_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr) (rp_1 : Lean.Grind.CommRing.Poly) (p'_1 : Int.Internal.Linear.Poly),
  (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnCommRing e p re rp p' =
      Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defnCommRing e_1 p_1 re_1 rp_1 p'_1) =
    (e = e_1 ∧ p = p_1 ∧ re = re_1 ∧ rp = rp_1 ∧ p' = p'_1)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.instToJsonSaveOptions.toJson : Lean.Lsp.SaveOptions → Lean.Json
-- Init.Data.Order.PackageFactories
Std.LinearOrderPackage.toLawfulOrderMin : ∀ {α : Type u} [self : Std.LinearOrderPackage α], Std.LawfulOrderMin α
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instCommSemigroup : {α : Type u_1} → [CommSemigroup α] → CommSemigroup αᵐᵒᵖ
-- Lean.Elab.Tactic.Induction
/-- Check for the specific proof structure `induction h with n n_ih` that can arise from
Natural-Numbers-Game-style `induction` proofs being used in standard Lean style proofs.

These errors are provided with a custom error explanation.
 -/
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.checkForInductionWithNoAlts : String → Lean.Syntax → Lean.Elab.Tactic.TacticM Unit
-- Init.Data.Format.Basic
/-- Renders a `Format` using effects in the monad `m`, using the methods of `MonadPrettyFormat`.

Each line is emitted as soon as it is rendered, rather than waiting for the entire document to be
rendered.
* `w`: the total width
* `indent`: the initial indentation to use for wrapped lines (subsequent wrapping may increase the
  indentation)
 -/
Std.Format.prettyM : {m : Type → Type} → Std.Format → ℕ → optParam ℕ 0 → [Monad m] → [Std.Format.MonadPrettyFormat m] → m Unit
-- Mathlib.Algebra.Group.Even
/-- Alias of the forwards direction of `even_iff_exists_two_nsmul`.  -/
Even.exists_two_nsmul : ∀ {α : Type u_2} [inst : AddMonoid α] (a : α), Even a → ∃ r, a = 2 • r
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.size_inter_le_size_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp],
  (t₁ ∩ t₂).size ≤ t₂.size
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.IsHomogeneous.add : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {φ ψ : MvPolynomial σ R} {n : ℕ},
  φ.IsHomogeneous n → ψ.IsHomogeneous n → (φ + ψ).IsHomogeneous n
-- Lean.Data.KVMap
Lean.KVMap.eqv : Lean.KVMap → Lean.KVMap → Bool
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_add : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (x y : AddMonoidAlgebra R M), (x + y).coeff = x.coeff + y.coeff
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.tryRecv : {α : Type} → Std.CloseableChannel.Unbounded✝ α → BaseIO (Option α)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_minKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false → Std.Internal.List.getKey! (Std.Internal.List.minKey! l) l = Std.Internal.List.minKey! l
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.uniformEquiv_mk_coe_symm : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (a : α ≃ β)
  (b : UniformContinuous a.toFun) (c : UniformContinuous a.invFun),
  ⇑{ toEquiv := a, uniformContinuous_toFun := b, uniformContinuous_invFun := c }.symm = ⇑a.symm
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.IndepSets.union : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {s₁ s₂ s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ProbabilityTheory.Kernel.IndepSets s₁ s' κ μ →
    ProbabilityTheory.Kernel.IndepSets s₂ s' κ μ → ProbabilityTheory.Kernel.IndepSets (s₁ ∪ s₂) s' κ μ
-- Init.Data.String.Lemmas.Pattern.Find.Char
String.Slice.Pos.find?_char_eq_some_iff_splits : ∀ {c : Char} {s : String.Slice} {pos : s.Pos} {t u : String},
  pos.Splits t u →
    ∀ {pos' : s.Pos}, pos.find? c = some pos' ↔ ∃ v w, pos'.Splits (t ++ v) (String.singleton c ++ w) ∧ c ∉ v.toList
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Eta-expanded form of `contDiff_id`

---

The identity is `C^n`.  -/
contDiff_fun_id : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞}, ContDiff 𝕜 n fun x => x
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.core.sizeOf_spec : ∀ (a b : Lean.Expr) (ra rb : Lean.Grind.CommRing.Expr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.core a b ra rb) =
    1 + sizeOf a + sizeOf b + sizeOf ra + sizeOf rb
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.comp_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : S₁ ⟶ S₂) (φ₂₃ : S₂ ⟶ S₃),
  (CategoryTheory.CategoryStruct.comp φ₁₂ φ₂₃).τ₂ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₂ φ₂₃.τ₂
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso_inv_app_hom_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C]
  (X : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C)
  (X_1 : CategoryTheory.Discrete PUnit.{u + 1}),
  ((CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso C).inv.app X).hom.hom.app X_1 =
    CategoryTheory.CategoryStruct.id
      (X.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (CategoryTheory.Discrete PUnit.{u + 1})))
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.toAlgEquiv : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : TopologicalSpace A] →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] → [inst_5 : Algebra R A] → [inst_6 : Algebra R B] → (A ≃A[R] B) → A ≃ₐ[R] B
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The order of a formal power series is at least `n` if
the `d`th coefficient is `0` for all `d` such that `degree d < n`.  -/
MvPowerSeries.le_order : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R} {n : ℕ∞},
  (∀ (d : σ →₀ ℕ), ↑(Finsupp.degree d) < n → (MvPowerSeries.coeff d) f = 0) → n ≤ f.order
-- Mathlib.Analysis.InnerProductSpace.GramMatrix
Matrix.linearIndependent_of_det_gram_ne_zero : ∀ {E : Type u_1} {n : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype n] [inst_4 : DecidableEq n] {v : n → E},
  (Matrix.gram 𝕜 v).det ≠ 0 → LinearIndependent 𝕜 v
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.keyAtIdx?.induct_unfolding : ∀ {α : Type u} {β : α → Type v} (motive : Std.DTreeMap.Internal.Impl α β → ℕ → Option α → Prop),
  (∀ (x : ℕ), motive Std.DTreeMap.Internal.Impl.leaf x none) →
    (∀ (size : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (n : ℕ),
        compare n l.size = Ordering.lt →
          motive l n (l.keyAtIdx? n) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n (l.keyAtIdx? n)) →
      (∀ (size : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (n : ℕ),
          compare n l.size = Ordering.eq → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n (some k)) →
        (∀ (size : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (n : ℕ),
            compare n l.size = Ordering.gt →
              motive r (n - l.size - 1) (r.keyAtIdx? (n - l.size - 1)) →
                motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n (r.keyAtIdx? (n - l.size - 1))) →
          ∀ (a : Std.DTreeMap.Internal.Impl α β) (a_1 : ℕ), motive a a_1 (a.keyAtIdx? a_1)
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.extensionProductIter_bot : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C] (n : ℕ),
  ⊥.extensionProductIter n = ⊥
-- Mathlib.Algebra.Homology.TotalComplex
/-- A bicomplex has a total bicomplex if for any `i₁₂ : I₁₂`, the coproduct
of the objects `(K.X i₁).X i₂` such that `ComplexShape.π c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = i₁₂` exists.  -/
HomologicalComplex₂.HasTotal : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          {I₁₂ : Type u_4} →
            {c₁ : ComplexShape I₁} →
              {c₂ : ComplexShape I₂} →
                HomologicalComplex₂ C c₁ c₂ → (c₁₂ : ComplexShape I₁₂) → [TotalComplexShape c₁ c₂ c₁₂] → Prop
-- Mathlib.Algebra.BigOperators.Ring.Multiset
Multiset.prod_map_add : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : Multiset ι} {f g : ι → R},
  (Multiset.map (fun i => f i + g i) s).prod =
    (Multiset.map (fun p => (Multiset.map f p.1).prod * (Multiset.map g p.2).prod) s.antidiagonal).sum
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.StdWall.noConfusionType : Sort v✝ → Std.Time.TimeZone.StdWall → Std.Time.TimeZone.StdWall → Sort v✝
-- Mathlib.Combinatorics.Matroid.Rank.ENat
/-- **Alias** of `Matroid.eRk_le_eRk_inter_add_eRk_sdiff`. -/
Matroid.eRk_le_eRk_inter_add_eRk_diff : ∀ {α : Type u_1} (M : Matroid α) (X Y : Set α), M.eRk X ≤ M.eRk (X ∩ Y) + M.eRk (X \ Y)
-- Mathlib.NumberTheory.Cyclotomic.Basic
IsCyclotomicExtension.neZero_of_mem : ∀ (n : ℕ) [NeZero n] (S : Set ℕ) (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B]
  [inst_2 : Algebra A B] [IsCyclotomicExtension S A B] [IsDomain B], n ∈ S → NeZero ↑n
-- Mathlib.Algebra.Field.Defs
DivisionRing.toDivisionSemiring : {K : Type u_1} → [DivisionRing K] → DivisionSemiring K
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.values_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v}, ∅.values = []
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivAtFilter.tendsto_nhds : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {L : Filter 𝕜},
  L ≤ nhds x → HasDerivAtFilter f f' (L ×ˢ pure x) → Filter.Tendsto f L (nhds (f x))
-- Init.Data.Range.Polymorphic.SInt
Int64.instRxiHasSize.eq_1 : Int64.instRxiHasSize = { size := fun lo => (2 ^ 63 - lo.toInt).toNat }
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.uint64 : UInt64 → Lean.Compiler.LCNF.LitValue
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
/-- The canonical isomorphism from the opposite of an abstract product to the corresponding coproduct
in the opposite category.
 -/
CategoryTheory.Limits.opProductIsoCoproduct' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {α : Type u_1} →
      {Z : α → C} →
        {f : CategoryTheory.Limits.Fan Z} →
          {c : CategoryTheory.Limits.Cofan fun x => Opposite.op (Z x)} →
            CategoryTheory.Limits.IsLimit f → CategoryTheory.Limits.IsColimit c → (Opposite.op f.pt ≅ c.pt)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.tensorHom.eq_1 : ∀ (a a_1 a_2 a_3 : SimplexCategory) (f₁_2 : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1)
  (f₂_2 : CategoryTheory.WithInitial.of a_2 ⟶ CategoryTheory.WithInitial.of a_3),
  AugmentedSimplexCategory.tensorHom f₁_2 f₂_2 = AugmentedSimplexCategory.tensorHomOf f₁_2 f₂_2
-- Mathlib.Topology.Separation.GDelta
PerfectlyNormalSpace.toNormalSpace : ∀ {X : Type u} {inst : TopologicalSpace X} [self : PerfectlyNormalSpace X], NormalSpace X
-- Mathlib.Combinatorics.SimpleGraph.Partition
SimpleGraph.Partition.partOfVertex_ne_of_adj : ∀ {V : Type u} {G : SimpleGraph V} (P : G.Partition) {v w : V}, G.Adj v w → P.partOfVertex v ≠ P.partOfVertex w
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → (m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty)
-- Mathlib.Analysis.Normed.Lp.ProdLp
LinearIsometryEquiv.withLpProdAssoc_apply : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) (γ : Type u_4) [hp : Fact (1 ≤ p)] [inst : Semiring 𝕜]
  [inst_1 : SeminormedAddCommGroup α] [inst_2 : Module 𝕜 α] [inst_3 : SeminormedAddCommGroup β] [inst_4 : Module 𝕜 β]
  [inst_5 : SeminormedAddCommGroup γ] [inst_6 : Module 𝕜 γ] (a : WithLp p (WithLp p (α × β) × γ)),
  (LinearIsometryEquiv.withLpProdAssoc p 𝕜 α β γ) a = WithLp.toLp p (a.fst.fst, WithLp.toLp p (a.fst.snd, a.snd))
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₁₂ : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (self : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) (pq : κ), self.i₁ pq ≤ self.i₂ pq