mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Real.Embedding
Archimedean.embedRealFun_add : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [IsOrderedAddMonoid M] [inst_3 : One M]
  [ZeroLEOneClass M] [NeZero 1] [Archimedean M] (x y : M),
  Archimedean.embedRealFun (x + y) = Archimedean.embedRealFun x + Archimedean.embedRealFun y
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singleton_one : ∀ {α : Type u_2} [inst : One α], {1} = 1
-- Lean.Level
Lean.Level.max.injEq : ∀ (a a_1 a_2 a_3 : Lean.Level), (a.max a_1 = a_2.max a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Topology.Homotopy.TopCat.Basic
/-- The reverse of a homotopy `F` in `TopCat`.  -/
TopCat.Homotopy.symm : {X Y : TopCat} → {f₀ f₁ : X ⟶ Y} → TopCat.Homotopy f₀ f₁ → (TopCat.Hom.hom f₁).Homotopy (TopCat.Hom.hom f₀)
-- Init.Data.Int.Gcd
Int.gcd_eq_left_iff_dvd : ∀ {a b : ℤ}, 0 ≤ a → (↑(a.gcd b) = a ↔ a ∣ b)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₁₃_p₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃),
  CategoryTheory.CategoryStruct.comp h.p₁₃ h₁₃.p₂ = h.p₃
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.op_X₁ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} {X₂ : C₂}
  (L : Φ.LeftResolution X₂), L.op.X₁ = Opposite.op L.X₁
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.ofLinearEquiv_apply : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsAdicComplete I M] (x : M), (AdicCompletion.ofLinearEquiv I M) x = (AdicCompletion.of I M) x
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobjectMap_arrow : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X}
  [inst_1 : CategoryTheory.Limits.HasImage f] {g : Y ⟶ Z} [inst_2 : CategoryTheory.Limits.HasImage g]
  (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) [inst_3 : CategoryTheory.Limits.HasImageMap sq],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectMap sq)
      (CategoryTheory.Limits.imageSubobject g).arrow =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow
      (CategoryTheory.Arrow.Hom.right sq)
-- Mathlib.NumberTheory.Pell
/-- When `d` is negative, then `x` or `y` must be zero in a solution.  -/
Pell.Solution₁.eq_zero_of_d_neg : ∀ {d : ℤ}, d < 0 → ∀ (a : Pell.Solution₁ d), a.x = 0 ∨ a.y = 0
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.restrict_id : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.PartialMap Y), f.restrict f.domain ⋯ ⋯ = f
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.morphismRestrict_homOfLE_isoImage_ι_hom_assoc : ∀ {X : AlgebraicGeometry.Scheme} {U V : X.Opens} (e : U ≤ V) (W : TopologicalSpace.Opens ↥↑V)
  {Z : AlgebraicGeometry.Scheme} (h : ↑((AlgebraicGeometry.Scheme.Hom.opensFunctor V.ι).obj W) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.homOfLE e ∣_ W)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoImage V.ι W).hom h) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.isoImage U.ι ((TopologicalSpace.Opens.map (X.homOfLE e).base).obj W)).hom
      (CategoryTheory.CategoryStruct.comp (X.homOfLE ⋯) h)
-- Mathlib.Data.List.Cycle
Cycle.length_coe : ∀ {α : Type u_1} (l : List α), (↑l).length = l.length
-- Mathlib.CategoryTheory.Equivalence
/-- Promote a natural transformation `e.functor ⟶ f.functor` to a morphism in `C ≌ D`.  -/
CategoryTheory.Equivalence.mkHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → {e f : C ≌ D} → (e.functor ⟶ f.functor) → (e ⟶ f)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.unitInv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D), e.unitInv = e.unitIso.inv
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.of_mul_right : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {a b c d : M},
  Associated (a * b) (c * d) → Associated b d → b ≠ 0 → Associated a c
-- Init.Data.Range.Polymorphic.NatLemmas
/-- Induction principle for proving properties of `Nat`-based ranges of the form `a<...=b`
by varying the lower bound.

