mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Spectral.Hom
/-- A function between topological spaces is spectral if it is continuous and the preimage of
every compact open set is compact open.  -/
IsSpectralMap.isCompact_preimage_of_isOpen : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  IsSpectralMap f → ∀ ⦃s : Set β⦄, IsOpen s → IsCompact s → IsCompact (f ⁻¹' s)
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.getEntryLT?.go : {α : Type u} →
  {β : α → Type v} → [Ord α] → α → Option ((a : α) × β a) → Std.DTreeMap.Internal.Impl α β → Option ((a : α) × β a)
-- Mathlib.Data.Set.Lattice.Image
Set.iUnion₂_inter_iUnion₂ : ∀ {α : Type u_1} {ι₁ : Sort u_9} {κ₁ : Sort u_10} {ι₂ : ι₁ → Sort u_11} {k₂ : κ₁ → Sort u_12}
  (f : (i₁ : ι₁) → ι₂ i₁ → Set α) (g : (j₁ : κ₁) → k₂ j₁ → Set α),
  (⋃ i₁, ⋃ i₂, f i₁ i₂) ∩ ⋃ j₁, ⋃ j₂, g j₁ j₂ = ⋃ i₁, ⋃ i₂, ⋃ j₁, ⋃ j₂, f i₁ i₂ ∩ g j₁ j₂
-- Mathlib.Algebra.Group.Equiv.TypeTags
MulEquiv.piMultiplicative_symm_apply : ∀ {ι : Type u_1} (K : ι → Type u_4) [inst : (i : ι) → Add (K i)] (x : (i : ι) → Multiplicative (K i)),
  (MulEquiv.piMultiplicative K).symm x = Multiplicative.ofAdd fun i => Multiplicative.toAdd (x i)
-- Mathlib.CategoryTheory.Enriched.HomCongr
CategoryTheory.Iso.eHomCongr_hom : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] {X Y X₁ Y₁ : C}
  (α : X ≅ X₁) (β : Y ≅ Y₁),
  (CategoryTheory.Iso.eHomCongr V α β).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerRight V α.inv Y)
      (CategoryTheory.eHomWhiskerLeft V X₁ β.hom)
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
/-- Any two `IsKleinFour` groups are isomorphic via any equivalence which sends the identity of one
group to the identity of the other.  -/
IsKleinFour.mulEquiv : {G₁ : Type u_2} →
  {G₂ : Type u_3} →
    [inst : Group G₁] → [inst_1 : Group G₂] → [IsKleinFour G₁] → [IsKleinFour G₂] → (e : G₁ ≃ G₂) → e 1 = 1 → G₁ ≃* G₂
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- An `𝒪_{Spec R}` module `M` is quasicoherent if and only if it is isomorphic to `Γ(M)^~`.  -/
AlgebraicGeometry.isQuasicoherent_iff_isIso_fromTildeΓ : ∀ {R : CommRingCat} (M : (AlgebraicGeometry.Spec R).Modules),
  SheafOfModules.IsQuasicoherent M ↔ CategoryTheory.IsIso M.fromTildeΓ
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- The forgetful functor from `𝒪ₓ`-modules to presheaves of modules.
This is mostly useful to transport results from (pre)sheaves of modules to `𝒪ₓ`-modules and
usually shouldn't be used directly when working with actual `𝒪ₓ`-modules.  -/
AlgebraicGeometry.Scheme.Modules.toPresheafOfModules : (X : AlgebraicGeometry.Scheme) → CategoryTheory.Functor X.Modules X.PresheafOfModules
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.instIsCardinalPresentableObjIsCardinalPresentable : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  (X : (CategoryTheory.isCardinalPresentable C κ).FullSubcategory), CategoryTheory.IsCardinalPresentable X.obj κ
-- Mathlib.Algebra.Ring.InjSurj
/-- Pullback a `NonUnitalSemiring` instance along an injective function.  -/
Function.Injective.nonUnitalSemiring : {R : Type u_1} →
  {S : Type u_2} →
    (f : S → R) →
      Function.Injective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : SMul ℕ S] →
                [inst_4 : NonUnitalSemiring R] →
                  f 0 = 0 →
                    (∀ (x y : S), f (x + y) = f x + f y) →
                      (∀ (x y : S), f (x * y) = f x * f y) →
                        (∀ (n : ℕ) (x : S), f (n • x) = n • f x) → NonUnitalSemiring S
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_hom_ofRestrict : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict f).hom
      (Y.ofRestrict ⋯) =
    f
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_insertUnit_fold : ∀ {n : ℕ} {units : List (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))}
  (unitsAcc : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (b : Bool),
  (List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (unitsAcc, assignments, b) units).2.1.size =
    assignments.size
-- Mathlib.Data.List.Count
List.count_map_of_injective : ∀ {α : Type u_1} {β : Type u_2} [inst : BEq α] [LawfulBEq α] [inst_2 : BEq β] [LawfulBEq β] (l : List α) (f : α → β),
  Function.Injective f → ∀ (x : α), List.count (f x) (List.map f l) = List.count x l
-- Mathlib.CategoryTheory.Galois.EssSurj
_private.Mathlib.CategoryTheory.Galois.EssSurj.0.CategoryTheory.PreGaloisCategory.coconeQuotientDiag_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.GaloisCategory C] [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F]
  {V U : OpenSubgroup (CategoryTheory.Aut F)} (h : (↑U).Normal) {A : C}
  (u :
    (CategoryTheory.PreGaloisCategory.functorToAction F).obj A ≅
      Action.FintypeCat.ofMulAction (CategoryTheory.Aut F) (FintypeCat.of (CategoryTheory.Aut F ⧸ ↑U)))
  (hUinV : U ≤ V),
  (CategoryTheory.PreGaloisCategory.coconeQuotientDiag✝ h u hUinV).ι =
    CategoryTheory.SingleObj.natTrans
      (CategoryTheory.CategoryStruct.comp u.hom (Action.FintypeCat.quotientToQuotientOfLE (↑V) (↑U) hUinV)) ⋯
