mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.MonoidLocalization.Order
/-- An ordered cancellative monoid injects into its localization by
sending `a` to `a - b`.  -/
AddLocalization.mkOrderEmbedding : {α : Type u_1} →
  [inst : AddCommMonoid α] →
    [inst_1 : PartialOrder α] →
      [inst_2 : IsOrderedCancelAddMonoid α] → {s : AddSubmonoid α} → ↥s → α ↪o AddLocalization s
-- Mathlib.Analysis.InnerProductSpace.Laplacian
tensorIteratedFDerivWithinTwo.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F)
  (s : Set E) (e : E),
  tensorIteratedFDerivWithinTwo 𝕜 f s e = TensorProduct.lift (bilinearIteratedFDerivWithinTwo 𝕜 f s e)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], k ∉ m₁ → (m₁ \ m₂)[k]! = default
-- Mathlib.Algebra.FreeMonoid.Basic
_private.Mathlib.Algebra.FreeMonoid.Basic.0.FreeAddMonoid.sumAux.match_1.eq_1 : ∀ {M : Type u_1} (motive : List M → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (x : M) → (xs : List M) → motive (x :: xs)),
  (match [] with
    | [] => h_1 ()
    | x :: xs => h_2 x xs) =
    h_1 ()
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k fallback : α}, k ∉ m₁ → (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k fallback
-- Init.Data.String.Basic
/-- Given a position in `s`, obtain the corresponding position in `s.slice! p₀ p₁ h`, or panic if
taking `s.slice! p₀ p₁` already panicked or if the position is not between `p₀` and `p₁`.
 -/
String.Pos.slice! : {s : String} → s.Pos → (p₀ p₁ : s.Pos) → (s.slice! p₀ p₁).Pos
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdUniformlyOn.tendstoUniformlyOn_finsetRange : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] {g : β → α} {s : Set β} [inst_1 : UniformSpace α] {f : ℕ → β → α},
  HasProdUniformlyOn f g s → TendstoUniformlyOn (fun x1 x2 => ∏ i ∈ Finset.range x1, f i x2) g Filter.atTop s
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.IsInitial.hasInitial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (h : CategoryTheory.Limits.IsInitial X),
  CategoryTheory.Limits.HasInitial C
-- Mathlib.Data.Finset.Grade
Multiset.covBy_cons : ∀ {α : Type u_1} (s : Multiset α) (a : α), s ⋖ a ::ₘ s
-- Mathlib.Probability.Kernel.Composition.CompMap
ProbabilityTheory.Kernel.swap_swap : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β},
  (ProbabilityTheory.Kernel.swap α β).comp (ProbabilityTheory.Kernel.swap β α) = ProbabilityTheory.Kernel.id
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.H2π_comp_map_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : ↥(groupHomology.cycles₂ A)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.map f φ 2))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.H2π A)) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.H2π B))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.mapCycles₂ f φ)) x)
-- Mathlib.MeasureTheory.Function.LpSeminorm.SMul
MeasureTheory.eLpNormEssSup_const_smul_le : ∀ {α : Type u_1} {F : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup F]
  {f : α → F} {𝕜 : Type u_3} [inst_1 : NormedRing 𝕜] [inst_2 : MulActionWithZero 𝕜 F] [IsBoundedSMul 𝕜 F] {c : 𝕜},
  MeasureTheory.eLpNormEssSup (c • f) μ ≤ ‖c‖ₑ * MeasureTheory.eLpNormEssSup f μ
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Mapping from types to its "semiring id". We cache failures using `none`.
`stypeIdOf[type]` is `some id`, then `id < semirings.size`.
If a type is in this map, it is not in `typeIdOf`.
 -/
