mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator
PresheafOfModules.toFreeYonedaCoproduct.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (M : PresheafOfModules R),
  M.toFreeYonedaCoproduct =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel M.fromFreeYonedaCoproduct).fromFreeYonedaCoproduct
      (CategoryTheory.Limits.kernel.ι M.fromFreeYonedaCoproduct)
-- Mathlib.Data.Part
Part.pure_eq_some : ∀ {α : Type u_1} (a : α), pure a = Part.some a
-- Lean.MetavarContext
_private.Lean.MetavarContext.0.Lean.DependsOn.main : (Lean.FVarId → Bool) → (Lean.MVarId → Bool) → Lean.Expr → Lean.DependsOn.M✝ Bool
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {fallback : β}
  {f : β → β}, (t.modify k f).getD k fallback = (Option.map f t[k]?).getD fallback
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.instOfSubsingletonCarrierCarrierCommRingCatOfIsIntegral : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [Subsingleton ↥Y] [AlgebraicGeometry.IsIntegral Y],
  AlgebraicGeometry.Flat f
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.mkIso_hom : ∀ {M N : SemiNormedGrp} (f : M ≅ N) (i : (SemiNormedGrp.Hom.hom f.hom).NormNoninc)
  (i' : (SemiNormedGrp.Hom.hom f.inv).NormNoninc),
  (SemiNormedGrp₁.mkIso f i i').hom = SemiNormedGrp₁.mkHom (SemiNormedGrp.Hom.hom f.hom) i
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.sepByNoAntiquot.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Finset.Interval
Finset.Ico_eq_filter_ssubsets : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), Finset.Ico s t = {u ∈ t.ssubsets | s ⊆ u}
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.extend_union : ∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} (P0 : P ∅),
  m ∅ P0 = 0 →
    ∀ (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)),
      (∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)),
          Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) →
        ∀ {s₁ s₂ : Set α},
          Disjoint s₁ s₂ →
            P s₁ → P s₂ → MeasureTheory.extend m (s₁ ∪ s₂) = MeasureTheory.extend m s₁ + MeasureTheory.extend m s₂
-- Mathlib.Data.ZMod.Basic
ZMod.neg_eq_self_iff : ∀ {n : ℕ} (a : ZMod n), -a = a ↔ a = 0 ∨ 2 * a.val = n
-- Init.Data.SInt.Lemmas
ISize.toInt_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toInt = (↑n).bmod ISize.size
-- Lean.Parser.Do
Lean.Parser.Term.doMatchAlts : Lean.Parser.Parser
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.card_top : ∀ (R : Type u_1) [inst : NonAssocRing R] [inst_1 : Fintype R], Fintype.card ↥⊤ = Fintype.card R
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.aeval_bind₁ : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (f : τ → S) (g : σ → MvPolynomial τ R) (φ : MvPolynomial σ R),
  (MvPolynomial.aeval f) ((MvPolynomial.bind₁ g) φ) = (MvPolynomial.aeval fun i => (MvPolynomial.aeval f) (g i)) φ
-- Mathlib.Order.RelSeries
LTSeries.strictMono : ∀ {α : Type u_1} [inst : Preorder α] (x : LTSeries α), StrictMono x.toFun
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.comp_symm_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (e : α ≃+o β) (f : β → α) (g : α → α), g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv_base_pow : ∀ {p : ℕ}, 1 < p → ∀ (k : ℕ), p.maxPowDvdDiv (p ^ k) = (k, 1)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      m.contains k = false → (f (m.get? k)).isNone = true → (↑(m.alter k f)).size = (↑m).size
-- Init.Data.ByteArray.Basic
ByteArray.size_data : ∀ {a : ByteArray}, a.data.size = a.size
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
ModelWithCorners.isInteriorPoint_iff_not_isBoundaryPoint : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] (x : M), I.IsInteriorPoint x ↔ ¬I.IsBoundaryPoint x
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.ModuleHierarchy.mk.sizeOf_spec : ∀ (item : Lean.Lsp.LeanImport) (children : Array Lean.Lsp.Ipc.ModuleHierarchy),
  sizeOf { item := item, children := children } = 1 + sizeOf item + sizeOf children