In the `base` case, one proves that for any `a : Nat` and `b : Nat` with
`b ≤ a`, the statement holds for the empty range `a<...=b`.

In the `step` case, one proves that for any `a : Nat` and `b : Nat`, the
statement holds for nonempty ranges `a<...=b` if it holds for the smaller range
`(a + 1)<...=b`.

The following is an example reproving `length_toList_roc`.

```
example (a b : Nat) : (a<...=b).toList.length = b - a := by
  induction a, b using Nat.induct_roc_left
  case base =>
    simp only [Nat.toList_roc_eq_nil, List.length_nil, *]; omega
  case step =>
    simp only [Nat.toList_roc_eq_cons, List.length_cons, *]; omega
``` -/
Nat.induct_roc_left : ∀ (motive : ℕ → ℕ → Prop),
  (∀ (a b : ℕ), b ≤ a → motive a b) → (∀ (a b : ℕ), a < b → motive (a + 1) b → motive a b) → ∀ (a b : ℕ), motive a b
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.exists_fixed_point_of_prime : ∀ {α : Type u_1} [inst : Fintype α] {p n : ℕ} [hp : Fact (Nat.Prime p)],
  ¬p ∣ Fintype.card α → ∀ {σ : Equiv.Perm α}, σ ^ p ^ n = 1 → ∃ a, σ a = a
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.eRank_one : ∀ {m : Type um} {R : Type uR} [inst : Semiring R] [Nontrivial R] [inst_2 : DecidableEq m] [StrongRankCondition R],
  Matrix.eRank 1 = ENat.card m
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
MeasureTheory.AEStronglyMeasurable.integral_kernel_compProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  [inst_3 : NormedSpace ℝ E] ⦃f : β × γ → E⦄,
  MeasureTheory.AEStronglyMeasurable f ((κ.compProd η) a) →
    MeasureTheory.AEStronglyMeasurable (fun x => ∫ (y : γ), f (x, y) ∂η (a, x)) (κ a)
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
/-- `List.tail` as a `Products`.  -/
Profinite.NobelingProof.Products.Tail : {I : Type u} → [inst : LinearOrder I] → Profinite.NobelingProof.Products I → Profinite.NobelingProof.Products I
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
/-- A pullback cone `c` in the category of types is limit iff the
map `c.toPullbackObj : c.pt → Types.PullbackObj f g` is a bijection.  -/
CategoryTheory.Limits.PullbackCone.isLimitEquivBijective : {X Y S : Type v} →
  {f : X ⟶ S} →
    {g : Y ⟶ S} →
      (c : CategoryTheory.Limits.PullbackCone f g) →
        CategoryTheory.Limits.IsLimit c ≃ Function.Bijective c.toPullbackObj
-- Mathlib.Topology.Algebra.Group.Basic
continuous_zpow : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] (z : ℤ), Continuous fun a => a ^ z
-- Mathlib.Order.UpperLower.Closure
/-- `lowerClosure` forms a Galois insertion with the coercion from lower sets to sets.  -/
giLowerClosureCoe : {α : Type u_1} → [inst : Preorder α] → GaloisInsertion lowerClosure SetLike.coe
-- Mathlib.FieldTheory.KummerExtension
rootsOfUnity.mkOfPowEq.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] (ζ : M) {n : ℕ} [inst_1 : NeZero n] (h : ζ ^ n = 1),
  rootsOfUnity.mkOfPowEq ζ h = ⟨Units.ofPowEqOne ζ n h ⋯, ⋯⟩
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.instMonoι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData), CategoryTheory.Mono h.ι
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_le_ediv_iff_of_dvd_of_pos_of_pos : ∀ {a b c d : ℤ}, 0 < b → 0 < d → b ∣ a → d ∣ c → (a / b ≤ c / d ↔ d * a ≤ c * b)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.instInhabitedNormalExpr.default : Mathlib.Tactic.BicategoryLike.NormalExpr
-- Lean.Meta.Tactic.FVarSubst
/-- Given `e`, for each `(x => v)` in `s` replace `x` with `v` in `e`  -/
Lean.Meta.FVarSubst.apply : Lean.Meta.FVarSubst → Lean.Expr → Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.not_nil_iff_lt_length : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w}, ¬p.Nil ↔ 0 < p.length
-- Plausible.Gen
_private.Plausible.Gen.0.Plausible.Gen.runUntil.repeatGen : {α : Type} → Option ℕ → Plausible.Gen α → Plausible.Gen α
-- Mathlib.Order.Partition.Finpartition
Finpartition.empty_notMem_parts : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s), ∅ ∉ P.parts
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
AddSubgroup.zmultiples.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (g : G),
  AddSubgroup.zmultiples g = { carrier := Set.range fun x => x • g, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.SemiCartesianMonoidalCategory.toUnit_unique_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory C]
  {X : C} {f g : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C}, f = g ↔ True
