mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.Coset.Basic
/-- If `H ≤ K`, then `G/H ≃ G/K × K/H` nonconstructively.
The constructive version is `quotientEquivProdOfLE'`.  -/
Subgroup.quotientEquivProdOfLE : {α : Type u_1} → [inst : Group α] → {s t : Subgroup α} → s ≤ t → α ⧸ s ≃ (α ⧸ t) × ↥t ⧸ s.subgroupOf t
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsMulTorsion.of_surjective`.

---

The image of a surjective torsion group homomorphism is torsion.  -/
IsTorsion.of_surjective : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {f : G →* H},
  Function.Surjective ⇑f → IsMulTorsion G → IsMulTorsion H
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, (Set.Iic a).OrdConnected
-- Mathlib.Analysis.Calculus.Darboux
/-- **Darboux's theorem**: if `a ≤ b` and `f' b ≤ m ≤ f' a`, then `f' c = m` for some
`c ∈ [a, b]`.  -/
exists_hasDerivWithinAt_eq_of_le_of_ge : ∀ {a b : ℝ} {f f' : ℝ → ℝ},
  a ≤ b →
    (∀ x ∈ Set.Icc a b, HasDerivWithinAt f (f' x) (Set.Icc a b) x) →
      ∀ {m : ℝ}, f' a ≤ m → m ≤ f' b → m ∈ f' '' Set.Icc a b
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.Coalgebra.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (A : C) (a : A ⟶ G.obj A)
  (counit :
    autoParam (CategoryTheory.CategoryStruct.comp a (G.ε.app A) = CategoryTheory.CategoryStruct.id A)
      CategoryTheory.Comonad.Coalgebra.counit._autoParam)
  (coassoc :
    autoParam (CategoryTheory.CategoryStruct.comp a (G.δ.app A) = CategoryTheory.CategoryStruct.comp a (G.map a))
      CategoryTheory.Comonad.Coalgebra.coassoc._autoParam)
  (A_1 : C) (a_1 : A_1 ⟶ G.obj A_1)
  (counit_1 :
    autoParam (CategoryTheory.CategoryStruct.comp a_1 (G.ε.app A_1) = CategoryTheory.CategoryStruct.id A_1)
      CategoryTheory.Comonad.Coalgebra.counit._autoParam)
  (coassoc_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp a_1 (G.δ.app A_1) = CategoryTheory.CategoryStruct.comp a_1 (G.map a_1))
      CategoryTheory.Comonad.Coalgebra.coassoc._autoParam),
  ({ A := A, a := a, counit := counit, coassoc := coassoc } =
      { A := A_1, a := a_1, counit := counit_1, coassoc := coassoc_1 }) =
    (A = A_1 ∧ a ≍ a_1)
-- Std.Http.Data.Body.Empty
Std.Http.Body.instCoeContextAsyncResponseEmptyAny : Coe (Std.Async.ContextAsync (Std.Http.Response Std.Http.Body.Empty))
  (Std.Async.ContextAsync (Std.Http.Response Std.Http.Body.Any))
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.instBEqAltParamInfo.beq : Lean.Meta.Match.AltParamInfo → Lean.Meta.Match.AltParamInfo → Bool
-- Init.Data.Int.Cooper
Int.Cooper.resolve_left_dvd₁ : ∀ (a c d p x : ℤ), p ≤ a * x → a ∣ Int.Cooper.resolve_left a c d p x + p
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.invOf_submatrix_equiv_eq : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] (A : Matrix m m α) (e₁ e₂ : n ≃ m) [inst_5 : Invertible A]
  [inst_6 : Invertible (A.submatrix ⇑e₁ ⇑e₂)], ⅟(A.submatrix ⇑e₁ ⇑e₂) = (⅟A).submatrix ⇑e₂ ⇑e₁
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
/-- The (sup metric) nonnegative distance between `Pi.single i a` and `Pi.single j b` for
`i ≠ j` is `max (nndist a 0) (nndist b 0)`.  -/
nndist_single_single : ∀ {β : Type u_2} [inst : Fintype β] {Y : Type u_4} [inst_1 : PseudoMetricSpace Y] [inst_2 : Zero Y]
  [inst_3 : DecidableEq β] (i j : β) (a b : Y),
  i ≠ j → nndist (Pi.single i a) (Pi.single j b) = max (nndist a 0) (nndist b 0)
-- Mathlib.RingTheory.Jacobson.Ring
/-- If `R` is a Jacobson ring, and `P` is a maximal ideal of `R[X]`,
then `R → R[X]/P` is an integral map.  -/
Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing : ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal (Polynomial R)) [hP : P.IsMaximal] [IsJacobsonRing R],
  ((Ideal.Quotient.mk P).comp Polynomial.C).IsIntegral
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.lift_mk : ∀ {G : Type u_1} {M : Type u_4} [inst : Group G] [inst_1 : Monoid M] (N : Subgroup G) [nN : N.Normal] {φ : G →* M}
  (HN : N ≤ φ.ker) (g : G), (QuotientGroup.lift N φ HN) ↑g = φ g