-- Mathlib.RingTheory.HahnSeries.Multiplication
/-- Extending the domain of Hahn series is an algebra homomorphism.  -/
HahnSeries.embDomainAlgHom : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : PartialOrder Γ] →
        [inst_2 : IsOrderedCancelAddMonoid Γ] →
          [inst_3 : CommSemiring R] →
            {A : Type u_6} →
              [inst_4 : Semiring A] →
                [inst_5 : Algebra R A] →
                  {Γ' : Type u_7} →
                    [inst_6 : AddCommMonoid Γ'] →
                      [inst_7 : PartialOrder Γ'] →
                        [inst_8 : IsOrderedCancelAddMonoid Γ'] →
                          (f : Γ →+ Γ') →
                            Function.Injective ⇑f →
                              (∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g') → HahnSeries Γ A →ₐ[R] HahnSeries Γ' A
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- Auxiliary structure for the definition `OneHypercoverDenseData.sieve`.  -/
CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {X : C} →
                F.OneHypercoverDenseData J₀ J X → {X₀ : C₀} → (F.obj X₀ ⟶ X) → {Y₀ : C₀} → (Y₀ ⟶ X₀) → Type (max v w)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.w₃_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C}
  (h_1 : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.p₃ (CategoryTheory.CategoryStruct.comp f₃ h_1) =
    CategoryTheory.CategoryStruct.comp h.p h_1
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_one : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R], Polynomial.trailingDegree 1 = 0
-- Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating
AlternatingMap.instModuleAddCommGroup : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : AddCommGroup N] →
            [inst_3 : Module R M] → [inst_4 : Module R N] → {ι : Type u_5} → Module R (M [⋀^ι]→ₗ[R] N)
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.compHom.eq_1 : ∀ {M : Type uM} {N : Type uN} {P : Type uP} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P],
  AddMonoidHom.compHom =
    { toFun := fun g => { toFun := g.comp, map_zero' := ⋯, map_add' := ⋯ }, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
/-- If a measure space `X` is generated by an algebra of sets which contains a monotone countable
family of sets with finite measure spanning `X` (thus the measure is `σ`-finite), then this algebra
of sets is measure-dense.  -/
MeasureTheory.Measure.MeasureDense.of_generateFrom_isSetAlgebra_sigmaFinite : ∀ {X : Type u_1} [m : MeasurableSpace X] {μ : MeasureTheory.Measure X} {𝒜 : Set (Set X)},
  MeasureTheory.IsSetAlgebra 𝒜 → ∀ (S : μ.FiniteSpanningSetsIn 𝒜), m = MeasurableSpace.generateFrom 𝒜 → μ.MeasureDense 𝒜
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_int_add' : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddCommGroupWithOne G]
  [inst_2 : AddGroup H] [AddConstMapClass F G H 1 b] (f : F) (n : ℤ) (x : G), f (↑n + x) = f x + n • b
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeExtension.mk : ∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] [inst_1 : Semiring B] [inst_2 : ValuativeRel A]
  [inst_3 : ValuativeRel B] [inst_4 : Algebra A B],
  (∀ (a b : A), (algebraMap A B) a ≤ᵥ (algebraMap A B) b ↔ a ≤ᵥ b) → ValuativeExtension A B
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.HasRightHomology.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C}, Nonempty S.RightHomologyData → S.HasRightHomology
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isSome_max?_iff_isEmpty_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → (t.max?.isSome = true ↔ t.isEmpty = false)
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.norm_add_le_max : ∀ {S : Type u_1} [inst : SeminormedAddGroup S] [IsUltrametricDist S] (x y : S), ‖x + y‖ ≤ max ‖x‖ ‖y‖
-- Mathlib.Data.Num.Basic
/-- `divMod x y = (y / x, y % x)`.  -/
PosNum.divMod : PosNum → PosNum → Num × Num
-- Mathlib.Order.OrderIsoNat
/-- Given an eventually-constant monotone sequence `a₀ ≤ a₁ ≤ a₂ ≤ ...` in a partially-ordered
type, `monotonicSequenceLimitIndex a` is the least natural number `n` for which `aₙ` reaches the
constant value. For sequences that are not eventually constant, `monotonicSequenceLimitIndex a`
is defined, but is a junk value.  -/
monotonicSequenceLimitIndex : {α : Type u_1} → [inst : Preorder α] → (ℕ →o α) → ℕ
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.eqToIso.inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (p : X = Y),
  (CategoryTheory.eqToIso p).inv = CategoryTheory.eqToHom ⋯
-- Mathlib.LinearAlgebra.Finsupp.LSum
LinearMap.splittingOfFinsuppSurjective_splits : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α : Type u_4}
  (f : M →ₗ[R] α →₀ R) (s : Function.Surjective ⇑f), f ∘ₗ f.splittingOfFinsuppSurjective s = LinearMap.id
-- Init.Data.UInt.Bitwise
USize.shiftLeft_and : ∀ {a b c : USize}, (a &&& b) <<< c = a <<< c &&& b <<< c
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- **Alias** of the forward direction of `SimpleGraph.isClique_bot_iff`. -/
SimpleGraph.IsClique.subsingleton : ∀ {α : Type u_1} {s : Set α}, ⊥.IsClique s → s.Subsingleton
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.coe_zero : ∀ {X : Type u_1} [inst : NormedAddCommGroup X] {M : Type u_2} [inst_1 : Ring M] [inst_2 : Module M X], ↑0 = 0
-- Mathlib.Topology.Algebra.Constructions
/-- An auxiliary lemma that can be used to prove that coercion `Mˣ → M` is a topological embedding.
Use `Units.isEmbedding_val₀`, `Units.isEmbedding_val`, or `toUnits_homeomorph` instead.  -/
Units.embedding_val_mk : ∀ {M : Type u_4} [inst : DivisionMonoid M] [inst_1 : TopologicalSpace M],
  ContinuousOn Inv.inv {x | IsUnit x} → Topology.IsEmbedding Units.val
-- Mathlib.Data.List.Permutation
List.perm_permutations_iff : ∀ {α : Type u_1} {s t : List α}, s.permutations.Perm t.permutations ↔ s.Perm t
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- A restatement of `sum_ite_eq` with the equality test reversed.  -/
Finsupp.sum_ite_eq' : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : AddCommMonoid N] [inst_2 : DecidableEq α]
  (f : α →₀ M) (a : α) (b : α → M → N),
  (f.sum fun x v => if x = a then b x v else 0) = if a ∈ f.support then b a (f a) else 0
-- Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
/-- A smooth function of manifolds `f : M → N` induces a morphism of locally ringed spaces.  -/
ChartedSpace.locallyRingedSpaceMap : {𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_1} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_2} →
            [inst_3 : TopologicalSpace HM] →
              {IM : ModelWithCorners 𝕜 EM HM} →
                {M : Type u} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace HM M] →
                      {EN : Type u_3} →
                        [inst_6 : NormedAddCommGroup EN] →
                          [inst_7 : NormedSpace 𝕜 EN] →
                            {HN : Type u_4} →
                              [inst_8 : TopologicalSpace HN] →
                                {IN : ModelWithCorners 𝕜 EN HN} →
                                  {N : Type u} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace HN N] →
                                        (f : M → N) →
                                          ContMDiff IM IN (↑⊤) f →
                                            (ChartedSpace.locallyRingedSpace IM M ⟶
                                              ChartedSpace.locallyRingedSpace IN N)
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.isRoot_geom_sum : ∀ {R : Type u_4} {k : ℕ} [inst : CommRing R] [IsDomain R] {ζ : R},
  IsPrimitiveRoot ζ k → 1 < k → (∑ i ∈ Finset.range k, Polynomial.X ^ i).IsRoot ζ
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unmop_hom_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.unmop =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.unmop).hom
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (R : Type u_1)
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] (K L : CochainComplex C ℤ) (n a n' : ℤ) (hn' : n' + a = n)
  (a_1 : CochainComplex.HomComplex.Cochain K L n),
  (CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv R K L n a n' hn') a_1 = a_1.rightShift a n' hn'
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.neg : Lean.Meta.Grind.Arith.Linear.EqCnstr → Lean.Meta.Grind.Arith.Linear.EqCnstrProof
-- Mathlib.Algebra.Order.AddTorsor
IsOrderedCancelSMul.mk : ∀ {G : Type u_3} {P : Type u_4} [inst : LE G] [inst_1 : LE P] [inst_2 : SMul G P] [toIsOrderedSMul : IsOrderedSMul G P],
  (∀ (a : G) (b c : P), a • b ≤ a • c → b ≤ c) → (∀ (a b : G) (c : P), a • c ≤ b • c → a ≤ b) → IsOrderedCancelSMul G P
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.unop_iSup : ∀ {ι : Sort u_1} {R : Type u_2} [inst : NonAssocRing R] (S : ι → Subring Rᵐᵒᵖ), (iSup S).unop = ⨆ i, (S i).unop
-- Mathlib.NumberTheory.ModularForms.LFunction
ModularForm.hasSum_Λ : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.IsArithmetic] {k : ℤ} (hk : 0 < k) {F : Type u_1}
  [inst_1 : FunLike F UpperHalfPlane ℂ] (f : F) {s : ℂ} [inst_2 : ModularFormClass F Γ k],
  ↑k + 1 < s.re →
    HasSum
      (fun n =>
        ↑Real.pi ^ (-s) * Complex.Gamma s * (PowerSeries.coeff n) (UpperHalfPlane.qExpansion Γ.strictWidthInfty ⇑f) /
          ↑(2 * ↑n / Γ.strictWidthInfty) ^ s)
      (ModularForm.Λ hk f s)
