mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.Extr
/-- If `f` is monotone on `Iic b` and antitone on `Ico b a`, then the maximum of `f` on `Iio a`
is attained at `b`.  -/
isMaxOn_Iio_of_mono_anti : ∀ {α : Type u} {β : Type u_1} [inst : LinearOrder α] [inst_1 : Preorder β] {a b : α} {f : α → β},
  MonotoneOn f (Set.Iic b) → AntitoneOn f (Set.Ico b a) → IsMaxOn f (Set.Iio a) b
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxKey.congr_simp : ∀ {α : Type u} {β : α → Type v} (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (h : t.isEmpty = false),
  t.maxKey h = t_1.maxKey ⋯
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAtOfComplement.mem_domChart_source : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAtOfComplement F I J n f x), x ∈ h.domChart.source
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.fp_iff_derivFamily : ∀ {ι : Type u_1} {f : ι → Ordinal.{u} → Ordinal.{u}} [Small.{u, u_1} ι],
  (∀ (i : ι), Order.IsNormal (f i)) → ∀ {a : Ordinal.{u}}, (∀ (i : ι), f i a = a) ↔ ∃ o, Ordinal.derivFamily f o = a
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.smul_Lp_sub : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : SMul M α] [inst_3 : MeasureTheory.SMulInvariantMeasure M α μ]
  [inst_4 : MeasurableConstSMul M α] (c : Mᵈᵐᵃ) (f g : ↥(MeasureTheory.Lp E p μ)), c • (f - g) = c • f - c • g
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_sub_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R]
  [inst_4 : Sub R] [OrderedSub R] [ExistsAddOfLE R] (a : R), ⌊a - 1⌋₊ = ⌊a⌋₊ - 1
-- Mathlib.CategoryTheory.CodiscreteCategory
/-- Given two functors to a codiscrete category, there is a trivial natural transformation.  -/
CategoryTheory.Codiscrete.natTrans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type w} → {F G : CategoryTheory.Functor C (CategoryTheory.Codiscrete A)} → F ⟶ G
-- Mathlib.CategoryTheory.Iso
CategoryTheory.inv_comp_eq_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (g : X ⟶ Y) [inst_1 : CategoryTheory.IsIso g]
  {f : X ⟶ Y}, CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) f = CategoryTheory.CategoryStruct.id Y ↔ f = g
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.apply_eq_zero_of_isEmpty : ∀ {α : Type u_1} [IsEmpty α] {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α), μ s = 0
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k : α},
  (Std.ExtHashMap.unitOfList l).contains k = l.contains k
-- Lean.DocString.Types
/-- A genre-specific block. `container` specifies what kind of block it is, while `content` specifies
the content within the block.
 -/
Lean.Doc.Block.other : {i : Type u} → {b : Type v} → b → Array (Lean.Doc.Block i b) → Lean.Doc.Block i b
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `M` and `N` are linearly disjoint, if `M` is flat, then for any family of
`R`-linearly independent elements `{ m_i }` of `M`, and any family of
`R`-linearly independent elements `{ n_j }` of `N`, the family `{ m_i * n_j }` in `S` is
also `R`-linearly independent.  -/
Submodule.LinearDisjoint.linearIndependent_mul_of_flat_left : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N →
    ∀ [Module.Flat R ↥M] {κ : Type u_1} {ι : Type u_2} {m : κ → ↥M} {n : ι → ↥N},
      LinearIndependent R m → LinearIndependent R n → LinearIndependent R fun i => ↑(m i.1) * ↑(n i.2)
-- Mathlib.Analysis.Complex.Basic
/-- The `normSq` function on `ℂ` is proper.  -/
Complex.tendsto_normSq_cocompact_atTop : Filter.Tendsto (⇑Complex.normSq) (Filter.cocompact ℂ) Filter.atTop
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_sub : ∀ {a b : ENNReal}, a ≠ ⊤ ∨ b ≠ ⊤ → Filter.Tendsto (fun p => p.1 - p.2) (nhds (a, b)) (nhds (a - b))
-- Init.Data.Vector.Lemmas
Vector.pop_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} {size : xs.size = n}, (Vector.mk xs size).pop = Vector.mk xs.pop ⋯
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
/-- If `f : E → F` has an invertible derivative `f'` at `a` in the sense of strict differentiability
and `g (f x) = x` in a neighborhood of `a`, then `g` has derivative `f'.symm` at `f a`.