-- Mathlib.CategoryTheory.Bicategory.InducedBicategory
CategoryTheory.Bicategory.InducedBicategory.bicategory_Hom : ∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  (X Y : CategoryTheory.Bicategory.InducedBicategory C F), (X ⟶ Y) = X.Hom Y
-- Init.Data.Float.Float32
/-- Converts a floating-point number to an 8-bit unsigned integer.

If the given `Float32` is non-negative, truncates the value to a positive integer, rounding down and
clamping to the range of `UInt8`. Returns `0` if the `Float32` is negative or `NaN`, and returns the
largest `UInt8` value (i.e. `UInt8.size - 1`) if the float is larger than it.

This function has a logical model in terms of `Float32.Model`.
 -/
Float32.toUInt8 : Float32 → UInt8
-- Mathlib.Algebra.BigOperators.Finprod
/-- **Alias** of `finprod_mem_inter_mul_sdiff'`. -/
finprod_mem_inter_mul_diff' : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s : Set α} (t : Set α),
  (s ∩ Function.mulSupport f).Finite →
    (∏ᶠ (i : α) (_ : i ∈ s ∩ t), f i) * ∏ᶠ (i : α) (_ : i ∈ s \ t), f i = ∏ᶠ (i : α) (_ : i ∈ s), f i
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Subgroup.forall_mem_zpowers : ∀ {G : Type u_1} [inst : Group G] {x : G} {p : G → Prop}, (∀ g ∈ Subgroup.zpowers x, p g) ↔ ∀ (m : ℤ), p (x ^ m)
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
MeasureTheory.Measure.tendsto_IicSnd_atTop : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) {s : Set α},
  MeasurableSet s → Filter.Tendsto (fun r => (ρ.IicSnd ↑r) s) Filter.atTop (nhds (ρ.fst s))
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.instHSubOffset_2 : HSub Std.Time.PlainDateTime Std.Time.Hour.Offset Std.Time.PlainDateTime
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- Replacing a set by its closure does not change the Hausdorff distance.  -/
Metric.hausdorffDist_closure₁ : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α}, Metric.hausdorffDist (closure s) t = Metric.hausdorffDist s t
-- Mathlib.CategoryTheory.Adhesive.Basic
/-- If `a : A ⟶ Z` and `b : B ⟶ Z` are monomorphisms in an adhesive category, then the map
`pushout (pullback.fst a b) (pullback.snd a b) ⟶ Z` induced by their pullback is a monomorphism.
See Theorem 5.1 in Lack and Sobociński.  -/
CategoryTheory.Adhesive.desc_mono_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Adhesive C] {Z A B : C} {a : A ⟶ Z}
  {b : B ⟶ Z} [inst_2 : CategoryTheory.Mono a] [inst_3 : CategoryTheory.Mono b],
  CategoryTheory.Mono (CategoryTheory.Limits.pushout.desc a b ⋯)