-- Mathlib.Analysis.Calculus.Deriv.Mul
ContinuousLinearMap.hasStrictDerivAt_of_bilinear : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {G : Type u_1}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : 𝕜} {B : E →L[𝕜] F →L[𝕜] G} {u : 𝕜 → E} {v : 𝕜 → F}
  {u' : E} {v' : F},
  HasStrictDerivAt u u' x →
    HasStrictDerivAt v v' x → HasStrictDerivAt (fun x => (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) x
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeGrammar.Produces.trans_derives : ∀ {T : Type u_1} {g : ContextFreeGrammar T} {u v w : List (Symbol T g.NT)},
  g.Produces u v → g.Derives v w → g.Derives u w
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instAddSubgroupClass : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G], AddSubgroupClass (OpenNormalAddSubgroup G) G
-- Mathlib.Algebra.Homology.BifunctorShift
/-- The condition that `((F.mapBifunctorHomologicalComplex _ _).obj K₁).obj K₂` has
a total cochain complex.  -/
CochainComplex.HasMapBifunctor : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] →
              [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂] →
                CochainComplex C₁ ℤ →
                  CochainComplex C₂ ℤ →
                    [inst_5 : CategoryTheory.Preadditive D] →
                      (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                        [F.PreservesZeroMorphisms] → [∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] → Prop
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_sum : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {ι : Type u_4} [inst_3 : Fintype ι] (f : ι → ↥S), ↑(∑ i, f i) = ∑ i, ↑(f i)
-- Mathlib.Order.Filter.AtTopBot.Basic
/-- The `atTop` filter for `↑(Ici a)` comes from the `atTop` filter in the ambient order.  -/
Filter.atTop_Ici_eq : ∀ {α : Type u_3} [inst : Preorder α] [IsDirectedOrder α] (a : α), Filter.atTop = Filter.comap Subtype.val Filter.atTop
-- Mathlib.Analysis.Calculus.ContDiff.Deriv
ContDiffOn.continuousOn_derivWithin : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {f : 𝕜 → F} {s : Set 𝕜},
  ContDiffOn 𝕜 n f s → UniqueDiffOn 𝕜 s → 1 ≤ n → ContinuousOn (derivWithin f s) s
-- Mathlib.ModelTheory.ElementarySubstructures
/-- The Tarski-Vaught test for elementarity of a substructure.  -/
FirstOrder.Language.Substructure.isElementary_of_exists : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (S : L.Substructure M),
  (∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → ↥S) (a : M),
      φ.Realize default (Fin.snoc (Subtype.val ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (Subtype.val ∘ x) ↑b)) →
    S.IsElementary
-- Mathlib.Topology.UniformSpace.Pi
uniformContinuous_pi : ∀ {ι : Type u_1} {α : ι → Type u} [U : (i : ι) → UniformSpace (α i)] {β : Type u_4} [inst : UniformSpace β]
  {f : β → (i : ι) → α i}, UniformContinuous f ↔ ∀ (i : ι), UniformContinuous fun x => f x i
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Section.mk.inj : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} {inst : AddGroup N} {inst_1 : AddGroup E} {inst_2 : AddGroup G}
  {S : AddGroupExtension N E G} {toFun : G → E} {rightInverse_rightHom : Function.RightInverse toFun ⇑S.rightHom}
  {toFun_1 : G → E} {rightInverse_rightHom_1 : Function.RightInverse toFun_1 ⇑S.rightHom},
  { toFun := toFun, rightInverse_rightHom := rightInverse_rightHom } =
      { toFun := toFun_1, rightInverse_rightHom := rightInverse_rightHom_1 } →
    toFun = toFun_1
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.isInitialMul_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasStrictInitialObjects C]
  {I : C} (X : C) [inst_2 : CategoryTheory.Limits.HasBinaryProduct I X] (hI : CategoryTheory.Limits.IsInitial I),
  (CategoryTheory.Limits.isInitialMul X hI).inv = hI.to (I ⨯ X)
