mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.ComputeDegree
/-- `monicity` tries to solve a goal of the form `Monic f`.
It converts the goal into a goal of the form `natDegree f ≤ n` and one of the form `f.coeff n = 1`
and calls `compute_degree` on those two goals.

The variant `monicity!` starts like `monicity`, but calls `compute_degree!` on the two side-goals.
 -/
Mathlib.Tactic.ComputeDegree.monicityMacro : Lean.ParserDescr
-- Mathlib.Algebra.Order.Positive.Ring
Positive.addLeftStrictMono : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : Preorder M] [inst_2 : AddLeftStrictMono M],
  AddLeftStrictMono { x // 0 < x }
-- Mathlib.Analysis.Convex.Strong
_private.Mathlib.Analysis.Convex.Strong.0.aux_sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {a b m : ℝ} {x y : E} {f : E → ℝ},
  0 ≤ a →
    0 ≤ b →
      a + b = 1 →
        a * (f x - m / 2 * ‖x‖ ^ 2) + b * (f y - m / 2 * ‖y‖ ^ 2) + m / 2 * ‖a • x + b • y‖ ^ 2 =
          a * f x + b * f y - m / 2 * a * b * ‖x - y‖ ^ 2
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
/-- Returns `true` if the variables in the given polynomial are sorted
in decreasing order.
 -/
Int.Internal.Linear.Poly.isSorted : Int.Internal.Linear.Poly → Bool
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.ofEssentiallySmall : ∀ {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 u_2}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  [inst_4 : CategoryTheory.EssentiallySmall.{w, v₁, u₁} C]
  [∀ (X : Cᵒᵖ),
      CategoryTheory.Limits.HasLimitsOfShape
        (CategoryTheory.StructuredArrow X (CategoryTheory.equivSmallModel C).inverse.op) A]
  [((CategoryTheory.equivSmallModel C).inverse.inducedTopology J).WEqualsLocallyBijective A],
  J.WEqualsLocallyBijective A
-- Mathlib.Data.Multiset.Sym
Multiset.setOfPred_mem_sym2 : ∀ {α : Type u_1} {m : Multiset α}, {z | z ∈ m.sym2} = {x | x ∈ m}.sym2
-- Mathlib.Probability.Independence.CharacteristicFunction
/-- **Alias** of `ProbabilityTheory.iIndepFun.charFun_map_finsetSum_eq_prod`. -/
ProbabilityTheory.iIndepFun.charFun_map_finset_sum_eq_prod : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} {s : Finset ι} {E : Type u_3}
  [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {X : ι → Ω → E}
  [inst_4 : InnerProductSpace ℝ E],
  (∀ i ∈ s, AEMeasurable (X i) P) →
    ProbabilityTheory.iIndepFun (s.restrict X) P →
      MeasureTheory.charFun (MeasureTheory.Measure.map (∑ i ∈ s, X i) P) =
        ∏ i ∈ s, MeasureTheory.charFun (MeasureTheory.Measure.map (X i) P)
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.j_mul_k : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (q : QuaternionAlgebra.Basis A c₁ c₂ c₃), q.j * q.k = (c₂ * c₃) • 1 - c₃ • q.i
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.contDiffAt_finsum : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {F : Type uF}
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {s : Set E}
  (f : SmoothPartitionOfUnity ι (modelWithCornersSelf ℝ E) E s) {x₀ : E} {g : ι → E → F},
  (∀ (i : ι), x₀ ∈ tsupport ⇑(f i) → ContDiffAt ℝ (↑n) (g i) x₀) →
    ContDiffAt ℝ (↑n) (fun x => ∑ᶠ (i : ι), (f i) x • g i x) x₀
-- Mathlib.Data.Fintype.Pi
Fintype.coe_piFinset : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {δ : α → Type u_4} (t : (a : α) → Finset (δ a)),
  ↑(Fintype.piFinset t) = Set.univ.pi fun a => ↑(t a)
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.ne_top_iff_exists_maximal : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α}, I ≠ ⊤ ↔ ∃ M, M.IsMaximal ∧ I ≤ M
-- Mathlib.Data.Int.ModEq
Int.ModEq.sub : ∀ {n a b c d : ℤ}, a ≡ b [ZMOD n] → c ≡ d [ZMOD n] → a - c ≡ b - d [ZMOD n]
-- Mathlib.Algebra.Field.Subfield.Basic
/-- Sum of a multiset of elements in a `Subfield` is in the `Subfield`.  -/
Subfield.multiset_sum_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) (m : Multiset K), (∀ a ∈ m, a ∈ s) → m.sum ∈ s
-- Mathlib.Order.Filter.Map
Filter.map_comm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {φ : α → β} {θ : α → γ} {ψ : β → δ} {ρ : γ → δ},
  ψ ∘ φ = ρ ∘ θ → ∀ (F : Filter α), Filter.map ψ (Filter.map φ F) = Filter.map ρ (Filter.map θ F)
