mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Sets.Opens
/-- Preimage of an open neighborhood of `f x` under a continuous map `f` as a `LatticeHom`.  -/
TopologicalSpace.OpenNhdsOf.comap : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        (f : C(α, β)) → (x : α) → LatticeHom (TopologicalSpace.OpenNhdsOf (f x)) (TopologicalSpace.OpenNhdsOf x)
-- Init.Data.Slice.Array.Lemmas
Subarray.mkSlice_roc_eq_mkSlice_roo : ∀ {α : Type u_1} {xs : Subarray α} {lo hi : ℕ},
  (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = Std.Roo.Sliceable.mkSlice xs lo<...hi + 1
-- Mathlib.Topology.Category.TopCat.Limits.Basic
TopCat.forget_preservesColimitsOfSize : CategoryTheory.Limits.PreservesColimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget TopCat)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.instFullGrpForget₂Grp : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C], (CategoryTheory.CommGrp.forget₂Grp C).Full
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.isMaximal_of_isIntegral_of_isMaximal_comap : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsIntegral R S] (I : Ideal S) [I.IsPrime], (Ideal.comap (algebraMap R S) I).IsMaximal → I.IsMaximal
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.orbitRel_of_subMul : ∀ {R : Type u} {M : Type v} [inst : Group R] [inst_1 : MulAction R M] (p : SubMulAction R M),
  MulAction.orbitRel R ↥p = Setoid.comap Subtype.val (MulAction.orbitRel R M)
-- Mathlib.Data.Num.ZNum
ZNum.addMonoidWithOne : AddMonoidWithOne ZNum
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivWithinAt.comp_hasDerivAt_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {h : 𝕜 → 𝕜'} {h₂ : 𝕜' → 𝕜'} {h' h₂' y : 𝕜'} {t : Set 𝕜'},
  HasDerivWithinAt h₂ h₂' t y →
    HasDerivAt h h' x → (∀ᶠ (x' : 𝕜) in nhds x, h x' ∈ t) → y = h x → HasDerivAt (h₂ ∘ h) (h₂' * h') x
-- Init.Data.Int.Order
Int.le_add_of_neg_le_sub_left : ∀ {a b c : ℤ}, -a ≤ b - c → c ≤ a + b
-- Mathlib.Order.Basic
PartialOrder.ext_lt : ∀ {α : Type u_2} {A B : PartialOrder α}, (∀ (x y : α), x < y ↔ x < y) → A = B
-- Mathlib.Topology.UniformSpace.Basic
/-- Open elements of `𝓤 α` form a basis of `𝓤 α`.  -/
uniformity_hasBasis_open : ∀ {α : Type ua} [inst : UniformSpace α], (uniformity α).HasBasis (fun V => V ∈ uniformity α ∧ IsOpen V) id
-- Mathlib.FieldTheory.IntermediateField.ExtendRight
IntermediateField.extendRight.instSMulSubtypeMem : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          (F : IntermediateField K L) →
            (M : Type u_3) →
              [inst_3 : Field M] →
                [inst_4 : Algebra K M] →
                  [inst_5 : Algebra L M] →
                    [inst_6 : IsScalarTower K L M] →
                      {S : Type u_5} →
                        [inst_7 : CommRing S] →
                          [inst_8 : Algebra S ↥F] →
                            [inst_9 : Algebra S M] → [IsScalarTower S (↥F) M] → SMul S ↥(F.extendRight M)
