mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.fromLocalizedModule'_smul : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] (r : R) (x : LocalizedModule S M),
  r • IsLocalizedModule.fromLocalizedModule' S f x = IsLocalizedModule.fromLocalizedModule' S f (r • x)
-- Mathlib.Order.Filter.Ultrafilter.Defs
/-- An ultrafilter is nontrivial.  -/
Ultrafilter.neBot' : ∀ {α : Type u_2} (self : Ultrafilter α), (↑self).NeBot
-- Init.Data.Vector.Lemmas
Vector.getElem?_set_self : ∀ {α : Type u_1} {n i : ℕ} {xs : Vector α n} {x : α} (hi : i < n), (xs.set i x hi)[i]? = some x
-- Std.Http.Data.Status
Std.Http.Status.conflict.sizeOf_spec : sizeOf Std.Http.Status.conflict = 1
-- Mathlib.Analysis.Seminorm
Seminorm.uniformSpace_eq_of_hasBasis : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {ι : Sort u_12} [inst_3 : UniformSpace E] [IsUniformAddGroup E] [ContinuousConstSMul 𝕜 E] {p' : ι → Prop}
  {s : ι → Set E} (p : Seminorm 𝕜 E),
  (nhds 0).HasBasis p' s →
    (∃ r, p.closedBall 0 r ∈ nhds 0) →
      (∀ (i : ι), p' i → ∃ r > 0, p.ball 0 r ⊆ s i) → inst_3 = PseudoMetricSpace.toUniformSpace
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_himp_le_meet : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P' Q' : l}
  [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.PartialOrder.rel (Lean.Order.meet P' (Lean.Order.himp P' Q')) (Lean.Order.meet P' Q')
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.functorPullback_map_functorPullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X : C} (R : CategoryTheory.Presieve (F.obj X)),
  CategoryTheory.Presieve.functorPullback F
      (CategoryTheory.Presieve.map F (CategoryTheory.Presieve.functorPullback F R)) =
    CategoryTheory.Presieve.functorPullback F R
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.term.inj : ∀ {i i_1 : Lean.Term}, Aesop.Frontend.Feature.term i = Aesop.Frontend.Feature.term i_1 → i = i_1
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Projective.π_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.EnoughProjectives C] (X : C),
  CategoryTheory.Epi (CategoryTheory.Projective.π X)
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.zipWithLeft'TR.go.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      (motive : List α → List β → Array γ → Sort u_4) →
        (x : List α) →
          (x_1 : List β) →
            (x_2 : Array γ) →
              ((bs : List β) → (acc : Array γ) → motive [] bs acc) →
                ((as : List α) → (acc : Array γ) → (as = [] → False) → motive as [] acc) →
                  ((a : α) →
                      (as : List α) → (b : β) → (bs : List β) → (acc : Array γ) → motive (a :: as) (b :: bs) acc) →
                    motive x x_1 x_2
-- Batteries.Logic
funext₂ : ∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {f g : (a : α) → (b : β a) → γ a b},
  (∀ (a : α) (b : β a), f a b = g a b) → f = g
-- Init.Data.Nat.Basic
Nat.sub_eq_iff_eq_add' : ∀ {b a c : ℕ}, b ≤ a → (a - b = c ↔ a = b + c)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.le_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {k : α}, (cmp k t.min!).isLE = true ↔ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.NumberTheory.Dioph
Poly.instAdd : {α : Type u_1} → Add (Poly α)
-- Mathlib.MeasureTheory.Measure.Support
/-- A point `x` lies outside the support of `μ` iff all of the subsets of one of its neighborhoods
have measure zero.  -/
MeasureTheory.Measure.notMem_support_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X} {x : X},
  x ∉ μ.support ↔ ∀ᶠ (u : Set X) in (nhds x).smallSets, μ u = 0