-- Std.Do.PostCond
Std.Do.ExceptConds.snd_const : ∀ {ε : Type u} {ps : Std.Do.PostShape} (p : Prop), (Std.Do.ExceptConds.const p).2 = Std.Do.ExceptConds.const p
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.modifyStruct : (Lean.Meta.Grind.AC.Struct → Lean.Meta.Grind.AC.Struct) → Lean.Meta.Grind.AC.ACM Unit
-- Mathlib.SetTheory.Ordinal.Basic
/-- `typeLT α` is an abbreviation for the order type of the `<` relation of `α`.  -/
Ordinal.termTypeLT_ : Lean.ParserDescr
-- Init.Data.Int.Linear
/-- Converts the given expression into a polynomial.  -/
Int.Internal.Linear.Expr.toPoly' : Int.Internal.Linear.Expr → Int.Internal.Linear.Poly
-- Mathlib.Data.Set.Function
Set.image_eq_iff_surjOn_mapsTo : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, f '' s = t ↔ Set.SurjOn f s t ∧ Set.MapsTo f s t
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
AlgebraicGeometry.HasAffineProperty.coprodDesc_affineAnd : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme},
  AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
      (∀ {R S T : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T] (f : R →+* S) (g : R →+* T),
          Q f → Q g → Q (f.prod g)) →
        ∀ {U V X : AlgebraicGeometry.Scheme} (f : U ⟶ X) (g : V ⟶ X),
          P f → P g → P (CategoryTheory.Limits.coprod.desc f g)
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
/-- Any structure `IsColimitCore.{max w₂ w₃} c` can be
lowered to `IsColimitCore.{w₂} c`  -/
CategoryTheory.Functor.CoconeTypes.IsColimitCore.down : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {F : CategoryTheory.Functor J (Type w₀)} → {c : F.CoconeTypes} → c.IsColimitCore → c.IsColimitCore
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_div_iff_mul_le : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulRightMono α] {a b c : α}, a ≤ c / b ↔ a * b ≤ c
-- Mathlib.RingTheory.Multiplicity
dvd_iff_emultiplicity_pos : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, 0 < emultiplicity a b ↔ a ∣ b
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.sum_take_succ : ∀ {M : Type u_4} [inst : AddMonoid M] (L : List M) (i : ℕ) (p : i < L.length),
  (List.take (i + 1) L).sum = (List.take i L).sum + L[i]
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
/-- The "grid-lines lemma" (not a standard name), stated with a general parameter `p` as the
exponent.  Compare with `lintegral_prod_lintegral_pow_le`.

For any finite dependent product `Π i : ι, A i` of sigma-finite measure spaces, for any
nonnegative real number `p` such that `(#ι - 1) * p ≤ 1`, for any function `f` from `Π i, A i` into
the extended nonnegative reals, we consider an associated "grid-lines quantity", the integral of an
associated function from `Π i, A i` into the extended nonnegative reals.  The value of this function
at `x : Π i, A i` is obtained by multiplying a certain power of `f` with the product, for each
co-ordinate `i`, of a certain power of the integral of `f` along the "grid line" in the `i`
direction through `x`.