-- Init.Data.SInt.Lemmas
Int64.le_refl : ∀ (a : Int64), a ≤ a
-- Mathlib.Data.ENNReal.BigOperators
/-- **Alias** of `ENNReal.ofNNReal_finsetProd`. -/
ENNReal.coe_finset_prod : ∀ {ι : Type u_1} (s : Finset ι) (f : ι → NNReal), ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_affine_Icc' : ∀ {K : Type u_2} [inst : DivisionSemiring K] [inst_1 : PartialOrder K] [PosMulReflectLT K] [IsOrderedCancelAddMonoid K]
  [ExistsAddOfLE K] {a : K},
  0 < a → ∀ (b c d : K), (fun x => a * x + b) '' Set.Icc c d = Set.Icc (a * c + b) (a * d + b)
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_eq_zero : ∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℝ), ↑g 1 0 = 0 → ∃ u v, (fun x => g • x) = (fun x => v +ᵥ x) ∘ fun x => u • x
-- Mathlib.Data.EReal.Inv
/-- Extension for the `positivity` tactic: ratio of two `EReal`s.  -/
Mathlib.Meta.Positivity.evalERealDiv : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.Order.WellFoundedSet
Set.partiallyWellOrderedOn_iff_finite_antichains : ∀ {α : Type u_2} {r : α → α → Prop} {s : Set α} [Std.Refl r] [Std.Symm r],
  s.PartiallyWellOrderedOn r ↔ ∀ t ⊆ s, IsAntichain r t → t.Finite
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.instNonemptyInfinitePlaceOfRingHomComplex : ∀ (K : Type u_1) [inst : Field K] [Nonempty (K →+* ℂ)], Nonempty (NumberField.InfinitePlace K)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp),
  t = t_1 → ∀ (fallback fallback_1 : α), fallback = fallback_1 → t.minKeyD fallback = t_1.minKeyD fallback_1
