mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.MeanInequalities
Real.inner_le_Lp_mul_Lq_tsum_of_nonneg : ∀ {ι : Type u} {f g : ι → ℝ} {p q : ℝ},
  p.HolderConjugate q →
    (∀ (i : ι), 0 ≤ f i) →
      (∀ (i : ι), 0 ≤ g i) →
        (Summable fun i => f i ^ p) →
          (Summable fun i => g i ^ q) →
            ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
-- Mathlib.NumberTheory.Dioph
Poly.coe_sub : ∀ {α : Type u_1} (f g : Poly α), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_fun_sum : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {ι : Type u_1} {u : Finset ι} {A : ι → 𝕜 → F},
  (∀ i ∈ u, DifferentiableAt 𝕜 (A i) x) → deriv (fun y => ∑ i ∈ u, A i y) x = ∑ i ∈ u, deriv (A i) x
-- Mathlib.Algebra.Order.Floor.Extended
ENat.gc_ceil_toENNReal : GaloisConnection ENat.ceil ENat.toENNReal
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [CategoryTheory.EnoughInjectives C] [CategoryTheory.Mono f] (n₀ n₁ : ℤ),
  (∀ i ≤ n₀, QuasiIsoAt f i) →
    autoParam (n₀ + 1 = n₁) CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₁._auto_1✝ →
      ∃ F,
        CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.quasiIsoLE✝ n₀ F ∧
          CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.isIsoLE✝ n₀ F ∧
            CategoryTheory.Mono (HomologicalComplex.homologyMap F.obj.ι n₁)
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
HasStrictFDerivAt.localInverse.congr_simp : ∀ {𝕜 : 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 f_1 : E → F)
  (e_f : f = f_1) (f' f'_1 : E ≃L[𝕜] F) (e_f' : f' = f'_1) (a a_1 : E) (e_a : a = a_1) [inst_5 : CompleteSpace E]
  (hf : HasStrictFDerivAt f (↑f') a) (a_2 a_3 : F),
  a_2 = a_3 → HasStrictFDerivAt.localInverse f f' a hf a_2 = HasStrictFDerivAt.localInverse f_1 f'_1 a_1 ⋯ a_3
-- Init.Data.String.Lemmas.TakeDrop
String.toList_copy_takeEnd : ∀ {s : String} {n : ℕ}, (s.takeEnd n).copy.toList = List.drop (s.toList.length - n) s.toList
-- Mathlib.Data.Analysis.Filter
/-- A realizer for filter `f` is a cfilter which generates `f`.  -/
Filter.Realizer : {α : Type u_1} → Filter α → Type (max u_1 (u_5 + 1))
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
/-- The derivation `Derivation' φ'` is universal.  -/
PresheafOfModules.DifferentialsConstruction.isUniversal' : {D : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} D] →
    {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} →
      (φ' : S' ⟶ R) →
        PresheafOfModules.Derivation.Universal (PresheafOfModules.DifferentialsConstruction.derivation' φ')
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.inv_hom : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.IsIso f],
  CategoryTheory.MorphismProperty.Comma.Hom.hom (CategoryTheory.inv f) =
    CategoryTheory.inv (CategoryTheory.MorphismProperty.Comma.Hom.hom f)
-- Mathlib.RingTheory.LaurentSeries
/-- The Hasse derivative of Laurent series, as a linear map.  -/
LaurentSeries.hasseDeriv : (R : Type u_2) →
  {V : Type u_3} →
    [inst : AddCommGroup V] → [inst_1 : Semiring R] → [inst_2 : Module R V] → ℕ → LaurentSeries V →ₗ[R] LaurentSeries V
-- Mathlib.Analysis.Complex.Exponential
_private.Mathlib.Analysis.Complex.Exponential.0.Real.add_one_le_exp_of_nonneg : ∀ {x : ℝ}, 0 ≤ x → x + 1 ≤ Real.exp x
-- Mathlib.LinearAlgebra.Alternating.Basic
LinearMap.compAlternatingMap_zero : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {N₂ : Type u_11} [inst_5 : AddCommMonoid N₂]
  [inst_6 : Module R N₂] (g : N →ₗ[R] N₂), g.compAlternatingMap 0 = 0
-- Mathlib.MeasureTheory.Function.L2Space
/-- For bounded continuous functions `f`, `g` on a finite-measure topological space `α`, the L^2
inner product is the integral of their pointwise inner product.  -/
MeasureTheory.BoundedContinuousFunction.inner_toLp : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [inst_2 : BorelSpace α]
  [inst_3 : RCLike 𝕜] (μ : MeasureTheory.Measure α) [inst_4 : MeasureTheory.IsFiniteMeasure μ]
  (f g : BoundedContinuousFunction α 𝕜),
  inner 𝕜 ((BoundedContinuousFunction.toLp 2 μ 𝕜) f) ((BoundedContinuousFunction.toLp 2 μ 𝕜) g) =
    ∫ (x : α), g x * (starRingEnd 𝕜) (f x) ∂μ
-- Lean.Meta.Sym.Pattern
Lean.Meta.Sym.Pattern.mk.injEq : ∀ (levelParams : List Lean.Name) (varTypes : Array Lean.Expr) (varInfos? : Option Lean.Meta.Sym.ProofInstInfo)
  (pattern : Lean.Expr) (fnInfos : Lean.AssocList Lean.Name Lean.Meta.Sym.ProofInstInfo)
  (checkTypeMask? : Option (Array Bool)) (levelParams_1 : List Lean.Name) (varTypes_1 : Array Lean.Expr)
  (varInfos?_1 : Option Lean.Meta.Sym.ProofInstInfo) (pattern_1 : Lean.Expr)
  (fnInfos_1 : Lean.AssocList Lean.Name Lean.Meta.Sym.ProofInstInfo) (checkTypeMask?_1 : Option (Array Bool)),
  ({ levelParams := levelParams, varTypes := varTypes, varInfos? := varInfos?, pattern := pattern, fnInfos := fnInfos,
        checkTypeMask? := checkTypeMask? } =
      { levelParams := levelParams_1, varTypes := varTypes_1, varInfos? := varInfos?_1, pattern := pattern_1,
        fnInfos := fnInfos_1, checkTypeMask? := checkTypeMask?_1 }) =
    (levelParams = levelParams_1 ∧
      varTypes = varTypes_1 ∧
        varInfos? = varInfos?_1 ∧ pattern = pattern_1 ∧ fnInfos = fnInfos_1 ∧ checkTypeMask? = checkTypeMask?_1)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- The difference from `quasispectrumRestricts_iff_spectrumRestricts_inr` is that the
`Unitization` may be taken with respect to a different scalar field.  -/
quasispectrumRestricts_iff_spectrumRestricts_inr' : ∀ {R : Type u_3} {S' : Type u_4} {A : Type u_5} (S : Type u_6) [inst : Semifield R] [inst_1 : Semifield S']
  [inst_2 : Field S] [inst_3 : NonUnitalRing A] [inst_4 : Module R A] [inst_5 : Module S' A] [inst_6 : Module S A]
  [inst_7 : IsScalarTower S A A] [inst_8 : SMulCommClass S A A] [inst_9 : Algebra R S'] [inst_10 : Algebra S' S]
  [inst_11 : Algebra R S] [inst_12 : IsScalarTower S' S A] [inst_13 : IsScalarTower R S A] {a : A} {f : S' → R},
  QuasispectrumRestricts a f ↔ SpectrumRestricts (↑a) f
-- Init.Data.Int.DivMod.Basic
/-- Integer division that uses the E-rounding convention. Usually accessed via the `/` operator.
Division by zero is defined to be zero, rather than an error.

In the E-rounding convention (Euclidean division), `Int.emod x y` satisfies `0 ≤ Int.emod x y < Int.natAbs y`
for `y ≠ 0` and `Int.ediv` is the unique function satisfying `Int.emod x y + (Int.ediv x y) * y = x`
for `y ≠ 0`.

This means that `Int.ediv x y` is `⌊x / y⌋` when `y > 0` and `⌈x / y⌉` when `y < 0`.

This function is overridden by the compiler with an efficient implementation. This definition is
the logical model.

Examples:
* `(7 : Int) / (0 : Int) = 0`
* `(0 : Int) / (7 : Int) = 0`
* `(12 : Int) / (6 : Int) = 2`
* `(12 : Int) / (-6 : Int) = -2`
* `(-12 : Int) / (6 : Int) = -2`
* `(-12 : Int) / (-6 : Int) = 2`
* `(12 : Int) / (7 : Int) = 1`
* `(12 : Int) / (-7 : Int) = -1`
* `(-12 : Int) / (7 : Int) = -2`
* `(-12 : Int) / (-7 : Int) = 2`
 -/
Int.ediv : ℤ → ℤ → ℤ
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatWeekdayTwoLetter : Std.Time.DateFormatSymbols → Std.Time.Weekday → String
-- Mathlib.LinearAlgebra.Dimension.Finite
LinearIndependent.setFinite : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Finite R M] {b : Set M}, (LinearIndependent R fun (x : ↑b) => ↑x) → b.Finite
-- Mathlib.LinearAlgebra.Dual.Lemmas
Submodule.dualCoannihilator_top : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.Projective R M], ⊤.dualCoannihilator = ⊥
-- Mathlib.Order.Filter.IndicatorFunction
Filter.EventuallyEq.of_mulIndicator_const : ∀ {α : Type u_1} {β : Type u_2} [inst : One β] {l : Filter α} {c : β},
  c ≠ 1 → ∀ {s t : Set α}, ((s.mulIndicator fun x => c) =ᶠ[l] t.mulIndicator fun x => c) → s =ᶠ[l] t
-- Mathlib.Algebra.Module.StablyFree.Basic
Module.IsStablyFree.of_free_prod' : ∀ (R : Type u) [inst : Ring R] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Type w)
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.Finite R N] [Module.Free R N] [Module.Free R (N × M)],
  Module.IsStablyFree R M
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- `tprod_iSup_decode₂` specialized to the complete lattice of sets.  -/
tprod_iUnion_decode₂ : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} {β : Type u_4}
  [inst_2 : Encodable β] (m : Set α → M),
  m ∅ = 1 → ∀ (s : β → Set α), ∏' (i : ℕ), m (⋃ b ∈ Encodable.decode₂ β i, s b) = ∏' (b : β), m (s b)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.braiding_leftUnitor_aux₂ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
      (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Analysis.Distribution.DerivNotation
LineDeriv.laplacianCLM.eq_1 : ∀ (R : Type u_4) (E : Type u_6) (V₁ : Type u_8) {V₂ : Type u_9} {V₃ : Type u_10} [inst : LineDeriv E V₁ V₂]
  [inst_1 : LineDeriv E V₂ V₃] [inst_2 : AddCommGroup V₁] [inst_3 : AddCommGroup V₂] [inst_4 : AddCommGroup V₃]
  [inst_5 : NormedAddCommGroup E] [inst_6 : InnerProductSpace ℝ E] [inst_7 : FiniteDimensional ℝ E]
  [inst_8 : CommRing R] [inst_9 : Module R V₁] [inst_10 : Module R V₂] [inst_11 : Module R V₃]
  [inst_12 : TopologicalSpace V₁] [inst_13 : TopologicalSpace V₂] [inst_14 : TopologicalSpace V₃]
  [inst_15 : IsTopologicalAddGroup V₃] [inst_16 : LineDerivAdd E V₁ V₂] [inst_17 : LineDerivSMul R E V₁ V₂]
  [inst_18 : ContinuousLineDeriv E V₁ V₂] [inst_19 : LineDerivAdd E V₂ V₃] [inst_20 : LineDerivSMul R E V₂ V₃]
  [inst_21 : ContinuousLineDeriv E V₂ V₃],
  LineDeriv.laplacianCLM R E V₁ =
    ∑ i,
      LineDeriv.lineDerivOpCLM R V₂ ((stdOrthonormalBasis ℝ E) i) ∘SL
        LineDeriv.lineDerivOpCLM R V₁ ((stdOrthonormalBasis ℝ E) i)
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- The space of continuous linear maps between finite-dimensional spaces is finite-dimensional.  -/
ContinuousLinearMap.instModuleFinite : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommGroup F] [inst_3 : TopologicalSpace F] [inst_4 : IsTopologicalAddGroup F] [inst_5 : CommRing 𝕜]
  [inst_6 : Module 𝕜 E] [Module.Finite 𝕜 E] [inst_8 : Module 𝕜 F] [IsNoetherian 𝕜 F]
  [inst_10 : ContinuousConstSMul 𝕜 F], Module.Finite 𝕜 (E →L[𝕜] F)