This lemma bounds the Lebesgue integral of the grid-lines quantity by a power of the Lebesgue
integral of `f`.  -/
MeasureTheory.lintegral_mul_prod_lintegral_pow_le : ∀ {ι : Type u_1} {A : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → MeasureTheory.Measure (A i))
  [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {p : ℝ},
  0 ≤ p →
    (↑(Fintype.card ι) - 1) * p ≤ 1 →
      ∀ {f : ((i : ι) → A i) → ENNReal},
        Measurable f →
          ∫⁻ (x : (i : ι) → A i),
              f x ^ (1 - (↑(Fintype.card ι) - 1) * p) *
                ∏ i, (∫⁻ (xᵢ : A i), f (Function.update x i xᵢ) ∂μ i) ^ p ∂MeasureTheory.Measure.pi μ ≤
            (∫⁻ (x : (i : ι) → A i), f x ∂MeasureTheory.Measure.pi μ) ^ (1 + p)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.FormatType.match_1.eq_2 : ∀ (motive : Std.Time.FormatString → Sort u_1) (val : String) (xs : List Std.Time.FormatPart)
  (h_1 :
    (entry : Std.Time.Modifier) → (xs : List Std.Time.FormatPart) → motive (Std.Time.FormatPart.modifier entry :: xs))
  (h_2 : (val : String) → (xs : List Std.Time.FormatPart) → motive (Std.Time.FormatPart.string val :: xs))
  (h_3 : Unit → motive []),
  (match Std.Time.FormatPart.string val :: xs with
    | Std.Time.FormatPart.modifier entry :: xs => h_1 entry xs
    | Std.Time.FormatPart.string val :: xs => h_2 val xs
    | [] => h_3 ()) =
    h_2 val xs
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.extendScalarsId_hom_app_one_tmul : ∀ {R : Type u₁} [inst : CommRing R] (M : ModuleCat R) (m : ↑M),
  (CategoryTheory.ConcreteCategory.hom ((ModuleCat.extendScalarsId R).hom.app M)) (1 ⊗ₜ[R] m) = m
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkSpecializes_refl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) (x : ↑X), F.stalkSpecializes ⋯ = CategoryTheory.CategoryStruct.id (F.stalk x)
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.instInhabitedElimAltInfo.default : Lean.Meta.ElimAltInfo
-- Mathlib.Order.Category.Preord
Preord.instInhabited : Inhabited Preord
-- Mathlib.Topology.MetricSpace.Completion
/-- Reformulate `Completion.mem_uniformity_dist` in terms that are suitable for the definition
of the metric space structure.  -/
UniformSpace.Completion.uniformity_dist' : ∀ {α : Type u} [inst : PseudoMetricSpace α],
  uniformity (UniformSpace.Completion α) = ⨅ ε, Filter.principal {p | dist p.1 p.2 < ↑ε}
-- Mathlib.RingTheory.Etale.Finite
CommAlgCat.instCoeSortFiniteEtaleType : (R : Type u) → [inst : CommRing R] → CoeSort (CommAlgCat.FiniteEtale R) (Type v)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.toList_nil : ∀ {α : Type u}, Stream'.Seq.nil.toList ⋯ = []
-- Mathlib.Analysis.Complex.BorelCaratheodory
/-- **Borel-Carathéodory theorem**.

If `f` is analytic on the open ball `‖z‖ < R` and satisfies `(f z).re ≤ M` for all such `z`,
then `‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖)` for all `‖z‖ < R`.  -/
Complex.borelCaratheodory : ∀ {f : ℂ → ℂ} {M R : ℝ} {z : ℂ},
  0 < M →
    DifferentiableOn ℂ f (Metric.ball 0 R) →
      Set.MapsTo f (Metric.ball 0 R) {z | z.re ≤ M} →
        0 < R → z ∈ Metric.ball 0 R → ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖) + ‖f 0‖ * (R + ‖z‖) / (R - ‖z‖)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LongExactSequence
