mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Constructions.NoConfusion
/-- Given arrays `x1,x2,..,xn` and `y1,y2,..,yn`, bring fresh variables and expressions of types `x1 = y1`, `x2 = y2`,
.., `xn = yn` (using `HEq` where necessary) into scope.
 -/
_private.Lean.Meta.Constructions.NoConfusion.0.Lean.withEqTelescope : {α : Type} → [Inhabited α] → Array Lean.Expr → Array Lean.Expr → (Array Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.RingTheory.Algebraic.Denominator
IsAlgebraic.natDenominator_ne_zero : ∀ {S : Type u_2} [inst : CommRing S] {x : S}, IsAlgebraic ℤ x → Algebra.natDenominator x ≠ 0
-- Lean.Data.Json.FromToJson.Basic
Lean.instToJsonBool : Lean.ToJson Bool
-- Mathlib.Analysis.Meromorphic.Basic
/-- `MeromorphicOn` is invariant under translation.  -/
MeromorphicOn.meromorphicOn_comp_add_const_iff_meromorphicOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {c : 𝕜} {U : Set 𝕜},
  MeromorphicOn (f ∘ fun x => x + c) U ↔ MeromorphicOn f (U + {c})
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- **Alias** of `Matroid.IsBasis.sdiff_subset_loops_contract`. -/
Matroid.IsBasis.diff_subset_loops_contract : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → X \ I ⊆ (M.contract I).loops
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.eq_toIterM_iter : ∀ {α : Type u} {β : α → Type v} (it : Std.IterM Id ((a : α) × β a)), it = it.internalState.iter.toIterM
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.associator_inv_naturality_left : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h))
      (CategoryTheory.Bicategory.associator f' g h).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison'_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData)
  [inst_2 : CategoryTheory.IsIso (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)],
  (CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison' h₁ h₂).right = h₂
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_prod`. -/
EMetric.infEdist_prod : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (x : α × β) (s : Set α)
  (t : Set β), Metric.infEDist x (s ×ˢ t) = max (Metric.infEDist x.1 s) (Metric.infEDist x.2 t)
-- Init.Data.BitVec.Lemmas
BitVec.neg_add : ∀ {w : ℕ} {x y : BitVec w}, -(x + y) = -x - y
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.linearIndependent_single_one : ∀ (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} [inst : DecidableEq ι] [inst_1 : Ring 𝕜],
  LinearIndependent 𝕜 fun i => PiLp.single p i 1
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.sub_left : ∀ {n a b c : ℕ}, b ≤ a → c ≤ a → b ≡ c [MOD n] → a - b ≡ a - c [MOD n]
-- Init.Data.Array.Lemmas
Array.empty_eq : ∀ {α : Type u_1} {xs : Array α}, #[] = xs ↔ xs = #[]
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimit.fac : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes}
  (hc : c.IsColimit) (c' : F.CoconeTypes) (j : J), hc.desc c' ∘ c.ι j = c'.ι j
-- Qq.Delab
_private.Qq.Delab.0.Qq.Impl.failureOnError : {α : Type} → Lean.MetaM α → Lean.PrettyPrinter.Delaborator.DelabM α
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.quasiIso_iff_of_arrow_mk_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ S₄ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology]
  [inst_4 : S₃.HasHomology] [inst_5 : S₄.HasHomology] (φ : S₁ ⟶ S₂) (φ' : S₃ ⟶ S₄)
  (e : CategoryTheory.Arrow.mk φ ≅ CategoryTheory.Arrow.mk φ'),
  CategoryTheory.ShortComplex.QuasiIso φ ↔ CategoryTheory.ShortComplex.QuasiIso φ'
-- Mathlib.Data.List.MinMax
List.not_maximum_lt_of_mem : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLT α] {l : List α} {a m : α}, a ∈ l → l.maximum = ↑m → ¬m < a
-- Mathlib.LinearAlgebra.Matrix.Stochastic
Matrix.colStochastic.congr_simp : ∀ (R : Type u_3) (n : Type u_4) [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R], Matrix.colStochastic R n = Matrix.colStochastic R n
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Finsupp.logb_prod : ∀ {b : ℝ} {α : Type u_1} {β : Type u_2} [inst : Zero β] (f : α →₀ β) (g : α → β → ℝ),
  (∀ (a : α), g a (f a) = 0 → f a = 0) → Real.logb b (f.prod g) = f.sum fun a c => Real.logb b (g a c)
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape.inverseImage : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : Type u') [inst_2 : CategoryTheory.Category.{v', u'} J]
  (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) [P.IsClosedUnderLimitsOfShape J]
  [CategoryTheory.Limits.PreservesLimitsOfShape J F], (P.inverseImage F).IsClosedUnderLimitsOfShape J
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.setIntegral_measure_zero : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  (f : α → G) {μ : MeasureTheory.Measure α} {s : Set α}, μ s = 0 → ∫ (x : α) in s, f x ∂μ = 0
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.compMeasurePreserving.congr_simp : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {β : Type u_7} [inst_1 : MeasurableSpace β] {μb : MeasureTheory.Measure β}
  (f f_1 : α → β) (e_f : f = f_1) (hf : MeasureTheory.MeasurePreserving f μ μb),
  MeasureTheory.Lp.compMeasurePreserving f hf = MeasureTheory.Lp.compMeasurePreserving f_1 ⋯
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.instIsMonHomWhiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y Z : C} [inst_3 : CategoryTheory.MonObj X]
  [inst_4 : CategoryTheory.MonObj Y] [inst_5 : CategoryTheory.MonObj Z] {f : X ⟶ Y} [CategoryTheory.IsMonHom f],
  CategoryTheory.IsMonHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.endsWith_slice_eq_false_iff : ∀ {pat s : String.Slice}, s.endsWith pat = false ↔ ¬pat.copy.toList <:+ s.copy.toList
-- Mathlib.Analysis.Normed.Operator.NormedSpace
/-- An operator is zero iff its norm vanishes.  -/
ContinuousLinearMap.opNorm_zero_iff : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [RingHomIsometric σ₁₂],
  ‖f‖ = 0 ↔ f = 0
-- Init.Data.List.Lemmas
List.flatten_replicate_nil : ∀ {n : ℕ} {α : Type u_1}, (List.replicate n []).flatten = []
-- Mathlib.Algebra.Module.StablyFree.Basic
Module.IsStablyFree.equiv : ∀ {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] (e : M ≃ₗ[R] N) [Module.IsStablyFree R M], Module.IsStablyFree R N
-- Lean.Data.Trie
Lean.Data.Trie.node.inj : ∀ {α : Type} {a : Option α} {a_1 : ByteArray} {a_2 : Array (Lean.Data.Trie α)} {a_3 : Option α} {a_4 : ByteArray}
  {a_5 : Array (Lean.Data.Trie α)},
  Lean.Data.Trie.node a a_1 a_2 = Lean.Data.Trie.node a_3 a_4 a_5 → a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.map₂_span_singleton_eq_map : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : M →ₗ[R] N →ₗ[R] P) (m : M), Submodule.map₂ f (R ∙ m) = Submodule.map (f m)
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
/-- Pull back a term of `Meq P S` with respect to a morphism `f : Y ⟶ X` in `C`.  -/
CategoryTheory.Meq.pullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          {FD : D → D → Type u_1} →
            {CD : D → Type t} →
              [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
                [inst_3 : CategoryTheory.ConcreteCategory D FD] →
                  {Y X : C} →
                    {P : CategoryTheory.Functor Cᵒᵖ D} →
                      {S : J.Cover X} →
                        CategoryTheory.Meq P S → (f : Y ⟶ X) → CategoryTheory.Meq P ((J.pullback f).obj S)
-- Init.Prelude
/-- Mutates the current state that has the explicitly-provided type `σ`, replacing its value with the
result of applying `f` to it. When the current monad has multiple state types available, this
function selects one of them.

It is equivalent to `do set (f (← get))`. However, using `modify` may lead to higher performance
because it doesn't add a new reference to the state value. Additional references can inhibit
in-place updates of data.
 -/
modifyThe : (σ : Type u) → {m : Type u → Type v} → [MonadStateOf σ m] → (σ → σ) → m PUnit.{u + 1}
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
/-- The space of affine maps to a module inherits an `R`-action from the action on its codomain.  -/
AffineMap.distribMulAction : {R : Type u_1} →
  {k : Type u_2} →
    {V1 : Type u_3} →
      {P1 : Type u_4} →
        {V2 : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V1] →
              [inst_2 : AddTorsor V1 P1] →
                [inst_3 : AddCommGroup V2] →
                  [inst_4 : Module k V1] →
                    [inst_5 : Module k V2] →
                      [inst_6 : Monoid R] →
                        [inst_7 : DistribMulAction R V2] → [SMulCommClass k R V2] → DistribMulAction R (P1 →ᵃ[k] V2)
-- Mathlib.Topology.FiberBundle.Constructions
instMemTrivializationAtlasProdProd : ∀ {B : Type u_1} [inst : TopologicalSpace B] (F₁ : Type u_2) [inst_1 : TopologicalSpace F₁] (E₁ : B → Type u_3)
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] (F₂ : Type u_4) [inst_3 : TopologicalSpace F₂]
  (E₂ : B → Type u_5) [inst_4 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_5 : (x : B) → Zero (E₁ x)]
  [inst_6 : (x : B) → Zero (E₂ x)] [inst_7 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_8 : (x : B) → TopologicalSpace (E₂ x)] [inst_9 : FiberBundle F₁ E₁] [inst_10 : FiberBundle F₂ E₂]
  {e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj}
  [MemTrivializationAtlas e₁] [MemTrivializationAtlas e₂], MemTrivializationAtlas (e₁.prod e₂)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.map_inf : ∀ {F : Type w} {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S]
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (s t : NonUnitalSubring R) (f : F),
  Function.Injective ⇑f → NonUnitalSubring.map f (s ⊓ t) = NonUnitalSubring.map f s ⊓ NonUnitalSubring.map f t
-- Mathlib.RingTheory.Finiteness.Quotient
/-- `B ⧸ P` is a finitely generated `A ⧸ p`-algebra if `B` is a finitely generated `A`-algebra.  -/
algebra_finiteType_of_liesOver : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (P : Ideal B)
  (p : Ideal A) [inst_3 : P.LiesOver p] [Algebra.FiniteType A B], Algebra.FiniteType (A ⧸ p) (B ⧸ P)
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.mapDomainAlgHom.eq_1 : ∀ (R : Type u_1) (A : Type u_4) {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddMonoid M] [inst_4 : AddMonoid N] (f : M →+ N),
  AddMonoidAlgebra.mapDomainAlgHom R A f = { toRingHom := AddMonoidAlgebra.mapDomainRingHom A f, commutes' := ⋯ }
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.leftDerived_ext : ∀ {C : Type u_3} {D : Type u_1} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_1} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (LF : CategoryTheory.Functor D H) {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : L.comp LF ⟶ F) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [LF.IsLeftDerivedFunctor α W] (G : CategoryTheory.Functor D H) (γ₁ γ₂ : G ⟶ LF),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft γ₁) α = CategoryTheory.CategoryStruct.comp (L.whiskerLeft γ₂) α →
    γ₁ = γ₂
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
Contravariant.toAddRightCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddSemigroup α] [inst_1 : PartialOrder α] [inst_2 : AddRightReflectLE α],
  Contravariant.toAddRightCancelSemigroup = { toAddSemigroup := inst, toIsRightCancelAdd := ⋯ }
-- Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
MvPowerSeries.X_mem_nonzeroDivisors : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {i : σ}, MvPowerSeries.X i ∈ nonZeroDivisors (MvPowerSeries σ R)
-- Mathlib.Algebra.Free
FreeAddMagma.instMonad.eq_1 : FreeAddMagma.instMonad =
  { map := fun {α β} f x => (fun {α β} x f => (FreeAddMagma.lift f) x) x ((fun {α} => FreeAddMagma.of) ∘ f),
    pure := fun {α} => FreeAddMagma.of,
    seq := fun {α β} f x =>
      (fun {α β} x f => (FreeAddMagma.lift f) x) f fun y =>
        (fun {α β} x f => (FreeAddMagma.lift f) x) (x ()) ((fun {α} => FreeAddMagma.of) ∘ y),
    seqLeft := fun {α β} x y =>
      (fun {α β} x f => (FreeAddMagma.lift f) x) x fun a =>
        (fun {α β} x f => (FreeAddMagma.lift f) x) (y ()) fun x => (fun {α} => FreeAddMagma.of) a,
    seqRight := fun {α β} x y => (fun {α β} x f => (FreeAddMagma.lift f) x) x fun x => y (),
    bind := fun {α β} x f => (FreeAddMagma.lift f) x }
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_univ : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  (v : MeasureTheory.VectorMeasure α M), v.restrict Set.univ = v
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_le_ediv_iff_of_dvd_of_neg_of_pos : ∀ {a b c d : ℤ}, b < 0 → 0 < d → b ∣ a → d ∣ c → (a / b ≤ c / d ↔ c * b ≤ d * a)
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Functoriality
ContinuousCohomology.cochainsMap_comp_assoc : ∀ {k : Type u} {G H K : Type v} [inst : Ring k] [inst_1 : TopologicalSpace k] [inst_2 : Group G]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] [inst_5 : Group H] [inst_6 : TopologicalSpace H]
  [inst_7 : IsTopologicalGroup H] [inst_8 : Group K] [inst_9 : TopologicalSpace K] [inst_10 : IsTopologicalGroup K]
  {X : TopRep k G} {Y : TopRep k H} {Z : TopRep k K} (φ : H →ₜ* G) (ψ : K →ₜ* H) (f : TopRep.res (↑φ) X ⟶ Y)
  (g : TopRep.res (↑ψ) Y ⟶ Z) {Z_1 : CochainComplex (TopModuleCat k) ℕ} (h : Z.homogeneousCochains ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (ContinuousCohomology.cochainsMap (φ.comp ψ)
        (CategoryTheory.CategoryStruct.comp (TopRep.ofHom (ContIntertwiningMap.restrict (↑ψ) (TopRep.Hom.hom f))) g))
      h =
    CategoryTheory.CategoryStruct.comp (ContinuousCohomology.cochainsMap φ f)
      (CategoryTheory.CategoryStruct.comp (ContinuousCohomology.cochainsMap ψ g) h)
-- Batteries.Data.List.Perm
List.Perm.idxBij_symm_rightInverse_idxBij : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs ys : List α} (h : xs.Perm ys),
  Function.RightInverse ⋯.idxBij h.idxBij
-- Mathlib.NumberTheory.Height.Basic
/-- The logarithmic height of a product of field elements is bounded above by the sum
of their logarithmic heights.  -/
Height.logHeight₁_prod_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} (s : Finset ι) (x : ι → K),
  Height.logHeight₁ (∏ i ∈ s, x i) ≤ ∑ i ∈ s, Height.logHeight₁ (x i)
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.unpack_eq_zero_iff_of_valid : ∀ {spec : Float.Model.Format} {sign : Float.Model.UnpackedFloat.Sign} {b : BitVec spec.numBits},
  spec.Valid b →
    autoParam (2 ≤ spec.exponentBits) Float.Model.UnpackedFloat.unpack_eq_zero_iff_of_valid._auto_1 →
      (Float.Model.UnpackedFloat.unpack spec b = Float.Model.UnpackedFloat.zero sign ↔
        b = Float.Model.UnpackedFloat.packedZero spec sign)
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xn_modEq_x4n_add : ∀ {a : ℕ} (a1 : 1 < a) (n j : ℕ), Pell.xn a1 (4 * n + j) ≡ Pell.xn a1 j [MOD Pell.xn a1 n]
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity_inv_app : ∀ (X : CommRingCat), AlgebraicGeometry.LocallyRingedSpace.SpecΓIdentity.inv.app X = AlgebraicGeometry.toSpecΓ X
-- Mathlib.Order.InitialSeg
InitialSeg.monotone : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] [inst_1 : PartialOrder α] (f : α ≤i β), Monotone ⇑f
-- Mathlib.Data.Option.Basic
Option.map_coe : ∀ {α β : Type u_5} {a : α} {f : α → β}, f <$> some a = some (f a)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instMonoidCoeOfSubmonoidClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → Monoid (R i)] →
              [∀ (i : ι), SubmonoidClass (S i) (R i)] → Monoid (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.mk.congr_simp : ∀ {G : Type u_6} [inst : Group G] (toFun toFun_1 : G → ℝ) (e_toFun : toFun = toFun_1) (map_one' : toFun 1 = 0)
  (mul_le' : ∀ (x y : G), toFun (x * y) ≤ toFun x + toFun y) (inv' : ∀ (x : G), toFun x⁻¹ = toFun x),
  { toFun := toFun, map_one' := map_one', mul_le' := mul_le', inv' := inv' } =
    { toFun := toFun_1, map_one' := ⋯, mul_le' := ⋯, inv' := ⋯ }
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
Quiver.StronglyConnectedComponent.mk_eq_mk : ∀ {V : Type u_2} [inst : Quiver V] {a b : V},
  Quiver.StronglyConnectedComponent.mk a = Quiver.StronglyConnectedComponent.mk b ↔
    Nonempty (Quiver.Path a b) ∧ Nonempty (Quiver.Path b a)
-- Mathlib.Tactic.Translate.Reorder
_private.Mathlib.Tactic.Translate.Reorder.0.Array.map_unattach.match_1.eq_1 : ∀ {α : Type u_1} {P : α → Prop} (motive : Subtype P → Sort u_2) (x : α) (h : P x)
  (h_1 : (x : α) → (h : P x) → motive ⟨x, h⟩),
  (match ⟨x, h⟩ with
    | ⟨x, h⟩ => h_1 x h) =
    h_1 x h
-- Mathlib.Order.Concept
upperPolar_lowerPolar_upperPolar : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α),
  upperPolar r (lowerPolar r (upperPolar r s)) = upperPolar r s
-- Mathlib.Data.PFunctor.Multivariate.Basic
/-- Split polynomial functor, get a univariate functor
from an `n+1`-ary functor  -/
MvPFunctor.last : {n : ℕ} → MvPFunctor.{u} (n + 1) → PFunctor.{u, u}
-- Mathlib.Data.Stream.Init
Stream'.head_cons : ∀ {α : Type u} (a : α) (s : Stream' α), (Stream'.cons a s).head = a
-- Mathlib.CategoryTheory.Sites.CoversTop.Basic
CategoryTheory.GrothendieckTopology.coversTop_iff_of_isTerminal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C)
  (hX : CategoryTheory.Limits.IsTerminal X) {I : Type u_1} (Y : I → C),
  J.CoversTop Y ↔ CategoryTheory.Sieve.ofObjects Y X ∈ J X
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.Proj.toLocallyRingedSpace.eq_1 : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜],
  AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜 =
    { toSheafedSpace := AlgebraicGeometry.Proj.toSheafedSpace 𝒜, isLocalRing := ⋯ }
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `IsPreorder` instance if available  -/
Lean.Meta.Grind.Arith.Linear.NatStruct.isPreorderInst? : Lean.Meta.Grind.Arith.Linear.NatStruct → Option Lean.Expr
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddRightCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddRightCancelMonoid α],
  Colex.instAddRightCancelMonoid = { toAddMonoid := Colex.instAddMonoid, toIsRightCancelAdd := ⋯ }
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.findSomeM?.match_1.eq_2 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (fx : γ) (h_1 : Unit → motive none) (h_2 : (fx : γ) → motive (some fx)),
  (match some fx with
    | none => h_1 ()
    | some fx => h_2 fx) =
    h_2 fx
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
/-- **Alias** of `MeasurableSet.setOfPred_finite`. -/
MeasurableSet.setOf_finite : ∀ {α : Type u_1} [Countable α], MeasurableSet {s | s.Finite}
-- Mathlib.Data.Rel
SetRel.isRefl_mono : ∀ {α : Type u_1} {R₁ R₂ : SetRel α α} [R₁.IsRefl], R₁ ⊆ R₂ → R₂.IsRefl
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
Real.eulerMascheroniSeq'_six_lt_two_thirds : Real.eulerMascheroniSeq' 6 < 2 / 3
-- Mathlib.RingTheory.Ideal.Defs
/-- For two elements `m` and `m'` in an `R`-module `M`, the set of elements `r : R` with
equal scalar product with `m` and `m'` is an ideal of `R`. If `M` is a group, this coincides
with the kernel of `LinearMap.toSpanSingleton R M (m - m')`.  -/
Module.eqIdeal : (R : Type u_1) → {M : Type u_2} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → M → M → Ideal R
-- Mathlib.GroupTheory.Coset.Basic
Subgroup.quotientiInfSubgroupOfEmbedding.eq_1 : ∀ {α : Type u_1} [inst : Group α] {ι : Type u_2} (f : ι → Subgroup α) (H : Subgroup α),
  Subgroup.quotientiInfSubgroupOfEmbedding f H =
    { toFun := fun q i => Subgroup.quotientSubgroupOfMapOfLE H ⋯ q, inj' := ⋯ }
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
ContinuousMultilinearMap.toContinuousLinearMap.congr_simp : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (f f_1 : ContinuousMultilinearMap R M₁ M₂),
  f = f_1 →
    ∀ {inst_7 : DecidableEq ι} [inst_8 : DecidableEq ι] (m m_1 : (i : ι) → M₁ i),
      m = m_1 → ∀ (i : ι), f.toContinuousLinearMap m i = f_1.toContinuousLinearMap m_1 i
-- Mathlib.Tactic.Widget.SelectInsertParamsClass
SelectInsertParamsClass.mk : {α : Type} →
  (α → Lean.Lsp.Position) →
    (α → Array Lean.Widget.InteractiveGoal) →
      (α → Array Lean.SubExpr.GoalsLocation) → (α → Lean.Lsp.Range) → SelectInsertParamsClass α
-- Mathlib.Data.Complex.Basic
Complex.div_ofReal_re : ∀ (z : ℂ) (x : ℝ), (z / ↑x).re = z.re / x
-- Mathlib.Algebra.Module.Torsion.Free
instIsTorsionFreeMulOpposite : ∀ {R : Type u_1} [inst : Semiring R], Module.IsTorsionFree Rᵐᵒᵖ R
-- Mathlib.Topology.Order.Monotone
/-- A monotone map has a limit to the right of any point `x`, equal to `sInf (f '' (Ioi x))`.  -/
Monotone.tendsto_nhdsGT : ∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Monotone f → ∀ (x : α), Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (sInf (f '' Set.Ioi x)))
-- Lean.Util.Trace
Lean.MonadTrace : (Type → Type) → Type
-- Mathlib.Data.Nat.Multiplicity
Nat.Prime.emultiplicity_mul : ∀ {p m n : ℕ}, Nat.Prime p → emultiplicity p (m * n) = emultiplicity p m + emultiplicity p n
-- Mathlib.Algebra.Tropical.Basic
/-- Reinterpret `x : R` as an element of `Tropical R`, preserving the order.  -/
Tropical.tropOrderIso : {R : Type u} → [inst : Preorder R] → R ≃o Tropical R
-- Init.Data.List.Lemmas
List.concat_nil : ∀ {α : Type u_1} {a : α}, [].concat a = [a]