-- Mathlib.Topology.UniformSpace.Closeds
TotallyBounded.exists_prodMk_finset_mem_hausdorffEntourage : ∀ {α : Type u_1} [inst : UniformSpace α] {s : Set α},
  TotallyBounded s → ∀ {U : SetRel α α}, U ∈ uniformity α → ∃ t, (↑t, s) ∈ hausdorffEntourage U
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.lim_map : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C] {X Y : CategoryTheory.Functor J C} (α : X ⟶ Y),
  CategoryTheory.Limits.lim.map α = CategoryTheory.Limits.limMap α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonRenameOptions.fromJson : Lean.Json → Except String Lean.Lsp.RenameOptions
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.distortion_of_const : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) [inst : Fintype ι] {c : NNReal},
  π.boxes.Nonempty → (∀ J ∈ π, J.distortion = c) → π.distortion = c
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- Return `true` if `declName` is tagged to be unfolded using `unfoldDefinition?` (i.e., without using equational theorems).  -/
Lean.Meta.SimpTheorems.isDeclToUnfold : Lean.Meta.SimpTheorems → Lean.Name → Bool
-- Mathlib.Algebra.Algebra.Unitization
/-- To show a property hold on all `Unitization R A` it suffices to show it holds
on terms of the form `inl r + a`.

This can be used as `induction x`.  -/
Unitization.ind : ∀ {R : Type u_5} {A : Type u_6} [inst : AddZeroClass R] [inst_1 : AddZeroClass A] {P : Unitization R A → Prop},
  (∀ (r : R) (a : A), P (Unitization.inl r + ↑a)) → ∀ (x : Unitization R A), P x
-- Mathlib.Order.CompleteLattice.Basic
sSup_range : ∀ {α : Type u_1} {ι : Sort u_4} [inst : SupSet α] {f : ι → α}, sSup (Set.range f) = iSup f
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
Complex.polarCoord_symm_apply : ∀ (p : ℝ × ℝ), ↑Complex.polarCoord.symm p = ↑p.1 * (↑(Real.cos p.2) + ↑(Real.sin p.2) * Complex.I)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_map_sum_map : ∀ {ι : Type u_2} {κ : Type u_3} {M : Type u_5} [inst : AddCommMonoid M] (m : Multiset ι) (n : Multiset κ)
  {f : ι → κ → M},
  (Multiset.map (fun a => (Multiset.map (fun b => f a b) n).sum) m).sum =
    (Multiset.map (fun b => (Multiset.map (fun a => f a b) m).sum) n).sum