-- Mathlib.Analysis.Complex.Exponential
/-- This is a useful version of `exp_nsmul` for q-expansions of modular forms.  -/
Complex.exp_nsmul' : ∀ (x a p : ℂ) (n : ℕ), Complex.exp (a * ↑n * x / p) = Complex.exp (a * x / p) ^ n
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_X₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles._auto_1),
  (X.kernelSequenceCycles f g n₀ n₁ hn₁).X₂ = (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g)
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.subtype_mk : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {p : β → Prop} {f : α → β},
  Measurable f → ∀ {h : ∀ (x : α), p (f x)}, Measurable fun x => ⟨f x, ⋯⟩
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.isEquivalent_zero_iff_eventually_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {u : α → β} {l : Filter α},
  Asymptotics.IsEquivalent l u 0 ↔ u =ᶠ[l] 0
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Multipliable.tprod_subtype_le : ∀ {κ : Type u_4} {γ : Type u_5} [inst : CommGroup γ] [inst_1 : PartialOrder γ] [IsOrderedMonoid γ]
  [inst_3 : UniformSpace γ] [IsUniformGroup γ] [OrderClosedTopology γ] [CompleteSpace γ] (f : κ → γ) (β : Set κ),
  (∀ (a : κ), 1 ≤ f a) → Multipliable f → ∏' (b : ↑β), f ↑b ≤ ∏' (a : κ), f a
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.ne_ofReal : ∀ (z : UpperHalfPlane) (x : ℝ), ↑z ≠ ↑x
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Instance : Type
-- Mathlib.RingTheory.Extension.Generators
/-- Construct `Generators` from a family of generators of `S`.  -/
Algebra.Generators.ofSet : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → [inst_2 : Algebra R S] → {s : Set S} → Algebra.adjoin R s = ⊤ → Algebra.Generators R S ↑s
-- Mathlib.RingTheory.OrzechProperty
OrzechProperty.mk : ∀ {R : Type u} [inst : Semiring R],
  (∀ {M : Type u} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Finite R M] {N : Submodule R M}
      (f : ↥N →ₗ[R] M), Function.Surjective ⇑f → Function.Injective ⇑f) →
    OrzechProperty R
-- Mathlib.Analysis.Convex.Integral
/-- **Jensen's inequality**: if a function `g : E → ℝ` is concave and continuous on a convex closed
set `s`, `μ` is a finite non-zero measure on `α`, and `f : α → E` is a function sending
`μ`-a.e. points of a set `t` to `s`, then the average value of `g ∘ f` over `t` is less than or
equal to the value of `g` at the average value of `f` over `t` provided that both `f` and `g ∘ f`
are integrable.  -/
ConcaveOn.set_average_mem_hypograph : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E} {g : E → ℝ},
  ConcaveOn ℝ s g →
    ContinuousOn g s →
      IsClosed s →
        μ t ≠ 0 →
          μ t ≠ ⊤ →
            (∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s) →
              MeasureTheory.IntegrableOn f t μ →
                MeasureTheory.IntegrableOn (g ∘ f) t μ →
                  (⨍ (x : α) in t, f x ∂μ, ⨍ (x : α) in t, g (f x) ∂μ) ∈ {p | p.1 ∈ s ∧ p.2 ≤ g p.1}
