mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.TensorProduct.Map
/-- This is a binary version of `TensorProduct.map`: Given a bilinear map `f : M ⟶ P ⟶ Q` and a
bilinear map `g : N ⟶ S ⟶ T`, if we think `f` and `g` as semilinear maps with two inputs, then
`map₂ f g` is a bilinear map taking two inputs `M ⊗ N → P ⊗ S → Q ⊗ S` defined by
`map₂ f g (m ⊗ n) (p ⊗ s) = f m p ⊗ g n s`.

Mathematically, `TensorProduct.map₂` is defined as the composition
`M ⊗ N -map→ Hom(P, Q) ⊗ Hom(S, T) -homTensorHomMap→ Hom(P ⊗ S, Q ⊗ T)`.
 -/
TensorProduct.map₂ : {R : Type u_1} →
  {R₂ : Type u_2} →
    {R₃ : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring R₂] →
          [inst_2 : CommSemiring R₃] →
            {σ₂₃ : R₂ →+* R₃} →
              {σ₁₃ : R →+* R₃} →
                {M : Type u_7} →
                  {N : Type u_8} →
                    {M₂ : Type u_12} →
                      {M₃ : Type u_13} →
                        {N₂ : Type u_14} →
                          {N₃ : Type u_15} →
                            [inst_3 : AddCommMonoid M] →
                              [inst_4 : AddCommMonoid N] →
                                [inst_5 : AddCommMonoid M₂] →
                                  [inst_6 : AddCommMonoid N₂] →
                                    [inst_7 : AddCommMonoid M₃] →
                                      [inst_8 : AddCommMonoid N₃] →
                                        [inst_9 : Module R M] →
                                          [inst_10 : Module R N] →
                                            [inst_11 : Module R₂ M₂] →
                                              [inst_12 : Module R₂ N₂] →
                                                [inst_13 : Module R₃ M₃] →
                                                  [inst_14 : Module R₃ N₃] →
                                                    (M →ₛₗ[σ₁₃] M₂ →ₛₗ[σ₂₃] M₃) →
                                                      (N →ₛₗ[σ₁₃] N₂ →ₛₗ[σ₂₃] N₃) →
                                                        TensorProduct R M N →ₛₗ[σ₁₃]
                                                          TensorProduct R₂ M₂ N₂ →ₛₗ[σ₂₃] TensorProduct R₃ M₃ N₃
-- Mathlib.Order.MinMax
Monotone.map_min : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β} {a b : α},
  Monotone f → f (min a b) = min (f a) (f b)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.opEquiv.match_13.splitter : (C : Type u_1) →
  (motive : CategoryTheory.WithTerminal Cᵒᵖ → Sort u_2) →
    (x : CategoryTheory.WithTerminal Cᵒᵖ) →
      ((x : Cᵒᵖ) → motive (CategoryTheory.WithTerminal.of x)) →
        (Unit → motive CategoryTheory.WithTerminal.star) → motive x
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.instCategoryPullbackShift : (C : Type u_2) →
  [inst : CategoryTheory.Category.{u_1, u_2} C] →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst_1 : AddMonoid A] →
          [inst_2 : AddMonoid B] →
            [inst_3 : CategoryTheory.HasShift C B] →
              (x : A →+ B) → CategoryTheory.Category.{u_1, u_2} (CategoryTheory.PullbackShift C x)
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.outsidePart_nest : ∀ {p : DyckWord}, p.nest.outsidePart = 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.getKey? (t.minKeyD fallback) = some (t.minKeyD fallback)
-- Mathlib.Data.Prod.Basic
Prod.map_surjective : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Nonempty γ] [Nonempty δ] {f : α → γ} {g : β → δ},
  Function.Surjective (Prod.map f g) ↔ Function.Surjective f ∧ Function.Surjective g