-- Mathlib.Lean.Linter
/-- Runs a `CommandElabM` action when the provided linter option is `true`.

This function assumes you have already called `withSetOptionIn`; use `whenLinterActivated`
to do so automatically. At the start of linter code, `whenLinterActivated` should be preferred when
possible.

Note: this definition is marked as `@[macro_inline]`, so it is okay to supply it with a linter
option which has been registered in the same module.
 -/
Lean.Linter.whenLinterOption : {m : Type → Type} → [Monad m] → [Lean.MonadOptions m] → [Lean.MonadEnv m] → Lean.Option Bool → m Unit → m Unit
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- Negating a rotation by -π / 2 is equivalent to rotation by π / 2.  -/
Orientation.neg_rotation_neg_pi_div_two : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V), -(o.rotation ↑(-Real.pi / 2)) x = (o.rotation ↑(Real.pi / 2)) x
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor_obj_left_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.toArrowArrowFunctor.obj sq).left.right = sq.X₃
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.monoidHomCongrRightEquiv.eq_1 : ∀ {M : Type u_4} {N₁ : Type u_9} {N₂ : Type u_10} [inst : MulOneClass M] [inst_1 : Monoid N₁] [inst_2 : Monoid N₂]
  (e : N₁ ≃* N₂),
  e.monoidHomCongrRightEquiv =
    { toFun := e.toMonoidHom.comp, invFun := e.symm.toMonoidHom.comp, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.RingTheory.Frobenius
AlgHom.IsArithFrobAt.localize_algebraMap : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {φ : S →ₐ[R] S}
  {Q : Ideal S} (H : φ.IsArithFrobAt Q) [inst_3 : Q.IsPrime] (x : S),
  H.localize ((algebraMap S (Localization.AtPrime Q)) x) = (algebraMap S (Localization.AtPrime Q)) (φ x)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.instIsNegApply : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N], IsNegApply (QuadraticMap R M N) M N
-- Mathlib.CategoryTheory.Filtered.Basic
/-- The triangles of consisting of a morphism in `H` and the maps to `sup O H` commute.
 -/
CategoryTheory.IsFiltered.toSup_commutes : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFiltered C] (O : Finset C)
  (H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))) {X Y : C} (mX : X ∈ O) (mY : Y ∈ O)
  {f : X ⟶ Y},
  ⟨X, ⟨Y, ⟨mX, ⟨mY, f⟩⟩⟩⟩ ∈ H →
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsFiltered.toSup O H mY) =
      CategoryTheory.IsFiltered.toSup O H mX