-- Batteries.Data.String.Lemmas
String.any_iff : ∀ (s : String) (p : Char → Bool), String.Legacy.any s p = true ↔ ∃ c ∈ s.toList, p c = true
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.or_intro_r' : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (P ⊢ₛ R) → P ⊢ₛ Q ∨ R
-- Mathlib.Algebra.Module.Bimodule
/-- Forgetting the `A` action, a `Submodule` over `A ⊗[R] B` is just a `Submodule` over `B`.  -/
Subbimodule.toSubmodule' : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {M : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : Semiring A] →
                [inst_4 : Semiring B] →
                  [inst_5 : Module A M] →
                    [inst_6 : Module B M] →
                      [inst_7 : Algebra R A] →
                        [inst_8 : Algebra R B] →
                          [inst_9 : IsScalarTower R A M] →
                            [inst_10 : IsScalarTower R B M] →
                              [inst_11 : SMulCommClass A B M] → Submodule (TensorProduct R A B) M → Submodule B M
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.η_def : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] (i : I),
  CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.Pi.eval C i) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (C i))
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The ring of integers of a `p ^ k`-th cyclotomic extension of `ℚ` is a cyclotomic extension.  -/
IsPrimitiveRoot.IsCyclotomicExtension.ringOfIntegersOfPrimePow : ∀ {p k : ℕ} {K : Type u} [inst : Field K] [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [IsCyclotomicExtension {p ^ k} ℚ K], IsCyclotomicExtension {p ^ k} ℤ (NumberField.RingOfIntegers K)
-- Init.Data.UInt.Bitwise
UInt8.ofFin_and : ∀ (a b : Fin UInt8.size), UInt8.ofFin (a &&& b) = UInt8.ofFin a &&& UInt8.ofFin b
-- Mathlib.Algebra.Module.ZLattice.Covolume
ZLattice.covolume.tendsto_card_le_div : ∀ {ι : Type u_1} [inst : Fintype ι] (L : Submodule ℤ (ι → ℝ)) [inst_1 : DiscreteTopology ↥L] [IsZLattice ℝ L]
  {X : Set (ι → ℝ)},
  (∀ ⦃x : ι → ℝ⦄ ⦃r : ℝ⦄, x ∈ X → 0 < r → r • x ∈ X) →
    ∀ {F : (ι → ℝ) → ℝ},
      (∀ (x : ι → ℝ) ⦃r : ℝ⦄, 0 ≤ r → F (r • x) = r ^ Fintype.card ι * F x) →
        Bornology.IsBounded {x | x ∈ X ∧ F x ≤ 1} →
          MeasurableSet {x | x ∈ X ∧ F x ≤ 1} →
            MeasureTheory.volume (frontier {x | x ∈ X ∧ F x ≤ 1}) = 0 →
              ∀ [Nonempty ι],
                Filter.Tendsto (fun c => ↑(Nat.card ↑({x | x ∈ X ∧ F x ≤ c} ∩ ↑L)) / c) Filter.atTop
                  (nhds (MeasureTheory.volume.real {x | x ∈ X ∧ F x ≤ 1} / ZLattice.covolume L MeasureTheory.volume))
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
panicking if no such pair exists.
 -/
Std.TreeMap.Raw.getEntryLT! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited (α × β)] → Std.TreeMap.Raw α β cmp → α → α × β
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_erase : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α}, (m.erase k).get! a = if (k == a) = true then default else m.get! a
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
norm_iteratedFDeriv_fderiv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {n : ℕ}, ‖iteratedFDeriv 𝕜 n (fderiv 𝕜 f) x‖ = ‖iteratedFDeriv 𝕜 (n + 1) f x‖
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.Unsafe.exprsEqualUpToIdsCore₂ : Lean.Expr → Lean.Expr → Aesop.EqualUpToIds.ExprsEqualUpToIdsM Bool
-- Mathlib.Algebra.Group.Basic
nsmul_add : ∀ {M : Type u_4} [inst : AddCommMonoid M] (a b : M) (n : ℕ), n • (a + b) = n • a + n • b
-- Mathlib.Algebra.Divisibility.Basic
RightDvd.of_eq : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, a = b → a ∣ᵣ b
-- Mathlib.RingTheory.Spectrum.Maximal.Defs
MaximalSpectrum.mk.injEq : ∀ {R : Type u_1} [inst : CommSemiring R] (asIdeal : Ideal R) (isMaximal : asIdeal.IsMaximal) (asIdeal_1 : Ideal R)
  (isMaximal_1 : asIdeal_1.IsMaximal),
  ({ asIdeal := asIdeal, isMaximal := isMaximal } = { asIdeal := asIdeal_1, isMaximal := isMaximal_1 }) =
    (asIdeal = asIdeal_1)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singleton_div_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] (a b : α), {a} / {b} = {a / b}
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
/-- Derivative of `z ↦ (denom g z) ^ k`: $\frac{d}{dz}[(cz+d)^k] = k \cdot c \cdot (cz+d)^{k-1}$.  -/
UpperHalfPlane.hasDerivAt_denom_zpow : ∀ (g : GL (Fin 2) ℝ) (k : ℤ) (τ : UpperHalfPlane),
  HasDerivAt (fun z => UpperHalfPlane.denom g z ^ k) (↑k * ↑(↑g 1 0) * UpperHalfPlane.denom g ↑τ ^ (k - 1)) ↑τ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.comp_zsmul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G X Y : C} [inst_2 : CategoryTheory.AddGrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) (n : ℤ),
  CategoryTheory.CategoryStruct.comp f (n • g) = n • CategoryTheory.CategoryStruct.comp f g
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_one : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P], ⇑1 = id
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.inr_pushoutZeroZeroIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr 0 0)
      (CategoryTheory.Limits.pushoutZeroZeroIso X Y).hom =
    CategoryTheory.Limits.coprod.inr
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice : {α : Type u_5} → [self : ConditionallyCompleteLinearOrder α] → ConditionallyCompleteLattice α
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.instUniqueOfIsEmpty : {α : Type u} → [IsEmpty α] → Unique (FreeGroup α)
-- Mathlib.GroupTheory.Submonoid.Centralizer
Submonoid.decidableMemCentralizer : {M : Type u_1} →
  {S : Set M} →
    [inst : Monoid M] → (a : M) → [Decidable (∀ b ∈ S, b * a = a * b)] → Decidable (a ∈ Submonoid.centralizer S)