-- Init.Tactics
/-- For every hypothesis `h : a ~ b` where a `@[symm]` lemma is available,
add a hypothesis `h_symm : b ~ a`.  -/
Lean.Parser.Tactic.symmSaturate : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Affine.Simplex
Affine.Simplex.regular_reindex_iff : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring R] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : Module R V] [inst_4 : NormedAddTorsor V P] {m n : ℕ}
  {s : Affine.Simplex R P m} (e : Fin (m + 1) ≃ Fin (n + 1)), (s.reindex e).Regular ↔ s.Regular
-- Mathlib.LinearAlgebra.Projectivization.Constructions
/-- Cross product on the projective plane.  -/
Projectivization.cross : {F : Type u_1} →
  [inst : Field F] →
    [DecidableEq F] → Projectivization F (Fin 3 → F) → Projectivization F (Fin 3 → F) → Projectivization F (Fin 3 → F)
-- Std.Do.WP.SimpLemmas
Std.Do.WP.controlAt_MonadControlT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {n : Type u → Type u_1} {α : Type u} {Q : Std.Do.PostCond α ps}
  [inst : Bind n] [inst_1 : Std.Do.WP n ps] [inst_2 : MonadControlT m n]
  (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)),
  (Std.Do.wp (controlAt m f)).apply Q = (Std.Do.wp (liftWith f >>= restoreM)).apply Q
