mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.LawfulBackwardPattern.skipSuffixOfNonempty?_eq : ∀ {ρ : Type} {pat : ρ} {inst : String.Slice.Pattern.BackwardPattern pat}
  [self : String.Slice.Pattern.LawfulBackwardPattern pat] {s : String.Slice} (h : s.isEmpty = false),
  String.Slice.Pattern.BackwardPattern.skipSuffixOfNonempty? pat s h =
    String.Slice.Pattern.BackwardPattern.skipSuffix? pat s
-- Mathlib.Algebra.Group.Nat.Hom
powersMulHom_apply : ∀ {M : Type u_1} [inst : CommMonoid M] (x : M) (n : Multiplicative ℕ),
  ((powersMulHom M) x) n = x ^ Multiplicative.toAdd n
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.replicateCol_eq_zero : ∀ {m : Type u_2} {α : Type v} {ι : Type u_6} [inst : Zero α] [Nonempty ι] (v : m → α),
  Matrix.replicateCol ι v = 0 ↔ v = 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
fderivWithin_sin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E},
  DifferentiableWithinAt ℝ f s x →
    UniqueDiffWithinAt ℝ s x → fderivWithin ℝ (fun x => Real.sin (f x)) s x = Real.cos (f x) • fderivWithin ℝ f s x
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.instInhabitedIdTrue : {X : Type u} →
  [inst : TopologicalSpace X] → Inhabited ((ContinuousMap.id X).HomotopyWith (ContinuousMap.id X) fun x => True)
-- Mathlib.Analysis.Convex.Slope
/-- A function `f : 𝕜 → 𝕜` is strictly concave iff for any three points `x < y < z` the slope of
the secant line of `f` on `[x, y]` is strictly greater than the slope of the secant line of `f` on
`[y, z]`.  -/
strictConcaveOn_iff_slope_strict_anti_adjacent : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  StrictConcaveOn 𝕜 s f ↔
    Convex 𝕜 s ∧ ∀ ⦃x y z : 𝕜⦄, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) < (f y - f x) / (y - x)
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion
_private.Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Torsion.0.IsCovariantDerivativeOn.torsionAux.eq_1 : ∀ {𝕜 : 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]
  (cov : ((x : M) → TangentSpace I x) → (x : M) → TangentSpace I x →L[𝕜] TangentSpace I x)
  (X Y : (x : M) → TangentSpace I x) (x : M),
  IsCovariantDerivativeOn.torsionAux✝ cov X Y x = (cov Y x) (X x) - (cov X x) (Y x) - VectorField.mlieBracket I X Y x
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If `s` is any colimit cokernel cocone over `f` and `i` is an isomorphism such that
`s.π ≫ i.hom = l`, then `l` is a cokernel of `f`.  -/
CategoryTheory.Limits.IsCokernel.cokernelIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          {Z : C} →
            (l : Y ⟶ Z) →
              {s : CategoryTheory.Limits.CokernelCofork f} →
                CategoryTheory.Limits.IsColimit s →
                  (i : s.pt ≅ Z) →
                    (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π s) i.hom = l) →
                      CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ l ⋯)
-- Mathlib.Order.Category.DistLat
DistLat.instCategory : CategoryTheory.Category.{u, u + 1} DistLat
-- Mathlib.Data.Set.Lattice
Set.iInter₂_mono' : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} {κ : ι → Sort u_8} {κ' : ι' → Sort u_11} {s : (i : ι) → κ i → Set α}
  {t : (i' : ι') → κ' i' → Set α},
  (∀ (i' : ι') (j' : κ' i'), ∃ i j, s i j ⊆ t i' j') → ⋂ i, ⋂ j, s i j ⊆ ⋂ i', ⋂ j', t i' j'
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
/-- The bounded below derived category of an abelian category.  -/
DerivedCategory.Plus : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → [HasDerivedCategory C] → Type (max u v)
-- Mathlib.RingTheory.Etale.Descent
RingHom.FormallyUnramified.codescendsAlong_faithfullyFlat : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] => RingHom.FormallyUnramified)
  fun {R S} [CommRing R] [CommRing S] => RingHom.FaithfullyFlat