-- Init.Omega.Int
Lean.Omega.Nat.lt_of_gt : ∀ {x y : ℕ}, x > y → y < x
-- Mathlib.Control.Bitraversable.Instances
Sum.bitraverse.eq_2 : ∀ {F : Type u → Type u} [inst : Applicative F] {α : Type u_1} {α' : Type u} {β : Type u_2} {β' : Type u} (f : α → F α')
  (f' : β → F β') (x_1 : β), Sum.bitraverse f f' (Sum.inr x_1) = Sum.inr <$> f' x_1
-- Mathlib.CategoryTheory.Triangulated.Orthogonal
CategoryTheory.ObjectProperty.isColocal_trW : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty 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]
  [inst_5 : CategoryTheory.Pretriangulated C] [P.IsTriangulated], P.trW.isColocal = P.leftOrthogonal
-- Init.Data.Array.Lemmas
Array.reverse_inj : ∀ {α : Type u_1} {xs ys : Array α}, xs.reverse = ys.reverse ↔ xs = ys
-- Mathlib.CategoryTheory.EssentiallySmall
/-- A category is `w`-locally small if every hom set is `w`-small.

See `ShrinkHoms C` for a category instance where every hom set has been replaced by a small model.
 -/
CategoryTheory.LocallySmall : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.linearCombination_repr : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (x : M), (Finsupp.linearCombination R ⇑b) (b.repr x) = x
-- Mathlib.Order.RelClasses
/-- Set notation form of `lt_or_eq_of_le` -/
ssubset_or_eq_of_subset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a ⊆ b → a ⊂ b ∨ a = b
-- Init.Data.UInt.Bitwise
UInt64.ofNatLT_shiftLeft : ∀ {a b : ℕ} (ha : a <<< b < UInt64.size) (hb : b < 64),
  UInt64.ofNatLT (a <<< b) ha = UInt64.ofNatLT a ⋯ <<< UInt64.ofNatLT b ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.toList_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp}, t.keysArray.toList = t.keys