-- Mathlib.RingTheory.Conductor
Localization.localRingHom_bijective_of_not_conductor_le : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S} {P : Ideal S}
  [inst_3 : P.IsPrime],
  ¬conductor R x ≤ P →
    ∀ {s : Subalgebra R S},
      s = R[x] →
        ∀ (p : Ideal ↥s) [inst_4 : p.IsPrime] [inst_5 : P.LiesOver p],
          Function.Bijective ⇑(Localization.localRingHom p P (algebraMap (↥s) S) ⋯)
-- Batteries.Data.List.Lemmas
List.idxOfNth_zero : ∀ {α : Type u_1} {xs : List α} {x : α} [inst : BEq α], List.idxOfNth x xs 0 = List.idxOf x xs
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderivWithin_const_add : ∀ {𝕜 : 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} {s : Set E} (c : F), fderivWithin 𝕜 (fun y => c + f y) s x = fderivWithin 𝕜 f s x
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- If `μ` has finite spanning sets in `C` and `C ⊆ D` then `μ` has finite spanning sets in `D`.  -/
MeasureTheory.Measure.FiniteSpanningSetsIn.mono : {α : Type u_1} →
  {m0 : MeasurableSpace α} →
    {μ : MeasureTheory.Measure α} → {C D : Set (Set α)} → μ.FiniteSpanningSetsIn C → C ⊆ D → μ.FiniteSpanningSetsIn D
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
/-- An infinite cyclic additive group is isomorphic to `ℤ`.  -/
intCyclicAddEquiv : {G : Type u_2} → [Infinite G] → [inst : AddGroup G] → [IsAddCyclic G] → ℤ ≃+ G
-- Mathlib.Topology.Order.LeftRight
nhdsLT_le_nhdsNE : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] (a : α), nhdsWithin a (Set.Iio a) ≤ nhdsWithin a {a}ᶜ
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
/-- Construct a pseudofunctor from a lax functor whose `mapId` and `mapComp` are isomorphisms.  -/
CategoryTheory.Pseudofunctor.mkOfLax' : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (F : CategoryTheory.LaxFunctor B C) →
          [∀ (a : B), CategoryTheory.IsIso (F.mapId a)] →
            [∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.IsIso (F.mapComp f g)] →
              CategoryTheory.Pseudofunctor B C
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
/-- As `⨆ i, f i = 0` when the domain of the real-valued function `f` is empty,
it suffices to show that all values of `f` are nonpositive to show that `⨆ i, f i ≤ 0`.  -/
Real.iSup_nonpos : ∀ {ι : Sort u_1} {f : ι → ℝ}, (∀ (i : ι), f i ≤ 0) → ⨆ i, f i ≤ 0
-- Mathlib.Data.Finset.Sort
Finset.orderIsoOfFin.congr_simp : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k), s.orderIsoOfFin h = s.orderIsoOfFin h
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.map_some : ∀ {X : Type u_1} {Y : Type u_2} (f : X → Y) (x : X), OnePoint.map f ↑x = ↑(f x)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftId_inv_app_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L R),
  ((CategoryTheory.Comma.mapLeftId L R).inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
/-- When applying the inverse of `lpMeasToLpTrimLie` (which takes a function in the Lp space of
the sub-sigma algebra and returns its version in the larger Lp space) to an indicator of the
sub-sigma-algebra, we obtain an indicator in the Lp space of the larger sigma-algebra.  -/
MeasureTheory.lpMeasToLpTrimLie_symm_indicator : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  [one_le_p : Fact (1 ≤ p)] [inst_1 : NormedSpace ℝ F] {hm : m ≤ m0} {s : Set α} {μ : MeasureTheory.Measure α}
  (hs : MeasurableSet s) (hμs : (μ.trim hm) s ≠ ⊤) (c : F),
  ↑((MeasureTheory.lpMeasToLpTrimLie F ℝ p μ hm).symm (MeasureTheory.indicatorConstLp p hs hμs c)) =
    MeasureTheory.indicatorConstLp p ⋯ ⋯ c
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
/-- A model for the Theory of algebraically closed fields is a Field. After introducing
this as a local instance on a particular Type, you should usually also introduce
`modelField_of_modelACF p M`, `compatibleRingOfModelField` and `isAlgClosed_of_model_ACF`  -/
FirstOrder.Field.fieldOfModelACF : (p : ℕ) →
  (K : Type u_2) → [inst : FirstOrder.Language.ring.Structure K] → [h : K ⊨ FirstOrder.Language.Theory.ACF p] → Field K
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.SubmersivePresentation.basisKaehler.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ),
  P.basisKaehler = P.basisKaehlerOfIsCompl ⋯ ⋯
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
cfcₙ_tsub : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : PartialOrder A] [inst_3 : StarRing A]
  [inst_4 : StarOrderedRing A] [inst_5 : Module ℝ A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : SMulCommClass ℝ A A]
  [IsTopologicalRing A] [T2Space A] [inst_10 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_11 : NonnegSpectrumClass ℝ A] (f g : NNReal → NNReal) (a : A),
  (∀ x ∈ quasispectrum NNReal a, g x ≤ f x) →
    autoParam (0 ≤ a) cfcₙ_tsub._auto_1 →
      autoParam (ContinuousOn f (quasispectrum NNReal a)) cfcₙ_tsub._auto_3 →
        autoParam (f 0 = 0) cfcₙ_tsub._auto_5 →
          autoParam (ContinuousOn g (quasispectrum NNReal a)) cfcₙ_tsub._auto_7 →
            autoParam (g 0 = 0) cfcₙ_tsub._auto_9 → cfcₙ (fun x => f x - g x) a = cfcₙ f a - cfcₙ g a
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Make a morphism in `P.Arrow Q X` from morphisms in `T` with compatibilities.  -/
CategoryTheory.MorphismProperty.Arrow.homMk : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P Q W : CategoryTheory.MorphismProperty T} →
      [inst_1 : Q.IsMultiplicative] →
        [inst_2 : W.IsMultiplicative] →
          {A B : P.Arrow Q W} →
            (f : A.left ⟶ B.left) →
              (g : A.right ⟶ B.right) →
                autoParam (CategoryTheory.CategoryStruct.comp f B.hom = CategoryTheory.CategoryStruct.comp A.hom g)
                    CategoryTheory.MorphismProperty.Arrow.homMk._auto_1 →
                  autoParam (Q f) CategoryTheory.MorphismProperty.Arrow.homMk._auto_3 →
                    autoParam (W g) CategoryTheory.MorphismProperty.Arrow.homMk._auto_5 → (A ⟶ B)
