mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- Heterobasic version of `TensorProduct.lift.equiv`:

A linear equivalence constructing a linear map `M ⊗[R] N →[A] P` given a
bilinear map `M →[A] N →[R] P` with the property that its composition with the
canonical bilinear map `M →[A] N →[R] M ⊗[R] N` is the given bilinear map `M →[A] N →[R] P`.  -/
TensorProduct.AlgebraTensorModule.lift.equiv : (R : Type uR) →
  (A : Type uA) →
    (B : Type uB) →
      (M : Type uM) →
        (N : Type uN) →
          (P : Type uP) →
            [inst : CommSemiring R] →
              [inst_1 : Semiring A] →
                [inst_2 : Semiring B] →
                  [inst_3 : Algebra R A] →
                    [inst_4 : Algebra R B] →
                      [inst_5 : AddCommMonoid M] →
                        [inst_6 : Module R M] →
                          [inst_7 : Module A M] →
                            [inst_8 : IsScalarTower R A M] →
                              [inst_9 : AddCommMonoid N] →
                                [inst_10 : Module R N] →
                                  [inst_11 : AddCommMonoid P] →
                                    [inst_12 : Module R P] →
                                      [inst_13 : Module A P] →
                                        [inst_14 : IsScalarTower R A P] →
                                          [inst_15 : Module B P] →
                                            [inst_16 : IsScalarTower R B P] →
                                              [inst_17 : SMulCommClass A B P] →
                                                (M →ₗ[A] N →ₗ[R] P) ≃ₗ[B] TensorProduct R M N →ₗ[A] P
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- To check that a function is `n` times continuously differentiable, it suffices to check that its
first `n` derivatives are differentiable. This is slightly too strong as the condition we
require on the `n`-th derivative is differentiability instead of continuity, but it has the
advantage of avoiding the discussion of continuity in the proof (and for `n = ∞` this is optimal).
 -/
contDiff_of_differentiable_iteratedDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {n : ℕ∞},
  (∀ (m : ℕ), ↑m ≤ n → Differentiable 𝕜 (iteratedDeriv m f)) → ContDiff 𝕜 (↑n) f
-- Mathlib.Data.Matrix.Diagonal
Matrix.one_apply : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α] {i j : n},
  1 i j = if i = j then 1 else 0
-- Aesop.Util.OrderedHashSet
/-- A hash set that preserves the order of insertions.  -/
Aesop.OrderedHashSet : (α : Type u_1) → [BEq α] → [Hashable α] → Type u_1
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.instFourierInvPair : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_3} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  [CompleteSpace E], FourierInvPair (SchwartzMap V E) (SchwartzMap V E)
-- Mathlib.Algebra.Group.Action.Basic
IsAddUnit.vadd_left_cancel : ∀ {α : Type u_5} {β : Type u_6} [inst : AddMonoid α] [inst_1 : AddAction α β] {a : α},
  IsAddUnit a → ∀ {x y : β}, a +ᵥ x = a +ᵥ y ↔ x = y
-- Mathlib.Data.List.Lattice
List.cons_bagInter_of_not_mem : ∀ {α : Type u_1} {l₂ : List α} {a : α} [inst : DecidableEq α] (l₁ : List α),
  a ∉ l₂ → (a :: l₁).bagInter l₂ = l₁.bagInter l₂
-- Mathlib.NumberTheory.Padics.Complex
/-- `ℂ_[p]` is a normed field, where the norm extends from `PadicAlgCl` along completion.  -/
PadicComplex.normedField : (p : ℕ) → [hp : Fact (Nat.Prime p)] → NormedField ℂ_[p]
-- Mathlib.Data.Set.Pairwise.Basic
Set.PairwiseDisjoint.image_of_le : ∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] {s : Set ι} {f : ι → α},
  s.PairwiseDisjoint f → ∀ {g : ι → ι}, f ∘ g ≤ f → (g '' s).PairwiseDisjoint f
-- Mathlib.Topology.ContinuousOn
/-- Preimage of a set neighborhood of `t` under a continuous map `f` is a set neighborhood of `s`
provided that `f` maps `s` to `t`.  -/
Continuous.tendsto_nhdsSet : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {f : α → β}
  {t : Set β}, Continuous f → Set.MapsTo f s t → Filter.Tendsto f (nhdsSet s) (nhdsSet t)
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- A nilpotent endomorphism has nilpotent eigenvalues.

