mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.Ascoli
/-- Let `X` be a topological space, `𝔖` a covering of `X` by compact subsets, `α` a uniform space,
and `F : ι → (X → α)` a family which is equicontinuous on each `K ∈ 𝔖`. Then, the uniform
structures of uniform convergence on `𝔖` and pointwise convergence induce the same
uniform structure on `ι`.

This is a specialization of `EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi'` to
the case where `𝔖` covers `X`.  -/
EquicontinuousOn.isUniformInducing_uniformOnFun_iff_pi : ∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  [inst_2 : UniformSpace ι] {𝔖 : Set (Set X)},
  ⋃₀ 𝔖 = Set.univ →
    (∀ K ∈ 𝔖, IsCompact K) →
      (∀ K ∈ 𝔖, EquicontinuousOn F K) → (IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsUniformInducing F)
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_lt_ediv_of_lt : ∀ {a b c : ℤ}, a < b → c ∣ b → 0 < c → a / c < b / c
-- Init.Grind.Interactive
/-- `first (tac) ...` runs each `tac` until one succeeds, or else fails.  -/
Lean.Parser.Tactic.Grind.first : Lean.ParserDescr
-- Mathlib.Algebra.Lie.UniversalEnveloping
instInhabitedUniversalEnvelopingAlgebra : (R : Type u_1) →
  (L : Type u_2) →
    [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → Inhabited (UniversalEnvelopingAlgebra R L)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.paramSet.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (a a_1 : NumberField.mixedEmbedding.realSpace K),
  a = a_1 →
    NumberField.mixedEmbedding.fundamentalCone.paramSet K a = NumberField.mixedEmbedding.fundamentalCone.paramSet K a_1
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.ReflectsFiniteColimits.reflects : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.ReflectsFiniteColimits F] (J : Type)
  [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J],
  CategoryTheory.Limits.ReflectsColimitsOfShape J F
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- If `R` and `ι` lie in the same universe, the rank of `(ι →₀ R)` is `# ι`.  -/
rank_finsupp_self' : ∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R] {ι : Type u}, Module.rank R (ι →₀ R) = Cardinal.mk ι
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- If `F ⊣ G`, then the pushforwards along `F` and `G` are also adjoint.  -/
SheafOfModules.pushforwardPushforwardAdj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {K : CategoryTheory.GrothendieckTopology D} →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D C} →
                {S : CategoryTheory.Sheaf J RingCat} →
                  {R : CategoryTheory.Sheaf K RingCat} →
                    [inst_2 : F.IsContinuous J K] →
                      [inst_3 : G.IsContinuous K J] →
                        (adj : F ⊣ G) →
                          (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) →
                            (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S) →
                              CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op adj.counit) R.obj =
                                  CategoryTheory.CategoryStruct.comp ψ.hom (G.op.whiskerLeft φ.hom) →
                                CategoryTheory.CategoryStruct.comp φ.hom
                                      (CategoryTheory.CategoryStruct.comp (F.op.whiskerLeft ψ.hom)
                                        (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op adj.unit)
                                          S.obj)) =
                                    CategoryTheory.CategoryStruct.id S.obj →
                                  (SheafOfModules.pushforward φ ⊣ SheafOfModules.pushforward ψ)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insert_eq_insert! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {k : α} {v : β k} {l : Std.DTreeMap.Internal.Impl α β} {h : l.Balanced},
  (Std.DTreeMap.Internal.Impl.insert k v l h).impl = Std.DTreeMap.Internal.Impl.insert! k v l
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- The difference with `Finset.sum_involution` is that the involution is a
non-dependent function, rather than being allowed to use membership of the domain of the sum.  -/
Finset.sum_ninvolution : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] {f : ι → M} (g : ι → ι),
  (∀ (a : ι), f a + f (g a) = 0) →
    (∀ (a : ι), f a ≠ 0 → g a ≠ a) → (∀ (a : ι), g a ∈ s) → (∀ (a : ι), g (g a) = a) → ∑ x ∈ s, f x = 0