-- Mathlib.Topology.Category.TopCat.Monoidal
/-- The unit interval `TopCat.I` is homeomorphic to `unitInterval`.  -/
TopCat.I.homeomorph : ↑TopCat.I ≃ₜ ↑unitInterval
-- Mathlib.Topology.Continuous
ContinuousAt.iterate : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} {f : X → X},
  ContinuousAt f x → f x = x → ∀ (n : ℕ), ContinuousAt f^[n] x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGetEntryGT?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α}, t₁.Equiv t₂ → Std.DTreeMap.Const.getEntryGT? t₁ k = Std.DTreeMap.Const.getEntryGT? t₂ k
-- Std.Http.Data.Body.Stream
_private.Std.Http.Data.Body.Stream.0.Std.Http.Body.Channel.Consumer.resolve : Std.Http.Body.Channel.Consumer✝ → Option Std.Http.Chunk → BaseIO Bool
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.equivCongrLeft_apply : ∀ {ι : Type u} {β : ι → Type v} {κ : Type u_1} [inst : (i : ι) → Zero (β i)] (h : ι ≃ κ) (f : Π₀ (i : ι), β i),
  (DFinsupp.equivCongrLeft h) f = DFinsupp.comapDomain' ⇑h.symm ⋯ f
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Semiring.addFn? : Lean.Meta.Sym.Arith.Semiring → Option Lean.Expr
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeExtension.compatible_comap : ∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : ValuativeRel A]
  [inst_3 : ValuativeRel B] [inst_4 : Algebra A B] [ValuativeExtension A B] {Γ : Type u_3}
  [inst_6 : LinearOrderedCommMonoidWithZero Γ] (w : Valuation B Γ) [w.Compatible],
  (Valuation.comap (algebraMap A B) w).Compatible
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_filter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] [inst_2 : Inhabited α] {f : (a : α) → β a → Bool} {k : α} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl.getKey! k = ((t.getKey? k).pfilter fun x h' => f x (t.get x ⋯)).get!
-- Std.Async.System
Std.Async.System.instReprUserId : Repr Std.Async.System.UserId
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isSome_get?_iff_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {a : α},
  (t.get? a).isSome = true ↔ a ∈ t
-- Mathlib.Analysis.SpecialFunctions.Exp
/-- If `f` has sum `a`, then `exp ∘ f` has product `exp a`.  -/
HasSum.rexp : ∀ {ι : Type u_1} {f : ι → ℝ} {a : ℝ}, HasSum f a → HasProd (Real.exp ∘ f) (Real.exp a)
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.SimpCongrTheorems.lemmas : Lean.Meta.SimpCongrTheorems → Lean.SMap Lean.Name (List Lean.Meta.SimpCongrTheorem)
-- Mathlib.MeasureTheory.PiSystem
generatePiSystem_measurableSet : ∀ {α : Type u_1} [M : MeasurableSpace α] {S : Set (Set α)},
  (∀ s ∈ S, MeasurableSet s) → ∀ t ∈ generatePiSystem S, MeasurableSet t
-- Mathlib.Algebra.Module.Presentation.Basic
/-- Given `relations : Relations A`, this is the obvious solution to `relations`
in the quotient `relations.Quotient`.  -/
Module.Relations.Solution.ofQuotient : {A : Type u} → [inst : Ring A] → (relations : Module.Relations A) → relations.Solution relations.Quotient
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.toFun_tendsto_bot_of_firstNonzeroIsPos : ∀ {coef : ℝ} {exps : Tactic.ComputeAsymptotics.UnitMonomial} {basis : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.WellFormedBasis basis →
    List.length exps = List.length basis →
      coef < 0 →
        exps.FirstNonzeroIsPos →
          have t := { coef := coef, unit := exps };
          Filter.Tendsto (t.toFun basis) Filter.atTop Filter.atBot
-- Mathlib.Order.Category.BoolAlg
BoolAlg.ofHom_hom : ∀ {X Y : BoolAlg} (f : X ⟶ Y), BoolAlg.ofHom (BoolAlg.Hom.hom f) = f
-- Mathlib.Data.List.Sort
List.sortedGT_map_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List αᵒᵈ}, (List.map (⇑OrderDual.ofDual) l).SortedGT ↔ l.SortedLT
-- Mathlib.MeasureTheory.Group.Arithmetic
Pi.measurableMul₂ : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : (i : ι) → Mul (α i)] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  [∀ (i : ι), MeasurableMul₂ (α i)], MeasurableMul₂ ((i : ι) → α i)
-- Lean.Meta.Tactic.Grind.Action
/-- Helper action for satellite solvers that use `CheckResult`.
 -/