-- Mathlib.Analysis.Calculus.FDeriv.Affine
ContinuousAffineMap.fderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E →ᴬ[𝕜] F)
  {x : E}, fderiv 𝕜 (⇑f) x = f.contLinear
-- Mathlib.Probability.UniformOn
/-- The uniform measure on a product of sets is the product of the uniform measures.  -/
ProbabilityTheory.uniformOn_pi : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [MeasurableSingletonClass Ω] {ι : Type u_2} [inst_2 : Fintype ι] [Finite Ω]
  {f : ι → Set Ω},
  ProbabilityTheory.uniformOn (Set.univ.pi f) = MeasureTheory.Measure.pi fun i => ProbabilityTheory.uniformOn (f i)
-- Mathlib.Algebra.Group.EvenFunction
Function.Even.smul_even : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg α] {γ : Type u_3} {f : α → β} {g : α → γ} [inst_1 : SMul β γ],
  Function.Even f → Function.Even g → Function.Even (f • g)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.restrictVar.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] (a : α)
  (f : ↥(FirstOrder.Language.var a).varFinset → β),
  (FirstOrder.Language.var a).restrictVar f = FirstOrder.Language.var (f ⟨a, ⋯⟩)
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (U : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  (F : CategoryTheory.Functor C V)
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution U F] (x : C),
  (CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor U F).inv.app x =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj x)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.DayConvolutionUnit.can
          (F.obj x))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.MonoidalCategory.DayConvolution.unit U F).app
            (CategoryTheory.MonoidalCategoryStruct.tensorUnit C, x))
          ((CategoryTheory.MonoidalCategory.DayConvolution.convolution U F).map
            (CategoryTheory.MonoidalCategoryStruct.leftUnitor x).hom)))
-- Mathlib.Algebra.Algebra.Hom.Rat
RingEquiv.equivRatAlgEquiv_apply : ∀ (R : Type u_1) (S : Type u_2) [inst : Ring R] [inst_1 : Ring S] [inst_2 : Algebra ℚ R] [inst_3 : Algebra ℚ S]
  (f : R ≃+* S), (RingEquiv.equivRatAlgEquiv R S) f = f.toRatAlgEquiv
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.ordered_prependMap_done : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β}
  {ord_t : t.Ordered}, (Std.DTreeMap.Internal.Zipper.prependMap t Std.DTreeMap.Internal.Zipper.done).Ordered
-- Mathlib.Probability.Decision.BayesEstimator
ProbabilityTheory.HasArgminEstimator.isArgminEstimator_argminEstimator : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ}
  [inst : StandardBorelSpace Θ] [inst_1 : Nonempty Θ] [inst_2 : ProbabilityTheory.IsFiniteKernel P]
  [inst_3 : MeasureTheory.IsFiniteMeasure π] (h : ProbabilityTheory.HasArgminEstimator ℓ P π),
  ProbabilityTheory.IsArgminEstimator ℓ P π h.argminEstimator