-- Mathlib.Algebra.Order.Star.Basic
conjugate_le_conjugate_of_nonneg : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {a b : R}, a ≤ b → ∀ {c : R}, 0 ≤ c → c * a * c ≤ c * b * c
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.LocalizerMorphism.commShift_iso_hom_app_assoc : ∀ {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₂) {M : Type u_3}
  [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C₁ M] [inst_4 : CategoryTheory.HasShift C₂ M]
  [inst_5 : Φ.functor.CommShift M] {D₁ : Type u_4} {D₂ : Type u_5} [inst_6 : CategoryTheory.Category.{v_3, u_4} D₁]
  [inst_7 : CategoryTheory.Category.{v_4, u_5} D₂] (L₁ : CategoryTheory.Functor C₁ D₁) [inst_8 : L₁.IsLocalization W₁]
  (L₂ : CategoryTheory.Functor C₂ D₂) [inst_9 : CategoryTheory.HasShift D₁ M] [inst_10 : CategoryTheory.HasShift D₂ M]
  [inst_11 : L₁.CommShift M] [inst_12 : L₂.CommShift M] (G : CategoryTheory.Functor D₁ D₂)
  (e : Φ.functor.comp L₂ ≅ L₁.comp G) (m : M) (X : C₁) {Z : D₂}
  (h : (CategoryTheory.shiftFunctor D₂ m).obj (G.obj (L₁.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso G m).hom.app (L₁.obj X)) h =
    CategoryTheory.CategoryStruct.comp (G.map ((CategoryTheory.Functor.commShiftIso L₁ m).inv.app X))
      (CategoryTheory.CategoryStruct.comp (e.inv.app ((CategoryTheory.shiftFunctor C₁ m).obj X))
        (CategoryTheory.CategoryStruct.comp (L₂.map ((CategoryTheory.Functor.commShiftIso Φ.functor m).hom.app X))
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso L₂ m).hom.app (Φ.functor.obj X))
            (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D₂ m).map (e.hom.app X)) h))))
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.ofLeftInverse.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {g : N →+ G}
  (h : Function.LeftInverse ⇑g ⇑f),
  AddMonoidHom.ofLeftInverse h =
    { toFun := ⇑f.rangeRestrict, invFun := ⇑g ∘ ⇑f.range.subtype, left_inv := h, right_inv := ⋯, map_add' := ⋯ }
-- Init.Data.List.Basic
/-- Constructs a single-element list.

Examples:
* `List.singleton 5 = [5]`.
* `List.singleton "green" = ["green"]`.
* `List.singleton [1, 2, 3] = [[1, 2, 3]]`
 -/
List.singleton : {α : Type u} → α → List α
-- Mathlib.Algebra.Module.Submodule.Map
/-- `map f` and `comap f` form a `GaloisInsertion` when `f` is surjective.  -/
Submodule.giMapComap : {R : Type u_1} →
  {R₂ : Type u_3} →
    {M : Type u_5} →
      {M₂ : Type u_7} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R₂ M₂] →
                    {σ₁₂ : R →+* R₂} →
                      [inst_6 : RingHomSurjective σ₁₂] →
                        {f : M →ₛₗ[σ₁₂] M₂} →
                          Function.Surjective ⇑f → GaloisInsertion (Submodule.map f) (Submodule.comap f)
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.isExample : Array Lean.Elab.DefView → Bool
-- Mathlib.Logic.Basic
/-- A version of `byContradiction` that uses types instead of propositions.  -/
Classical.byContradiction' : {α : Sort u_2} → (¬∀ (a : α), False) → α
-- Lean.LocalContext
Lean.LocalDeclKind.ofNat : ℕ → Lean.LocalDeclKind
-- Mathlib.LinearAlgebra.RootSystem.Reduced
/-- See also `RootPairing.linearIndependent_iff_coxeterWeightIn_ne_four`.  -/
RootPairing.linearIndependent_iff_coxeterWeight_ne_four : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) {i j : ι} [Finite ι]
  [CharZero R] [IsDomain R] [Module.IsTorsionFree R M],
  LinearIndependent R ![P.root i, P.root j] ↔ P.coxeterWeight i j ≠ 4