-- Mathlib.Data.DFinsupp.Module
/-- Coercion from a `DFinsupp` to a pi type is a `LinearMap`.  -/
DFinsupp.coeFnLinearMap : {ι : Type u} →
  (γ : Type w) →
    {β : ι → Type v} →
      [inst : Semiring γ] →
        [inst_1 : (i : ι) → AddCommMonoid (β i)] →
          [inst_2 : (i : ι) → Module γ (β i)] → (Π₀ (i : ι), β i) →ₗ[γ] (i : ι) → β i
-- Mathlib.Topology.Algebra.ConstMulAction
IsOpen.vadd_left : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [ContinuousConstVAdd G α] {s : Set G} {t : Set α}, IsOpen t → IsOpen (s +ᵥ t)
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_inf_mul_relfinrank : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A B C : IntermediateField F E),
  A.relfinrank (B ⊓ C) * B.relfinrank C = (A ⊓ B).relfinrank C
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.fstₗ.eq_1 : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β],
  OrderMonoidHom.fstₗ α β = { toFun := fun p => (ofLex p).1, map_one' := ⋯, map_mul' := ⋯, monotone' := ⋯ }
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.State.mk.sizeOf_spec : ∀ (goals : List Lean.MVarId), sizeOf { goals := goals } = 1 + sizeOf goals
-- Init.Data.List.Nat.Range
List.snd_lt_add_of_mem_zipIdx : ∀ {α : Type u_1} {x : α × ℕ} {l : List α} {k : ℕ}, x ∈ l.zipIdx k → x.2 < k + l.length
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
/-- The real power function with any exponent is not integrable on `(0, +∞)`.  -/
not_integrableOn_Ioi_rpow : ∀ (s : ℝ), ¬MeasureTheory.IntegrableOn (fun x => x ^ s) (Set.Ioi 0) MeasureTheory.volume
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.RespectsLeft.precomp : ∀ {C : Type u} {inst : CategoryTheory.CategoryStruct.{v, u} C} {P Q : CategoryTheory.MorphismProperty C}
  [self : P.RespectsLeft Q] {X Y Z : C} (i : X ⟶ Y),
  Q i → ∀ (f : Y ⟶ Z), P f → P (CategoryTheory.CategoryStruct.comp i f)
-- Mathlib.CategoryTheory.Localization.Linear
CategoryTheory.Localization.instLinearLocalization : (R : Type w) →
  [inst : Ring R] →
    {C : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          (W : CategoryTheory.MorphismProperty C) →
            [CategoryTheory.Linear R C] →
              [inst_4 : CategoryTheory.Preadditive W.Localization] →
                [W.Q.Additive] → CategoryTheory.Linear R W.Localization
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.takeWhileTR.go.eq_2 : ∀ {α : Type u_1} (p : α → Bool) (l : List α) (a : Array α) (a_1 : α) (as : List α),
  List.takeWhileTR.go✝ p l (a_1 :: as) a = bif p a_1 then List.takeWhileTR.go✝ p l as (a.push a_1) else a.toList
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolParams.mk : Lean.Lsp.TextDocumentIdentifier → Lean.Lsp.DocumentSymbolParams
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.preΨ'_even : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (m : ℕ),
  W.preΨ' (2 * (m + 3)) =
    W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) - W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2
-- Lean.Meta.Basic
Lean.Meta.Context.configKey : Lean.Meta.Context → UInt64
-- Mathlib.CategoryTheory.MorphismProperty.RetractArgument
CategoryTheory.MorphismProperty.llp_eq_of_le_llp_of_hasFactorization_of_isStableUnderRetracts : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C}
  [W₁.HasFactorization W₂] [W₁.IsStableUnderRetracts], W₁ ≤ W₂.llp → W₂.llp = W₁
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_union_Icc_eq_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a < b → b ≤ c → Set.Ioc a b ∪ Set.Icc b c = Set.Ioc a c
-- Mathlib.Algebra.GroupWithZero.Action.Hom
AddMonoidHom.coe_smul : ∀ {M : Type u_1} {A : Type u_3} {B : Type u_4} [inst : AddZeroClass A] [inst_1 : AddZeroClass B]
  [inst_2 : DistribSMul M B] (m : M) (f : A →+ B), ⇑(m • f) = m • ⇑f