-- Mathlib.Data.Finset.Sups
Finset.diffs_compls_eq_infs : ∀ {α : Type u_2} [inst : BooleanAlgebra α] [inst_1 : DecidableEq α] (s t : Finset α), s.diffs t.compls = s ⊼ t
-- Mathlib.Algebra.Module.Equiv.Basic
/-- An equivalence whose underlying function is linear is a linear equivalence.  -/
Equiv.toLinearEquiv : {R : Type u_1} →
  {M : Type u_5} →
    {M₂ : Type u_7} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommMonoid M₂] → [inst_4 : Module R M₂] → (e : M ≃ M₂) → IsLinearMap R ⇑e → M ≃ₗ[R] M₂
-- Mathlib.Topology.UniformSpace.Defs
/-- Defining a `UniformSpace.Core` from a filter basis satisfying some uniformity-like axioms.  -/
UniformSpace.Core.mkOfBasis : {α : Type u} →
  (B : FilterBasis (α × α)) →
    (∀ r ∈ B, ∀ (x : α), (x, x) ∈ r) →
      (∀ r ∈ B, ∃ t ∈ B, t ⊆ Prod.swap ⁻¹' r) → (∀ r ∈ B, ∃ t ∈ B, SetRel.comp t t ⊆ r) → UniformSpace.Core α
-- Lean.Widget.InteractiveCode
Lean.Widget.SubexprInfo.mk : Lean.Server.WithRpcRef Lean.Elab.InfoWithCtx → Lean.SubExpr.Pos → Option Lean.Widget.DiffTag → Lean.Widget.SubexprInfo
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.AndKind.ofNat_ctorIdx : ∀ (x : Mathlib.Tactic.ITauto.AndKind), Mathlib.Tactic.ITauto.AndKind.ofNat x.ctorIdx = x
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.Kind.noConfusionType : Sort v✝ → Mathlib.Tactic.Widget.StringDiagram.Kind → Mathlib.Tactic.Widget.StringDiagram.Kind → Sort v✝
-- Mathlib.CategoryTheory.Category.Bipointed
/-- The free/forgetful adjunction between `PointedToBipointed_fst` and `BipointedToPointed_fst`.
 -/
pointedToBipointedFstBipointedToPointedFstAdjunction : pointedToBipointedFst ⊣ bipointedToPointedFst
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_diff : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  (t₁ \ t₂).get! k = if k ∈ t₂ then default else t₁.get! k
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
ENNReal.continuous_log : Continuous ENNReal.log
-- Lean.Meta.Basic
/-- Append an array of free variables `xs` to the local context and execute `k xs`.
`declInfos` takes the form of an array consisting of:
- the name of the variable
- the binder info of the variable
- a type constructor for the variable, where the array consists of all of the free variables
  defined prior to this one. This is needed because the type of the variable may depend on prior variables.

See `withLocalDeclsD` and `withLocalDeclsDND` for simpler variants.
 -/
Lean.Meta.withLocalDecls : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] →
      {α : Type} →
        [Inhabited α] →
          Array (Lean.Name × Lean.BinderInfo × (Array Lean.Expr → n Lean.Expr)) →
            (Array Lean.Expr → n α) → optParam Lean.LocalDeclKind Lean.LocalDeclKind.default → n α
-- Init.Data.Bool
Bool.not_inj : ∀ {x y : Bool}, (!x) = !y → x = y
-- Mathlib.Analysis.Normed.Group.Quotient
NormedAddGroupHom.IsQuotient.mk : ∀ {M : Type u_1} {N : Type u_2} [inst : SeminormedAddCommGroup M] [inst_1 : SeminormedAddCommGroup N]
  {f : NormedAddGroupHom M N},
  Function.Surjective ⇑f → (∀ (x : M), ‖f x‖ = sInf ((fun m => ‖x + m‖) '' ↑f.ker)) → f.IsQuotient