-- Mathlib.RingTheory.Noetherian.Defs
isNoetherianRing_iff : ∀ {R : Type u_1} [inst : Semiring R], IsNoetherianRing R ↔ IsNoetherian R R
-- Mathlib.Order.Filter.Pointwise
/-- The filter `f / g` is generated by `{s / t | s ∈ f, t ∈ g}` in scope `Pointwise`.  -/
Filter.instDiv : {α : Type u_2} → [Div α] → Div (Filter α)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k fallback : α}, k ∉ m₁ → (m₁ ∪ m₂).getD k fallback = m₂.getD k fallback
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSpanningSubgraph.trans : ∀ {α : Type u_1} {β : Type u_2} {G G₁ G₂ : Graph α β}, G ≤s G₁ → G₁ ≤s G₂ → G ≤s G₂
-- Mathlib.Algebra.Order.Monovary
Monovary.pow_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : CommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedMonoid β] {f : ι → α} {g : ι → β}, Monovary f g → ∀ (n : ℕ), Monovary f (g ^ n)
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.of_forall_mem_unit_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [LawfulBEq α] {m₁ m₂ : Std.HashMap α Unit},
  (∀ (k : α), k ∈ m₁ ↔ k ∈ m₂) → m₁.Equiv m₂
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.QuasiMeasurePreserving.snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {τ : MeasureTheory.Measure γ}
  {f : α → β × γ},
  MeasureTheory.Measure.QuasiMeasurePreserving f μ (ν.prod τ) →
    MeasureTheory.Measure.QuasiMeasurePreserving (fun x => (f x).2) μ τ
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.map_pure : ∀ {α β : Type u} (f : α → β) (x : α), f <$> pure x = pure (f x)
-- Mathlib.Data.Set.Lattice
Set.iInter_sum : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : α ⊕ β → Set γ}, ⋂ x, s x = (⋂ x, s (Sum.inl x)) ∩ ⋂ x, s (Sum.inr x)
-- Std.Data.DHashMap.Basic
/-- Returns an array of all keys present in the hash map in some order.  -/
Std.DHashMap.keysArray : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → Array α
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
/-- When `e₁` and `e₂` are complementary embeddings of complex shapes, with
`e₁.IsTruncLE` and `e₂.IsTruncGE`, then this is the canonical quasi-isomorphism
`(K.shortComplexTruncLE e₁).X₃ ⟶ K.truncGE e₂` where
`(K.shortComplexTruncLE e₁).X₃` is the cokernel of `K.ιTruncLE e₁ : K.truncLE e₁ ⟶ K`.  -/
HomologicalComplex.shortComplexTruncLEX₃ToTruncGE : {ι : Type u_1} →
  {ι₁ : Type u_2} →
    {ι₂ : Type u_3} →
      {c : ComplexShape ι} →
        {c₁ : ComplexShape ι₁} →
          {c₂ : ComplexShape ι₂} →
            {C : Type u_4} →
              [inst : CategoryTheory.Category.{v_1, u_4} C] →
                [inst_1 : CategoryTheory.Abelian C] →
                  (K : HomologicalComplex C c) →
                    {e₁ : c₁.Embedding c} →
                      {e₂ : c₂.Embedding c} →
                        [inst_2 : e₁.IsTruncLE] →
                          [inst_3 : e₂.IsTruncGE] →
                            e₁.AreComplementary e₂ → ((K.shortComplexTruncLE e₁).X₃ ⟶ K.truncGE e₂)