-- Lean.Environment
Lean.PersistentEnvExtensionState.mk.injEq : ∀ {α σ : Type} (importedEntries : Array (Array α)) (state : σ) (importedEntries_1 : Array (Array α)) (state_1 : σ),
  ({ importedEntries := importedEntries, state := state } =
      { importedEntries := importedEntries_1, state := state_1 }) =
    (importedEntries = importedEntries_1 ∧ state = state_1)
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.iterToSum_C_C : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (a : R),
  (MvPolynomial.iterToSum R S₁ S₂) (MvPolynomial.C (MvPolynomial.C a)) = MvPolynomial.C a
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
/-- The spheres `s₁` and `s₂` are externally tangent at some point.  -/
EuclideanGeometry.Sphere.IsExtTangent : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [NormedAddTorsor V P] → EuclideanGeometry.Sphere P → EuclideanGeometry.Sphere P → Prop
-- Mathlib.Algebra.Order.Hom.Monoid
/-- Any type satisfying `OrderMonoidIsoClass` can be cast into `OrderMonoidIso` via
`OrderMonoidIsoClass.toOrderMonoidIso`.  -/
instCoeTCOrderMonoidIsoOfOrderIsoClassOfMulEquivClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : Preorder α] →
        [inst_1 : Preorder β] →
          [inst_2 : MulOneClass α] →
            [inst_3 : MulOneClass β] →
              [inst_4 : EquivLike F α β] → [OrderIsoClass F α β] → [MulEquivClass F α β] → CoeTC F (α ≃*o β)
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.abs_sub_floor_le : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R] {a : R},
  0 ≤ a → |a - ↑⌊a⌋₊| ≤ 1
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_diagonal_pow : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_12} [inst : Semiring α] [inst_1 : Fintype n] [inst_2 : Fintype m]
  [inst_3 : DecidableEq n] [inst_4 : DecidableEq m] (A : Matrix n n α) (D : Matrix m m α) (k : ℕ),
  Matrix.fromBlocks A 0 0 D ^ k = Matrix.fromBlocks (A ^ k) 0 0 (D ^ k)
-- Mathlib.AlgebraicGeometry.StructureSheaf
/-- The ring homomorphism from the stalk of the structure sheaf of `R` at a point corresponding to
a prime ideal `p` to the localization of `R` at `p`,
formed by gluing the `openToLocalization` maps.  -/
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.stalkToLocalizationₗ : (R M : Type u) →
  [inst : CommRing R] →
    [inst_1 : AddCommGroup M] →
      [inst_2 : Module R M] →
        (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)) →
          (AlgebraicGeometry.structurePresheafInModuleCat R M).stalk x ⟶
            ModuleCat.of R (LocalizedModule x.asIdeal.primeCompl M)
