mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.PiSystem
piiUnionInter_singleton_left : ∀ {α : Type u_3} {ι : Type u_4} (s : ι → Set α) (S : Set ι),
  piiUnionInter (fun i => {s i}) S = {s' | ∃ t, ∃ (_ : ↑t ⊆ S), s' = ⋂ i ∈ t, s i}
-- Lean.Data.Lsp.Basic
Lean.Lsp.instHashableMarkupContent : Hashable Lean.Lsp.MarkupContent
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffAt_finsetProd : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {x : M} {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiffAt I' I n (f i) x) → ContMDiffAt I' I n (fun x => ∏ i ∈ t, f i x) x
-- Mathlib.AlgebraicTopology.SimplicialNerve
CategoryTheory.SimplicialThickening.Path.ext : ∀ {J : Type u_1} {inst : LinearOrder J} {i j : J} {x y : CategoryTheory.SimplicialThickening.Path i j},
  x.I = y.I → x = y
-- Init.Control.StateRef
StateRefT'.instMonadAttachOfMonad : {ω σ : Type} → {m : Type → Type} → [Monad m] → [MonadAttach m] → MonadAttach (StateRefT' ω σ m)
-- Init.Data.Array.Zip
_private.Init.Data.Array.Zip.0.Array.getElem?_zipWith.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Option α → Option β → Sort u_3) →
      (x : Option α) →
        (x_1 : Option β) →
          ((a : α) → (b : β) → motive (some a) (some b)) →
            ((x : Option α) →
                (x_2 : Option β) → (∀ (a : α) (b : β), x = some a → x_2 = some b → False) → motive x x_2) →
              motive x x_1
-- Init.Tactics
/-- * `change tgt'` will change the goal from `tgt` to `tgt'`,
  assuming these are definitionally equal.
* `change t' at h` will change hypothesis `h : t` to have type `t'`, assuming
  assuming `t` and `t'` are definitionally equal.
* `change a with b` will change occurrences of `a` to `b` in the goal,
  assuming `a` and `b` are definitionally equal.
* `change a with b at h` similarly changes `a` to `b` in the type of hypothesis `h`.
 -/
Lean.Parser.Tactic.change : Lean.ParserDescr
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.instLawfulVecOperatorBinaryRefVecBlast : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.BinaryRefVec fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.blast
-- Init.Data.Nat.Lemmas
Nat.div_lt_div_left : ∀ {a b c : ℕ}, a ≠ 0 → b ∣ a → c ∣ a → (a / b < a / c ↔ c < b)
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.pow.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] (n : M) (m : ℕ),
  Submonoid.pow n m = ((powersHom M) n).mrangeRestrict (Multiplicative.ofAdd m)
-- Mathlib.RingTheory.LocalProperties.Exactness
injective_of_isLocalized_span : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (Mₚ : ↑s → Type u_5) [inst_5 : (r : ↑s) → AddCommMonoid (Mₚ r)] [inst_6 : (r : ↑s) → Module R (Mₚ r)]
      (f : (r : ↑s) → M →ₗ[R] Mₚ r) [inst_7 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] (Nₚ : ↑s → Type u_6)
      [inst_8 : (r : ↑s) → AddCommMonoid (Nₚ r)] [inst_9 : (r : ↑s) → Module R (Nₚ r)] (g : (r : ↑s) → N →ₗ[R] Nₚ r)
      [inst_10 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)] (F : M →ₗ[R] N),
      (∀ (r : ↑s), Function.Injective ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)) →
        Function.Injective ⇑F
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedBilinearMap.map_sub_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : Module 𝕜 G] {f : E × F → G},
  IsBoundedBilinearMap 𝕜 f → ∀ {x : E} {y z : F}, f (x, y - z) = f (x, y) - f (x, z)
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
Topology.IsOpenEmbedding.toOpenPartialHomeomorph_source : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y)
  (h : Topology.IsOpenEmbedding f) [inst_2 : Nonempty X],
  (Topology.IsOpenEmbedding.toOpenPartialHomeomorph f h).source = Set.univ
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.symm : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  f =Θ[l] g → g =Θ[l] f
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instIsLeftCancelAddOfAddOpposite : ∀ {M : Type u_1} [inst : Add Mᵃᵒᵖ] [IsLeftCancelAdd Mᵃᵒᵖ], IsLeftCancelAdd Mᵈᵃᵃ
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isTrail_mapLe : ∀ {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v},
  (SimpleGraph.Walk.mapLe h p).IsTrail ↔ p.IsTrail
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
MeasureTheory.taylorWithinEval_charFun_two_zero' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
  {X : Ω → ℝ},
  AEMeasurable X P →
    ∫ (x : Ω), X x ∂P = 0 →
      ∫ (x : Ω), (X ^ 2) x ∂P = 1 →
        ∀ (t : ℝ),
          taylorWithinEval (MeasureTheory.charFun (MeasureTheory.Measure.map X P)) 2 Set.univ 0 t = 1 - ↑t ^ 2 / 2