-- Init.Data.ToString.Basic
instToStringId : {α : Type u_1} → [ToString α] → ToString (id α)
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.IsAlternating.mono : ∀ {V : Type u_1} {G G' G'' : SimpleGraph V}, G.IsAlternating G' → G'' ≤ G → G''.IsAlternating G'
-- Init.Data.SInt.Lemmas
Int8.toInt_ofIntTruncate : ∀ {x : ℤ}, Int8.minValue.toInt ≤ x → x ≤ Int8.maxValue.toInt → (Int8.ofIntClamp x).toInt = x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {a : α}
  {fallback : β}, t.contains a = false → Std.DTreeMap.Const.getD t a fallback = fallback
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.prodAssoc_apply : ∀ (R : Type u_8) (M₁ : Type u_9) (M₂ : Type u_10) (M₃ : Type u_11) [inst : Semiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] [inst_7 : TopologicalSpace M₁] [inst_8 : TopologicalSpace M₂] [inst_9 : TopologicalSpace M₃]
  (p₁ : M₁) (p₂ : M₂) (p₃ : M₃), (ContinuousLinearEquiv.prodAssoc R M₁ M₂ M₃) ((p₁, p₂), p₃) = (p₁, p₂, p₃)
-- Mathlib.Data.Int.Bitwise
Int.lor.eq_3 : ∀ (m n : ℕ), (Int.negSucc m).lor (Int.ofNat n) = Int.negSucc (m.ldiff n)
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.truncateFun_out : ∀ {p n : ℕ} {R : Type u_1} [inst : CommRing R] (x : TruncatedWittVector p n R), WittVector.truncateFun n x.out = x
-- Mathlib.Combinatorics.Tiling.Tile
/-- A `PlacedTile ps` is an image of a tile in the protoset `p` under an element of the group `G`.
This is represented using a quotient so that images under group elements differing only by a
symmetry of the tile are equal.  -/
DiscreteTiling.PlacedTile : {G : Type u_1} →
  {X : Type u_2} →
    {ιₚ : Type u_3} → [inst : Group G] → [inst_1 : MulAction G X] → DiscreteTiling.Protoset G X ιₚ → Type (max u_1 u_3)
-- Mathlib.CategoryTheory.Adjunction.CompositionIso
CategoryTheory.Adjunction.conjugateEquiv_leftAdjointIdIso_hom : ∀ {C₀ : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C₀] {F G : CategoryTheory.Functor C₀ C₀} (adj : F ⊣ G)
  (e : G ≅ CategoryTheory.Functor.id C₀),
  (CategoryTheory.conjugateEquiv CategoryTheory.Adjunction.id adj) (adj.leftAdjointIdIso e).hom = e.inv
-- Mathlib.RingTheory.AlgebraTower
Module.Basis.isScalarTower_of_nonempty : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid A]
  [inst_3 : Module R S] [inst_4 : Module S A] [inst_5 : Module R A] [IsScalarTower R S A] {ι : Type u_5} [Nonempty ι]
  (b : Module.Basis ι S A), IsScalarTower R S S
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.main : Lean.Meta.SimpAll.M (Option Lean.MVarId)
-- Init.Data.Bool
Bool.or'_eq_or : ∀ (a b : Bool), a.or' b = (a || b)
-- Batteries.Data.Array.Scan
Subarray.scanlM_eq_scanlM_extract : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} [inst : Monad m] [LawfulMonad m] {f : β → α → m β}
  {as : Subarray α}, Subarray.scanlM f init as = Array.scanlM f init (as.array.extract as.start as.stop)
-- Mathlib.Algebra.Order.Group.MinMax
abs_max_sub_max_le_abs : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] (a b c : α),
  |max a c - max b c| ≤ |a - b|
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `L` are linearly disjoint over `F`, then `A ⊗[F] L` is a domain.  -/
IntermediateField.LinearDisjoint.isDomain : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L → IsDomain (TensorProduct F (↥A) L)
-- Mathlib.Analysis.Analytic.Basic
AnalyticOnNhd.mono : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s t : Set E},
  AnalyticOnNhd 𝕜 f t → s ⊆ t → AnalyticOnNhd 𝕜 f s
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k fallback : α}, (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k (m₁.getKeyD k fallback)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
PresheafOfModules.instReflectsFiniteLimitsSheafOfModulesSheafAddCommGrpCatToSheaf : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat}, CategoryTheory.Limits.ReflectsFiniteLimits (SheafOfModules.toSheaf R)
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.setOfPred_root_add_zsmul_mem_eq_Icc : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  LinearIndependent R ![P.root i, P.root j] →
    {k | P.root j + k • P.root i ∈ Set.range ⇑P.root} =
      Set.Icc (-↑(RootPairing.chainBotCoeff i j)) ↑(RootPairing.chainTopCoeff i j)
-- Mathlib.Topology.CompactOpen
ContinuousMap.continuousOn_mkD_restrict_of_uncurry : ∀ {X : Type u_2} {Y : Type u_3} {T : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace T] {s : Set T} {t : Set X} (f : T → X → Y) (g : C(↑t, Y)),
  ContinuousOn (Function.uncurry f) (s ×ˢ t) → ContinuousOn (fun x => ContinuousMap.mkD (t.domRestrict (f x)) g) s