For a version assuming `f (g y) = y` and continuity of `g` at `f a` but not `[CompleteSpace E]`
see `of_local_left_inverse`.  -/
HasStrictFDerivAt.to_local_left_inverse : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E ≃L[𝕜] F} {a : E} [CompleteSpace E],
  HasStrictFDerivAt f (↑f') a →
    ∀ {g : F → E}, (∀ᶠ (x : E) in nhds a, g (f x) = x) → HasStrictFDerivAt g (↑f'.symm) (f a)
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.closure_pi : ∀ {η : Type u_3} {f : η → Type u_4} [inst : (i : η) → AddGroup (f i)] [Finite η] {s : (i : η) → Set (f i)},
  (∀ (i : η), 0 ∈ s i) →
    AddSubgroup.closure (Set.univ.pi fun i => s i) = AddSubgroup.pi Set.univ fun i => AddSubgroup.closure (s i)
-- Mathlib.Data.Multiset.AddSub
/-- `erase s a` is the multiset that subtracts 1 from the multiplicity of `a`.  -/
Multiset.erase : {α : Type u_1} → [DecidableEq α] → Multiset α → α → Multiset α
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List ((a : α) × β a)} {k fallback : α},
      (List.map Sigma.fst l).contains k = false → (m.insertMany l).getKeyD k fallback = m.getKeyD k fallback
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_sub_eq_of_lt_left : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  {x y : R}, v x < v y → v (x - y) = v x
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
/-- The finset of those partitions in which every part satisfies a certain condition.  -/
Nat.Partition.restricted : (n : ℕ) → (p : ℕ → Prop) → [DecidablePred p] → Finset n.Partition
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Text.parseRes : Std.Internal.Parsec.ByteArray.Parser (ℕ × Array ℕ)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.toList_filter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} {f : α → β → Bool},
  t.WF →
    Std.DTreeMap.Internal.Impl.Const.toList (Std.DTreeMap.Internal.Impl.filter! f t) =
      List.filter (fun p => f p.1 p.2) (Std.DTreeMap.Internal.Impl.Const.toList t)
-- Lean.Server.Requests
Lean.Server.RequestTask.pure : {α : Type u_1} → α → Lean.Server.RequestTask α
-- Mathlib.Analysis.Convolution
HasCompactSupport.convolutionExistsAt : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : MeasurableSpace G] {μ : MeasureTheory.Measure G} [inst_8 : AddGroup G]
  [inst_9 : TopologicalSpace G] [IsTopologicalAddGroup G] [BorelSpace G] {x₀ : G},
  (HasCompactSupport fun t => (L (f t)) (g (x₀ - t))) →
    MeasureTheory.LocallyIntegrable f μ → Continuous g → MeasureTheory.ConvolutionExistsAt f g x₀ L μ