-- Mathlib.Order.Minimal
maximalFor_eq_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : LE α] {f : ι → α} {i j : ι}, MaximalFor (fun x => x = j) f i ↔ i = j
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {k k' : α} {v : β},
      Array.find? (fun a => a.1 == k) (Std.DHashMap.Raw.Const.toArray m) = some (k', v) ↔
        m.getKey? k = some k' ∧ Std.DHashMap.Raw.Const.get? m k = some v
-- Mathlib.Analysis.MellinTransform
HasMellin.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℝ → E) (s : ℂ) (m : E),
  HasMellin f s m = (MellinConvergent f s ∧ mellin f s = m)
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- Coefficients of a section `s` of `V` w.r.t. a local frame `{s i}` on `u`.
Outside of `u`, this returns the junk value 0.  -/
IsLocalFrameOn.coeff : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [inst_12 : FiberBundle F V] →
                                        {ι : Type u_7} →
                                          {s : ι → (x : M) → V x} →
                                            {u : Set M} →
                                              {n : WithTop ℕ∞} → IsLocalFrameOn I F n s u → ι → (x : M) → V x →ₗ[𝕜] 𝕜
-- Mathlib.Algebra.Homology.ImageToKernel
imageToKernel.congr_simp : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (f : A ⟶ B) [inst_2 : CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [inst_3 : CategoryTheory.Limits.HasKernel g]
  (w : CategoryTheory.CategoryStruct.comp f g = 0), imageToKernel f g w = imageToKernel f g w
-- Lean.CoreM
/-- Snapshot trees of asynchronous subtasks. As these are untyped and reported only at the end of the
command's main elaboration thread, they are only useful for basic message log reporting; for
incremental reporting and reuse within a long-running elaboration thread, types rooted in
`CommandParsedSnapshot` need to be adjusted.
 -/
Lean.Core.State.snapshotTasks : Lean.Core.State → Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_ofList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)} {k : α}
  {fallback : β},
  (List.map Prod.fst l).contains k = false → Std.DHashMap.Const.getD (Std.DHashMap.Const.ofList l) k fallback = fallback
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- A global integer is in the local integers.  -/
IsDedekindDomain.HeightOneSpectrum.coe_mem_adicCompletionIntegers : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R),
  ↑r ∈ IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers K v
-- Mathlib.Data.List.ReduceOption
List.reduceOption_eq_concat_iff : ∀ {α : Type u_1} (l : List (Option α)) (l' : List α) (a : α),
  l.reduceOption = l'.concat a ↔ ∃ l₁ l₂, l = l₁ ++ some a :: l₂ ∧ l₁.reduceOption = l' ∧ l₂.reduceOption = []
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α} [inst_3 : Inhabited (β k)],
  (List.map Sigma.fst l).contains k = false → (Std.DTreeMap.Raw.ofList l cmp).get! k = default