Lean.Meta.Grind.Action.solverAction : Lean.Meta.Grind.GoalM Lean.Meta.Grind.CheckResult →
  Lean.Meta.Grind.GrindM Lean.Meta.Grind.TGrind → Lean.Meta.Grind.Action
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Connected.set_univ_walk_nonempty : ∀ {V : Type u} {G : SimpleGraph V}, G.Connected → ∀ (u v : V), Set.univ.Nonempty
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
/-- For any `x : ℝ` the sequence $\frac{f^n(x)-x}{n}$ tends to the translation number of `f`.
In particular, this limit does not depend on `x`.  -/
CircleDeg1Lift.tendsto_translationNumber : ∀ (f : CircleDeg1Lift) (x : ℝ), Filter.Tendsto (fun n => ((f ^ n) x - x) / ↑n) Filter.atTop (nhds f.translationNumber)
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- A class asserting the existence of a left adjoint.  -/
CategoryTheory.Functor.IsRightAdjoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor D C → Prop
-- Mathlib.Analysis.SpecialFunctions.Exp
/-- `Real.exp` as an order isomorphism between `ℝ` and `(0, +∞)`.  -/
Real.expOrderIso : ℝ ≃o ↑(Set.Ioi 0)
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_solve_elim_cert.eq_2 : ∀ (d₁ : ℤ) (p₁ : Int.Internal.Linear.Poly) (d₂ : ℤ) (p₂ : Int.Internal.Linear.Poly) (d : ℤ)
  (p : Int.Internal.Linear.Poly),
  (∀ (a₁ : ℤ) (x₁ : Int.Internal.Linear.Var) (p₁_1 : Int.Internal.Linear.Poly) (a₂ : ℤ) (x₂ : Int.Internal.Linear.Var)
      (p₂_1 : Int.Internal.Linear.Poly),
      p₁ = Int.Internal.Linear.Poly.add a₁ x₁ p₁_1 → p₂ = Int.Internal.Linear.Poly.add a₂ x₂ p₂_1 → False) →
    Int.Internal.Linear.dvd_solve_elim_cert d₁ p₁ d₂ p₂ d p = false
-- Mathlib.Algebra.Group.Defs
/-- A monoid is Dedekind-finite if every element with a left inverse also has a right inverse.  -/
IsDedekindFiniteMonoid.of_exists_self_mul_eq_one : ∀ (M : Type u_2) [inst : Monoid M], (∀ (x y : M), x * y = 1 → ∃ z, y * z = 1) → IsDedekindFiniteMonoid M
-- Mathlib.Algebra.Field.GeomSum
geom_sum_Ico' : ∀ {K : Type u_2} [inst : DivisionRing K] {x : K},
  x ≠ 1 → ∀ {m n : ℕ}, m ≤ n → ∑ i ∈ Finset.Ico m n, x ^ i = (x ^ m - x ^ n) / (1 - x)
-- Lean.Meta.DiscrTree.Basic
Lean.Meta.DiscrTree.instToExprKey : Lean.ToExpr Lean.Meta.DiscrTree.Key
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Int.Internal.Linear.Expr.denoteExpr : (ℕ → Lean.Expr) → Int.Internal.Linear.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.map_zero : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_S_M₂ : Module S M₂}
  {σ : R →+* S} {σ' : S →+* R} {re₁ : RingHomInvPair σ σ'} {re₂ : RingHomInvPair σ' σ} (e : M ≃ₛₗ[σ] M₂), e 0 = 0
-- Lean.DocString.Extension
Lean.removeDocStringCore : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → [Lean.MonadEnv m] → [MonadLiftT BaseIO m] → Lean.Name → m Unit
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.OmissionReason.deep.sizeOf_spec : sizeOf Lean.PrettyPrinter.Delaborator.OmissionReason.deep = 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_insertManyIfNewUnit_list_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α (fun x => Unit) cmp} [inst : Std.TransCmp cmp]
  {l : List α}, (Std.ExtDTreeMap.Const.insertManyIfNewUnit t l).size ≤ t.size + l.length
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono : ∀ (N : Type u_2) [inst : Add N] [IsLeftCancelAdd N] [inst_2 : PartialOrder N] [AddLeftMono N], AddLeftStrictMono N
-- Batteries.Control.Nondet.Basic
/-- Convert a non-deterministic value into a lazy list, keeping the backtrackable state.
Be careful that monadic operations on the `MLList` will not respect this state!
 -/