groupHomology.mono_δ_of_isZero : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) (n : ℕ),
  CategoryTheory.Limits.IsZero (groupHomology X.X₂ (n + 1)) → CategoryTheory.Mono (groupHomology.δ hX (n + 1) n ⋯)
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_isoBot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {X Y : C} {f : X ⟶ Y} [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  (c : CategoryTheory.TransfiniteCompositionOfShape J f) {J' : Type w'} [inst_5 : LinearOrder J'] [inst_6 : OrderBot J']
  [inst_7 : SuccOrder J'] [inst_8 : WellFoundedLT J'] (e : J' ≃o J),
  (c.ofOrderIso e).isoBot = c.F.mapIso (CategoryTheory.eqToIso ⋯) ≪≫ c.isoBot
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.beq_iff_equiv : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {m₁ m₂ : Std.DTreeMap.Raw α β cmp} [inst : (k : α) → BEq (β k)]
  [inst_1 : Std.LawfulEqCmp cmp] [Std.TransCmp cmp] [∀ (k : α), LawfulBEq (β k)],
  m₁.WF → m₂.WF → (m₁.beq m₂ = true ↔ m₁.Equiv m₂)
-- Mathlib.Data.List.Induction
_private.Mathlib.Data.List.Induction.0.List.bidirectionalRec.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a b : α) (l : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → motive [a]) (h_3 : (a b : α) → (l : List α) → motive (a :: b :: l)),
  (match a :: b :: l with
    | [] => h_1 ()
    | [a] => h_2 a
    | a :: b :: l => h_3 a b l) =
    h_3 a b l
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedInjectiveInfo : Inhabited Lean.Meta.Grind.InjectiveInfo
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- A category of costructured arrows for a functor `toOver F X` identifies
to a category of costructured arrows for `F`.  -/
CategoryTheory.CostructuredArrow.costructuredArrowToOverEquivalence : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor D T) →
          {X : T} →
            (Y : CategoryTheory.Over X) →
              CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.toOver F X) Y ≌
                CategoryTheory.CostructuredArrow F Y.left
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coroot_root_two : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι),
  (P.flip (P.coroot i)) (P.root i) = 2
-- Std.Do.Triple.SpecLemmas
List.Cursor.ext_iff : ∀ {α : Type u} {l : List α} {x y : l.Cursor}, x = y ↔ x.prefix = y.prefix ∧ x.suffix = y.suffix
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
finsuppTensorFinsuppRid_self : ∀ (R : Type u_1) (ι : Type u_5) (κ : Type u_6) [inst : CommSemiring R],
  finsuppTensorFinsuppRid R R ι κ = finsuppTensorFinsupp' R ι κ
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_inter_nonempty_iff : ∀ {α : Type u_2} [inst : Group α] {s t : Set α} {x : α}, (x • s ∩ t).Nonempty ↔ ∃ a b, (a ∈ t ∧ b ∈ s) ∧ a * b⁻¹ = x
-- Std.Http.Server
/-- Indicates when the server has successfully shut down.
 -/
Std.Http.Server.shutdownPromise : Std.Http.Server → Std.Channel Unit
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.coe_mk : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (e : A ≃ₗc[R] B) (h : ∀ (x y : A), e.toFun (x * y) = e.toFun x * e.toFun y), ↑{ toCoalgEquiv := e, map_mul' := h } = e
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.instGetElem?Mem : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → [inst : Std.TransCmp cmp] → GetElem? (Std.ExtTreeMap α β cmp) α β fun m a => a ∈ m
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- Every point is either an interior or a boundary point.  -/
ModelWithCorners.isInteriorPoint_or_isBoundaryPoint : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (x : M), I.IsInteriorPoint x ∨ I.IsBoundaryPoint x
-- Mathlib.RingTheory.Coalgebra.Equiv
/-- An equivalence of coalgebras is an invertible coalgebra homomorphism.  -/
CoalgEquiv : (R : Type u_5) →
  [inst : CommSemiring R] →
    (A : Type u_6) →
      (B : Type u_7) →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : AddCommMonoid B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] → [CoalgebraStruct R A] → [CoalgebraStruct R B] → Type (max u_6 u_7)
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.toCompacts_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  (K : TopologicalSpace.NonemptyCompacts α) (L : TopologicalSpace.NonemptyCompacts β),
  (K ×ˢ L).toCompacts = K.toCompacts ×ˢ L.toCompacts