-- Mathlib.CategoryTheory.Equivalence
/-- An equivalence of categories.

We define an equivalence between `C` and `D`, with notation `C ≌ D`, as a half-adjoint equivalence:
a pair of functors `F : C ⥤ D` and `G : D ⥤ C` with a unit `η : 𝟭 C ≅ F ⋙ G` and counit
`ε : G ⋙ F ≅ 𝟭 D`, such that the natural isomorphisms `η` and `ε` satisfy the triangle law for
`F`: namely, `Fη ≫ εF = 𝟙 F`. Or, in other words, the composite `F` ⟶ `F ⋙ G ⋙ F` ⟶ `F` is the
identity.

In `unit_inverse_comp`, we show that this is sufficient to establish a full adjoint
equivalence. I.e., the composite `G` ⟶ `G ⋙ F ⋙ G` ⟶ `G` is also the identity.

The triangle equation `functor_unitIso_comp` is written as a family of equalities between
morphisms. It is more complicated if we write it as an equality of natural transformations, because
then we would either have to insert natural transformations like `F ⟶ F𝟭` or abuse defeq.  -/
CategoryTheory.Equivalence : (C : Type u₁) →
  (D : Type u₂) →
    [CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.Category.{v₂, u₂} D] → Type (max (max (max u₁ u₂) v₁) v₂)