-- Mathlib.NumberTheory.RamificationInertia.Galois
Ideal.coe_smul_primesOver_eq_map_galRestrict : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {p : Ideal A}
  (K : Type u_4) (L : Type u_5) [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K]
  [inst_6 : IsFractionRing A K] [inst_7 : Algebra B L] [inst_8 : Algebra K L] [inst_9 : Algebra A L]
  [inst_10 : IsScalarTower A B L] [inst_11 : IsScalarTower A K L] [inst_12 : IsIntegralClosure B A L]
  [inst_13 : FiniteDimensional K L] (σ : Gal(L/K)) (P : ↑(p.primesOver B)),
  ↑(σ • P) = Ideal.map ((galRestrict A K L B) σ) ↑P
-- Mathlib.Algebra.Module.Basic
Set.indicator_const_smul : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : SMulZeroClass R M] (s : Set α) (r : R)
  (f : α → M), (s.indicator fun x => r • f x) = fun x => r • s.indicator f x
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- If `s ⊆ fixedBy α g`, then `g +ᵥ s = s`, which means that `s ∈ fixedBy (Set α) g`.

Note that the reverse implication is in general not true, as `s ∈ fixedBy (Set α) g` is a
weaker statement (it allows for points `x ∈ s` for which `g +ᵥ x ≠ x` and `g +ᵥ x ∈ s`).  -/
AddAction.set_mem_fixedBy_of_subset_fixedBy : ∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {s : Set α} {g : G},
  s ⊆ AddAction.fixedBy α g → s ∈ AddAction.fixedBy (Set α) g
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- **Alias** of `FunLike.coe_zero`. -/
SlashInvariantForm.coe_zero : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Zero β]
  [IsZeroApply F α β], ⇑0 = 0
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.instCompleteLattice : {C : Type u} → [inst : CategoryTheory.Groupoid C] → CompleteLattice (CategoryTheory.Subgroupoid C)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.continuousOn_ofComplex_I_mul : ContinuousOn (fun t => ↑UpperHalfPlane.ofComplex (↑UpperHalfPlane.I * ↑t)) (Set.Ioi 0)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- A base angle of an isosceles triangle is acute, oriented angle-at-point form.  -/
EuclideanGeometry.abs_oangle_right_toReal_lt_pi_div_two_of_dist_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P}, dist p₁ p₂ = dist p₁ p₃ → |(EuclideanGeometry.oangle p₁ p₂ p₃).toReal| < Real.pi / 2
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  (CategoryTheory.kernelCokernelCompSequence.snakeInput f g).L₀.f =
    CategoryTheory.Limits.kernel.map f (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id X) g ⋯
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCircuit.mk : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.IsTrail → p ≠ SimpleGraph.Walk.nil → p.IsCircuit
-- Mathlib.Algebra.GroupWithZero.Defs
/-- `a ^ (n + 1) = a ^ n * a`  -/
GroupWithZero.zpow_succ' : ∀ {G₀ : Type u} [self : GroupWithZero G₀] (n : ℕ) (a : G₀), a ^ ↑n.succ = a ^ ↑n * a
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- A version of `Matroid.contract_spanning_iff` without the ground-set hypothesis.  -/
Matroid.contract_spanning_iff' : ∀ {α : Type u_1} {M : Matroid α} {X C : Set α}, (M.contract C).Spanning X ↔ M.Spanning (X ∪ C ∩ M.E) ∧ Disjoint X C