Lean.Meta.Grind.Arith.CommRing.State.stypeIdOf : Lean.Meta.Grind.Arith.CommRing.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.disjUnion.eq_1 : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π₁ π₂ : BoxIntegral.Prepartition I) (h : Disjoint π₁.iUnion π₂.iUnion),
  π₁.disjUnion π₂ h = { boxes := π₁.boxes ∪ π₂.boxes, le_of_mem' := ⋯, pairwiseDisjoint := ⋯ }
-- Lean.Meta.Tactic.ExposeNames
/-- Creates a temporary local context where all names are exposed, and executes `k`  -/
Lean.Meta.withExposedNames : {α : Type} → Lean.MetaM α → Lean.MetaM α
-- Mathlib.Data.Fin.SuccPred
/-- Embedding `i : Fin n` into `Fin (n + 1)` using a pivot `p` that is lesser
results in a value that is greater than `p`.  -/
Fin.lt_succAbove_iff_le_castSucc : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), p < p.succAbove i ↔ p ≤ i.castSucc
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.eq_lift_neg_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddGrpObj B] (f g h : A ⟶ B),
  f =
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.CartesianMonoidalCategory.lift g
          (CategoryTheory.CategoryStruct.comp h CategoryTheory.AddGrpObj.neg))
        CategoryTheory.AddMonObj.add ↔
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f h)
        CategoryTheory.AddMonObj.add =
      g
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo_wd' : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  (i : M →ₗ[R] N) (f : M →ₗ[R] Q) [inst_7 : Fact (Function.Injective ⇑i)] (h : Module.Baer R Q) {y : N} (r : R),
  r • y = 0 → (Module.Baer.ExtensionOfMaxAdjoin.extendIdealTo i f h y) r = 0
-- Mathlib.Topology.Hom.ContinuousEvalConst
/-- A typeclass saying that `F` is a type of bundled morphisms (in the sense of `DFunLike`)
with a topology on `F` such that evaluation at a point is continuous in `f : F`.  -/
ContinuousEvalConst : (F : Type u_1) →
  (α : outParam (Type u_2)) →
    (X : outParam (Type u_3)) → [FunLike F α X] → [TopologicalSpace F] → [TopologicalSpace X] → Prop
-- Mathlib.Analysis.Fourier.FourierTransform
Real.fourierInv_eq : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  (f : V → E) (w : V), FourierTransformInv.fourierInv f w = ∫ (v : V), Real.fourierChar (inner ℝ v w) • f v
-- Mathlib.LinearAlgebra.Matrix.Echelon.Pivot
Matrix.IsPivotedBy.isPivotEntry : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Zero R] [inst_1 : LT m] [inst_2 : LT n] {A : Matrix m n R}
  {l : m → WithTop n}, A.IsPivotedBy l → ∀ (i : m), (∀ (j : n), ↑j < l i → A i j = 0) ∧ ∀ (c : n), l i = ↑c → A i c ≠ 0
-- Lean.Elab.Tactic.RCases
Lean.Elab.Tactic.RCases.RCasesPatt.one.sizeOf_spec : ∀ (ref : Lean.Syntax) (a : Lean.Name), sizeOf (Lean.Elab.Tactic.RCases.RCasesPatt.one ref a) = 1 + sizeOf ref + sizeOf a
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.subgroupOf_eq_top : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.subgroupOf K = ⊤ ↔ K ≤ H
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.forIn'_eq_match_step.match_1.eq_1 : ∀ {γ : Type u_1} (motive : ForInStep γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive (ForInStep.yield c))
  (h_2 : (c : γ) → motive (ForInStep.done c)),
  (match ForInStep.yield c with
    | ForInStep.yield c => h_1 c
    | ForInStep.done c => h_2 c) =
    h_1 c
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.Tree.mk.inj : ∀ {α : Type u} {β : α → Type v} {size : ℕ} {impl : Std.DTreeMap.Internal.Impl α β} {balanced_impl : impl.Balanced}
  {size_impl : impl.size = size} {impl_1 : Std.DTreeMap.Internal.Impl α β} {balanced_impl_1 : impl_1.Balanced}
  {size_impl_1 : impl_1.size = size},
  { impl := impl, balanced_impl := balanced_impl, size_impl := size_impl } =
      { impl := impl_1, balanced_impl := balanced_impl_1, size_impl := size_impl_1 } →
    impl = impl_1