-- Mathlib.LinearAlgebra.Trace
/-- The trace of an endomorphism is invariant under conjugation  -/
LinearMap.trace_conj : ∀ (R : Type u) [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (g : M →ₗ[R] M)
  (f : (M →ₗ[R] M)ˣ), (LinearMap.trace R M) (↑f * g * ↑f⁻¹) = (LinearMap.trace R M) g
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_assoc : ∀ {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
  (f : R →+* S₁) (g : σ → S₁) (q : S₂ → MvPolynomial σ R) (p : MvPolynomial S₂ R),
  MvPolynomial.eval₂ f (fun t => MvPolynomial.eval₂ f g (q t)) p =
    MvPolynomial.eval₂ f g (MvPolynomial.eval₂ MvPolynomial.C q p)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instMul.eq_1 : ∀ {α : Type u} {R : Type u_2} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace R] [inst_2 : Mul R]
  [inst_3 : BoundedMul R] [inst_4 : ContinuousMul R],
  BoundedContinuousFunction.instMul =
    { mul := fun f g => { toFun := fun x => f x * g x, continuous_toFun := ⋯, map_bounded' := ⋯ } }
-- Mathlib.Algebra.Free
/-- The length of an element of a free additive magma is positive.  -/
FreeAddMagma.length_pos : ∀ {α : Type u} (x : FreeAddMagma α), 0 < x.length
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.filter_eq_empty_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {f : α → Bool},
  Std.ExtTreeSet.filter f t = ∅ ↔ ∀ (k : α) (h : k ∈ t), f (t.get k h) = false
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.comp_flip_uncurry_eq : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  {D : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor B D)
  (G : CategoryTheory.Functor D (CategoryTheory.Functor C E)),
  CategoryTheory.Functor.uncurry.obj (F.comp G).flip =
    ((CategoryTheory.Functor.id C).prod F).comp (CategoryTheory.Functor.uncurry.obj G.flip)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.coe_mul : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {S : NonUnitalSubalgebra R A} (x y : ↥S), ↑(x * y) = ↑x * ↑y
-- Mathlib.LinearAlgebra.Basis.Fin
Module.Basis.coe_mkFinSnoc : ∀ {R : Type u_3} {M : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {n : ℕ}
  {N : Submodule R M} (b : Module.Basis (Fin n) R ↥N) (y : M) (hli : ∀ (c : R), ∀ x ∈ N, c • y + x = 0 → c = 0)
  (hsp : ∀ (z : M), ∃ c, z + c • y ∈ N), ⇑(b.mkFinSnoc y hli hsp) = Fin.snoc (Subtype.val ∘ ⇑b) y
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_trans : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b c : ℤ) (hab : a ≤ b) (hbc : b ≤ c),
  CategoryTheory.CategoryStruct.comp (t.natTransTruncLEOfLE a b hab) (t.natTransTruncLEOfLE b c hbc) =
    t.natTransTruncLEOfLE a c ⋯
-- Mathlib.Order.Filter.Prod
Filter.eventually_swap_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β} {p : α × β → Prop},
  (∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap
-- Init.Data.Range.Polymorphic.PRange
/-- Every element of the intersection is an element of both original ranges.
   -/
Std.Rco.LawfulRcoIntersection.mem_intersection_iff : ∀ {α : Type w} {inst : LT α} {inst_1 : LE α} {inst_2 : Std.Rco.HasRcoIntersection α}
  [self : Std.Rco.LawfulRcoIntersection α] {a : α} {r s : Std.Rco α},
  a ∈ Std.Rco.HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s
-- Mathlib.Analysis.Normed.Operator.NormedSpace
ContinuousLinearEquiv.norm_symm_pos : ∀ {𝕜 : 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] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] [RingHomIsometric σ₂₁] [RingHomIsometric σ₁₂]
  [Nontrivial E] (e : E ≃SL[σ₁₂] F), 0 < ‖↑e.symm‖