-- Mathlib.Analysis.RCLike.Basic
/-- The real part of a K Cauchy sequence, as a real Cauchy sequence.  -/
RCLike.cauSeqRe : {K : Type u_1} → [inst : RCLike K] → CauSeq K norm → CauSeq ℝ abs
-- Mathlib.Topology.Compactness.Compact
Filter.cocompact_eq_bot : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactSpace X], Filter.cocompact X = ⊥
-- Mathlib.Data.Rat.Defs
Rat.num_one : Rat.num 1 = 1
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.le_pointwise_smul_iff₀ : ∀ {M : Type u_1} {R : Type u_2} [inst : GroupWithZero M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M},
  a ≠ 0 → ∀ {S T : Subsemiring R}, S ≤ a • T ↔ a⁻¹ • S ≤ T
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.ker.eq_1 : ∀ {G : Type u_1} [inst : Group G] {M : Type u_7} [inst_1 : MulOneClass M] (f : G →* M),
  f.ker = { toSubmonoid := MonoidHom.mker f, inv_mem' := ⋯ }
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  {F₁ F₂ F₃ : CategoryTheory.Functor Cᵒᵖ A} {f₁ : F₁ ⟶ F₂} {f₂ : F₂ ⟶ F₃} (f₃ : F₁ ⟶ F₃),
  CategoryTheory.CategoryStruct.comp f₁ f₂ = f₃ →
    ∀ [CategoryTheory.Presheaf.IsLocallySurjective J f₃] [CategoryTheory.Presheaf.IsLocallyInjective J f₂],
      CategoryTheory.Presheaf.IsLocallySurjective J f₁
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.Y : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Year.Offset
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndep.precomp : ∀ {Ω : Type u_1} {ι : Type u_2} {m : ι → MeasurableSpace Ω} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {ι' : Type u_6} {g : ι' → ι}, Function.Injective g → ProbabilityTheory.iIndep m μ → ProbabilityTheory.iIndep (m ∘ g) μ
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.instT3Space : T3Space UpperHalfPlane
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpolyAux_coeff_eval : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [inst : CommRing R]
  [inst_1 : AddCommGroup L] [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  (φ : L →ₗ[R] Module.End R M) [inst_5 : Fintype ι] [inst_6 : Fintype ιM] [inst_7 : DecidableEq ι]
  [inst_8 : DecidableEq ιM] (b : Module.Basis ι R L) (bₘ : Module.Basis ιM R M) [inst_9 : Module.Finite R M]
  [inst_10 : Module.Free R M] (x : L) (i : ℕ),
  (MvPolynomial.eval ⇑(b.repr x)) ((φ.polyCharpolyAux b bₘ).coeff i) = (LinearMap.charpoly (φ x)).coeff i
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.ofFunctor.sizeOf_spec : ∀ {C D : CategoryTheory.Cat} (toFunctor : CategoryTheory.Functor ↑C ↑D),
  sizeOf { toFunctor := toFunctor } = 1 + sizeOf toFunctor
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.is_local : ∀ {H : Type u_1} {H' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace H'] {G : StructureGroupoid H}
  {G' : StructureGroupoid H'} {P : (H → H') → Set H → H → Prop},
  G.LocalInvariantProp G' P →
    ∀ {s : Set H} {x : H} {u : Set H} {f : H → H'}, IsOpen u → x ∈ u → (P f s x ↔ P f (s ∩ u) x)
-- Mathlib.Topology.Compactness.SigmaCompact
SigmaCompactSpace.mk : ∀ {X : Type u_4} [inst : TopologicalSpace X], IsSigmaCompact Set.univ → SigmaCompactSpace X
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
/-- Multiplicity of the ideal norm, for powers of prime ideals.  -/
cardQuot_pow_of_prime : ∀ {S : Type u_1} [inst : CommRing S] {P : Ideal S} [P_prime : P.IsPrime] [IsDedekindDomain S],
  P ≠ ⊥ → ∀ {i : ℕ}, Submodule.cardQuot (P ^ i) = Submodule.cardQuot P ^ i
-- Mathlib.NumberTheory.FactorisationProperties
Nat.Deficient.eq_1 : ∀ (n : ℕ), n.Deficient = (∑ i ∈ n.properDivisors, i < n)
-- Init.Data.List.Basic
List.intersperse_singleton : ∀ {α : Type u} {x sep : α}, List.intersperse sep [x] = [x]
-- Init.Data.UInt.Lemmas
UInt16.toUSize_ofNatLT : ∀ {n : ℕ} (h : n < UInt16.size), (UInt16.ofNatLT n h).toUSize = USize.ofNatLT n ⋯
-- Mathlib.Order.Filter.Finite
/-- **Alias** of `Filter.frequently_exists_finite`. -/
Set.Finite.frequently_exists : ∀ {α : Type u} {ι : Type u_2} {I : Set ι},
  I.Finite → ∀ {l : Filter α} {p : ι → α → Prop}, (∃ᶠ (x : α) in l, ∃ i ∈ I, p i x) ↔ ∃ i ∈ I, ∃ᶠ (x : α) in l, p i x
-- Mathlib.Analysis.Complex.CauchyIntegral
DifferentiableOn.analyticOn : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {s : Set ℂ} {f : ℂ → E},
  DifferentiableOn ℂ f s → IsOpen s → AnalyticOn ℂ f s
-- Lean.Elab.Command
Lean.Elab.Command.ModuleLinter.mk.injEq : ∀ (run : Array Lean.Syntax → Lean.Elab.Command.CommandElabM Unit)
  (name : autoParam Lean.Name Lean.Elab.Command.ModuleLinter.name._autoParam)
  (run_1 : Array Lean.Syntax → Lean.Elab.Command.CommandElabM Unit)
  (name_1 : autoParam Lean.Name Lean.Elab.Command.ModuleLinter.name._autoParam),
  ({ run := run, name := name } = { run := run_1, name := name_1 }) = (run = run_1 ∧ name = name_1)
-- ProofWidgets.Presentation.Expr
ProofWidgets.GetExprPresentationsParams.mk.injEq : ∀ (expr expr_1 : Lean.Server.WithRpcRef ProofWidgets.ExprWithCtx),
  ({ expr := expr } = { expr := expr_1 }) = (expr = expr_1)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_lt_div_iff_right : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulRightStrictMono α] {a b : α} (c : α), a / c < b / c ↔ a < b
-- Mathlib.Analysis.Calculus.FDeriv.Congr
Filter.EventuallyEq.fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {x : E}, f₁ =ᶠ[nhds x] f → fderiv 𝕜 f₁ =ᶠ[nhds x] fderiv 𝕜 f
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- Given a sheaf of `R`-modules `M` and a `Presentation M`, we may construct the quasi-coherent
data on the trivial cover.  -/
SheafOfModules.Presentation.quasicoherentData : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.Limits.HasBinaryProducts C] →
      {J : CategoryTheory.GrothendieckTopology C} →
        {R : CategoryTheory.Sheaf J RingCat} →
          [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat] →
            [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat] →
              [inst_4 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] →
                [inst_5 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
                  {M : SheafOfModules R} → M.Presentation → M.QuasicoherentData
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTGE_obj_obj₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (j : C), ((t.triangleLTGE n).obj j).obj₃ = (t.truncGE n).obj j
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticOn.const_smul` -/
AnalyticOn.fun_const_smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E}
  {R : Type u_9} [inst_5 : NormedRing R] [inst_6 : Module R F] [IsBoundedSMul R F] [SMulCommClass 𝕜 R F] {c : R},
  AnalyticOn 𝕜 f s → AnalyticOn 𝕜 (fun i => c • f i) s
-- Lean.Elab.ConfigEval.Types
/-- A type that can be used when constructing expression for the `TermInfo`.
 -/
Lean.Elab.ConfigEval.EvalTerm.typeExpr : (α : Type) → [self : Lean.Elab.ConfigEval.EvalTerm α] → Lean.Expr
-- Mathlib.Tactic.NormNum.Irrational
Mathlib.Meta.NormNum.irrational_sqrt_nat : ∀ {x : ℝ} {n k : ℕ}, Mathlib.Meta.NormNum.IsNat x n → k ^ 2 < n → n < (k + 1) ^ 2 → Irrational √x
-- Mathlib.RingTheory.Jacobson.Ring
_private.Mathlib.RingTheory.Jacobson.Ring.0.MvPolynomial.aux_IH : ∀ {R : Type u} {S : Type v} {T : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [IsJacobsonRing S] [inst_4 : Algebra R S] [inst_5 : Algebra R T],
  (∀ (Q : Ideal S), Q.IsMaximal → (algebraMap R (S ⧸ Q)).IsIntegral) →
    ∀ (v : Polynomial S ≃ₐ[R] T) (P : Ideal T), P.IsMaximal → (algebraMap R (T ⧸ P)).IsIntegral
-- Lean.Meta.Transform
Lean.TransformStep.done.injEq : ∀ (e e_1 : Lean.Expr), (Lean.TransformStep.done e = Lean.TransformStep.done e_1) = (e = e_1)
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiable.finsum_section_of_locallyFinite : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {ι : Type u_9}
  {t : ι → (x : B) → E x},
  (LocallyFinite fun i => {x | t i x ≠ 0}) → (∀ (i : ι), MDiff (T% t)) → MDiff fun x => ⟨x, ∑ᶠ (i : ι), t i x⟩
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIcc_val : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} (h : a ≤ b) (x : ↑(Set.Icc a b)), Set.projIcc a b h ↑x = x
-- Mathlib.Topology.Category.LightProfinite.Basic
LightProfinite.forget_reflectsIsomorphisms : (CategoryTheory.forget LightProfinite).ReflectsIsomorphisms
-- Lean.HeadIndex
Lean.HeadIndex.const.injEq : ∀ (constName constName_1 : Lean.Name),
  (Lean.HeadIndex.const constName = Lean.HeadIndex.const constName_1) = (constName = constName_1)
-- Mathlib.Algebra.Module.Submodule.LinearMap
/-- If two submodules `p` and `p'` satisfy `p ⊆ p'`, then `inclusion p p'` is the linear map version
of this inclusion.  -/
Submodule.inclusion : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → {p p' : Submodule R M} → p ≤ p' → ↥p →ₗ[R] ↥p'
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.id.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C),
  X.id = { base := CategoryTheory.CategoryStruct.id ↑X, c := CategoryTheory.CategoryStruct.id X.presheaf }
-- Mathlib.Algebra.Category.ModuleCat.Limits
/-- Construction of a limit cone in `ModuleCat R`.
(Internal use only; use the limits API.)
 -/
ModuleCat.HasLimits.limitCone : {R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (ModuleCat R)) →
          [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections] → CategoryTheory.Limits.Cone F
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.SavedState.tactic : Lean.Elab.Tactic.Grind.SavedState → Lean.Elab.Tactic.Grind.State
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The isomorphism expressing the commutation between taking
the homotopy cofiber of a morphism of homological complexes and
applying an additive functor.  -/
HomologicalComplex.homotopyCofiber.mapHomologicalComplexObjIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {F G : HomologicalComplex C c} →
            (φ : F ⟶ G) →
              [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
                [inst_3 : DecidableRel c.Rel] →
                  {D : Type u_3} →
                    [inst_4 : CategoryTheory.Category.{v_2, u_3} D] →
                      [inst_5 : CategoryTheory.Preadditive D] →
                        (H : CategoryTheory.Functor C D) →
                          [inst_6 : H.Additive] →
                            [inst_7 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)] →
                              (H.mapHomologicalComplex c).obj (HomologicalComplex.homotopyCofiber φ) ≅
                                HomologicalComplex.homotopyCofiber ((H.mapHomologicalComplex c).map φ)
-- Mathlib.Algebra.Group.Equiv.Opposite
AddMonoidHom.fromOpposite.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N)
  (hf : ∀ (x y : M), AddCommute (f x) (f y)),
  f.fromOpposite hf = { toFun := ⇑f ∘ AddOpposite.unop, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.quotientBot.eq_1 : ∀ {G : Type u} [inst : Group G],
  QuotientGroup.quotientBot = QuotientGroup.quotientKerEquivOfRightInverse (MonoidHom.id G) id ⋯
-- Mathlib.Data.Multiset.AddSub
Multiset.coe_add : ∀ {α : Type u_1} (s t : List α), ↑s + ↑t = ↑(s ++ t)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.map_negDblY : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Jacobian R} (f : R →+* S)
  (P : Fin 3 → R), (W'.map f).negDblY (⇑f ∘ P) = f (W'.negDblY P)
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
isCompactOperator_id : ∀ {E : Type u_1} [inst : AddGroup E] [inst_1 : TopologicalSpace E] [IsTopologicalAddGroup E] [LocallyCompactSpace E],
  IsCompactOperator id
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the largest key that is less than the given key,
returning `none` if no such key exists.
 -/
Std.TreeMap.Raw.getKeyLT? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → Option α
-- Mathlib.Data.Finsupp.Basic
Finsupp.image_fst_graph : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] [inst_1 : DecidableEq α] (f : α →₀ M),
  Finset.image Prod.fst f.graph = f.support
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteMulSupport.comp : ∀ {α : Type u_1} {M : Type u_2} [inst : One M] {N : Type u_3} [inst_1 : One N] {g : M → N} {f : α → M},
  Function.HasFiniteMulSupport f → g 1 = 1 → Function.HasFiniteMulSupport (g ∘ f)
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.inftyValuation.C : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)] {k : F},
  k ≠ 0 → (RatFunc.inftyValuation F) (RatFunc.C k) = 1
-- Batteries.Lean.LawfulMonadLift
_private.Batteries.Lean.LawfulMonadLift.0.EIO.toBaseIO.match_1.eq_2 : ∀ {ε α : Type} (motive : EST.Out ε IO.RealWorld α → Sort u_1) (ex : ε) (s : Void IO.RealWorld)
  (h_1 : (a : α) → (s : Void IO.RealWorld) → motive (EST.Out.ok a s))
  (h_2 : (ex : ε) → (s : Void IO.RealWorld) → motive (EST.Out.error ex s)),
  (match EST.Out.error ex s with
    | EST.Out.ok a s => h_1 a s
    | EST.Out.error ex s => h_2 ex s) =
    h_2 ex s
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If three points are not collinear, the angle between them is positive.  -/
EuclideanGeometry.angle_pos_of_not_collinear : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P}, ¬Collinear ℝ {p₁, p₂, p₃} → 0 < EuclideanGeometry.angle p₁ p₂ p₃
-- Mathlib.Order.Ideal
Order.Ideal.isProper_of_ne_top : ∀ {P : Type u_1} [inst : LE P] [inst_1 : IsDirectedOrder P] [inst_2 : Nonempty P] {I : Order.Ideal P},
  I ≠ ⊤ → I.IsProper