-- Mathlib.Data.Complex.Basic
Complex.ofReal_eq_zero : ∀ {z : ℝ}, ↑z = 0 ↔ z = 0
-- Init.Data.List.Sublist
List.reverse_infix : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.reverse <:+: l₂.reverse ↔ l₁ <:+: l₂
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- Transport an exact pairing across isomorphisms.  -/
CategoryTheory.exactPairingCongr : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X X' Y Y' : C} → [CategoryTheory.ExactPairing X' Y'] → (X ≅ X') → (Y ≅ Y') → CategoryTheory.ExactPairing X Y
-- Mathlib.Data.FunLike.Fintype
FunLike.toDecidableEq : {F : Type u_1} → {α : Type u_2} → {β : Type u_3} → [DecidableEq β] → [Fintype α] → [FunLike F α β] → DecidableEq F
-- Mathlib.NumberTheory.JacobiSum.Basic
_private.Mathlib.NumberTheory.JacobiSum.Basic.0.MulChar.exists_apply_sub_one_mul_apply_sub_one : ∀ {F : Type u_1} {R : Type u_2} [inst : Field F] [inst_1 : CommRing R] [IsDomain R] [Finite F] {n : ℕ} [NeZero n]
  {χ ψ : MulChar F R} {μ : R},
  χ ^ n = 1 → ψ ^ n = 1 → IsPrimitiveRoot μ n → ∀ (x : F), ∃ z ∈ ℤ[μ], (χ x - 1) * (ψ (1 - x) - 1) = z * (μ - 1) ^ 2