-- Mathlib.CategoryTheory.LiftingProperties.PushoutProduct
/-- `f □ g` lifts against `X ⟶ ⋆` if and only if `g` lifts against `B ⟹ X ⟶ A ⟹ X`.  -/
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.hasLiftingProperty_mk_isTerminal_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [CategoryTheory.Limits.HasPullbacks C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] {A B K L X Y : C} {f : A ⟶ B} {g : K ⟶ L}
  (t : CategoryTheory.Limits.IsTerminal Y),
  CategoryTheory.HasLiftingProperty (CategoryTheory.Arrow.mk f □ CategoryTheory.Arrow.mk g).hom (t.from X) ↔
    CategoryTheory.HasLiftingProperty g ((CategoryTheory.MonoidalClosed.pre f).app X)
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.coe_ofBijective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] {f : A →ₗc[R] B} (hf : Function.Bijective ⇑f), ⇑(CoalgEquiv.ofBijective hf) = ⇑f
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- Consider a real set `s`. If a property is true almost everywhere in `s ∩ (a, b)` for
all `a, b ∈ s`, then it is true almost everywhere in `s`. Formulated with bare membership.
See also `ae_restrict_of_ae_restrict_inter_Ioo`.  -/
ae_of_mem_of_ae_of_mem_inter_Ioo : ∀ {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ] {s : Set ℝ} {p : ℝ → Prop},
  (∀ (a b : ℝ), a ∈ s → b ∈ s → a < b → ∀ᵐ (x : ℝ) ∂μ, x ∈ s ∩ Set.Ioo a b → p x) → ∀ᵐ (x : ℝ) ∂μ, x ∈ s → p x
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.mk.inj : ∀ {carrier : Type u} {str : CommGroup carrier} {carrier_1 : Type u} {str_1 : CommGroup carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp_app_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (U : TopologicalSpace.Opens ↑↑X) {F : C → C → Type uF}
  {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
  [inst_1 : CategoryTheory.ConcreteCategory C F] (x : carrier (X.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom
        (f.c.app (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).obj U))))
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f U)) x) =
    (CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.eqToHom ⋯))) x
-- Lean.Parser.Module
Lean.Parser.ModuleParserState : Type
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.SavedState.mk.injEq : ∀ (term : Lean.Elab.Term.SavedState) (tactic : Lean.Elab.Tactic.State) (term_1 : Lean.Elab.Term.SavedState)
  (tactic_1 : Lean.Elab.Tactic.State),
  ({ term := term, tactic := tactic } = { term := term_1, tactic := tactic_1 }) = (term = term_1 ∧ tactic = tactic_1)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
mul_inv_le_iff_le_mul : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulRightMono α] {a b c : α}, a * b⁻¹ ≤ c ↔ a ≤ c * b
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.rightInvSeq.eq_2 : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B) (ω_2 : List B),
  cs.rightInvSeq (i :: ω_2) = (cs.wordProd ω_2)⁻¹ * cs.simple i * cs.wordProd ω_2 :: cs.rightInvSeq ω_2