-- Mathlib.Order.Partition.Basic
Partition.rel_iff_partOf_eq_partOf : ∀ {α : Type u_1} {x y : α} {u : Set α} (P : Partition u), P.Rel x y ↔ ∃ (_ : x ∈ u) (_ : y ∈ u), P.partOf x = P.partOf y
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
TProd.instMeasurableSpace : {δ : Type u_4} →
  (X : δ → Type u_6) → [(i : δ) → MeasurableSpace (X i)] → (l : List δ) → MeasurableSpace (List.TProd X l)
-- Mathlib.Analysis.Calculus.ContDiff.Convolution
/-- The convolution `g * f` is `C^n` when `f` is locally integrable and `g` is `C^n` and compactly
supported. Version where `g` depends on an additional parameter in an open subset `s` of a
parameter space `P` (and the compact support `k` is independent of the parameter in `s`).  -/
MeasureTheory.contDiffOn_convolution_left_with_param : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} {P : Type uP} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] [inst_3 : RCLike 𝕜] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F] [inst_8 : MeasurableSpace G]
  [inst_9 : NormedAddCommGroup G] [BorelSpace G] [inst_11 : NormedSpace 𝕜 G] [inst_12 : NormedAddCommGroup P]
  [inst_13 : NormedSpace 𝕜 P] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] [μ.IsNegInvariant]
  (L : E' →L[𝕜] E →L[𝕜] F) {f : G → E} {n : ℕ∞} {g : P → G → E'} {s : Set P} {k : Set G},
  IsOpen s →
    IsCompact k →
      (∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0) →
        MeasureTheory.LocallyIntegrable f μ →
          ContDiffOn 𝕜 (↑n) (↿g) (s ×ˢ Set.univ) →
            ContDiffOn 𝕜 (↑n) (fun q => MeasureTheory.convolution (g q.1) f L μ q.2) (s ×ˢ Set.univ)
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroup.setoid : (R : Type u_1) → [Rack R] → Setoid (Rack.PreEnvelGroup R)
-- Mathlib.NumberTheory.Primorial
primorial_lt_four_pow : ∀ (n : ℕ), n ≠ 0 → primorial n < 4 ^ n
-- Mathlib.GroupTheory.OrderOfElement
coe_smulCardAddSubgroup : ∀ {G : Type u_6} [inst : AddGroup G] [inst_1 : Fintype G] (S : Set G) (hS : S.Nonempty),
  ↑(smulCardAddSubgroup S hS) = Fintype.card G • S
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `f'` is nonpositive, then
`f` is an antitone function on `D`.  -/
antitoneOn_of_hasDerivWithinAt_nonpos : ∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f f' : ℝ → ℝ},
      ContinuousOn f D →
        (∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x) → (∀ x ∈ interior D, f' x ≤ 0) → AntitoneOn f D
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Subgroup.npow_mem_zpowers : ∀ {G : Type u_1} [inst : Group G] (g : G) (k : ℕ), g ^ k ∈ Subgroup.zpowers g
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_ofNatTruncate_of_le : ∀ {n : ℕ},
  UInt64.size ≤ n →
    (UInt64.ofNatClamp n).toUInt32 = UInt32.ofNatLT (UInt32.size - 1) UInt64.toUInt32_ofNatClamp_of_le._proof_1
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.toRatVec : {ι : Type u_3} → (ι → ℕ) →+ ι → ℚ
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
MvPowerSeries.WithPiTopology.hasSum_iff_hasSum_coeff : ∀ {σ : Type u_1} {R : Type u_2} [inst : TopologicalSpace R] [inst_1 : Semiring R] {ι : Type u_3}
  {f : ι → MvPowerSeries σ R} {g : MvPowerSeries σ R},
  HasSum f g ↔ ∀ (d : σ →₀ ℕ), HasSum (fun i => (MvPowerSeries.coeff d) (f i)) ((MvPowerSeries.coeff d) g)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.condIndepSet_iff_condIndep : ∀ {Ω : Type u_1} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] (hm' : m' ≤ mΩ)
  (s t : Set Ω) (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.CondIndepSet m' hm' s t μ ↔
    ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom {s}) (MeasurableSpace.generateFrom {t}) hm' μ