See also `LinearMap.isNilpotent_trace_of_isNilpotent`.  -/
Module.End.HasEigenvalue.isNilpotent_of_isNilpotent : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] {f : Module.End R M}, IsNilpotent f → ∀ {μ : R}, f.HasEigenvalue μ → IsNilpotent μ
-- Mathlib.Data.Complex.Basic
/-- This shortcut instance ensures we do not find `AddCommMonoid` via the noncomputable
`Complex.instNormedField` instance.  -/
Complex.instAddCommMonoid : AddCommMonoid ℂ
-- Lean.Expr
Lean.ExprStructEq.hash : Lean.ExprStructEq → UInt64
-- Mathlib.SetTheory.Cardinal.Free
FreeRing.eq_1 : ∀ (α : Type u), FreeRing α = FreeAbelianGroup (FreeMonoid α)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
ModularGroup.coe_T_inv : ↑ModularGroup.T⁻¹ = !![1, -1; 0, 1]
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.instBot : {C : Type u} → [inst : CategoryTheory.Groupoid C] → Bot (CategoryTheory.Subgroupoid C)
-- Batteries.Lean.Position
/-- If `pos` is a `Lean.Position`, then `pos.getDeclsAfter` returns the array of names of declarations
whose selection range begins in position at least `pos`. By using the `selectionRange`, which is
usually smaller than the `range`, we err on the side of including declarations when possible.

By default, this only inspects the local branch of the environment. This is compatible with being
used to find declarations from the current command in a linter, where we have already waited for
async tasks/parallel branches to complete. Further, since the environment exposed to linters does
not include constants added after the elaboration of the current command, it is safe to use this on
the command's start position without picking up later declarations.
 -/
Lean.Position.getDeclsAfter : Lean.Environment →
  Lean.Position → optParam Lean.EnvExtension.AsyncMode Lean.EnvExtension.AsyncMode.local → Array Lean.Name
-- Mathlib.Logic.Small.Set
small_sInter' : ∀ {α : Type u1} {s : Set (Set α)} [Nonempty ↑s] [∀ (t : ↑s), Small.{u, u1} ↑↑t], Small.{u, u1} ↑(⋂₀ s)
-- Mathlib.LinearAlgebra.Dual.Basis
/-- A vector space is linearly equivalent to its dual space.  -/
Module.Basis.toDualEquiv : {R : Type uR} →
  {M : Type uM} →
    {ι : Type uι} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → [DecidableEq ι] → Module.Basis ι R M → [Finite ι] → M ≃ₗ[R] Module.Dual R M