-- Init.Data.ByteArray.Lemmas
ByteArray.extract.eq_1 : ∀ (a : ByteArray) (b e : ℕ), a.extract b e = a.copySlice b ByteArray.empty 0 (e - b)
-- Mathlib.Data.Semiquot
Semiquot.mem_univ : ∀ {α : Type u_1} [inst : Inhabited α] (a : α), a ∈ Semiquot.univ
-- Mathlib.Analysis.Meromorphic.FactorizedRational
/-- Factorized rational functions are nowhere locally constant zero.
 -/
Function.FactorizedRational.meromorphicOrderAt_ne_top : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {z : 𝕜} (d : 𝕜 → ℤ),
  meromorphicOrderAt (∏ᶠ (u : 𝕜), (fun x => x - u) ^ d u) z ≠ ⊤
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.leval_coe_eq_smeval : ∀ {R : Type u_3} [inst : Semiring R] (r : R), ⇑(Polynomial.leval r) = fun p => p.smeval r
-- Init.Data.Array.Zip
Array.zip_append : ∀ {α : Type u_1} {β : Type u_2} {as bs : Array α} {cs ds : Array β},
  as.size = cs.size → (as ++ bs).zip (cs ++ ds) = as.zip cs ++ bs.zip ds
-- Mathlib.Order.Filter.Lift
Filter.comap_lift_eq2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {m : β → α} {g : Set β → Filter γ},
  Monotone g → (Filter.comap m f).lift g = f.lift (g ∘ Set.preimage m)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `monovaryOn_inv_right`. -/
AntivaryOn.inv_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : CommGroup β] [inst_2 : PartialOrder β]
  [IsOrderedMonoid β] {s : Set ι} {f : ι → α} {g : ι → β}, AntivaryOn f g s → MonovaryOn f g⁻¹ s
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.mem_toArray_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {k : α} {v : β k}, ⟨k, v⟩ ∈ (↑m).toArray ↔ m.get? k = some v
-- Lean.Elab.Command
Lean.Elab.Command.instTypeNameMacroExpandedSnapshot : TypeName Lean.Elab.Command.MacroExpandedSnapshot
-- Mathlib.Topology.Compactness.Compact
Subsingleton.compactSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [Subsingleton X], CompactSpace X
-- Mathlib.MeasureTheory.Measure.Prod
/-- The product of two uniformly locally doubling measures is a uniformly locally doubling measure,
assuming the second one is s-finite.
 -/
IsUnifLocDoublingMeasure.prod : ∀ {X : Type u_4} {Y : Type u_5} [inst : PseudoMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : PseudoMetricSpace Y]
  [inst_3 : MeasurableSpace Y] (μ : MeasureTheory.Measure X) (ν : MeasureTheory.Measure Y) [MeasureTheory.SFinite ν]
  [IsUnifLocDoublingMeasure μ] [IsUnifLocDoublingMeasure ν], IsUnifLocDoublingMeasure (μ.prod ν)
-- Std.Time.Date.Unit.Year
/-- Creates an `Offset` from a natural number.
 -/
Std.Time.Year.Offset.ofNat : ℕ → Std.Time.Year.Offset
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey?_unitOfList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k : α}, l.contains k = false → (Std.ExtDTreeMap.Const.unitOfList l cmp).getKey? k = none
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion₂_vadd : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : VAdd α β] (s : (i : ι) → κ i → Set α)
  (t : Set β), (⋃ i, ⋃ j, s i j) +ᵥ t = ⋃ i, ⋃ j, s i j +ᵥ t
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.log_inv : ∀ {G : Type u_5} [inst : AddGroup G] (x : WithZero (Multiplicative G)), x⁻¹.log = -x.log
-- Mathlib.Analysis.Normed.Group.Uniform
/-- A homomorphism `f` of seminormed groups is continuous, if there exists a constant `C` such that
for all `x`, one has `‖f x‖ ≤ C * ‖x‖`.  -/
MonoidHomClass.continuous_of_bound : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F]
  [inst_2 : FunLike 𝓕 E F] [MonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ), (∀ (x : E), ‖f x‖ ≤ C * ‖x‖) → Continuous ⇑f
