mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.reduce_fold_fn.match_3.eq_1 : ∀ {n : ℕ}
  (motive : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty)
  (h_3 :
    (l' : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
      motive (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l'))
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit),
  (match Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth with
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l' => h_3 l'
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit => h_4 ()) =
    h_1 ()
-- Mathlib.Data.Seq.Computation
Computation.liftRel_think_left : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (ca : Computation α) (cb : Computation β),
  Computation.LiftRel R ca.think cb ↔ Computation.LiftRel R ca cb
-- Std.Time.Format.Modifier
Std.Time.OffsetX.hourMinuteSecond.sizeOf_spec : sizeOf Std.Time.OffsetX.hourMinuteSecond = 1
-- Std.Do.WP.Monad
Std.Do.Id.instWPMonad : Std.Do.WPMonad Id Std.Do.PostShape.pure
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedGoalState : Inhabited Lean.Meta.Grind.GoalState
-- Mathlib.AlgebraicGeometry.Sites.ConstantSheaf
/-- `continuousMapPresheafAb` viewed as a type valued sheaf is isomorphic to
`continuousMapPresheaf`.  -/
AlgebraicGeometry.continuousMapPresheafAbForgetIso : (A : Type v) →
  [inst : TopologicalSpace A] →
    [inst_1 : AddCommGroup A] →
      [inst_2 : IsTopologicalAddGroup A] →
        (AlgebraicGeometry.continuousMapPresheafAb A).comp (CategoryTheory.forget Ab) ≅
          AlgebraicGeometry.continuousMapPresheaf A
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.norm_ofNormedAddCommGroup_le : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] {f : α → β}
  (hfc : Continuous f) {C : ℝ},
  0 ≤ C → ∀ (hfC : ∀ (x : α), ‖f x‖ ≤ C), ‖BoundedContinuousFunction.ofNormedAddCommGroup f hfc C hfC‖ ≤ C
-- Init.Data.Nat.Simproc
Nat.Simproc.beqFalseOfEqFalse : ∀ {a b : ℕ}, (a = b) = False → (a == b) = false
-- Init.Core
/-- `break s` means that `break` was called, meaning that we should exit
from the containing loop  -/
DoResultPRBC.break : {α β σ : Type u} → σ → DoResultPRBC α β σ
-- Mathlib.RingTheory.Artinian.Module
IsArtinianRing.isUnitSubmonoid_eq : ∀ (R : Type u_1) [inst : Ring R] [IsArtinianRing R], IsUnit.submonoid R = nonZeroDivisors R
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.MorphismProperty.pretopology_monotone : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {P Q : CategoryTheory.MorphismProperty C} [inst_2 : P.IsMultiplicative] [inst_3 : P.IsStableUnderBaseChange]
  [inst_4 : Q.IsMultiplicative] [inst_5 : Q.IsStableUnderBaseChange], P ≤ Q → P.pretopology ≤ Q.pretopology
-- Mathlib.Algebra.Star.Basic
toEquiv_starAddEquiv : ∀ {R : Type u} [inst : AddMonoid R] [inst_1 : StarAddMonoid R], ↑starAddEquiv = Equiv.Perm.star
-- Mathlib.RingTheory.Grassmannian
Module.Grassmannian.ext_iff : ∀ {R : Type u} [inst : CommRing R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {k : ℕ}
  {N₁ N₂ : Module.Grassmannian R M k}, N₁ = N₂ ↔ N₁.toSubmodule = N₂.toSubmodule
-- Init.Data.BitVec.Lemmas
BitVec.flattenList_eq_flattenListFast : @BitVec.flattenList = @BitVec.flattenListFast
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.comapIso_inv_subschemeι : ∀ {X Y : AlgebraicGeometry.Scheme} (I : Y.IdealSheafData) (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (I.comapIso f).inv (I.comap f).subschemeι =
    CategoryTheory.Limits.pullback.fst f I.subschemeι
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
cmp_add_left : ∀ {α : Type u_3} [inst : Add α] [inst_1 : LinearOrder α] [AddLeftStrictMono α] (a b c : α),
  cmp (a + b) (a + c) = cmp b c
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.map_id : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (z : N), (f.map ⋯ f) z = z
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.LaxTrans.comp_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {X Y Z : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.LaxTrans X Y) (θ : CategoryTheory.Lax.LaxTrans Y Z)
  (a : B), (CategoryTheory.CategoryStruct.comp η θ).app a = CategoryTheory.CategoryStruct.comp (η.app a) (θ.app a)
-- Init.Data.Vector.Lemmas
Vector.contains_push : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {xs : Vector α n} {a b : α}, (xs.push a).contains b = (xs.contains b || b == a)
-- Mathlib.Topology.Category.TopCat.Basic
/-- Any homeomorphisms induces an isomorphism in `Top`.  -/
TopCat.isoOfHomeo : {X Y : TopCat} → ↑X ≃ₜ ↑Y → (X ≅ Y)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddSemigroup : {α : Type u_1} → {l : Filter α} → {M : Type u_5} → [AddSemigroup M] → AddSemigroup (l.Germ M)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.hasPullback_symmetry_of_hasPullbacksAlong : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {S X Y : C} {f : X ⟶ S}
  [CategoryTheory.Limits.HasPullbacksAlong f] {g : Y ⟶ S}, CategoryTheory.Limits.HasPullback f g
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartRing.leibniz_mul_right : ∀ {A₁ : Type u_2} {L₁ : Type u_3} [inst : CommRing A₁] [inst_1 : LieRing L₁] [inst_2 : Module A₁ L₁]
  [inst_3 : LieRingModule L₁ A₁] [LieRinehartRing A₁ L₁] (x : L₁) (a b : A₁), ⁅x, a * b⁆ = a • ⁅x, b⁆ + ⁅x, a⁆ * b
-- Aesop.Tree.Data
Aesop.NodeState.unknown : Aesop.NodeState
-- Mathlib.Analysis.Convex.Strict
/-- **Alias** of the forward direction of `strictConvex_iff_ordConnected`. -/
StrictConvex.ordConnected : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [inst_3 : TopologicalSpace 𝕜]
  [OrderTopology 𝕜] {s : Set 𝕜}, StrictConvex 𝕜 s → s.OrdConnected
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.FirstByte.twoMore.sizeOf_spec : sizeOf ByteArray.utf8DecodeChar?.FirstByte.twoMore = 1
-- Init.Data.Order.ClassesExtra
Std.LawfulOrderOrd.isLE_compare_eq_false : ∀ {α : Type u} [inst : Ord α] [inst_1 : LE α] [Std.LawfulOrderOrd α] {a b : α}, (compare a b).isLE = false ↔ ¬a ≤ b
-- Mathlib.Algebra.Lie.Weights.Killing
/-- The embedded `sl₂` associated to a root.  -/
LieAlgebra.IsKilling.sl2SubalgebraOfRoot : {K : Type u_2} →
  {L : Type u_3} →
    [inst : LieRing L] →
      [inst_1 : Field K] →
        [inst_2 : LieAlgebra K L] →
          [FiniteDimensional K L] →
            {H : LieSubalgebra K L} →
              [inst_4 : H.IsCartanSubalgebra] →
                [LieAlgebra.IsKilling K L] →
                  [LieModule.IsTriangularizable K (↥H) L] →
                    [CharZero K] → {α : LieModule.Weight K (↥H) L} → α.IsNonZero → LieSubalgebra K L
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
/-- Constructor for short complexes in `ModuleCat.{v} R` taking as inputs
morphisms `f` and `g` and the assumption `LinearMap.range f ≤ LinearMap.ker g`.  -/
CategoryTheory.ShortComplex.moduleCatMkOfKerLERange : {R : Type u} →
  [inst : Ring R] →
    {X₁ X₂ X₃ : ModuleCat R} →
      (f : X₁ ⟶ X₂) →
        (g : X₂ ⟶ X₃) →
          (ModuleCat.Hom.hom f).range ≤ (ModuleCat.Hom.hom g).ker → CategoryTheory.ShortComplex (ModuleCat R)
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.coe_prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e₁ : α ↪ β) (e₂ : γ ↪ δ),
  ⇑(e₁.prodMap e₂) = Prod.map ⇑e₁ ⇑e₂
-- Mathlib.Algebra.Algebra.Hom
/-- R-Alg ⥤ R-Mod  -/
AlgHom.toLinearMap : {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] → (A →ₐ[R] B) → A →ₗ[R] B
-- Init.Data.String.Termination
String.Pos.remainingBytes_eq_byteDistance : ∀ {s : String} {p : s.Pos}, p.remainingBytes = p.offset.byteDistance s.endPos.offset
-- Mathlib.Algebra.Ring.Commute
mul_neg_one_pow_eq_zero_iff : ∀ {R : Type u} [inst : Ring R] {a : R} {n : ℕ}, a * (-1) ^ n = 0 ↔ a = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.ι_colimitFiberwiseColimitIso_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)
  [inst_2 :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))]
  [inst_3 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.fiberwiseColimit G)] (X : C) (d : ↑(F.obj X))
  {Z : H} (h : CategoryTheory.Limits.colimit G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Grothendieck.ι F X).comp G) d)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Limits.fiberwiseColimit G) X)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitFiberwiseColimitIso G).hom h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G { base := X, fiber := d }) h
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.equivEssImageOfReflective_counitIso : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {i : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Reflective i],
  CategoryTheory.equivEssImageOfReflective.counitIso =
    CategoryTheory.Functor.fullyFaithfulCancelRight i.essImage.ι
      (CategoryTheory.NatIso.ofComponents
        (fun X => (CategoryTheory.asIso ((CategoryTheory.reflectorAdjunction i).unit.app X.obj)).symm) ⋯)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The product of an antitone function and a strictly antitone function is strictly antitone.  -/