-- Mathlib.Data.Set.Subsingleton
Set.Subsingleton.coe_sort : ∀ {α : Type u} {s : Set α}, s.Subsingleton → Subsingleton ↑s
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_assignments_confirmRupHint : ∀ {n : ℕ} (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (derivedLits : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (b1 b2 : Bool) (id : ℕ),
  (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint clauses (assignments, derivedLits, b1, b2)
          id).1.size =
    assignments.size
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- The composition of the vector measure with the linear pairing, giving the reference
vector measure.  -/
MeasureTheory.VectorMeasure.transpose : {X : Type u_2} →
  {E : Type u_4} →
    {F : Type u_5} →
      {G : Type u_6} →
        {mX : MeasurableSpace X} →
          [inst : NormedAddCommGroup E] →
            [inst_1 : NormedSpace ℝ E] →
              [inst_2 : NormedAddCommGroup F] →
                [inst_3 : NormedSpace ℝ F] →
                  [inst_4 : NormedAddCommGroup G] →
                    [inst_5 : NormedSpace ℝ G] →
                      MeasureTheory.VectorMeasure X F → (E →L[ℝ] F →L[ℝ] G) → MeasureTheory.VectorMeasure X (E →L[ℝ] G)
-- Mathlib.Topology.Algebra.Ring.Basic
NonUnitalSubsemiring.topologicalClosure_coe : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalSemiring R] [inst_2 : IsSemitopologicalSemiring R]
  (s : NonUnitalSubsemiring R), ↑s.topologicalClosure = closure ↑s
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.combine : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.Algebra.Field.Opposite
MulOpposite.instDivisionRing : {α : Type u_1} → [DivisionRing α] → DivisionRing αᵐᵒᵖ
-- Init.Data.Array.MinMax
Array.max_toList : ∀ {α : Type u_1} [inst : Max α] {xs : Array α} {h : xs.toList ≠ []}, xs.toList.max h = xs.max ⋯
-- Init.Data.List.Impl
List.eraseIdx.eq_2 : ∀ {α : Type u} (head : α) (as : List α), (head :: as).eraseIdx 0 = as
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `M` and `N` are linearly disjoint, if `N` is a flat `R`-module, then for any family of
`R`-linearly independent elements `{ m_i }` of `M`, they are also `N`-linearly independent,
in the sense that the `R`-linear map from `ι →₀ N` to `S` which maps `{ n_i }`
to the sum of `m_i * n_i` (`Submodule.mulLeftMap N m`) has trivial kernel.  -/
Submodule.LinearDisjoint.linearIndependent_left_of_flat : ∀ {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 ↥N] {ι : Type u_1} {m : ι → ↥M}, LinearIndependent R m → (Submodule.mulLeftMap N m).ker = ⊥
-- Mathlib.Data.Nat.Nth
Nat.nth_lt_nth : ∀ {p : ℕ → Prop}, (Set.ofPred p).Infinite → ∀ {k n : ℕ}, Nat.nth p k < Nat.nth p n ↔ k < n
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.prod_cons : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {i : ι} (g : G i)
  (w : Monoid.PushoutI.NormalWord d) (hmw : w.fstIdx ≠ some i) (hgr : g ∉ (φ i).range),
  (Monoid.PushoutI.NormalWord.cons g w hmw hgr).prod = (Monoid.PushoutI.of i) g * w.prod
-- Lean.Data.Json.FromToJson.Basic
Lean.instToJsonOption : {α : Type u_1} → [Lean.ToJson α] → Lean.ToJson (Option α)
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ker_comp_of_injective : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {P : Type u_8} [inst_2 : AddZeroClass P]
  (f : G →+ N) (g : N →+ P), Function.Injective ⇑g → (g.comp f).ker = f.ker
-- Mathlib.GroupTheory.Coset.Basic
MonoidHom.fiberEquivKerOfSurjective.eq_1 : ∀ {α : Type u_1} [inst : Group α] {H : Type u_2} [inst_1 : Group H] {f : α →* H} (hf : Function.Surjective ⇑f) (h : H),
  MonoidHom.fiberEquivKerOfSurjective hf h = ⋯ ▸ f.fiberEquivKer ⋯.choose
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.commRingNorm.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr) (e : Lean.Meta.Grind.Arith.CommRing.RingExpr)
  (p : Lean.Grind.CommRing.Poly),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.commRingNorm c e p) = 1 + sizeOf c + sizeOf e + sizeOf p
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
CategoryTheory.Abelian.Ext.hom_comp_singleFunctor_map_shift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] [inst_3 : HasDerivedCategory C] {X Y Z : C} {n : ℕ}
  (x : CategoryTheory.Abelian.Ext X Y n) (f : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp x.hom
      ((CategoryTheory.shiftFunctor (DerivedCategory C) ↑n).map ((DerivedCategory.singleFunctor C 0).map f)) =
    (x.comp (CategoryTheory.Abelian.Ext.mk₀ f) ⋯).hom
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.weight.eq_2 : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : Monoid R] (w : {i j : V} → (i ⟶ j) → R) (x x_1 b : V)
  (p : Quiver.Path x b) (e : b ⟶ x_1), Quiver.Path.weight w (p.cons e) = Quiver.Path.weight (fun {i j} => w) p * w e