-- Mathlib.CategoryTheory.Functor.FullyFaithful
/-- The equivalence `(X ≅ Y) ≃ (F.obj X ≅ F.obj Y)` given by `h : F.FullyFaithful`.  -/
CategoryTheory.Functor.FullyFaithful.isoEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} → F.FullyFaithful → {X Y : C} → (X ≅ Y) ≃ (F.obj X ≅ F.obj Y)
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.upperCentralSeries.eq_top : ∀ {G : Type u_1} [inst : AddGroup G] [AddGroup.IsNilpotent G] {a b : ℕ},
  a ≠ b →
    AddSubgroup.upperCentralSeries G a = AddSubgroup.upperCentralSeries G b → AddSubgroup.upperCentralSeries G a = ⊤
-- Mathlib.LinearAlgebra.Pi
/-- This is `Equiv.piOptionEquivProd` as a `LinearEquiv`  -/
LinearEquiv.piOptionEquivProd : (R : Type u) →
  [inst : Semiring R] →
    {ι : Type u_4} →
      {M : Option ι → Type u_5} →
        [inst_1 : (i : Option ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : Option ι) → Module R (M i)] → ((i : Option ι) → M i) ≃ₗ[R] M none × ((i : ι) → M (some i))
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.toFinset_normalizedFactors : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a : M} [inst_3 : DecidableEq M],
  (UniqueFactorizationMonoid.normalizedFactors a).toFinset = UniqueFactorizationMonoid.primeFactors a