AntitoneOn.mul_strictAnti' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {s : Set β}
  [MulLeftStrictMono α] [MulRightMono α] {f g : β → α},
  AntitoneOn f s → StrictAntiOn g s → StrictAntiOn (fun x => f x * g x) s
-- Init.Data.Vector.Lemmas
/-- We can prove that two folds over the same vector are related (by some arbitrary relation)
if we know that the initial elements are related and the folding function, for each element of the
vector, preserves the relation.
 -/
Vector.foldl_rel : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {γ : Type u_3} {xs : Vector α n} {f : β → α → β} {g : γ → α → γ} {a : β} {b : γ}
  {r : β → γ → Prop},
  r a b →
    (∀ a ∈ xs, ∀ (c : β) (c' : γ), r c c' → r (f c a) (g c' a)) →
      r (Vector.foldl (fun acc a => f acc a) a xs) (Vector.foldl (fun acc a => g acc a) b xs)
-- Std.Time.Duration
Std.Time.Duration.instHSubOffset_6 : HSub Std.Time.Duration Std.Time.Millisecond.Offset Std.Time.Duration
-- Mathlib.Algebra.Order.ToIntervalMod
toIocDiv_apply_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a : α), toIocDiv hp a a = -1
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₁ → (m₁ \ m₂)[k]? = none
-- Mathlib.Data.Finset.Update
/-- `updateFinset x s y` is the vector `x` with the coordinates in `s` changed to the values of `y`.
 -/
Function.updateFinset : {ι : Type u_1} →
  {π : ι → Sort u_2} → [DecidableEq ι] → ((i : ι) → π i) → (s : Finset ι) → ((i : ↥s) → π ↑i) → (i : ι) → π i
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.extension₂_coe_coe : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  (pkg' : AbstractCompletion.{vβ, uβ} β) {γ : Type uγ} [inst_2 : UniformSpace γ] [T0Space γ] {f : α → β → γ},
  UniformContinuous (Function.uncurry f) → ∀ (a : α) (b : β), pkg.extend₂ pkg' f (pkg.coe a) (pkg'.coe b) = f a b
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.symm_mk_zsmul : ∀ {M : Type u_1} [inst : SubNegMonoid M] (a : Mᵈᵃᵃ) (n : ℤ), DomAddAct.mk.symm (n • a) = n • DomAddAct.mk.symm a
-- Mathlib.Order.PrimeIdeal
/-- A pair of an `Order.Ideal` and an `Order.PFilter` which form a partition of `P`.
 -/
Order.Ideal.PrimePair : (P : Type u_2) → [Preorder P] → Type u_2
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_add : ∀ {α : Type u_2} {_m0 : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) (s : Set α),
  (μ + ν).restrict s = μ.restrict s + ν.restrict s
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.denoteS_mulMon_nc_go : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (k : ℤ)
  (m : Lean.Grind.CommRing.Mon) (p acc : Lean.Grind.CommRing.Poly),
  k ≥ 0 →
    p.NonnegCoeffs →
      acc.NonnegCoeffs →
        Lean.Grind.CommRing.Poly.denoteS ctx (Lean.Grind.CommRing.Poly.mulMon_nc.go k m p acc) =
          ↑k.toNat * Lean.Grind.CommRing.Mon.denote ctx m * Lean.Grind.CommRing.Poly.denoteS ctx p +
            Lean.Grind.CommRing.Poly.denoteS ctx acc
-- Mathlib.Data.Nat.Factorization.Basic
Nat.prod_primeFactors_coe_pow_factorization : ∀ {n : ℕ}, n ≠ 0 → n = ∏ p, ↑p ^ n.factorization ↑p
-- Lean.Meta.Tactic.Simp.SimpAll
_private.Lean.Meta.Tactic.Simp.SimpAll.0.Lean.Meta.SimpAll.initEntries : Lean.Meta.SimpAll.M Unit
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.map_ofFunction_le : ∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} {β : Type u_2} (f : α → β),
  (MeasureTheory.OuterMeasure.map f) (MeasureTheory.OuterMeasure.ofFunction m m_empty) ≤
    MeasureTheory.OuterMeasure.ofFunction (fun s => m (f ⁻¹' s)) m_empty
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn.faceι_ι_assoc : ∀ {n : ℕ} (i j : Fin (n + 1)) (hij : j ≠ i) {Z : SSet} (h : SSet.stdSimplex.obj { len := n } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.horn.faceι i j hij)
      (CategoryTheory.CategoryStruct.comp (SSet.horn n i).ι h) =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.face {j}ᶜ).ι h
-- Mathlib.Data.Vector.Basic
/-- Providing an empty vector to `scanl` gives the starting value `b : β`.  -/
List.Vector.scanl_nil : ∀ {α : Type u_1} {β : Type u_6} (f : β → α → β) (b : β), List.Vector.scanl f b List.Vector.nil = b ::ᵥ List.Vector.nil
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
CategoryTheory.Precoverage.HasIsos.of_preZeroHypercoverFamily : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.PreZeroHypercoverFamily C},
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y) [CategoryTheory.IsIso f], P.property (CategoryTheory.PreZeroHypercover.singleton f)) →
    P.precoverage.HasIsos