-- Mathlib.Topology.UniformSpace.Dini
/-- **Dini's theorem**: if `F n` is a monotone increasing collection of continuous functions on a
compact set `s` converging pointwise to a continuous function `f`, then `F n` converges uniformly
to `f`.  -/
Monotone.tendstoUniformlyOn_of_forall_tendsto : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : NormedAddCommGroup G] [inst_3 : Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → α → G}
  {f : α → G} {s : Set α},
  IsCompact s →
    (∀ (i : ι), ContinuousOn (F i) s) →
      (∀ x ∈ s, Monotone fun x_1 => F x_1 x) →
        ContinuousOn f s →
          (∀ x ∈ s, Filter.Tendsto (fun x_1 => F x_1 x) Filter.atTop (nhds (f x))) →
            TendstoUniformlyOn F f Filter.atTop s
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.varsToConstants.match_1.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u_3} {γ : Type u_4} (motive : L.Term (γ ⊕ α) → Sort u_5) (c : γ)
  (h_1 : (a : α) → motive (FirstOrder.Language.var (Sum.inr a)))
  (h_2 : (c : γ) → motive (FirstOrder.Language.var (Sum.inl c)))
  (h_3 : (l : ℕ) → (f : L.Functions l) → (ts : Fin l → L.Term (γ ⊕ α)) → motive (FirstOrder.Language.func f ts)),
  (match FirstOrder.Language.var (Sum.inl c) with
    | FirstOrder.Language.var (Sum.inr a) => h_1 a
    | FirstOrder.Language.var (Sum.inl c) => h_2 c
    | FirstOrder.Language.func f ts => h_3 l f ts) =
    h_2 c
-- Mathlib.Order.WellQuasiOrder
wellQuasiOrdered_iff_exists_monotone_subseq : ∀ {α : Type u_1} {r : α → α → Prop} [IsPreorder α r],
  WellQuasiOrdered r ↔ ∀ (f : ℕ → α), ∃ g, ∀ (m n : ℕ), m ≤ n → r (f (g m)) (f (g n))
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.volume_preserving_piFinsetUnion : ∀ {ι : Type u_4} [inst : DecidableEq ι] (α : ι → Type u_5) {s t : Finset ι} (h : Disjoint s t)
  [inst_1 : (i : ι) → MeasureTheory.MeasureSpace (α i)] [∀ (i : ι), MeasureTheory.SigmaFinite MeasureTheory.volume],
  MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.piFinsetUnion α h)) MeasureTheory.volume MeasureTheory.volume
-- Lean.Data.Json.Basic
Lean.JsonNumber.mk.injEq : ∀ (mantissa : ℤ) (exponent : ℕ) (mantissa_1 : ℤ) (exponent_1 : ℕ),
  ({ mantissa := mantissa, exponent := exponent } = { mantissa := mantissa_1, exponent := exponent_1 }) =
    (mantissa = mantissa_1 ∧ exponent = exponent_1)
-- Mathlib.Data.NNReal.Defs
NNReal.exists_mem_Ioc_zpow : ∀ {x y : NNReal}, x ≠ 0 → 1 < y → ∃ n, x ∈ Set.Ioc (y ^ n) (y ^ (n + 1))
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.natDegree_map : ∀ {R : Type u} {S : Type v} [inst : Ring R] [IsSimpleRing R] [inst_2 : Semiring S] [Nontrivial S] {p : Polynomial R}
  (f : R →+* S), (Polynomial.map f p).natDegree = p.natDegree