-- Lean.Elab.Arg
Lean.Elab.Term.Arg.stx.injEq : ∀ (val val_1 : Lean.Syntax), (Lean.Elab.Term.Arg.stx val = Lean.Elab.Term.Arg.stx val_1) = (val = val_1)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- `QuadraticMap.polar` as a function from `Sym2`.  -/
QuadraticMap.polarSym2 : {M : Type u_4} → {N : Type u_5} → [AddCommGroup M] → [AddCommGroup N] → (M → N) → Sym2 M → N
-- Mathlib.Algebra.Regular.ULift
ULift.isAddRegular_up : ∀ {R : Type v} [inst : Add R] {a : R}, IsAddRegular { down := a } ↔ IsAddRegular a
-- Mathlib.Topology.Continuous
IsClosed.preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Continuous f → ∀ {t : Set Y}, IsClosed t → IsClosed (f ⁻¹' t)
-- Batteries.Data.DList.Basic
Batteries.DList.mk.inj : ∀ {α : Type u} {apply : List α → List α} {invariant : ∀ (l : List α), apply l = apply [] ++ l}
  {apply_1 : List α → List α} {invariant_1 : ∀ (l : List α), apply_1 l = apply_1 [] ++ l},
  { apply := apply, invariant := invariant } = { apply := apply_1, invariant := invariant_1 } → apply = apply_1
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.trans_assoc : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {R₄ : Type u_4} {E : Type u_5} {E₂ : Type u_6} {E₃ : Type u_7}
  {E₄ : Type u_8} [inst : Semiring R] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : Semiring R₄]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {σ₁₃ : R →+* R₃} {σ₃₁ : R₃ →+* R} {σ₁₄ : R →+* R₄} {σ₄₁ : R₄ →+* R}
  {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {σ₂₄ : R₂ →+* R₄} {σ₄₂ : R₄ →+* R₂} {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃}
  [inst_4 : RingHomInvPair σ₁₂ σ₂₁] [inst_5 : RingHomInvPair σ₂₁ σ₁₂] [inst_6 : RingHomInvPair σ₁₃ σ₃₁]
  [inst_7 : RingHomInvPair σ₃₁ σ₁₃] [inst_8 : RingHomInvPair σ₂₃ σ₃₂] [inst_9 : RingHomInvPair σ₃₂ σ₂₃]
  [inst_10 : RingHomInvPair σ₁₄ σ₄₁] [inst_11 : RingHomInvPair σ₄₁ σ₁₄] [inst_12 : RingHomInvPair σ₂₄ σ₄₂]
  [inst_13 : RingHomInvPair σ₄₂ σ₂₄] [inst_14 : RingHomInvPair σ₃₄ σ₄₃] [inst_15 : RingHomInvPair σ₄₃ σ₃₄]
  [inst_16 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_17 : RingHomCompTriple σ₁₂ σ₂₄ σ₁₄]
  [inst_18 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_19 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
  [inst_20 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] [inst_21 : RingHomCompTriple σ₄₂ σ₂₁ σ₄₁]
  [inst_22 : RingHomCompTriple σ₄₃ σ₃₂ σ₄₂] [inst_23 : RingHomCompTriple σ₄₃ σ₃₁ σ₄₁]
  [inst_24 : SeminormedAddCommGroup E] [inst_25 : SeminormedAddCommGroup E₂] [inst_26 : SeminormedAddCommGroup E₃]
  [inst_27 : SeminormedAddCommGroup E₄] [inst_28 : Module R E] [inst_29 : Module R₂ E₂] [inst_30 : Module R₃ E₃], ⋯
-- Mathlib.Topology.Algebra.Group.Basic
map_mul_right_nhds : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] (x y : G),
  Filter.map (fun x_1 => x_1 * x) (nhds y) = nhds (y * x)
-- Mathlib.Computability.EpsilonNFA
εNFA.IsPath.below.cons : ∀ {α : Type u} {σ : Type v} {M : εNFA α σ} {motive : (a a_1 : σ) → (a_2 : List (Option α)) → M.IsPath a a_1 a_2 → Prop}
  (t s u : σ) (a : Option α) (x : List (Option α)) (a_1 : t ∈ M.step s a) (a_2 : M.IsPath t u x),
  εNFA.IsPath.below a_2 → motive t u x a_2 → εNFA.IsPath.below ⋯
-- Lean.Data.NameMap.Basic
Lean.NameMap : Type → Type
-- Mathlib.Analysis.Convex.Between
wbtw_rotate_iff : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V] {y z : P}
  (x : P), Wbtw R x y z ∧ Wbtw R z x y ↔ x = y
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.instFinitePresentationKaehlerDifferentialOfEssFiniteType : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [Algebra.EssFiniteType R A]
  [Algebra.FormallySmooth R A], Module.FinitePresentation A Ω[A⁄R]
-- Mathlib.Algebra.Algebra.Operations
Submodule.mem_div_iff_smul_subset : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {x : A}
  {I J : Submodule R A}, x ∈ I / J ↔ x • ↑J ⊆ ↑I
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.id.eq_1 : Turing.ToPartrec.Code.id = Turing.ToPartrec.Code.tail.comp Turing.ToPartrec.Code.zero'
-- Init.Data.Array.Lemmas
Array.anyM_eq_anyM_loop : ∀ {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] {p : α → m Bool} {as : Array α} {start stop : ℕ},
  Array.anyM p as start stop = Array.anyM.loop p as (min stop as.size) ⋯ start
-- Mathlib.Data.Matrix.PEquiv
PEquiv.single_mul_single : ∀ {k : Type u_1} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype n] [inst_1 : DecidableEq k]
  [inst_2 : DecidableEq m] [inst_3 : DecidableEq n] [inst_4 : NonAssocSemiring α] (a : m) (b : n) (c : k),
  (PEquiv.single a b).toMatrix * (PEquiv.single b c).toMatrix = (PEquiv.single a c).toMatrix
-- Init.Data.Rat.Lemmas
Rat.intCast_le_intCast : ∀ {a b : ℤ}, ↑a ≤ ↑b ↔ a ≤ b
-- Mathlib.Algebra.Group.Hom.Defs
MulHom.cancel_left : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] {g : N →ₙ* P}
  {f₁ f₂ : M →ₙ* N}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Order.Interval.Basic