Nondet.toMLList : {σ : Type} → {m : Type → Type} → [inst : Lean.MonadBacktrack σ m] → {α : Type} → Nondet m α → MLList m (α × σ)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate the expression `η ▷ f` into a normalized form.  -/
Mathlib.Tactic.BicategoryLike.MkEval.mkEvalWhiskerRight : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEval m] →
    Mathlib.Tactic.BicategoryLike.Mor₂ →
      Mathlib.Tactic.BicategoryLike.Mor₁ →
        Mathlib.Tactic.BicategoryLike.NormalExpr →
          Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Data.Multiset.Bind
Multiset.instSProd : {α : Type u_1} → {β : Type v} → SProd (Multiset α) (Multiset β) (Multiset (α × β))
-- Mathlib.MeasureTheory.Measure.Real
/-- **Alias** of `MeasureTheory.measureReal_add_sdiff`. -/
MeasureTheory.measureReal_add_diff : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s →
    autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_add_sdiff._auto_1 →
      autoParam (μ t ≠ ⊤) MeasureTheory.measureReal_add_sdiff._auto_3 → μ.real s + μ.real (t \ s) = μ.real (s ∪ t)
-- Mathlib.Algebra.Lie.Basic
/-- An equivalence of Lie algebra modules (denoted as `M ≃ₗ⁅R,L⁆ N`) is a linear equivalence
which is also a morphism of Lie algebra modules.  -/
LieModuleEquiv : (R : Type u) →
  (L : Type v) →
    (M : Type w) →
      (N : Type w₁) →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [Module R M] → [Module R N] → [LieRingModule L M] → [LieRingModule L N] → Type (max w w₁)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
Dense.lipschitzWith_extend : ∀ {α : Type u_4} {β : Type u_5} [inst : PseudoEMetricSpace α] [inst_1 : EMetricSpace β] [CompleteSpace β] {s : Set α}
  (hs : Dense s) {f : ↑s → β} {K : NNReal}, LipschitzWith K f → LipschitzWith K (hs.extend f)
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.kroneckerTMulBilinear_apply : ∀ (R : Type u_1) {S : Type u_2} {α : Type u_3} {β : Type u_5} {l : Type u_9} {m : Type u_10} {n : Type u_11}
  {p : Type u_12} [inst : CommSemiring R] [inst_1 : AddCommMonoid α] [inst_2 : AddCommMonoid β] [inst_3 : Module R α]
  [inst_4 : Module R β] [inst_5 : Semiring S] [inst_6 : Module S α] [inst_7 : SMulCommClass R S α] (A : Matrix l m α)
  (B : Matrix n p β), ((Matrix.kroneckerTMulBilinear R S) A) B = Matrix.kroneckerMap (TensorProduct.tmul R) A B
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.insert_dep : ∀ {α : Type u_1} {M : Matroid α} {B : Set α} {e : α}, M.IsBase B → e ∈ M.E \ B → M.Dep (insert e B)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.fst_swap : ∀ {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst_1 : AddMonoid N] (x : AddMonoid.Coprod M N),
  AddMonoid.Coprod.fst ((AddMonoid.Coprod.swap M N) x) = AddMonoid.Coprod.snd x