-- Mathlib.Algebra.GroupWithZero.Action.Defs
DistribSMul.ext_iff : ∀ {M : Type u_12} {A : Type u_13} {inst : AddZeroClass A} {x y : DistribSMul M A}, x = y ↔ SMul.smul = SMul.smul
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.coe_mapAlgHom : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (f : S →ₐ[R] T) (p : Polynomial S) (q : Polynomial T)
  (h : q ∣ Polynomial.map (↑f) p), ⇑(AdjoinRoot.mapAlgHom f p q h) = ⇑(AdjoinRoot.map (↑f) p q h)
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the reverse direction of `lowerHemicontinuousOn_iff_frequently`. -/
LowerHemicontinuousOn.of_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {s : Set α},
  (∀ x ∈ s, ∀ (t : Set β), IsClosed t → (∃ᶠ (x' : α) in nhdsWithin x s, f x' ⊆ t) → f x ⊆ t) → LowerHemicontinuousOn f s
-- Mathlib.Data.ENat.Basic
ENat.natCast_le_of_coe_top_le_withTop : ∀ {N : WithTop ℕ∞}, ↑⊤ ≤ N → ∀ (n : ℕ), ↑n ≤ N
-- Mathlib.Analysis.InnerProductSpace.PiL2
Pi.orthonormalBasis.eq_1 : ∀ {η : Type u_7} [inst : Fintype η] {ι : η → Type u_8} [inst_1 : (i : η) → Fintype (ι i)] {𝕜 : Type u_9}
  [inst_2 : RCLike 𝕜] {E : η → Type u_10} [inst_3 : (i : η) → NormedAddCommGroup (E i)]
  [inst_4 : (i : η) → InnerProductSpace 𝕜 (E i)] (B : (i : η) → OrthonormalBasis (ι i) 𝕜 (E i)),
  Pi.orthonormalBasis B =
    {
      repr :=
        (LinearIsometryEquiv.piLpCongrRight 2 fun i => (B i).repr).trans
          (LinearIsometryEquiv.piLpCurry 𝕜 2 fun x x_1 => 𝕜).symm }
-- Mathlib.Data.List.Cycle
Cycle.Chain.nil : ∀ {α : Type u_1} (r : α → α → Prop), Cycle.Chain r Cycle.nil
-- Init.Data.String.Lemmas.Basic
String.Slice.Pos.startPos_le : ∀ {s : String.Slice} (p : s.Pos), s.startPos ≤ p
-- Lean.Elab.PreDefinition.Structural.BRecOn
/-- Calculates the `.brecOn` functional argument corresponding to one structural recursive function.
The `value` is the function with (only) the fixed parameters moved into the context,
The `FType` is the expected type of the argument.
The `recArgInfos` is used to transform the body of the function to replace recursive calls with
uses of the `below` induction hypothesis.
 -/
Lean.Elab.Structural.mkBRecOnF : Array Lean.Elab.Structural.RecArgInfo →
  Lean.Elab.Structural.Positions → Lean.Elab.Structural.RecArgInfo → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteSAsRing.eq_8 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (a : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Expr.denoteSAsRing ctx a.neg = 0
-- Mathlib.LinearAlgebra.LinearPMap
/-- Define a `LinearPMap` from its graph.

In the case that the submodule is not a graph of a `LinearPMap` then the underlying linear map
is just the zero map.  -/
Submodule.toLinearPMap : {R : Type u_1} →
  [inst : Ring R] →
    {E : Type u_4} →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Module R E] →
          {F : Type u_5} → [inst_3 : AddCommGroup F] → [inst_4 : Module R F] → Submodule R (E × F) → E →ₗ.[R] F
-- Mathlib.Algebra.Module.ULift
ULift.mulAction'.eq_1 : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M],
  ULift.mulAction' = { toSMul := ULift.smul, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Data.Stream.Init
Stream'.corec_id_id_eq_const : ∀ {α : Type u} (a : α), Stream'.corec id id a = Stream'.const a
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f)
  (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)} (h : (F.map f₁₃).toFunctor.obj ((F.map f₀₁).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).hom.toNatTrans.app X) h) =
    CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp
        ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X)) h)
-- Mathlib.Algebra.Order.Hom.Basic
/-- Diamond inheritance cannot depend on `outParam`s in the following circumstances:
* there are three classes `Top`, `Middle`, `Bottom`
* all of these classes have a parameter `(α : outParam _)`
* all of these classes have an instance parameter `[Root α]` that depends on this `outParam`
* the `Root` class has two child classes: `Left` and `Right`, these are siblings in the hierarchy
* the instance `Bottom.toMiddle` takes a `[Left α]` parameter
* the instance `Middle.toTop` takes a `[Right α]` parameter
* there is a `Leaf` class that inherits from both `Left` and `Right`.

In that case, given instances `Bottom α` and `Leaf α`, Lean cannot synthesize a `Top α` instance,
even though the hypotheses of the instances `Bottom.toMiddle` and `Middle.toTop` are satisfied.

There are two workarounds:
* You could replace the bundled inheritance implemented by the instance `Middle.toTop` with
  unbundled inheritance implemented by adding a `[Top α]` parameter to the `Middle` class. This is
  the preferred option since it is also more compatible with Lean 4, at the cost of being more work
  to implement and more verbose to use.
* You could weaken the `Bottom.toMiddle` instance by making it depend on a subclass of
  `Middle.toTop`'s parameter, in this example replacing `[Left α]` with `[Leaf α]`.
 -/
LibraryNote.«out-param_inheritance» : Batteries.Util.LibraryNote
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.coe_fst : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {x : Z}, x ∈ e.source → (↑e x).1 = proj x