-- Mathlib.Order.Bounds.Basic
isLeast_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b ≤ a → IsLeast (Set.Icc b a) b
-- Std.Do.Triple.SpecLemmas
List.Cursor.tail_at : ∀ {α : Type u_1} {n : ℕ} (l : List α) (h : n < l.length), (List.Cursor.at l n).tail ⋯ = List.Cursor.at l (n + 1)
-- Mathlib.LinearAlgebra.Matrix.Basis
Module.Basis.toMatrix_map : ∀ {ι : Type u_1} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Type u_9} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (b : Module.Basis ι R M) (f : M ≃ₗ[R] N) (v : ι → N),
  (b.map f).toMatrix v = b.toMatrix (⇑f.symm ∘ v)
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
contDiffOn_infty_iff_derivWithin : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜},
  UniqueDiffOn 𝕜 s → (ContDiffOn 𝕜 (↑⊤) f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (↑⊤) (derivWithin f s) s)
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_ofRestrict : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {U : TopCat}
  (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (x : ↑U),
  (X.restrictStalkIso h x).inv = AlgebraicGeometry.PresheafedSpace.Hom.stalkMap (X.ofRestrict h) x
-- Init.Grind.Module.NatModuleNorm
_private.Init.Grind.Module.NatModuleNorm.0.Lean.Grind.Linarith.Expr.denoteN.match_1.eq_7 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (k : ℕ) (a : Lean.Grind.Linarith.Expr)
  (h_1 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b)) (h_2 : (a : Lean.Grind.Linarith.Expr) → motive a.neg)
  (h_3 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_4 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_5 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_6 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_7 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a)),
  (match Lean.Grind.Linarith.Expr.natMul k a with
    | a.sub b => h_1 a b
    | a.neg => h_2 a
    | Lean.Grind.Linarith.Expr.intMul k a => h_3 k a
    | Lean.Grind.Linarith.Expr.zero => h_4 ()
    | Lean.Grind.Linarith.Expr.var v => h_5 v
    | a.add b => h_6 a b
    | Lean.Grind.Linarith.Expr.natMul k a => h_7 k a) =
    h_7 k a
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.pow.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (k : ℕ) → motive k.succ),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | k.succ => h_3 k) =
    h_2 ()
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqPoly.beq.eq_def : ∀ (x x_1 : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.instBEqPoly.beq x x_1 =
    match x, x_1 with
    | Lean.Grind.CommRing.Poly.num a, Lean.Grind.CommRing.Poly.num b => a == b
    | Lean.Grind.CommRing.Poly.add a a_1 a_2, Lean.Grind.CommRing.Poly.add b b_1 b_2 =>
      a == b && (a_1 == b_1 && Lean.Grind.CommRing.instBEqPoly.beq a_2 b_2)
    | x, x_2 => false
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} {aig : Std.Sat.AIG α} (input : aig.RefVec w)
  (distance curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst.go input distance curr hcurr s =
    if hidx : curr < w then
      if hdist : distance + curr < w then
        have s := s.push (input.get (distance + curr) hdist);
        Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst.go input distance (curr + 1) ⋯ s
      else
        have s := s.push (input.get (w - 1) ⋯);
        Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRightConst.go input distance (curr + 1) ⋯ s
    else
      have hcurr := ⋯;
      hcurr ▸ s
-- Init.Data.SInt.Bitwise
Int64.neg_one_or : ∀ {a : Int64}, -1 ||| a = -1
-- Mathlib.Data.Set.Prod
Set.univ_pi_eq_empty : ∀ {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)} {i : ι}, t i = ∅ → Set.univ.pi t = ∅
-- Init.Data.List.Nat.InsertIdx
List.length_insertIdx_of_length_lt : ∀ {α : Type u} {as : List α} {i : ℕ}, as.length < i → ∀ (a : α), (as.insertIdx i a).length = as.length
-- Std.Data.DTreeMap.AdditionalOperations
/-- Updates the values of the map by applying the given function to all mappings, keeping
only those mappings where the function returns `some` value.
 -/