-- Mathlib.Order.RelIso.Basic
RelIso.toEquiv_toMap : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (f : α ≃ β), ↑(RelIso.toMap r f) = f
-- Mathlib.Algebra.Group.Hom.Defs
/-- Copy of a `ZeroHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities.  -/
ZeroHom.copy : {M : Type u_4} →
  {N : Type u_5} → [inst : Zero M] → [inst_1 : Zero N] → (f : ZeroHom M N) → (f' : M → N) → f' = ⇑f → ZeroHom M N
-- Mathlib.LinearAlgebra.Basis.Fin
Module.Basis.coe_finTwoProd_repr : ∀ {R : Type u_7} [inst : Semiring R] (x : R × R), ⇑((Module.Basis.finTwoProd R).repr x) = ![x.1, x.2]
-- Mathlib.Order.GaloisConnection.Basic
OrderIso.bddBelow_preimage : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) {s : Set β},
  BddBelow (⇑e ⁻¹' s) ↔ BddBelow s
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- `simp`-normal form of `bot_arrow_eq_zero`.  -/
CategoryTheory.MonoOver.initialTo_b_eq_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {B : C}, CategoryTheory.Limits.initial.to B = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.eval_polynomial_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  P 2 ≠ 0 →
    (MvPolynomial.eval P) W.polynomial / P 2 ^ 6 =
      Polynomial.evalEval (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3) W.toAffine.polynomial
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.forgetMapTerminal_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T)
  (X_1 : CategoryTheory.Over X),
  (CategoryTheory.Over.forgetMapTerminal X hT).inv.app X_1 = CategoryTheory.CategoryStruct.id X_1.left
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
CategoryTheory.WalkingIso.equiv_apply_snd_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor CategoryTheory.WalkingIso C),
  (CategoryTheory.WalkingIso.equiv F).snd.snd = CategoryTheory.WalkingIso.toIso F
-- Mathlib.Tactic.DeriveTraversable
/-- The deriving handler for `Functor`.  -/
Mathlib.Deriving.Traversable.functorDeriveHandler : Lean.Elab.DerivingHandler
-- Mathlib.Tactic.ITauto
/-- The variable `x` here names the variable that will be used in the elaborated proof.
* `(p: ((x:A) → B) → C) ⊢ B → C`
 -/
Mathlib.Tactic.ITauto.Proof.impImpSimp : Lean.Name → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftIso_functor_map_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) {X Y : CategoryTheory.Comma L₁ R} (f : X ⟶ Y),
  ((CategoryTheory.Comma.mapLeftIso R i).functor.map f).right = f.right
-- Mathlib.Tactic.CasesM
/-- Common implementation of `casesm` and `casesm!`.  -/
Mathlib.Tactic.elabCasesM : Array Lean.Term → Bool → Bool → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.limitsOfShape_le_of_initial : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {J' : Type u''} [inst_2 : CategoryTheory.Category.{v'', u''} J']
  (G : CategoryTheory.Functor J J') [G.Initial], P.limitsOfShape J' ≤ P.limitsOfShape J
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- **Alias** of `Topology.IsQuotientMap.locallyPathConnectedSpace`.

---

Quotients of locally path-connected spaces are locally path-connected.  -/
Topology.IsQuotientMap.locPathConnectedSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [LocallyPathConnectedSpace X]
  {f : X → Y}, Topology.IsQuotientMap f → LocallyPathConnectedSpace Y
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.contains_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [h : Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β k}, (t.insert k v).contains a = (cmp k a == Ordering.eq || t.contains a)
-- Mathlib.MeasureTheory.Group.Arithmetic
AddUnits.instMeasurableSpace.eq_1 : ∀ {M : Type u_4} [inst : AddMonoid M] [inst_1 : MeasurableSpace M],
  AddUnits.instMeasurableSpace = MeasurableSpace.comap AddUnits.val inst_1
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.radius_compContinuousLinearMap_linearIsometryEquiv_eq : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [Nontrivial E] (p : FormalMultilinearSeries 𝕜 F G)
  (u : E ≃ₗᵢ[𝕜] F), (p.compContinuousLinearMap u.toLinearIsometry.toContinuousLinearMap).radius = p.radius
-- Mathlib.CategoryTheory.EssentialImage
CategoryTheory.Functor.essSurj_of_surj : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}, Function.Surjective F.obj → F.EssSurj
-- Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
/-- Let `R` be a complete nonarchimedean ring. If functions `f : α → R` and `g : β → R` are
summable, then so is `fun i : α × β ↦ f i.1 * g i.2`. We will prove later that the assumption that
`R` is complete is not necessary.  -/
_private.Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean.0.Summable.mul_of_complete_nonarchimedean : ∀ {α : Type u_1} {β : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : UniformSpace R] [IsUniformAddGroup R]
  [NonarchimedeanRing R] [CompleteSpace R] {f : α → R} {g : β → R},
  Summable f → Summable g → Summable fun i => f i.1 * g i.2
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.add_assoc : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S]
  (x y z : AddOreLocalization S R), x + y + z = x + (y + z)