-- Init.PropLemmas
/-- `∨` distributes over `∧` (on the right).  -/
and_or_right : ∀ {a b c : Prop}, a ∧ b ∨ c ↔ (a ∨ c) ∧ (b ∨ c)
-- Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
compactlySupported_eq_top_of_isCompact : ∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : NonUnitalNormedRing γ],
  IsCompact Set.univ → compactlySupported α γ = ⊤
-- Batteries.Recycling.RBTree.WF
/-- The `erase` function preserves the ordering invariants.  -/
RBTree.RBNode.Ordered.erase : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : RBTree.RBNode α},
  RBTree.RBNode.Ordered cmp t → RBTree.RBNode.Ordered cmp (RBTree.RBNode.erase cut t)
-- Mathlib.Topology.Sheaves.SheafCondition.Sites
/-- If a family `B` of open sets forms a basis of the topology on `X`, and if `F'`
is a sheaf on `X`, then a homomorphism between a presheaf `F` on `X` and `F'`
is equivalent to a homomorphism between their restrictions to the indexing type
`ι` of `B`, with the induced category structure on `ι`.  -/
TopCat.Sheaf.restrictHomEquivHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : TopCat} →
      {ι : Type u_1} →
        {B : ι → TopologicalSpace.Opens ↑X} →
          (F : TopCat.Presheaf C X) →
            (F' : TopCat.Sheaf C X) →
              TopologicalSpace.Opens.IsBasis (Set.range B) →
                ((CategoryTheory.inducedFunctor B).op.comp F ⟶ (CategoryTheory.inducedFunctor B).op.comp F'.obj) ≃
                  (F ⟶ F'.obj)
-- Mathlib.Tactic.TermCongr
Mathlib.Tactic.TermCongr.CongrType.noConfusionType : Sort v✝ → Mathlib.Tactic.TermCongr.CongrType → Mathlib.Tactic.TermCongr.CongrType → Sort v✝
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- `x ↦ fderiv 𝕜 (f x) (g x)` is smooth at `x₀`.  -/
ContDiffAt.fderiv : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x₀ : E} {m n : WithTop ℕ∞} {f : E → F → G} {g : E → F},
  ContDiffAt 𝕜 n (Function.uncurry f) (x₀, g x₀) →
    ContDiffAt 𝕜 m g x₀ → m + 1 ≤ n → ContDiffAt 𝕜 m (fun x => fderiv 𝕜 (f x) (g x)) x₀
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.ofHom.eq_1 : ∀ {X Y : Type u} [inst : CommMonoid X] [inst_1 : CommMonoid Y] (f : X →* Y),
  CommMonCat.ofHom f = CategoryTheory.ConcreteCategory.ofHom f
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomMulAct.instSMulAEEqFun : {M : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : MeasurableSpace α] →
        {μ : MeasureTheory.Measure α} →
          [inst_1 : TopologicalSpace β] →
            [inst_2 : SMul M α] →
              [MeasurableConstSMul M α] → [MeasureTheory.SMulInvariantMeasure M α μ] → SMul Mᵈᵐᵃ (α →ₘ[μ] β)
-- Mathlib.Computability.RegularExpressions
_private.Mathlib.Computability.RegularExpressions.0.RegularExpression.deriv.match_1.eq_3 : ∀ {α : Type u_1} (motive : RegularExpression α → α → Sort u_2) (a₁ a₂ : α)
  (h_1 : (x : α) → motive RegularExpression.zero x) (h_2 : (x : α) → motive RegularExpression.epsilon x)
  (h_3 : (a₁ a₂ : α) → motive (RegularExpression.char a₁) a₂)
  (h_4 : (P Q : RegularExpression α) → (a : α) → motive (P.plus Q) a)
  (h_5 : (P Q : RegularExpression α) → (a : α) → motive (P.comp Q) a)
  (h_6 : (P : RegularExpression α) → (a : α) → motive P.star a),
  (match RegularExpression.char a₁, a₂ with
    | RegularExpression.zero, x => h_1 x
    | RegularExpression.epsilon, x => h_2 x
    | RegularExpression.char a₁, a₂ => h_3 a₁ a₂
    | P.plus Q, a => h_4 P Q a
    | P.comp Q, a => h_5 P Q a
    | P.star, a => h_6 P a) =
    h_3 a₁ a₂
-- Init.Data.Array.Lemmas
Array.getElem_set_ne : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h' : i < xs.size) {v : α} {j : ℕ} (pj : j < xs.size),
  i ≠ j → (xs.set i v h')[j] = xs[j]
-- Mathlib.Algebra.Star.SelfAdjoint
IsStarNormal.mk : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Star R] {x : R}, Commute (star x) x → IsStarNormal x
-- Mathlib.Algebra.Lie.Rank
/-- Let `L` be a Lie algebra over a nontrivial commutative ring `R`,
and assume that `L` is finite free as `R`-module.
Then the coefficients of the characteristic polynomial of `ad R L x` are polynomial in `x`.
The *rank* of `L` is the smallest `n` for which the `n`-th coefficient is not the zero polynomial.
 -/
LieAlgebra.rank : (R : Type u_1) →
  (L : Type u_3) →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → [Module.Finite R L] → [Module.Free R L] → ℕ
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.hsymm_isSymmetric : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] [inst_2 : DecidableEq σ] (n : ℕ),
  (MvPolynomial.hsymm σ R n).IsSymmetric
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- Module containing the constant whose import failed.  -/
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.ImportFailure.module : Lean.Meta.RefinedDiscrTree.ImportFailure✝ → Lean.Name
-- Mathlib.Data.Set.Pairwise.Lattice
/-- In a disjoint union we can identify the unique set an element belongs to.  -/
pairwiseDisjoint_unique : ∀ {α : Type u_1} {ι : Type u_2} {f : ι → Set α} {s : Set ι} {y : α},
  s.PairwiseDisjoint f → y ∈ ⋃ i ∈ s, f i → ∃! i, i ∈ s ∧ y ∈ f i
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.add_mul_right_right_iff : ∀ {R : Type u} [inst : CommRing R] {x y z : R}, IsCoprime x (y + z * x) ↔ IsCoprime x y
-- Init.Data.BitVec.Lemmas
BitVec.toFin_sshiftRight' : ∀ {w : ℕ} {x y : BitVec w},
  (x.sshiftRight' y).toFin =
    if x.msb = true then Fin.ofNat (2 ^ w) (2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> y.toNat)
    else Fin.ofNat (2 ^ w) (x.toNat >>> y.toNat)
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
CategoryTheory.MonoidalCategory.externalProductFlip_inv_app_app_app_app : ∀ (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [inst : CategoryTheory.Category.{v₁, u₁} J₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.MonoidalCategory C] [inst_4 : CategoryTheory.BraidedCategory C]
  (X : CategoryTheory.Functor J₁ C) (X_1 : CategoryTheory.Functor J₂ C) (X_2 : J₂) (X_3 : J₁),
  ((((CategoryTheory.MonoidalCategory.externalProductFlip J₁ J₂ C).inv.app X).app X_1).app X_2).app X_3 =
    (β_ (X.obj X_3) (X_1.obj X_2)).inv
-- Std.Async.Basic
Std.Async.MaybeTask.pure.inj : ∀ {α : Type} {a a_1 : α}, Std.Async.MaybeTask.pure a = Std.Async.MaybeTask.pure a_1 → a = a_1
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
/-- The free functor `Type u ⥤ ModuleCat R` is a monoidal functor.  -/
ModuleCat.instMonoidalFree : (R : Type u) → [inst : CommRing R] → (ModuleCat.free R).Monoidal
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- If `lfpApprox f x a` is a fixed point, then the supremum of the whole
ordinal-indexed sequence equals the value at `a`.  -/
OrdinalApprox.iSup_lfpApprox_eq_of_mem_fixedPoints : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} {a : Ordinal.{u}},
  OrdinalApprox.lfpApprox f x a ∈ Function.fixedPoints ⇑f →
    ⨆ i, OrdinalApprox.lfpApprox f x i = OrdinalApprox.lfpApprox f x a
-- Mathlib.Order.Disjoint
disjoint_toDual_iff : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b : α},
  Disjoint (OrderDual.toDual a) (OrderDual.toDual b) ↔ Codisjoint a b
-- Mathlib.Order.Interval.Finset.Basic
Finset.Icc_subset_Ici_self : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] [inst_2 : LocallyFiniteOrder α],
  Finset.Icc a b ⊆ Finset.Ici a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.isoPullback_inv_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z}
  {g : Y ⟶ Z} (h : CategoryTheory.IsPullback fst snd f g) [inst_1 : CategoryTheory.Limits.HasPullback f g],
  CategoryTheory.CategoryStruct.comp h.isoPullback.inv fst = CategoryTheory.Limits.pullback.fst f g