-- Mathlib.LinearAlgebra.FreeModule.PID
Submodule.smithNormalFormBotBasis_def : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsDomain R] [inst_4 : IsPrincipalIdealRing R] {N : Submodule R M} [inst_5 : Finite ι]
  (b : Module.Basis ι R M) (h : Module.finrank R ↥N = Module.finrank R M) (i : ι),
  ↑((Submodule.smithNormalFormBotBasis b h) i) =
    Submodule.smithNormalFormCoeffs b h i • (Submodule.smithNormalFormTopBasis b h) i
-- Mathlib.NumberTheory.NumberField.Discriminant.Defs
NumberField.discr_ne_zero : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], NumberField.discr K ≠ 0
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_eq_extractLsb' : ∀ {v : ℕ} {x : BitVec v} {w : ℕ}, w ≤ v → BitVec.setWidth w x = BitVec.extractLsb' 0 w x
-- Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Matrix.IsPrimitive.nonneg : ∀ {n : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : Fintype n] [inst_3 : DecidableEq n]
  {A : Matrix n n R}, A.IsPrimitive → ∀ (i j : n), 0 ≤ A i j
-- Init.System.IO
/-- The current state of a `Task` in the Lean runtime's task manager.  -/
IO.TaskState : Type
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_inter_inv_smul : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) (s t : Set α),
  μ (s ∩ c⁻¹ • t) = μ (c • s ∩ t)
-- Mathlib.NumberTheory.Padics.RingHoms
/-- One part of the universal property of `ℤ_[p]` as a projective limit.
See also `PadicInt.lift_spec`.
 -/
PadicInt.lift_unique : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)]
  (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1) (g : R →+* ℤ_[p]),
  (∀ (n : ℕ), (PadicInt.toZModPow n).comp g = f n) → PadicInt.lift f_compat = g
-- Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
AddMonoidHom.coe_finsetSum : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] (f : ι → M →+ N)
  (s : Finset ι), ⇑(∑ x ∈ s, f x) = ∑ x ∈ s, ⇑(f x)
-- Mathlib.RingTheory.Kaehler.JacobiZariski
/-- Given algebras $R \to S \to T$ and $T$ flat over $S$, the sequence
$T \otimes_S H_1(L_{S/R}) \to H_1(L_{T/R}) \to H_1(L_{T/S})$
is exact.  -/
Algebra.H1Cotangent.exact_liftBaseChange_map_of_flat : ∀ (R : Type u₁) (S : Type u₂) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u₃)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] [Module.Flat S T],
  Function.Exact ⇑(LinearMap.liftBaseChange T (Algebra.H1Cotangent.map R R S T)) ⇑(Algebra.H1Cotangent.map R S T T)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.HomotopyWith.apply_one : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  {P : C(X, Y) → Prop} (F : f₀.HomotopyWith f₁ P) (x : X), F (1, x) = f₁ x
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.ThinSkeleton.fromThinSkeleton_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : Quiver.IsThin C]
  {x y : CategoryTheory.ThinSkeleton C} (a : x ⟶ y),
  (CategoryTheory.ThinSkeleton.fromThinSkeleton C).map a =
    Quotient.recOnSubsingleton₂ (motive := fun x x_1 => (x ⟶ x_1) → (Quotient.out x ⟶ Quotient.out x_1)) x y
      (fun X Y f =>
        CategoryTheory.CategoryStruct.comp (Nonempty.some ⋯).hom
          (CategoryTheory.CategoryStruct.comp (Nonempty.some ⋯) (Nonempty.some ⋯).inv))
      a
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.pullback_to_base_isOpenImmersion : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) (g : Y ⟶ Z)
  [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  [inst : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion g],
  AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion
    (CategoryTheory.Limits.limit.π (CategoryTheory.Limits.cospan f g) CategoryTheory.Limits.WalkingCospan.one)
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.left_unit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (self : CategoryTheory.Monad C) (X : C),
  CategoryTheory.CategoryStruct.comp (self.η.app (self.obj X)) (self.μ.app X) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).obj (self.obj X))
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.relNorm_mono : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S] {I J : Ideal S},
  I ≤ J → (Ideal.relNorm R) I ≤ (Ideal.relNorm R) J