-- Init.Data.Int.Order
Int.natAbs_add_of_nonneg : ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → (a + b).natAbs = a.natAbs + b.natAbs
-- Mathlib.CategoryTheory.Shift.Localization
/-- the condition that for all `a : A`, the morphism property `W` is not changed when
we take its inverse image by the shift functor by `a`  -/
CategoryTheory.MorphismProperty.IsCompatibleWithShift.condition : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {W : CategoryTheory.MorphismProperty C} {A : Type w}
  {inst_1 : AddMonoid A} {inst_2 : CategoryTheory.HasShift C A} [self : W.IsCompatibleWithShift A] (a : A),
  W.inverseImage (CategoryTheory.shiftFunctor C a) = W
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.basisOfBasisLeft_apply : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) {ι : Type u_1} (b : Module.Basis ι R ↥A) (i : ι),
  (H.basisOfBasisLeft H' b) i = (algebraMap (↥A) S) (b i)
-- Mathlib.Analysis.Convex.EGauge
le_egauge_smul_left : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] (c : 𝕜)
  (s : Set E) (x : E), egauge 𝕜 s x / ‖c‖ₑ ≤ egauge 𝕜 (c • s) x
-- Mathlib.Analysis.SpecialFunctions.Gamma.Beta
Complex.Gamma_eq_zero_iff : ∀ (s : ℂ), Complex.Gamma s = 0 ↔ ∃ m, s = -↑m
-- Mathlib.CategoryTheory.Preadditive.Mat
/-- A morphism in `Mat_ C` is a dependently typed matrix of morphisms.  -/
CategoryTheory.Mat_.Hom : {C : Type u₁} → [CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Mat_ C → CategoryTheory.Mat_ C → Type v₁
-- Mathlib.Data.Quot
Quotient.exact' : ∀ {α : Sort u_1} {s₁ : Setoid α} {a b : α}, Quotient.mk'' a = Quotient.mk'' b → s₁ a b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : (↑m).WF) {a b : α} (hab : (a == b) = true)
  {h' : m.contains a = true}, Std.DHashMap.Internal.Raw₀.Const.get m a h' = Std.DHashMap.Internal.Raw₀.Const.get m b ⋯
-- Mathlib.Order.CompleteLattice.SetLike
Sublattice.ext_mem_iff : ∀ {X : Type u_1} {L : Sublattice (Set X)} {S T : ↥L}, S = T ↔ ∀ (x : X), x ∈ S ↔ x ∈ T
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS.match_4.congr_eq_5 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n))
  (h_2 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_3 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_5 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_6 : (n : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast n))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)) (a : Lean.Grind.CommRing.Expr) (k : ℕ),
  x = a.pow k →
    (match x with
      | Lean.Grind.CommRing.Expr.num n => h_1 n
      | Lean.Grind.CommRing.Expr.var x => h_2 x
      | a.add b => h_3 a b
      | a.mul b => h_4 a b
      | a.pow k => h_5 a k
      | Lean.Grind.CommRing.Expr.natCast n => h_6 n
      | a.sub b => h_7 a b
      | a.neg => h_8 a
      | Lean.Grind.CommRing.Expr.intCast k => h_9 k) ≍
      h_5 a k
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.toArray_eq_nil_iff : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α], r.toArray = #[] ↔ ¬Std.PRange.UpwardEnumerable.least < r.upper
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.Functor.rightUnitor_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C), F.rightUnitor.hom.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Std.Http.Protocol.H1
/-- Enqueues body chunks into the writer buffer for encoding and sending.
 -/