-- Mathlib.Order.Lattice
Monotone.map_inf : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : SemilatticeInf β] {f : α → β},
  Monotone f → ∀ (x y : α), f (min x y) = f x ⊓ f y
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
ZeroHom.withTopMap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N] (f : ZeroHom M N),
  f.withTopMap = { toFun := WithTop.map ⇑f, map_zero' := ⋯ }
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.comp_id_left : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (B : LinearMap.BilinForm R M) (r : M →ₗ[R] M), B.comp LinearMap.id r = B.compRight r
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.liftRel_think_right : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (s : Stream'.WSeq α) (t : Stream'.WSeq β),
  Stream'.WSeq.LiftRel R s t.think ↔ Stream'.WSeq.LiftRel R s t
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.VariableChange.map_s : ∀ {R : Type u} [inst : CommRing R] (C : WeierstrassCurve.VariableChange R) {A : Type v} [inst_1 : CommRing A]
  (φ : R →+* A), (C.map φ).s = φ C.s
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.applyPartition.go.match_3.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] (k : α → Ordering) (l : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (m : Std.DTreeMap.Internal.Impl α β) →
      (Std.DTreeMap.Internal.Impl.contains' k l = true → Std.DTreeMap.Internal.Impl.contains' k m = true) → Sort u_3)
  (hm :
    Std.DTreeMap.Internal.Impl.contains' k l = true →
      Std.DTreeMap.Internal.Impl.contains' k Std.DTreeMap.Internal.Impl.leaf = true)
  (h_1 :
    (hm :
        Std.DTreeMap.Internal.Impl.contains' k l = true →
          Std.DTreeMap.Internal.Impl.contains' k Std.DTreeMap.Internal.Impl.leaf = true) →
      motive Std.DTreeMap.Internal.Impl.leaf hm)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l_1 r : Std.DTreeMap.Internal.Impl α β) →
            (hm :
                Std.DTreeMap.Internal.Impl.contains' k l = true →
                  Std.DTreeMap.Internal.Impl.contains' k (Std.DTreeMap.Internal.Impl.inner size k' v' l_1 r) = true) →
              motive (Std.DTreeMap.Internal.Impl.inner size k' v' l_1 r) hm),
  (match Std.DTreeMap.Internal.Impl.leaf, hm with
    | Std.DTreeMap.Internal.Impl.leaf, hm => h_1 hm
    | Std.DTreeMap.Internal.Impl.inner size k' v' l_1 r, hm => h_2 size k' v' l_1 r hm) =
    h_1 hm
-- Mathlib.Data.Set.Function
Set.InjOn.image_sdiff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {t : Set α},
  Set.InjOn f s → f '' (s \ t) = f '' s \ f '' (s ∩ t)
-- Init.Internal.Order.Basic
Lean.Order.instMonoBindIO : Lean.Order.MonoBind IO
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- Algebraic closure of isomorphic fields are isomorphic  -/
IsAlgClosure.equivOfEquiv : {R : Type u} →
  {S : Type u_3} →
    (L : Type v) →
      (M : Type w) →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Field L] →
              [inst_3 : Field M] →
                [inst_4 : Algebra R M] →
                  [inst_5 : Module.IsTorsionFree R M] →
                    [IsAlgClosure R M] →
                      [inst_7 : Algebra S L] →
                        [inst_8 : Module.IsTorsionFree S L] →
                          [IsAlgClosure S L] → [IsDomain R] → [IsDomain S] → S ≃+* R → L ≃+* M
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_of_equivalences : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₁' : CategoryTheory.MorphismProperty D₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [W₁'.RespectsIso] [W₂'.RespectsIso] [L.IsInduced]
  [L.functor.IsEquivalence] [R.IsInduced] [R.functor.IsEquivalence] [T.IsLeftDerivabilityStructure]
  (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor), B.IsLeftDerivabilityStructure
-- Mathlib.LinearAlgebra.Dual.Lemmas
TensorProduct.AlgebraTensorModule.dualDistrib_apply : ∀ {R : Type u_1} (A : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module A M] [inst_7 : Module R N] [inst_8 : IsScalarTower R A M] (f : Module.Dual A M) (g : Module.Dual R N)
  (m : M) (n : N), ((TensorProduct.AlgebraTensorModule.dualDistrib R A M N) (f ⊗ₜ[R] g)) (m ⊗ₜ[R] n) = g n • f m
-- Mathlib.Logic.Equiv.Sum
Equiv.prodSumDistrib_symm_apply_right : ∀ {α : Type u_9} {β : Type u_10} {γ : Type u_11} (a : α × γ),
  (Equiv.prodSumDistrib α β γ).symm (Sum.inr a) = (a.1, Sum.inr a.2)
-- Init.Grind.Interactive
/-- `show_term tac` runs `tac`, then displays the generated proof in the InfoView.
 -/
Lean.Parser.Tactic.Grind.showTerm : Lean.ParserDescr
-- Mathlib.Data.PFun
PFun.prodLift.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) (x : α),
  f.prodLift g x = { Dom := (f x).Dom ∧ (g x).Dom, get := fun h => ((f x).get ⋯, (g x).get ⋯) }