-- Lean.Data.AssocList
Lean.AssocList.erase : {α : Type u} → {β : Type v} → [BEq α] → α → Lean.AssocList α β → Lean.AssocList α β
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.mk.congr_simp : ∀ {Ω : Type u_1} {ι : Type u_2} [inst : Preorder ι] {m : MeasurableSpace Ω} (seq seq_1 : ι → MeasurableSpace Ω)
  (e_seq : seq = seq_1) (mono' : Monotone seq) (le' : ∀ (i : ι), seq i ≤ m),
  { seq := seq, mono' := mono', le' := le' } = { seq := seq_1, mono' := ⋯, le' := ⋯ }
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.canonicalEquiv_def : ∀ {R : Type u_5} [inst : CommRing R] (S : Submonoid R) (P : Type u_6) [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (P' : Type u_7) [inst_3 : CommRing P'] [inst_4 : Algebra R P'] [inst_5 : IsLocalization S P]
  [inst_6 : IsLocalization S P'],
  FractionalIdeal.canonicalEquiv S P P' =
    FractionalIdeal.mapEquiv
      (let __src := IsLocalization.ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯;
      { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ })
-- Mathlib.Algebra.Group.Hom.Defs
/-- `MulHom` is a type of multiplication-preserving homomorphisms  -/
MulHom.mulHomClass : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N], MulHomClass (M →ₙ* N) M N
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {f : α → β → Bool} {k : α} (h : t.WF),
  (Std.TreeMap.Raw.filter f t).getKey! k = ((t.getKey? k).pfilter fun x h' => f x t[x]).get!
-- Mathlib.Data.Finset.NAry
Finset.image₂_union_left : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {s s' : Finset α} {t : Finset β}
  [inst_1 : DecidableEq α], Finset.image₂ f (s ∪ s') t = Finset.image₂ f s t ∪ Finset.image₂ f s' t
-- Std.Sync.Channel
/-- Try to send a value to the channel. If this can be completed right away without blocking return
`true`; otherwise, don't send the value and return `false`.
 -/
Std.CloseableChannel.Sync.trySend : {α : Type} → Std.CloseableChannel.Sync α → α → BaseIO Bool
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.embDomain_one : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : PartialOrder Γ] {Γ' : Type u_6}
  [inst_2 : AddCommMonoid Γ'] [inst_3 : PartialOrder Γ'] [inst_4 : NonAssocSemiring R] (f : Γ ↪o Γ'),
  f 0 = 0 → HahnSeries.embDomain f 1 = 1
-- Mathlib.NumberTheory.FLT.Four
/-- Fermat's Last Theorem for $n=4$: if `a b c : ℕ` are all non-zero
then `a ^ 4 + b ^ 4 ≠ c ^ 4`.
 -/
fermatLastTheoremFour : FermatLastTheoremFor 4
-- Mathlib.Order.Interval.Set.Image
StrictMono.mapsTo_Iio : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {b : α},
  StrictMono f → Set.MapsTo f (Set.Iio b) (Set.Iio (f b))
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.tsupport_fderivCLM_subset : ∀ (𝕜 : Type u_2) {E : Type u_5} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace ℝ F] [inst_3 : RCLike 𝕜] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedSpace ℝ E]
  [inst_6 : SMulCommClass ℝ 𝕜 F] (f : SchwartzMap E F), tsupport ⇑((SchwartzMap.fderivCLM 𝕜 E F) f) ⊆ tsupport ⇑f
-- Mathlib.Algebra.Homology.Embedding.IsSupported
/-- If `K : HomologicalComplex C c'`, then `K.IsStrictlySupported e` holds for
an embedding `e : c.Embedding c'` of complex shapes if `K` is exact at `i'`
whenever `i'` is not of the form `e.f i` for some `i`.  -/
HomologicalComplex.IsSupported : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → HomologicalComplex C c' → c.Embedding c' → Prop
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.prod_eq_prod_fintype : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : (i : ι) → Zero (β i)]
  [inst_3 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_4 : CommMonoid γ] (v : Π₀ (i : ι), β i)
  {f : (i : ι) → β i → γ}, (∀ (i : ι), f i 0 = 1) → v.prod f = ∏ i, f i (DFinsupp.equivFunOnFintype v i)
-- Init.Data.UInt.Bitwise
UInt8.zero_and : ∀ {a : UInt8}, 0 &&& a = 0
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- If `R'` (resp. `S'`) is the localization of `R` (resp. `S`) and
`P` lies over `p` then the image of `P` in `S'` lies over the image of `p` in `R'`.  -/
IsLocalization.liesOver_of_isPrime_of_disjoint : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_4} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {R' : Type u_5}
  {S' : Type u_6} (M : Submonoid R) (T : Submonoid S) [inst_3 : CommSemiring R'] [inst_4 : CommSemiring S']
  [inst_5 : Algebra R R'] [inst_6 : Algebra S S'] [inst_7 : Algebra R' S'] [inst_8 : Algebra R S']
  [IsScalarTower R S S'] [IsScalarTower R R' S'] [IsLocalization M R'] [IsLocalization T S'] (p : Ideal R) {P : Ideal S}
  [P.IsPrime] [P.LiesOver p], Disjoint ↑T ↑P → (Ideal.map (algebraMap S S') P).LiesOver (Ideal.map (algebraMap R R') p)
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.Seq.startsWith.match_1.eq_3 : ∀ (motive : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq → Sort u_1) (x : Lean.Grind.AC.Var) (s : Lean.Grind.AC.Seq)
  (x_1 : Lean.Grind.AC.Var)
  (h_1 : (x y : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.var x) (Lean.Grind.AC.Seq.var y))
  (h_2 :
    (x y : Lean.Grind.AC.Var) → (s : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.var x) (Lean.Grind.AC.Seq.cons y s))
  (h_3 :
    (x : Lean.Grind.AC.Var) →
      (s : Lean.Grind.AC.Seq) →
        (x_2 : Lean.Grind.AC.Var) → motive (Lean.Grind.AC.Seq.cons x s) (Lean.Grind.AC.Seq.var x_2))
  (h_4 :
    (x : Lean.Grind.AC.Var) →
      (s₂ : Lean.Grind.AC.Seq) →
        (y : Lean.Grind.AC.Var) →
          (s₁ : Lean.Grind.AC.Seq) → motive (Lean.Grind.AC.Seq.cons x s₂) (Lean.Grind.AC.Seq.cons y s₁)),
  (match Lean.Grind.AC.Seq.cons x s, Lean.Grind.AC.Seq.var x_1 with
    | Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.var y => h_1 x y
    | Lean.Grind.AC.Seq.var x, Lean.Grind.AC.Seq.cons y s => h_2 x y s
    | Lean.Grind.AC.Seq.cons x s, Lean.Grind.AC.Seq.var x_2 => h_3 x s x_2
    | Lean.Grind.AC.Seq.cons x s₂, Lean.Grind.AC.Seq.cons y s₁ => h_4 x s₂ y s₁) =
    h_3 x s x_1
-- Init.Data.String.Lemmas.TakeDrop
String.takeEnd_toSlice : ∀ {s : String} {n : ℕ}, s.toSlice.takeEnd n = s.takeEnd n
-- Mathlib.Data.Num.Basic
/-- `bitm1 x` appends a `1` to the end of `x`, mapping `x` to `2 * x - 1`.  -/
ZNum.bitm1 : ZNum → ZNum
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.OfInvertibleFactorial.dpow_eq_of_mem : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] {m : ℕ} {x : A},
  x ∈ I → DividedPowers.OfInvertibleFactorial.dpow I m x = Ring.inverse ↑m.factorial * x ^ m
-- Mathlib.Data.List.Destutter
List.destutter'_cons : ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] {a b : α},
  List.destutter' R a (b :: l) = if R a b then a :: List.destutter' R b l else List.destutter' R a l