-- Mathlib.Topology.EMetricSpace.Defs
uniformity_basis_edist_le : ∀ {α : Type u} [inst : PseudoEMetricSpace α], (uniformity α).HasBasis (fun ε => 0 < ε) fun ε => {p | edist p.1 p.2 ≤ ε}
-- Init.Data.BitVec.Lemmas
BitVec.ofBool_and_ofBool : ∀ {b b' : Bool}, BitVec.ofBool b &&& BitVec.ofBool b' = BitVec.ofBool (b && b')
-- Mathlib.GroupTheory.GroupAction.Transitive
/-- An additive action of an additive group is pretransitive
iff any element can be moved from a fixed given one.  -/
AddAction.isPretransitive_iff_base : ∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] (a : X),
  AddAction.IsPretransitive G X ↔ ∀ (x : X), ∃ g, g +ᵥ a = x
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.quotKerTotalEquiv_symm_comp_D : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (↑(KaehlerDifferential.quotKerTotalEquiv R S).symm).compDer (KaehlerDifferential.D R S) =
    KaehlerDifferential.derivationQuotKerTotal R S
-- Mathlib.Data.Set.Finite.Lemmas
Set.Finite.fin_embedding : ∀ {α : Type u} {s : Set α}, s.Finite → ∃ n f, Set.range ⇑f = s
-- Mathlib.Analysis.Analytic.Binomial
Real.one_div_one_sub_sq_hasFPowerSeriesOnBall_zero : HasFPowerSeriesOnBall (fun x => 1 / (1 - x) ^ 2) (FormalMultilinearSeries.ofScalars ℝ fun n => ↑n + 1) 0 1
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_eval_preimage_null : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {i : ι} {s : Set (α i)},
  (μ i) s = 0 → (MeasureTheory.Measure.pi μ) (Function.eval i ⁻¹' s) = 0
-- Mathlib.Order.KrullDimension
/-- The Krull dimension is the supremum of the elements' coheights.

If `α` is `Nonempty`, then `krullDim_eq_iSup_coheight_of_nonempty`, with the coercion from
`ℕ∞` to `WithBot ℕ∞` outside the supremum, can be more convenient.
 -/
Order.krullDim_eq_iSup_coheight : ∀ {α : Type u_1} [inst : Preorder α], Order.krullDim α = ⨆ a, ↑(Order.coheight a)
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.NonemptyCompacts.isUniformEmbedding_coe : ∀ {α : Type u_1} [inst : UniformSpace α], IsUniformEmbedding SetLike.coe
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.restriction_of : ∀ {α : Type u} (s : Set α) [inst : DecidablePred fun x => x ∈ s] (p : α),
  (FreeCommRing.restriction s) (FreeCommRing.of p) = if H : p ∈ s then FreeCommRing.of ⟨p, H⟩ else 0
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Cell.Const.get?.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] {k : α} (c : Std.DTreeMap.Internal.Cell α (fun x => β) (compare k)),
  Std.DTreeMap.Internal.Cell.Const.get? c =
    match c.inner with
    | none => none
    | some p => some p.snd
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.opEquiv.match_13.eq_1 : ∀ (C : Type u_1) (motive : CategoryTheory.WithTerminal Cᵒᵖ → Sort u_2) (x : Cᵒᵖ)
  (h_1 : (x : Cᵒᵖ) → motive (CategoryTheory.WithTerminal.of x)) (h_2 : Unit → motive CategoryTheory.WithTerminal.star),
  (match CategoryTheory.WithTerminal.of x with
    | CategoryTheory.WithTerminal.of x => h_1 x
    | CategoryTheory.WithTerminal.star => h_2 ()) =
    h_1 x
-- Mathlib.GroupTheory.Congruence.BigOperators
/-- Additive congruence relations preserve sum indexed by a multiset.  -/
AddCon.multiset_sum : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (c : AddCon M) {s : Multiset ι} {f g : ι → M},
  (∀ x ∈ s, c (f x) (g x)) → c (Multiset.map f s).sum (Multiset.map g s).sum
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Expression of the `circleAverage` in terms of a `circleIntegral`.
 -/
Real.circleAverage_eq_circleIntegral : ∀ {c : ℂ} {R : ℝ} {F : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℂ F] {f : ℂ → F},
  R ≠ 0 → Real.circleAverage f c R = (2 * ↑Real.pi * Complex.I)⁻¹ • ∮ (z : ℂ) in C(c, R), (z - c)⁻¹ • f z
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
SymmetricAlgebra.algebraMap_inj : ∀ {R : Type u_1} (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x y : R),
  (algebraMap R (SymmetricAlgebra R M)) x = (algebraMap R (SymmetricAlgebra R M)) y ↔ x = y
-- Init.Data.UInt.Bitwise
UInt8.xor_zero : ∀ {a : UInt8}, a ^^^ 0 = a
-- Mathlib.RingTheory.SimpleModule.Isotypic
sSupIndep_isotypicComponents : ∀ (R : Type u_2) (M : Type u) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  sSupIndep (isotypicComponents R M)
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- A homotopy between `n+1`-dimensional loops `p` and `q` constant on the boundary
seen as a homotopy between two paths in the space of `n`-dimensional paths.  -/
GenLoop.homotopyTo : {N : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace X] →
      {x : X} →
        [DecidableEq N] →
          (i : N) →
            {p q : ↑(GenLoop N X x)} →
              (↑p).HomotopyRel (↑q) (Cube.boundary N) →
                C(↑unitInterval × ↑unitInterval, C({ j // j ≠ i } → ↑unitInterval, X))
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- Get the equalizer morphism from the typeclass `IsCosplitPair`.  -/
CategoryTheory.HasSplitEqualizer.equalizerι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (f g : X ⟶ Y) →
        [inst_1 : CategoryTheory.HasSplitEqualizer f g] → CategoryTheory.HasSplitEqualizer.equalizerOfSplit f g ⟶ X
-- Mathlib.Logic.Function.Basic
Function.instIsPreorderOnFun : ∀ {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) [IsPreorder β r], IsPreorder α (Function.onFun r f)
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of the reverse direction of `LinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff`.

---

`ker f` is invariant under `T` if and only if `f ∘ₗ T ∘ₗ f = f ∘ₗ T`,
for idempotent `f`.  -/
LinearMap.IsIdempotentElem.ker_mem_invtSubmodule : ∀ {E : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup E] [inst_2 : Module R E] {T f : E →ₗ[R] E},
  IsIdempotentElem f → f ∘ₗ T ∘ₗ f = f ∘ₗ T → f.ker ∈ Module.End.invtSubmodule T
-- Mathlib.CategoryTheory.GradedObject.Associator
CategoryTheory.GradedObject.ι_mapBifunctorAssociator_inv : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Category.{v_6, u_4} C₂₃]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)}
  (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃) {I₁ : Type u_7}
  {I₂ : Type u_8} {I₃ : Type u_9} {J : Type u_10} {r : I₁ × I₂ × I₃ → J}
  (ρ₁₂ : CategoryTheory.GradedObject.BifunctorComp₁₂IndexData r)
  (ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r) (X₁ : CategoryTheory.GradedObject I₁ C₁)
  (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃)
  [inst_6 : (((CategoryTheory.GradedObject.mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p]
  [inst_7 :
    (((CategoryTheory.GradedObject.mapBifunctor G ρ₁₂.I₁₂ I₃).obj
              (CategoryTheory.GradedObject.mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj
          X₃).HasMap
      ρ₁₂.q]
  [inst_8 : (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
  [inst_9 :
    (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
      ρ₂₃.q]
  [H₁₂ : CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃]
  [H₂₃ : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J)
  (h : r (i₁, i₂, i₃) = j),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h)
      ((CategoryTheory.GradedObject.mapBifunctorAssociator associator ρ₁₂ ρ₂₃ X₁ X₂ X₃).inv j) =
    CategoryTheory.CategoryStruct.comp (((associator.inv.app (X₁ i₁)).app (X₂ i₂)).app (X₃ i₃))
      (CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.ofList_nil : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v}, Std.DHashMap.Raw.Const.ofList [] = ∅
-- Mathlib.Analysis.Complex.Basic
Complex.instCompleteSpace : CompleteSpace ℂ
-- Std.Http.Data.URI.Basic
/-- Returns true if the path has no segments.
 -/
Std.Http.URI.Path.isEmpty : Std.Http.URI.Path → Bool
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- The `p`-adic value of an integer `z ≠ 0` is the multiplicity of `p` in `z`.  -/
padicValRat.of_int_multiplicity : ∀ {p : ℕ} {z : ℤ}, p ≠ 1 → z ≠ 0 → padicValRat p ↑z = ↑(multiplicity (↑p) z)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork_φH : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0)
  (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hg₂ : S₂.g = 0)
  (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt)
  (comm :
    CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f),
  (CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).φH = f
-- Mathlib.Algebra.BigOperators.Group.List.Defs
List.sum_induction : ∀ {M : Type u_2} [inst : Add M] [inst_1 : Zero M] {l : List M} (p : M → Prop),
  (∀ (a b : M), p a → p b → p (a + b)) → p 0 → (∀ x ∈ l, p x) → p l.sum
-- Batteries.Data.Stream
Std.Stream.takeTR.loop.eq_1 : ∀ {σ : Type u_1} {α : Type u_2} [inst : Std.Stream σ α] (s : σ) (acc : List α),
  Std.Stream.takeTR.loop s acc 0 = (acc.reverse, s)
-- Mathlib.Probability.CondVar
ProbabilityTheory.condVar_smul : ∀ {Ω : Type u_1} {m₀ m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} (c : ℝ) (X : Ω → ℝ),
  ProbabilityTheory.condVar m (c • X) μ =ᵐ[μ] c ^ 2 • ProbabilityTheory.condVar m X μ
-- Mathlib.MeasureTheory.Measure.Prod
/-- If `s ×ˢ t` is a null measurable set and `ν t ≠ 0`, then `s` is a null measurable set.  -/
MeasureTheory.NullMeasurableSet.left_of_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] {s : Set α} {t : Set β},
  MeasureTheory.NullMeasurableSet (s ×ˢ t) (μ.prod ν) → ν t ≠ 0 → MeasureTheory.NullMeasurableSet s μ
-- Mathlib.Data.Finset.Insert
Finset.singleton_subset_coe : ∀ {α : Type u_1} {s : Finset α} {a : α}, {a} ⊆ ↑s ↔ {a} ⊆ s
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.eraseIdx.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (x : ℕ) (h_1 : (x : ℕ) → motive [] x)
  (h_2 : (head : α) → (as : List α) → motive (head :: as) 0)
  (h_3 : (a : α) → (as : List α) → (n : ℕ) → motive (a :: as) n.succ),
  (match [], x with
    | [], x => h_1 x
    | head :: as, 0 => h_2 head as
    | a :: as, n.succ => h_3 a as n) =
    h_1 x
-- Init.Grind.Interactive
Lean.Parser.Tactic.Grind.grind_filter!_ : Lean.ParserDescr
-- Mathlib.Algebra.Group.Prod
MonoidHom.fst_comp_inr : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  (MonoidHom.fst M N).comp (MonoidHom.inr M N) = 1
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
intervalIntegral.FTCFilter.nhdsIcc : ∀ {x a b : ℝ} [h : Fact (x ∈ Set.Icc a b)],
  intervalIntegral.FTCFilter x (nhdsWithin x (Set.Icc a b)) (nhdsWithin x (Set.Icc a b))
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_inv_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Z : C}
  (f : Y ≅ Z) {Z_1 : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f.inv)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f.hom) h) =
    h
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- Similar to `ae_of_forall_measure_lt_top_ae_restrict`, but where you additionally get the
hypothesis that another σ-finite measure has finite values on `s`.  -/
MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (ν : MeasureTheory.Measure α)
  [MeasureTheory.SigmaFinite μ] [MeasureTheory.SigmaFinite ν] (P : α → Prop),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ν s < ⊤ → ∀ᵐ (x : α) ∂μ.restrict s, P x) → ∀ᵐ (x : α) ∂μ, P x
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updateReuseImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.LetValue pu →
    Lean.FVarId →
      Lean.Compiler.LCNF.CtorInfo → Bool → Array (Lean.Compiler.LCNF.Arg pu) → Lean.Compiler.LCNF.LetValue pu
-- Mathlib.Algebra.BigOperators.Finprod
MonoidHom.map_finprod_of_preimage_one : ∀ {M : Type u_2} {N : Type u_3} {α : Sort u_4} [inst : CommMonoid M] [inst_1 : CommMonoid N] (f : M →* N),
  (∀ (x : M), f x = 1 → x = 1) → ∀ (g : α → M), f (∏ᶠ (i : α), g i) = ∏ᶠ (i : α), f (g i)
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.mem_fixingSubgroup_iff : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (K : IntermediateField F E)
  (σ : Gal(E/F)), σ ∈ K.fixingSubgroup ↔ ∀ x ∈ K, σ x = x
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  (CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).f = T.mor₁
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.ae_sum_iff' : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} {μ : ι → MeasureTheory.Measure α} {p : α → Prop},
  MeasurableSet {x | p x} → ((∀ᵐ (x : α) ∂MeasureTheory.Measure.sum μ, p x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ i, p x)
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprod_inl_desc_f_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c}
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] {M : HomologicalComplex C c}
  (α : K ⟶ M) (β : L ⟶ M) (i : ι) {Z : C} (h : M.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.biprod.desc α β).f i) h) =
    CategoryTheory.CategoryStruct.comp (α.f i) h
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.map₂_associator_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(self.obj a)) {Z : ↑(self.obj d)}
  (h_1 :
    (self.map (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h))).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((self.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X)
      h_1 =
    CategoryTheory.CategoryStruct.comp ((self.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom.toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((self.map h).toFunctor.map ((self.mapComp f g).hom.toNatTrans.app X))
        (CategoryTheory.CategoryStruct.comp ((self.mapComp g h).inv.toNatTrans.app ((self.map f).toFunctor.obj X))
          (CategoryTheory.CategoryStruct.comp
            ((self.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv.toNatTrans.app X) h_1)))
-- Mathlib.Algebra.Group.Nat.Even
Nat.succ_mod_two_eq_one_iff : ∀ {m : ℕ}, (m + 1) % 2 = 1 ↔ m % 2 = 0
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.continuous_normAtAllPlaces : ∀ (K : Type u_1) [inst : Field K], Continuous NumberField.mixedEmbedding.normAtAllPlaces
-- Lean.Elab.DeclNameGen
/-- Elaborates the binders and type and then uses `mkBaseNameWithSuffix` to generate a name.
Furthermore, uses `mkUnusedBaseName` on the result.
 -/
Lean.Elab.Command.NameGen.mkBaseNameWithSuffix' : String → Array Lean.Syntax → Lean.Syntax → Lean.Elab.TermElabM Lean.Name
-- Init.Data.SInt.Bitwise
Int16.xor_self : ∀ {a : Int16}, a ^^^ a = 0
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.lift_omega0 : Ordinal.lift.{u_1, u_2} Ordinal.omega0 = Ordinal.omega0
-- Init.Data.SInt.Bitwise
Int8.or_eq_zero_iff : ∀ {a b : Int8}, a ||| b = 0 ↔ a = 0 ∧ b = 0
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitesimal_iff_infinite_inv : ∀ {x : ℝ*}, x ≠ 0 → (x.Infinitesimal ↔ x⁻¹.Infinite)
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
TopCat.Sheaf.interUnionPullbackCone_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} (F : TopCat.Sheaf C X)
  (U V : TopologicalSpace.Opens ↑X), (F.interUnionPullbackCone U V).snd = F.obj.map (CategoryTheory.homOfLE ⋯).op
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.findRev?.eq_1 : ∀ {α : Type} (p : α → Bool) (as : Array α), Array.findRev? p as = (Array.findRevM? (fun x => pure (p x)) as).run
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.piecewise : ∀ {α : Type u_1} {β : Type u_2} {l₁ : Filter α} {l₂ : Filter β} {f g : α → β} {s : Set α}
  [inst : (x : α) → Decidable (x ∈ s)],
  Filter.Tendsto f (l₁ ⊓ Filter.principal s) l₂ →
    Filter.Tendsto g (l₁ ⊓ Filter.principal sᶜ) l₂ → Filter.Tendsto (s.piecewise f g) l₁ l₂