-- Init.Data.Nat.Basic
Nat.lt_iff_le_and_not_ge : ∀ {m n : ℕ}, m < n ↔ m ≤ n ∧ ¬n ≤ m
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.SearchStep.rejected.sizeOf_spec : ∀ {s : String.Slice} (startPos endPos : s.Pos),
  sizeOf (String.Slice.Pattern.SearchStep.rejected startPos endPos) = 1 + sizeOf startPos + sizeOf endPos
-- Mathlib.Topology.ContinuousMap.Star
ContinuousMap.coe_star : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Star β]
  [inst_3 : ContinuousStar β] (f : C(α, β)), ⇑(star f) = star ⇑f
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso_inv_comp_rightHomologyι_assoc : ∀ {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) [inst_2 : S.HasRightHomology] {Z : C}
  (h_1 : S.opcycles ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.rightHomologyIso.inv (CategoryTheory.CategoryStruct.comp S.rightHomologyι h_1) =
    CategoryTheory.CategoryStruct.comp h.ι (CategoryTheory.CategoryStruct.comp h.opcyclesIso.inv h_1)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
/-- Pull an opposite submonoid back to a submonoid along `MulOpposite.op`  -/
Submonoid.unop : {M : Type u_2} → [inst : MulOneClass M] → Submonoid Mᵐᵒᵖ → Submonoid M
-- Mathlib.Algebra.GroupWithZero.Units.Basic
GroupWithZero.noZeroDivisors : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀], NoZeroDivisors G₀
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.HomologySequence.exact₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C))
  (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (n₀ n₁ : ℤ)
  (h : autoParam (n₀ + 1 = n₁) DerivedCategory.HomologySequence.exact₁._auto_1),
  { X₁ := (DerivedCategory.homologyFunctor C n₀).obj T.obj₃, X₂ := (DerivedCategory.homologyFunctor C n₁).obj T.obj₁,
      X₃ := (DerivedCategory.homologyFunctor C n₁).obj T.obj₂, f := DerivedCategory.HomologySequence.δ T n₀ n₁ h,
      g := (DerivedCategory.homologyFunctor C n₁).map T.mor₁, zero := ⋯ }.Exact
-- Mathlib.Order.Interval.Set.Basic
Set.notMem_Icc_of_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, c < a → c ∉ Set.Icc a b
-- Init.Data.Option.Attach
Option.attachWith_none : ∀ {α : Type u_1} {P : α → Prop} {H : ∀ (x : α), none = some x → P x}, none.attachWith P H = none
-- Std.Http.Data.Status
Std.Http.Status.switchingProtocols.sizeOf_spec : sizeOf Std.Http.Status.switchingProtocols = 1
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The snake input in the opposite category that is deduced from a snake input.  -/
CategoryTheory.ShortComplex.SnakeInput.op : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CategoryTheory.ShortComplex.SnakeInput C → CategoryTheory.ShortComplex.SnakeInput Cᵒᵖ
-- Lean.Meta.Sym.Simp.SimpM
/-- Simplified to `e'` with proof `proof : e = e'`.
If `done = true`, skip recursive simplification of `e'`.  -/
Lean.Meta.Sym.Simp.Result.step : Lean.Expr → Lean.Expr → optParam Bool false → optParam Bool false → Lean.Meta.Sym.Simp.Result
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_leftUnitor_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {X Y : C}
  (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) (g : X ⟶ Y) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom h) =
    CategoryTheory.CategoryStruct.comp g h
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.opEquiv_apply : ∀ {M : Type u_2} [inst : Mul M] (x : Subsemigroup M), Subsemigroup.opEquiv x = x.op
-- Mathlib.Control.Monad.Cont
MonadCont.goto : {α : Type u_1} → {β : Type u} → {m : Type u → Type v} → MonadCont.Label α m β → α → m β