Std.Http.Protocol.H1.Machine.sendData : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Array Std.Http.Chunk → Std.Http.Protocol.H1.Machine dir
-- Mathlib.Analysis.Normed.Group.Basic
norm_div_eq_norm_left : ∀ {E : Type u_5} [inst : SeminormedGroup E] (x : E) {y : E}, ‖y‖ = 0 → ‖x / y‖ = ‖x‖
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.getLE!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getLE! k = t₂.getLE! k
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.instCoeFunForallSetPresieve : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    CoeFun (CategoryTheory.Coverage C) fun x => (X : C) → Set (CategoryTheory.Presieve X)
-- Mathlib.Order.Filter.Pointwise
Filter.pure_mul : ∀ {α : Type u_2} [inst : Mul α] {g : Filter α} {a : α}, pure a * g = Filter.map (fun x => a * x) g
-- Init.Data.String.Lemmas.Pattern.Find.String
String.Slice.contains_string_eq_false_iff : ∀ {t : String} {s : String.Slice}, s.contains t = false ↔ ¬t.toList <:+: s.copy.toList
-- Mathlib.Topology.Constructions.SumProd
Topology.IsOpenEmbedding.sumSwap : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], Topology.IsOpenEmbedding Sum.swap
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.isBigO_log_const_mul_log_atTop : ∀ (c : ℝ), (fun x => Real.log (c * x)) =O[Filter.atTop] Real.log
-- Mathlib.Order.Filter.IsBounded
Filter.isCoboundedUnder_ge_of_le : ∀ {α : Type u_1} {ι : Type u_4} [inst : Preorder α] (l : Filter ι) [l.NeBot] {f : ι → α} {x : α},
  (∀ (i : ι), f i ≤ x) → Filter.IsCoboundedUnder (fun x1 x2 => x2 ≤ x1) l f
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.hasSum_fst : ∀ {α : Type u_1} {R : Type u_3} (M : Type u_4) [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid R] [inst_3 : AddCommMonoid M] {f : α → TrivSqZeroExt R M} {a : TrivSqZeroExt R M},
  HasSum f a → HasSum (fun x => (f x).fst) a.fst
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.locallySmall_fullSubcategory : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C]
  (P : CategoryTheory.ObjectProperty C), CategoryTheory.LocallySmall.{w, v, u} P.FullSubcategory
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.ofFixingAddSubgroup.append.eq_1 : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {s : Set α} {n : ℕ} [inst_2 : Finite ↑s]
  (x : Fin n ↪ ↥(SubAddAction.ofFixingAddSubgroup M s)),
  SubAddAction.ofFixingAddSubgroup.append x = Fin.Embedding.append ⋯
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.instCompletelyDistribLattice : {V : Type u} → {G : SimpleGraph V} → [Finite V] → CompletelyDistribLattice G.Finsubgraph
-- Mathlib.GroupTheory.Exponent
/-- **Alias** of the reverse direction of `Monoid.exponent_dvd_iff_forall_pow_eq_one`. -/
Monoid.exponent_dvd_of_forall_pow_eq_one : ∀ {G : Type u} [inst : Monoid G] {n : ℕ}, (∀ (g : G), g ^ n = 1) → Monoid.exponent G ∣ n
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- The Lévy-Prokhorov distance `levyProkhorovDist` makes `FiniteMeasure Ω` a pseudometric
space. The instance is recorded on the type synonym
`LevyProkhorov (FiniteMeasure Ω) := FiniteMeasure Ω`.  -/
MeasureTheory.LevyProkhorov.instPseudoMetricSpaceFiniteMeasure : {Ω : Type u_1} →
  [inst : MeasurableSpace Ω] →
    [inst_1 : PseudoEMetricSpace Ω] →
      [OpensMeasurableSpace Ω] → PseudoMetricSpace (MeasureTheory.LevyProkhorov (MeasureTheory.FiniteMeasure Ω))
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.map_smul_of_tower : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (φ : A →ₐc[R] B) {R' : Type u_6} [inst_7 : SMul R' A] [inst_8 : SMul R' B] [LinearMap.CompatibleSMul A B R' R]
  (r : R') (x : A), φ (r • x) = r • φ x
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.inf_comp_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A : C}
  (f g : CategoryTheory.Subobject A), CategoryTheory.CategoryStruct.comp ((f ⊓ g).ofLE f ⋯) f.arrow = (f ⊓ g).arrow
-- Mathlib.Topology.Connected.PathConnected
Specializes.joinedIn : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {F : Set X}, x ⤳ y → x ∈ F → y ∈ F → JoinedIn F x y
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Matrix.toBlocks₂₂.eq_1 : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (n ⊕ o) (l ⊕ m) α),
  M.toBlocks₂₂ = Matrix.of fun i j => M (Sum.inr i) (Sum.inr j)
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.Poly.checkCoeffs : Lean.Grind.CommRing.Poly → Bool