-- Lean.DocString.Types
/-- A footnote. In Verso's concrete syntax, their contents are specified elsewhere, but elaboration
places the contents at the use site.
 -/
Lean.Doc.Inline.footnote : {i : Type u} → String → Array (Lean.Doc.Inline i) → Lean.Doc.Inline i
-- Init.GrindInstances.ToInt
Lean.Grind.toInt_int64 : ∀ (x : Int64), ↑x = x.toInt
-- Mathlib.LinearAlgebra.AffineSpace.Centroid
/-- In the characteristic zero case, the weights in the centroid
indexed by a `Fintype` sum to 1 if the number of points is not
zero.  -/
Finset.sum_centroidWeightsIndicator_eq_one_of_card_ne_zero : ∀ (k : Type u_1) [inst : DivisionRing k] {ι : Type u_4} (s : Finset ι) [CharZero k] [inst_2 : Fintype ι],
  s.card ≠ 0 → ∑ i, Finset.centroidWeightsIndicator k s i = 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.map_baseChange : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) {S : Type s} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {A : Type v} [inst_3 : CommRing A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {B : Type w}
  [inst_7 : CommRing B] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B] (g : A →ₐ[S] B),
  (W.baseChange A).map ↑g = W.baseChange B
-- Mathlib.LinearAlgebra.DFinsupp
Submodule.mem_iSup_iff_exists_finsupp : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  (p : ι → Submodule R N) (x : N), x ∈ iSup p ↔ ∃ f, (∀ (i : ι), f i ∈ p i) ∧ (f.sum fun _i xi => xi) = x
-- Mathlib.Analysis.Fourier.AddCircle
fourierCoeffOn_congr_ae : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} (hab : a < b) {f g : ℝ → E},
  f =ᵐ[MeasureTheory.volume.restrict (Set.Ioc a b)] g → fourierCoeffOn hab f = fourierCoeffOn hab g
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.FixedParamPerm.isFixed : Lean.Elab.FixedParamPerm → ℕ → Bool
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.inner_add_right : ∀ {A : Type u_1} {E : Type u_2} {inst : NonUnitalSemiring A} {inst_1 : StarRing A} {inst_2 : Module ℂ A}
  {inst_3 : AddCommGroup E} {inst_4 : Module ℂ E} {inst_5 : PartialOrder A} {inst_6 : SMul A E} {inst_7 : Norm A}
  {inst_8 : Norm E} [self : CStarModule A E] {x y z : E}, inner A x (y + z) = inner A x y + inner A x z
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.saveEqnCandidate : Lean.Name → Lean.Meta.Try.Collector.M Unit
-- Mathlib.Data.PNat.Interval
PNat.Ioc_eq_finset_subtype : ∀ (a b : ℕ+), Finset.Ioc a b = Finset.subtype (fun n => 0 < n) (Finset.Ioc ↑a ↑b)
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_submatrix_sum_swap_right : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {p : Type u_5} {α : Type u_12} (A : Matrix n l α)
  (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (f : p → n ⊕ o),
  (Matrix.fromBlocks A B C D).submatrix f Sum.swap = (Matrix.fromBlocks B A D C).submatrix f id
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
/-- Mapping quasicoherent data under an isomorphism.  -/
SheafOfModules.QuasicoherentData.ofIsIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat] →
          [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] →
            {M N : SheafOfModules R} →
              (f : M ⟶ N) → [CategoryTheory.IsIso f] → M.QuasicoherentData → N.QuasicoherentData
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
Real.deriv_arctan : deriv Real.arctan = fun x => 1 / (1 + x ^ 2)
-- Mathlib.Logic.Embedding.Set
/-- `Set.image` as an embedding `Set α ↪ Set β`.  -/
Function.Embedding.image : {α : Type u_1} → {β : Type u_2} → (α ↪ β) → Set α ↪ Set β
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.Hom.mk.sizeOf_spec : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  {X X' : CategoryTheory.Abelian.SpectralObject C ι} [inst_3 : SizeOf C] [inst_4 : SizeOf ι]
  (hom : (n : ℤ) → X.H n ⟶ X'.H n)
  (comm :
    autoParam
      (∀ (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
        CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) ((hom n₁).app (CategoryTheory.ComposableArrows.mk₁ f)) =
          CategoryTheory.CategoryStruct.comp ((hom n₀).app (CategoryTheory.ComposableArrows.mk₁ g))
            (X'.δ f g n₀ n₁ hn₁))
      CategoryTheory.Abelian.SpectralObject.Hom.comm._autoParam),
  sizeOf { hom := hom, comm := comm } = 1
-- Mathlib.Order.Minimal
Minimal.notMem_of_prop_sdiff_singleton : ∀ {α : Type u_2} {x : α} {P : Set α → Prop} {s : Set α}, Minimal P s → P (s \ {x}) → x ∉ s
-- Mathlib.RingTheory.Ideal.Lattice
Ideal.eq_top_of_unit_mem : ∀ {α : Type u} [inst : Semiring α] (I : Ideal α) (x y : α), x ∈ I → y * x = 1 → I = ⊤
-- Mathlib.Order.Filter.CountableInter
Filter.CountableGenerateSets.below.sInter : ∀ {α : Type u_2} {g : Set (Set α)} {motive : (a : Set α) → Filter.CountableGenerateSets g a → Prop} {S : Set (Set α)}
  (a : S.Countable) (a_1 : ∀ s ∈ S, Filter.CountableGenerateSets g s),
  (∀ (s : Set α) (a : s ∈ S), Filter.CountableGenerateSets.below ⋯) →
    (∀ (s : Set α) (a : s ∈ S), motive s ⋯) → Filter.CountableGenerateSets.below ⋯
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.State.mk.injEq : ∀ (goals goals_1 : List Lean.MVarId), ({ goals := goals } = { goals := goals_1 }) = (goals = goals_1)
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.const_min : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {f : α → ℝ} {Kf : NNReal},
  LipschitzWith Kf f → ∀ (a : ℝ), LipschitzWith Kf fun x => min a (f x)
-- Mathlib.Order.Preorder.Chain
/-- Given a set `s`, if there exists a chain `t` strictly including `s`, then `SuccChain s`
is one of these chains. Otherwise it is `s`.  -/
SuccChain : {α : Type u_1} → (α → α → Prop) → Set α → Set α
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- If `M` and `N` are linearly disjoint, if one of `M` and `N` is flat, then any two commutative
elements of `↥(M ⊓ N)` are not `R`-linearly independent (namely, their span is not `R ^ 2`).  -/
Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_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 →
    ∀ [Nontrivial R],
      Module.Flat R ↥M ∨ Module.Flat R ↥N → ∀ (a b : ↥(M ⊓ N)), Commute ↑a ↑b → ¬LinearIndependent R ![a, b]
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.col_def : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α), A.col = fun j => A.transpose j
-- Mathlib.Algebra.GroupWithZero.Indicator
Function.mulSupport_one_sub' : ∀ {ι : Type u_1} {R : Type u_5} [inst : One R] [inst_1 : AddGroup R] (f : ι → R),
  Function.mulSupport (1 - f) = Function.support f
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.snd_swapRight : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)), κ.swapRight.snd = κ.fst
-- Mathlib.Probability.Martingale.BorelCantelli
MeasureTheory.BorelCantelli.predictablePart_process_ae_eq : ∀ {Ω : Type u_2} {m0 : MeasurableSpace Ω} (ℱ : MeasureTheory.Filtration ℕ m0) (μ : MeasureTheory.Measure Ω)
  (s : ℕ → Set Ω) (n : ℕ),
  MeasureTheory.predictablePart (MeasureTheory.BorelCantelli.process s) ℱ μ n =
    ∑ k ∈ Finset.range n, μ[(s (k + 1)).indicator 1 | ↑ℱ k]
-- Mathlib.GroupTheory.Perm.Fin
Fin.isCycle_cycleIcc : ∀ {n : ℕ} {i j : Fin n}, i < j → (i.cycleIcc j).IsCycle
-- Mathlib.Tactic.CategoryTheory.BicategoricalComp
CategoryTheory.BicategoricalCoherence.assoc : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          (h : c ⟶ d) →
            (i : a ⟶ d) →
              [CategoryTheory.BicategoricalCoherence
                    (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)) i] →
                CategoryTheory.BicategoricalCoherence
                  (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h) i
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.map_conv_continuousLinearMap : ∀ {E : Type u_2} {F : Type u_3} [inst : AddCommMonoid E] [inst_1 : AddCommMonoid F] [inst_2 : Module ℝ E]
  [inst_3 : Module ℝ F] [inst_4 : TopologicalSpace E] [inst_5 : TopologicalSpace F] {mE : MeasurableSpace E}
  [MeasurableAdd₂ E] {mF : MeasurableSpace F} [MeasurableAdd₂ F] [OpensMeasurableSpace E] [BorelSpace F]
  {μ ν : MeasureTheory.Measure E} [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] (L : E →L[ℝ] F),
  MeasureTheory.Measure.map (⇑L) (μ.conv ν) = (MeasureTheory.Measure.map (⇑L) μ).conv (MeasureTheory.Measure.map (⇑L) ν)