Interval.completeLattice : {α : Type u_1} → [inst : CompleteLattice α] → [DecidableLE α] → CompleteLattice (Interval α)
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.upperCentralSeries_eq_top_iff_nilpotencyClass_le : ∀ {G : Type u_1} [inst : AddGroup G] [hG : AddGroup.IsNilpotent G] {n : ℕ},
  AddSubgroup.upperCentralSeries G n = ⊤ ↔ AddGroup.nilpotencyClass G ≤ n
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.diag_σ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Z : C}
  (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diag X)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π (CategoryTheory.Limits.diag X))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.NonPreadditiveAbelian.r X)) h)) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Data.Set.Image
Set.preimage_range : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), f ⁻¹' Set.range f = Set.univ
-- Mathlib.AlgebraicGeometry.ResidueField
/-- For a field `K` and a scheme `X`, the morphisms `Spec K ⟶ X` bijectively correspond
to pairs of points `x` of `X` and embeddings `κ(x) ⟶ K`.  -/
AlgebraicGeometry.Scheme.SpecToEquivOfField : (K : Type u) →
  [inst : Field K] →
    (X : AlgebraicGeometry.Scheme) →
      (AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X) ≃ (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackComparison_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst_3 : CategoryTheory.Limits.HasPullback f g]
  [inst_4 : CategoryTheory.Limits.HasPullback (F.map f) (F.map g)]
  [inst_5 : CategoryTheory.Limits.HasPullback (G.map (F.map f)) (G.map (F.map g))]
  [inst_6 : CategoryTheory.Limits.HasPullback ((F.comp G).map f) ((F.comp G).map g)],
  CategoryTheory.Limits.pullbackComparison (F.comp G) f g =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pullbackComparison F f g))
      (CategoryTheory.Limits.pullbackComparison G (F.map f) (F.map g))
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_filter_eq_false_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {f : α → Bool},
  (Std.HashSet.filter f m).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ m), f (m.get k h) = true
-- Mathlib.Order.Bounds.Basic
isLeast_pair : ∀ {γ : Type u_3} [inst : LinearOrder γ] {a b : γ}, IsLeast {a, b} (min a b)
-- Mathlib.Analysis.Convex.Hull
convexHull_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E], (convexHull 𝕜) 0 = 0
-- Mathlib.Algebra.Order.Archimedean.Defs
exists_int_ge : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [Archimedean R] (x : R), ∃ n, x ≤ ↑n
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context.mvars : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context → Array Lean.Expr
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.functor.eq_1 : ∀ (P : TopCat → Prop) [inst : CompHausLike.HasExplicitFiniteCoproducts P] [inst_1 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)),
  CompHausLike.LocallyConstant.functor P hs =
    CategoryTheory.ObjectProperty.lift
      (CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology (CompHausLike P)))
      CompHausLike.LocallyConstant.functorToPresheaves ⋯
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
aemeasurable_deriv_with_param : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {α : Type u_4} [inst_3 : TopologicalSpace α] [inst_4 : MeasurableSpace α]
  [OpensMeasurableSpace α] [CompleteSpace F] [LocallyCompactSpace 𝕜] [inst_8 : MeasurableSpace 𝕜]
  [OpensMeasurableSpace 𝕜] [inst_10 : MeasurableSpace F] [BorelSpace F] {f : α → 𝕜 → F},
  Continuous (Function.uncurry f) → ∀ (μ : MeasureTheory.Measure (α × 𝕜)), AEMeasurable (fun p => deriv (f p.1) p.2) μ
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
/-- Construct a `Mor₂Iso` term from a Lean expression.  -/
Mathlib.Tactic.Bicategory.Mor₂IsoOfExpr : Lean.Expr → Mathlib.Tactic.Bicategory.BicategoryM Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Mathlib.CategoryTheory.Shift.Opposite
CategoryTheory.instHasShiftOppositeShift : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (A : Type u_2) →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] → CategoryTheory.HasShift (CategoryTheory.OppositeShift C A) A
-- Lean.Elab.PreDefinition.WF.Eqns
Lean.Elab.WF.EqnInfo.fixedParamPerms : Lean.Elab.WF.EqnInfo → Lean.Elab.FixedParamPerms