-- Std.Sync.SharedMutex
/-- `mutex.atomicallyRead k` runs `k` with read access to the mutex's state while locking the mutex
for shared read access.

Calling `mutex.atomicallyRead` while already holding the underlying `BaseSharedMutex` in the same
thread is undefined behavior.
 -/
Std.SharedMutex.atomicallyRead : {m : Type → Type u_1} →
  {α β : Type} → [Monad m] → [MonadLiftT BaseIO m] → [MonadFinally m] → Std.SharedMutex α → ReaderT α m β → m β
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.brecOn.eq : ∀ {pu : Lean.Compiler.LCNF.Purity} {motive_1 : Lean.Compiler.LCNF.Alt pu → Sort u}
  {motive_2 : Lean.Compiler.LCNF.FunDecl pu → Sort u} {motive_3 : Lean.Compiler.LCNF.Cases pu → Sort u}
  {motive_4 : Lean.Compiler.LCNF.Code pu → Sort u} {motive_5 : Array (Lean.Compiler.LCNF.Alt pu) → Sort u}
  {motive_6 : List (Lean.Compiler.LCNF.Alt pu) → Sort u} (t : Lean.Compiler.LCNF.Code pu)
  (F_1 : (t : Lean.Compiler.LCNF.Alt pu) → t.below → motive_1 t)
  (F_2 : (t : Lean.Compiler.LCNF.FunDecl pu) → t.below → motive_2 t)
  (F_3 : (t : Lean.Compiler.LCNF.Cases pu) → t.below → motive_3 t)
  (F_4 : (t : Lean.Compiler.LCNF.Code pu) → t.below → motive_4 t)
  (F_5 : (t : Array (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_1 t → motive_5 t)
  (F_6 : (t : List (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_2 t → motive_6 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 = F_4 t (Lean.Compiler.LCNF.Code.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6).2
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Morphisms of group objects preserve inverses.  -/
CategoryTheory.GrpObj.inv_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.GrpObj A] [inst_3 : CategoryTheory.GrpObj B] (f : A ⟶ B)
  [CategoryTheory.IsMonHom f] {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv h)
-- Mathlib.Data.PFun
PFun.comp_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) (a : α), f.comp g a = (g a).bind f
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_eq_iff' : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y z : P}, midpoint R x y = z ↔ (Equiv.pointReflection z) x = y
-- Mathlib.Topology.FiberBundle.Constructions
Bundle.Trivial.trivialization.eq_1 : ∀ (B : Type u_1) (F : Type u_2) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F],
  Bundle.Trivial.trivialization B F =
    { toOpenPartialHomeomorph := (Bundle.Trivial.homeomorphProd B F).toOpenPartialHomeomorph, baseSet := Set.univ,
      open_baseSet := ⋯, source_eq := ⋯, target_eq := ⋯, proj_toFun := ⋯ }
-- Mathlib.RingTheory.Derivation.Basic
Derivation.compAlgebraMapL_apply_apply : ∀ (R : Type u_1) (A : Type u_2) (B : Type u_3) (M : Type u_4) [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : AddCommMonoid M] [inst_4 : Algebra R A] [inst_5 : Algebra R B]
  [inst_6 : Module A M] [inst_7 : Module B M] [inst_8 : Module R M] [inst_9 : Algebra A B]
  [inst_10 : IsScalarTower R A B] [inst_11 : IsScalarTower A B M] [inst_12 : IsScalarTower R B M] (d : Derivation R B M)
  (x : A), ((Derivation.compAlgebraMapL R A B M) d) x = d ((algebraMap A B) x)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
/-- The derivative of `tan x - x` is `1/(cos x)^2 - 1` away from the zeroes of cos.  -/
Real.deriv_tan_sub_id : ∀ (x : ℝ), Real.cos x ≠ 0 → deriv (fun y => Real.tan y - y) x = 1 / Real.cos x ^ 2 - 1
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.left_distrib : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x y z : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F (x.mul (y.add z)) ((x.mul y).add (x.mul z))
-- Mathlib.CategoryTheory.Monoidal.Action.End
/-- A variant of
`CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedAction`
that takes value in the monoidal opposite of `D ⥤ D`.  -/
CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop : (C : Type u_1) →
  (D : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            CategoryTheory.Functor C (CategoryTheory.Functor D D)ᴹᵒᵖ
-- Mathlib.Algebra.Group.EvenFunction
Function.Odd.smul_odd : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg α] {γ : Type u_3} {f : α → β} {g : α → γ} [inst_1 : Ring β]
  [inst_2 : AddCommGroup γ] [inst_3 : Module β γ], Function.Odd f → Function.Odd g → Function.Even (f • g)
-- Mathlib.CategoryTheory.ComposableArrows.Basic
_private.Mathlib.CategoryTheory.ComposableArrows.Basic.0.CategoryTheory.ComposableArrows.Mk₁.map.match_1.splitter : (motive : (x x_1 : Fin 2) → x ≤ x_1 → Sort u_1) →
  (x x_1 : Fin 2) →
    (x_2 : x ≤ x_1) →
      ((isLt isLt_1 : 0 < 2) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_1⟩ x) →
        ((isLt : 0 < 2) → (isLt_1 : 1 < 2) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_1⟩ x) →
          ((isLt isLt_1 : 1 < 2) → (x : ⟨1, isLt⟩ ≤ ⟨1, isLt_1⟩) → motive ⟨1, isLt⟩ ⟨1, isLt_1⟩ x) → motive x x_1 x_2
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
/-- Two decomposition fields are isomorphic.  -/
IsDecompositionField.ringEquiv : (K : Type u_2) →
  (L : Type u_3) →
    {B : Type u_4} →
      [inst : Field K] →
        [inst_1 : Field L] →
          [inst_2 : Algebra K L] →
            [inst_3 : CommRing B] →
              (P : Ideal B) →
                (D : Type u_5) →
                  [inst_4 : Field D] →
                    [inst_5 : Algebra D L] →
                      [inst_6 : MulSemiringAction Gal(L/K) B] →
                        (D' : Type u_8) →
                          [inst_7 : Field D'] →
                            [inst_8 : Algebra D' L] →
                              [IsDecompositionField K L P D] → [IsDecompositionField K L P D'] → D ≃+* D'
-- Mathlib.Order.Filter.Pointwise
Filter.mul_mem_mul : ∀ {α : Type u_2} [inst : Mul α] {f g : Filter α} {s t : Set α}, s ∈ f → t ∈ g → s * t ∈ f * g
-- Mathlib.Computability.TuringMachine.Tape
/-- Replace the current value of the head on the tape.  -/
Turing.Tape.write : {Γ : Type u_1} → [inst : Inhabited Γ] → Γ → Turing.Tape Γ → Turing.Tape Γ
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.inr_f_triangle_mor₃_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (p : ℤ),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inr φ).f p)
      ((CochainComplex.mappingCone.triangle φ).mor₃.f p) =
    0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.minKey?_modify_eq_minKey? : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} {f : β → β}, (Std.DTreeMap.Raw.Const.modify t k f).minKey? = t.minKey?
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.endsWith_char_iff_get : ∀ {c : Char} {s : String}, s.endsWith c = true ↔ ∃ (h : s.endPos ≠ s.startPos), (s.endPos.prev h).get ⋯ = c
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_mul_self_eq_abs : ∀ (x : ℝ), √(x * x) = |x|
-- Mathlib.Data.Set.Lattice
/-- `⋃₀` and `𝒫` form a Galois insertion.  -/
Set.sUnionPowersetGI : {α : Type u_1} → GaloisInsertion (fun x => ⋃₀ x) fun x => 𝒫 x
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (hg : S.g = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork S hf hg c hc).φH =
    CategoryTheory.Limits.Fork.ι c
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey?_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β},
  (m.insert k v).getKey? a = if (k == a) = true then some k else m.getKey? a
-- Mathlib.Algebra.Order.Monoid.Basic
OrderEmbedding.mulRight.eq_1 : ∀ {α : Type u_2} [inst : Mul α] [inst_1 : LinearOrder α] [inst_2 : MulRightStrictMono α] (m : α),
  OrderEmbedding.mulRight m = OrderEmbedding.ofStrictMono (fun n => n * m) ⋯
-- Mathlib.Algebra.Algebra.Epi
Algebra.IsEpi.injective_lift_mul : ∀ {R : Type u_1} {A : Type u_2} {inst : CommSemiring R} {inst_1 : Semiring A} {inst_2 : Algebra R A}
  [self : Algebra.IsEpi R A], Function.Injective ⇑(TensorProduct.lift (LinearMap.mul R A))
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instMulAction_1.eq_1 : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α],
  OrderDual.instMulAction_1 = { toSMul := OrderDual.instSMul, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Sum
_private.Mathlib.Combinatorics.SimpleGraph.Sum.0.SimpleGraph.edgeSetSumEquiv.match_1.eq_4 : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W}
  (motive : (x x_1 : V ⊕ W) → (G ⊕g H).Adj x x_1 → Sort u_3) (u : W) (v : V) (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inl v))
  (h_1 : (u v : V) → (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inl v)) → motive (Sum.inl u) (Sum.inl v) h)
  (h_2 : (u v : W) → (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inr v)) → motive (Sum.inr u) (Sum.inr v) h)
  (h_3 : (u : V) → (v : W) → (h : (G ⊕g H).Adj (Sum.inl u) (Sum.inr v)) → motive (Sum.inl u) (Sum.inr v) h)
  (h_4 : (u : W) → (v : V) → (h : (G ⊕g H).Adj (Sum.inr u) (Sum.inl v)) → motive (Sum.inr u) (Sum.inl v) h),
  (match Sum.inr u, Sum.inl v, h with
    | Sum.inl u, Sum.inl v, h => h_1 u v h
    | Sum.inr u, Sum.inr v, h => h_2 u v h
    | Sum.inl u, Sum.inr v, h => h_3 u v h
    | Sum.inr u, Sum.inl v, h => h_4 u v h) =
    h_4 u v h
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roo_succ_succ : ∀ {m n : ℤ}, ((m + 1)<...n + 1).toArray = Array.map (fun x => x + 1) (m<...n).toArray
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.δ.congr_simp : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P P_1 : Algebra.Generators R S σ),
  P = P_1 → Algebra.Generators.H1Cotangent.δ Q P = Algebra.Generators.H1Cotangent.δ Q P_1
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
/-- Every two-sided ideal is also a left ideal.  -/
TwoSidedIdeal.asIdeal : {R : Type u_1} → [inst : Ring R] → TwoSidedIdeal R →o Ideal R
-- Mathlib.Data.Finset.Insert
Finset.singleton_nonempty : ∀ {α : Type u_1} (a : α), {a}.Nonempty
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.mk.congr_simp : ∀ {α : Type u_6} [inst : MeasurableSpace α] (toOuterMeasure toOuterMeasure_1 : MeasureTheory.OuterMeasure α)
  (e_toOuterMeasure : toOuterMeasure = toOuterMeasure_1)
  (m_iUnion :
    ∀ ⦃f : ℕ → Set α⦄,
      (∀ (i : ℕ), MeasurableSet (f i)) →
        Pairwise (Function.onFun Disjoint f) → toOuterMeasure (⋃ i, f i) = ∑' (i : ℕ), toOuterMeasure (f i))
  (trim_le : toOuterMeasure.trim ≤ toOuterMeasure),
  { toOuterMeasure := toOuterMeasure, m_iUnion := m_iUnion, trim_le := trim_le } =
    { toOuterMeasure := toOuterMeasure_1, m_iUnion := ⋯, trim_le := ⋯ }
-- Mathlib.GroupTheory.Coset.Basic
/-- The natural bijection between the cosets `s + g` and `s`.  -/
AddSubgroup.rightCosetEquivAddSubgroup : {α : Type u_1} → [inst : AddGroup α] → {s : AddSubgroup α} → (g : α) → ↑(AddOpposite.op g +ᵥ ↑s) ≃ ↥s
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.b₄_of_isShortNF_of_char_three : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] [CharP R 3], W.b₄ = -W.a₄
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
/-- Pushforward and pullback of ideal sheaves forms a Galois connection.  -/
AlgebraicGeometry.Scheme.IdealSheafData.map_gc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), GaloisConnection (fun x => x.comap f) fun x => x.map f
-- Mathlib.Algebra.Free
FreeSemigroup.lift_of_mul : ∀ {α : Type u} {β : Type v} [inst : Semigroup β] (f : α → β) (x : α) (y : FreeSemigroup α),
  (FreeSemigroup.lift f) (FreeSemigroup.of x * y) = f x * (FreeSemigroup.lift f) y
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.le_liminf_add : ∀ {α : Type u_3} {f : Filter α} {u v : α → EReal}, Filter.liminf u f + Filter.liminf v f ≤ Filter.liminf (u + v) f
-- Init.Data.Range.Polymorphic.PRange
Std.Ric.mk.injEq : ∀ {α : Type u} (upper upper_1 : α), ((*...=upper) = *...=upper_1) = (upper = upper_1)
-- Mathlib.Analysis.Convex.Basic
Convex.lineMap_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {s : Set E} [AddRightMono 𝕜],
  Convex 𝕜 s → ∀ {x y : E}, x ∈ s → y ∈ s → ∀ {t : 𝕜}, t ∈ Set.Icc 0 1 → (AffineMap.lineMap x y) t ∈ s
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.addRight_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A : C} [inst_2 : CategoryTheory.AddGrpObj A] (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ A),
  (CategoryTheory.AddGrpObj.addRight f).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id A)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A)
          (CategoryTheory.CategoryStruct.comp f CategoryTheory.AddGrpObj.neg)))
      CategoryTheory.AddMonObj.add
-- Mathlib.LinearAlgebra.Matrix.IsDiag
/-- Diagonal matrices are generated by the `Matrix.diagonal` of their `Matrix.diag`.  -/
Matrix.IsDiag.diagonal_diag : ∀ {α : Type u_1} {n : Type u_4} [inst : Zero α] [inst_1 : DecidableEq n] {A : Matrix n n α},
  A.IsDiag → Matrix.diagonal A.diag = A
-- Mathlib.Order.Comparable
not_incompRel_of_total : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Total r] (a b : α), ¬IncompRel r a b
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.baseChange_nonsingular : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  {f : A →ₐ[S] B},
  Function.Injective ⇑f → ∀ (x y : A), (W.baseChange B).Nonsingular (f x) (f y) ↔ (W.baseChange A).Nonsingular x y
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.ExprCnstr.mk.inj : ∀ {eq : Bool} {lhs rhs : Nat.Internal.Linear.Expr} {eq_1 : Bool} {lhs_1 rhs_1 : Nat.Internal.Linear.Expr},
  { eq := eq, lhs := lhs, rhs := rhs } = { eq := eq_1, lhs := lhs_1, rhs := rhs_1 } →
    eq = eq_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1