Std.DTreeMap.filterMap : {α : Type u} →
  {β : α → Type v} →
    {γ : α → Type w} →
      {cmp : α → α → Ordering} → ((a : α) → β a → Option (γ a)) → Std.DTreeMap α β cmp → Std.DTreeMap α γ cmp
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
LinearMap.toKerIsLocalized_apply_coe : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (p : Submonoid R) (f : M →ₗ[R] N)
  [inst_5 : IsLocalizedModule p f] {P : Type u_5} [inst_6 : AddCommMonoid P] [inst_7 : Module R P] {Q : Type u_6}
  [inst_8 : AddCommMonoid Q] [inst_9 : Module R Q] (f' : P →ₗ[R] Q) [inst_10 : IsLocalizedModule p f'] (g : M →ₗ[R] P)
  (c : ↥g.ker), ↑((LinearMap.toKerIsLocalized p f f' g) c) = f ↑c
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
/-- The intersection of the sphere of radius `√k` with the integer points in the positive
quadrant.  -/
Behrend.sphere : (n : ℕ) → ℕ → ℕ → Finset (Fin n → ℕ)
-- Mathlib.Algebra.Azumaya.Matrix
AlgHom.mulLeftRightMatrix.inv_comp : ∀ (R : Type u_1) (n : Type u_2) [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n],
  AlgHom.mulLeftRightMatrix_inv R n ∘ₗ (AlgHom.mulLeftRight R (Matrix n n R)).toLinearMap = LinearMap.id
-- Mathlib.Analysis.RCLike.Basic
RCLike.isCauSeq_im : ∀ {K : Type u_1} [inst : RCLike K] (f : CauSeq K norm), IsCauSeq abs fun n => RCLike.im (↑f n)
-- Init.Data.Slice.Array.Lemmas
Array.stop_mkSlice_roi : ∀ {α : Type u_1} {xs : Array α} {lo : ℕ}, (Std.Roi.Sliceable.mkSlice xs lo<...*).stop = xs.size
-- Lean.Meta.Match.CaseArraySizes
_private.Lean.Meta.Match.CaseArraySizes.0.Lean.Meta.introArrayLit.loop : Lean.MVarId →
  Lean.Expr →
    ℕ →
      Lean.Name →
        Lean.Expr → Lean.Expr → ℕ → Array Lean.Expr → Array Lean.Expr → Lean.MetaM (Lean.Expr × Array Lean.Expr)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β], Set.vadd = { vadd := Set.image2 fun x1 x2 => x1 +ᵥ x2 }
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.mapCompRight.eq_1 : ∀ (A : Type u_1) {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (F : CategoryTheory.Functor B C) (G : CategoryTheory.Functor C D),
  CategoryTheory.Join.mapCompRight A F G =
    CategoryTheory.Join.mapIsoWhiskerRight (CategoryTheory.Functor.id A).leftUnitor.symm (F.comp G) ≪≫
      CategoryTheory.Join.mapPairComp (CategoryTheory.Functor.id A) F (CategoryTheory.Functor.id A) G
-- Mathlib.Analysis.Calculus.BumpFunction.Convolution
/-- If `φ` is a normed bump function, approximate `(φ ⋆ g) x₀`
if `g` is near `g x₀` on a ball with radius `φ.rOut` around `x₀`.  -/
ContDiffBump.dist_normed_convolution_le : ∀ {G : Type uG} {E' : Type uE'} [inst : NormedAddCommGroup E'] {g : G → E'} [inst_1 : MeasurableSpace G]
  {μ : MeasureTheory.Measure G} [inst_2 : NormedSpace ℝ E'] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace ℝ G]
  [CompleteSpace E'] {φ : ContDiffBump 0} [BorelSpace G] [inst_7 : FiniteDimensional ℝ G] [μ.IsAddHaarMeasure] {x₀ : G}
  {ε : ℝ},
  MeasureTheory.AEStronglyMeasurable g μ →
    (∀ x ∈ Metric.ball x₀ φ.rOut, dist (g x) (g x₀) ≤ ε) →
      dist (MeasureTheory.convolution (φ.normed μ) g (ContinuousLinearMap.lsmul ℝ ℝ) μ x₀) (g x₀) ≤ ε
-- Std.Time.Format.Modifier
Std.Time.Modifier.N.injEq : ∀ (presentation presentation_1 : Std.Time.Number),
  (Std.Time.Modifier.N presentation = Std.Time.Modifier.N presentation_1) = (presentation = presentation_1)
-- Mathlib.Analysis.Convex.Body
/-- Convex bodies in a fixed normed space `V` form a metric space under the Hausdorff metric.  -/
ConvexBody.instMetricSpace : {V : Type u_1} → [inst : NormedAddCommGroup V] → [inst_1 : NormedSpace ℝ V] → MetricSpace (ConvexBody V)
-- Mathlib.Data.Multiset.Count
Multiset.count_eq_one_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, s.Nodup → a ∈ s → Multiset.count a s = 1
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.mk_le_mk_mul_of_mk_preimage_le : ∀ {α β : Type u} {c : Cardinal.{u}} (f : α → β),
  (∀ (b : β), Cardinal.mk ↑(f ⁻¹' {b}) ≤ c) → Cardinal.mk α ≤ Cardinal.mk β * c
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntInfo.ofWrap0? : Lean.Meta.Grind.Arith.Cutsat.ToIntInfo → Option Lean.Expr
-- Mathlib.GroupTheory.Sylow
/-- `Subgroup.pointwiseMulAction` preserves Sylow subgroups.  -/
Sylow.pointwiseMulAction : {p : ℕ} →
  {G : Type u_1} →
    [inst : Group G] → {α : Type u_2} → [inst_1 : Group α] → [MulDistribMulAction α G] → MulAction α (Sylow p G)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_inter_eq_iff : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {τ : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ) (s : Set Ω) (i : ι),
  MeasurableSet (s ∩ {ω | τ ω = ↑i}) ↔ MeasurableSet (s ∩ {ω | τ ω = ↑i})
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ofIsInitialRight_ι : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂)
  [inst_3 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.obj X₁)]
  [inst_4 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.obj Y₁)]
  (h : CategoryTheory.Limits.IsInitial X₂),
  (CategoryTheory.Functor.PushoutObjObj.ofIsInitialRight F f₁ f₂ h).ι = (F.map f₁).app Y₂
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv_symm`. -/
normalizedFactorsEquivOfQuotEquiv_symm : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDedekindDomain A] {I : Ideal R}
  {J : Ideal A} [inst_3 : IsDedekindDomain R] (f : R ⧸ I ≃+* A ⧸ J) (hI : I ≠ ⊥) (hJ : J ≠ ⊥),
  (IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv f hI hJ).symm =
    IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv f.symm hJ hI
-- Mathlib.RingTheory.LinearDisjoint
/-- Linear disjointness is symmetric if elements in the module commute.  -/
Subalgebra.LinearDisjoint.symm_of_commute : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B → (∀ (a : ↥A) (b : ↥B), Commute ↑a ↑b) → B.LinearDisjoint A
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
_private.Mathlib.LinearAlgebra.QuadraticForm.Signature.0.sigNeg.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : AddCommGroup M] [inst_1 : CommRing R] [inst_2 : LinearOrder R]
  [inst_3 : Module R M] (Q : QuadraticForm R M), sigNeg Q = sigPos (-Q)
-- Mathlib.Analysis.Normed.Ring.Basic
enorm_mul : ∀ {α : Type u_2} [inst : SeminormedAddCommGroup α] [inst_1 : Mul α] [NormMulClass α] (a b : α), ‖a * b‖ₑ = ‖a‖ₑ * ‖b‖ₑ
-- Mathlib.RingTheory.Kaehler.Basic
_private.Mathlib.RingTheory.Kaehler.Basic.0.termFinsupp_map : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Support
mulTSupport_inv : ∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [inst_1 : DivisionMonoid α] (f : X → α),
  mulTSupport f⁻¹ = mulTSupport f
-- Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
Real.BohrMollerup.le_logGammaSeq : ∀ {f : ℝ → ℝ} {x : ℝ},
  ConvexOn ℝ (Set.Ioi 0) f →
    (∀ {y : ℝ}, 0 < y → f (y + 1) = f y + Real.log y) →
      0 < x → x ≤ 1 → ∀ (n : ℕ), f x ≤ f 1 + x * Real.log (↑n + 1) - x * Real.log ↑n + Real.BohrMollerup.logGammaSeq x n
-- Mathlib.RepresentationTheory.Maschke
/-- The sum of the conjugates of `π` by each element `g : G`, as a `k`-linear map.

(We postpone dividing by the size of the group as long as possible.)
 -/
LinearMap.sumOfConjugates : {k : Type u_1} →
  [inst : CommRing k] →
    (G : Type u_2) →
      [inst_1 : Group G] →
        {V : Type u_3} →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Module k V] →
              [inst_4 : Module (MonoidAlgebra k G) V] →
                [IsScalarTower k (MonoidAlgebra k G) V] →
                  {W : Type u_4} →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : Module k W] →
                        [inst_8 : Module (MonoidAlgebra k G) W] →
                          [IsScalarTower k (MonoidAlgebra k G) W] → (W →ₗ[k] V) → [Fintype G] → W →ₗ[k] V
-- Mathlib.Topology.LocallyConstant.Algebra
/-- Evaluation as an `AlgHom`  -/
LocallyConstant.evalₐ : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      (R : Type u_6) →
        [inst_1 : CommSemiring R] → [inst_2 : Semiring Y] → [inst_3 : Algebra R Y] → X → LocallyConstant X Y →ₐ[R] Y
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.Exception.revertFailure.inj : ∀ {mctx : Lean.MetavarContext} {lctx : Lean.LocalContext} {toRevert : Array Lean.Expr} {varName : String}
  {mctx_1 : Lean.MetavarContext} {lctx_1 : Lean.LocalContext} {toRevert_1 : Array Lean.Expr} {varName_1 : String},
  Lean.MetavarContext.MkBinding.Exception.revertFailure mctx lctx toRevert varName =
      Lean.MetavarContext.MkBinding.Exception.revertFailure mctx_1 lctx_1 toRevert_1 varName_1 →
    mctx = mctx_1 ∧ lctx = lctx_1 ∧ toRevert = toRevert_1 ∧ varName = varName_1
-- Mathlib.Data.FunLike.Group
/-- Coercion as a monoid homomorphism.  -/
FunLike.coeMonoidHom : (F : Type u_1) →
  (α : Type u_2) →
    (β : Type u_3) →
      [inst : FunLike F α β] →
        [inst_1 : MulOne F] → [inst_2 : MulOneClass β] → [IsOneApply F α β] → [IsMulApply F α β] → F →* α → β
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.CofixA.intro.hinj : ∀ {F : PFunctor.{uA, uB}} {n : ℕ} {a : F.A} {a_1 : F.B a → PFunctor.Approx.CofixA F n} {F_1 : PFunctor.{uA, uB}}
  {n_1 : ℕ} {a_2 : F_1.A} {a_3 : F_1.B a_2 → PFunctor.Approx.CofixA F_1 n_1},
  F = F_1 →
    n.succ = n_1.succ →
      PFunctor.Approx.CofixA.intro a a_1 ≍ PFunctor.Approx.CofixA.intro a_2 a_3 →
        F = F_1 ∧ n = n_1 ∧ a ≍ a_2 ∧ a_1 ≍ a_3
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.RankPos.mk : ∀ {α : Type u_1} {M : Matroid α}, ¬M.IsBase ∅ → M.RankPos
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.String
String.reduceGT : Lean.Meta.Simp.Simproc
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.biconeCategoryStruct_id : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] (j : CategoryTheory.Bicone J),
  CategoryTheory.CategoryStruct.id j =
    CategoryTheory.Bicone.casesOn j CategoryTheory.BiconeHom.left_id CategoryTheory.BiconeHom.right_id fun k =>
      CategoryTheory.BiconeHom.diagram (CategoryTheory.CategoryStruct.id k)
-- Mathlib.Order.Hom.Lex
RelIso.sumLexComplRight_apply : ∀ {α : Type u_1} {r : α → α → Prop} {x : α} [inst : IsTrans α r] [inst_1 : Std.Trichotomous r] [inst_2 : DecidableRel r]
  (a : { x_1 // ¬r x x_1 } ⊕ Subtype (r x)), (RelIso.sumLexComplRight r x) a = (Equiv.sumCompl (r x)) a.swap
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.map_inf : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (S T : AddSubsemigroup M) (f : M →ₙ+ N),
  Function.Injective ⇑f → AddSubsemigroup.map f (S ⊓ T) = AddSubsemigroup.map f S ⊓ AddSubsemigroup.map f T
-- Mathlib.Algebra.Order.Hom.Basic
le_map_sub_add_map_sub : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : AddGroup α] [inst_2 : Add β]
  [inst_3 : LE β] [SubadditiveHomClass F α β] (f : F) (a b c : α), f (a - c) ≤ f (a - b) + f (b - c)
-- Lean.Elab.SyntheticMVars
/-- Try to synthesize the current list of pending synthetic metavariables.
Return `true` if at least one of them was synthesized.  -/
_private.Lean.Elab.SyntheticMVars.0.Lean.Elab.Term.synthesizeSyntheticMVarsStep : Bool → Bool → Lean.Elab.TermElabM Bool
-- Mathlib.AlgebraicTopology.DoldKan.Faces
AlgebraicTopology.DoldKan.Hσ.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q : ℕ),
  AlgebraicTopology.DoldKan.Hσ q = Homotopy.nullHomotopicMap' (AlgebraicTopology.DoldKan.hσ' q)
-- Init.Data.Nat.Lemmas
Nat.add_sub_one_le_mul : ∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → a + b - 1 ≤ a * b