-- Mathlib.Data.Finsupp.Weight
Finsupp.NonTorsionWeight.ne_zero : ∀ {σ : Type u_1} {M : Type u_2} (R : Type u_3) [inst : Semiring R] (w : σ → M) [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [Nontrivial R] [Finsupp.NonTorsionWeight R w] (s : σ), w s ≠ 0
-- Lean.Elab.App
Lean.Elab.Term.ElabAppArgs.Context.mk : Bool → Bool → Bool → ℕ → Lean.Elab.Term.ElabAppArgs.Context
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor.congr_simp : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f f_1 : X ⟶ Y) (e_f : f = f_1)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f =
    AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f_1
-- Mathlib.Data.Int.Log
Int.clog_of_left_le_one : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  {b : ℕ}, b ≤ 1 → ∀ (r : R), Int.clog b r = 0
-- Mathlib.Analysis.Convex.Quasiconvex
quasiconvexOn_iff_le_max : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder β] [inst_4 : SMul 𝕜 E] {s : Set E} {f : E → β},
  QuasiconvexOn 𝕜 s f ↔
    Convex 𝕜 s ∧
      ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ max (f x) (f y)
-- Init.Data.Vector.Algebra
Vector.getElem_add : ∀ {α : Type u_1} {n : ℕ} [inst : Add α] (xs ys : Vector α n) (i : ℕ) (h : i < n), (xs + ys)[i] = xs[i] + ys[i]
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.cyclesMap.eq_1 : ∀ {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) {i' j' k' : ι} (f' : i' ⟶ j')
  (g' : j' ⟶ k') (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g') (n : ℤ),
  X.cyclesMap f g f' g' α n =
    X.liftCycles f' g' n (n + 1) ⋯
      (CategoryTheory.CategoryStruct.comp (X.iCycles f g n)
        ((X.H n).map (CategoryTheory.ComposableArrows.homMk₁ (α.app 1) (α.app 2) ⋯)))
      ⋯
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- Two equivalent open partial homeomorphisms have the same source.  -/
OpenPartialHomeomorph.EqOnSource.source_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e e' : OpenPartialHomeomorph X Y}, e ≈ e' → e.source = e'.source
-- Mathlib.Data.Nat.Init
Nat.decreasingInduction_self : ∀ {n : ℕ} {motive : (m : ℕ) → m ≤ n → Sort u_1} (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯)
  (self : motive n ⋯), Nat.decreasingInduction of_succ self ⋯ = self
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
/-- a fibration that is a retraction of `i`  -/
HomotopicalAlgebra.FibrantBrownFactorization.r : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {X Y : C} → {f : X ⟶ Y} → (self : HomotopicalAlgebra.FibrantBrownFactorization f) → self.Z ⟶ X
-- Mathlib.CategoryTheory.ObjectProperty.Basic
/-- The strict image of a property of objects by a functor.  -/
CategoryTheory.ObjectProperty.strictMap : {C : Type u} →
  {D : Type u'} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        CategoryTheory.ObjectProperty C → CategoryTheory.Functor C D → CategoryTheory.ObjectProperty D
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.const_add : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : Add γ] [MeasurableAdd γ],
  ProbabilityTheory.IdentDistrib f g μ ν →
    ∀ (c : γ), ProbabilityTheory.IdentDistrib (fun x => c + f x) (fun x => c + g x) μ ν