-- Init.Data.BitVec.Lemmas
BitVec.replicate_succ' : ∀ {w n : ℕ} {x : BitVec w}, BitVec.replicate (n + 1) x = BitVec.cast ⋯ (BitVec.replicate n x ++ x)
-- Mathlib.Order.Basic
lt_of_forall_le_imp_ne : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, (∀ c ≤ a, c ≠ b) → a < b
-- Mathlib.Topology.UniformSpace.Ascoli
UniformSpace.mk.congr_simp : ∀ {α : Type u} [toTopologicalSpace : TopologicalSpace α] [toTopologicalSpace_1 : TopologicalSpace α]
  (e_toTopologicalSpace : toTopologicalSpace = toTopologicalSpace_1) (uniformity uniformity_1 : Filter (α × α))
  (e_uniformity : uniformity = uniformity_1) (symm : Filter.Tendsto Prod.swap uniformity uniformity)
  (comp : (uniformity.lift' fun s => SetRel.comp s s) ≤ uniformity)
  (nhds_eq_comap_uniformity : ∀ (x : α), nhds x = Filter.comap (Prod.mk x) uniformity),
  { toTopologicalSpace := toTopologicalSpace, uniformity := uniformity, symm := symm, comp := comp,
      nhds_eq_comap_uniformity := nhds_eq_comap_uniformity } =
    { toTopologicalSpace := toTopologicalSpace_1, uniformity := uniformity_1, symm := ⋯, comp := ⋯,
      nhds_eq_comap_uniformity := ⋯ }
-- Lean.Elab.Parallel
/-- Runs a list of TacticM computations in parallel (without cancellation hook).

Returns an iterator that yields results in completion order, wrapped in `Except Exception α`.
 -/
Lean.Elab.Tactic.TacticM.parIterGreedy : {α : Type} →
  List (Lean.Elab.Tactic.TacticM α) →
    Lean.Elab.Tactic.TacticM (Std.IterM Lean.Elab.Tactic.TacticM (Except Lean.Exception α))