-- Mathlib.Analysis.Complex.Trigonometric
Real.sin_sq_add_cos_sq : ∀ (x : ℝ), Real.sin x ^ 2 + Real.cos x ^ 2 = 1
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.mk_zpow : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {x : α} (hx : 0 ≤ x)
  (n : ℤ), ⟨x, hx⟩ ^ n = ⟨x ^ n, ⋯⟩
-- Mathlib.Computability.TuringMachine.Computable
/-- proof that this machine outputs `f` in at most `time(input.length)` steps  -/
Turing.TM2ComputableInPolyTime.outputsFun : {α β αΓ βΓ : Type} →
  {ea : α → List αΓ} →
    {eb : β → List βΓ} →
      {f : α → β} →
        (self : Turing.TM2ComputableInPolyTime ea eb f) →
          (a : α) →
            Turing.TM2OutputsInTime self.tm (List.map self.inputAlphabet.invFun (ea a))
              (some (List.map self.outputAlphabet.invFun (eb (f a)))) (Polynomial.eval (ea a).length self.time)
-- Mathlib.Order.Filter.Pointwise
Filter.subtractionMonoid.eq_1 : ∀ {α : Type u_2} [inst : SubtractionMonoid α],
  Filter.subtractionMonoid =
    { toAddMonoid := Filter.addMonoid, toNeg := Filter.instInvolutiveNeg.toNeg, toSub := Filter.instSub,
      toZSMul := ZSMul.ofSMul, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_neg := ⋯,
      neg_add_rev := ⋯, neg_eq_of_add := ⋯ }
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.v_eq_succ_vp : ∀ (u : PNat.XgcdType), u.v = PNat.XgcdType.succ₂ u.vp
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.ofScientific.eq_1 : ∀ (m : ℕ) (s : Bool) (e : ℕ), Rat.ofScientific m s e = if s = true then Rat.normalize (↑m) (10 ^ e) ⋯ else ↑(m * 10 ^ e)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isTrail_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w),
  (p.append q).IsTrail ↔ p.IsTrail ∧ q.IsTrail ∧ p.edges.Disjoint q.edges
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cont.then.eq_3 : ∀ (ns : List ℕ) (k : Turing.ToPartrec.Cont),
  (Turing.ToPartrec.Cont.cons₂ ns k).then = fun k' => Turing.ToPartrec.Cont.cons₂ ns (k.then k')
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
Complex.hasSum_cos' : ∀ (z : ℂ), HasSum (fun n => (z * Complex.I) ^ (2 * n) / ↑(2 * n).factorial) (Complex.cos z)
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Comon C} {f g : X ⟶ Y}, f = g ↔ f.hom = g.hom
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- The bijection `Ext X Y 0 ≃ (X ⟶ Y)`.  -/
CategoryTheory.Abelian.Ext.homEquiv₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] → {X Y : C} → CategoryTheory.Abelian.Ext X Y 0 ≃ (X ⟶ Y)
-- Batteries.Tactic.GeneralizeProofs
/-- The initial local context, for resetting when recursing.  -/
Batteries.Tactic.GeneralizeProofs.AContext.initLCtx : Batteries.Tactic.GeneralizeProofs.AContext → Lean.LocalContext
-- Mathlib.Order.BoundedOrder.Basic
/-- A subtype remains a `⊤`-order if the property holds at `⊤`.  -/
Subtype.orderTop : {α : Type u} → {p : α → Prop} → [inst : LE α] → [inst_1 : OrderTop α] → p ⊤ → OrderTop { x // p x }
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureInformation.mk.sizeOf_spec : ∀ (label : String) (documentation? : Option Lean.Lsp.MarkupContent)
  (parameters? : Option (Array Lean.Lsp.ParameterInformation)) (activeParameter? : Option ℕ),
  sizeOf
      { label := label, documentation? := documentation?, parameters? := parameters?,
        activeParameter? := activeParameter? } =
    1 + sizeOf label + sizeOf documentation? + sizeOf parameters? + sizeOf activeParameter?
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.instBoundedOrder.eq_1 : ∀ {α : Type u} [inst : Group α],
  GroupTopology.instBoundedOrder =
    { toTop := GroupTopology.instTop, le_top := ⋯, toBot := GroupTopology.instBot, bot_le := ⋯ }
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.B : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.ExtendedDayPeriod
-- Init.Data.SInt.Lemmas
Int32.mul_neg : ∀ (a b : Int32), a * -b = -(a * b)
-- Mathlib.Algebra.Group.Subgroup.Map
MonoidHom.closure_preimage_le : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) (s : Set N),
  Subgroup.closure (⇑f ⁻¹' s) ≤ Subgroup.comap f (Subgroup.closure s)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
/-- Action of the stabilizer of a point on the complement.  -/
SubMulAction.ofStabilizer : (G : Type u_1) →
  [inst : Group G] → {α : Type u_2} → [inst_1 : MulAction G α] → (a : α) → SubMulAction (↥(MulAction.stabilizer G a)) α
-- Mathlib.Topology.Compactness.Lindelof
isLindelof_diagonal : ∀ {X : Type u} [inst : TopologicalSpace X] [LindelofSpace X], IsLindelof (Set.diagonal X)
-- Mathlib.Order.SuccPred.Basic
Order.pred_le_and_le_iff : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] {a b : α},
  Order.pred a ≤ b ∧ b ≤ a ↔ b = a ∨ b = Order.pred a
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
Int.zmultiples_inf : ∀ (a b : ℤ), AddSubgroup.zmultiples a ⊓ AddSubgroup.zmultiples b = AddSubgroup.zmultiples ↑(a.lcm b)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.op_unop : ∀ {M : Type u_2} [inst : AddZeroClass M] (S : AddSubmonoid Mᵃᵒᵖ), S.unop.op = S
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.minKey?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.minKey? = t₂.minKey?