mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.opowAux2.match_3.eq_3 : ∀ (motive : ONote × ℕ → Sort u_1) (m : ℕ) (h_1 : Unit → motive (ONote.zero, 0)) (h_2 : Unit → motive (ONote.zero, 1))
  (h_3 : (m : ℕ) → motive (ONote.zero, m.succ))
  (h_4 : (a a0 : ONote) → (a_1 : ℕ+) → (a_2 : ONote) → a = a0.oadd a_1 a_2 → (m : ℕ) → motive (a0.oadd a_1 a_2, m)),
  (m = 0 → False) →
    (match (ONote.zero, m.succ) with
      | (ONote.zero, 0) => h_1 ()
      | (ONote.zero, 1) => h_2 ()
      | (ONote.zero, m.succ) => h_3 m
      | (a@h:(a0.oadd a_1 a_2), m) => h_4 a a0 a_1 a_2 h m) =
      h_3 m
-- Mathlib.Data.TypeVec
/-- turn an equality into an arrow  -/
TypeVec.Arrow.mp : {n : ℕ} → {α β : TypeVec.{u_1} n} → α = β → α.Arrow β
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Suggest merging two adjacent `rw` tactics if that also solves the goal.  -/
linter.tacticAnalysis.rwMerge : Lean.Option Bool
-- Mathlib.Algebra.MvPolynomial.Derivation
/-- If two derivations agree on `X i`, `i ∈ s`, then they agree on all polynomials from
`MvPolynomial.supported R s`.  -/
MvPolynomial.derivation_eqOn_supported : ∀ {σ : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Module (MvPolynomial σ R) A] {D₁ D₂ : Derivation R (MvPolynomial σ R) A} {s : Set σ},
  Set.EqOn (⇑D₁ ∘ MvPolynomial.X) (⇑D₂ ∘ MvPolynomial.X) s →
    ∀ {f : MvPolynomial σ R}, f ∈ MvPolynomial.supported R s → D₁ f = D₂ f
-- Mathlib.Data.String.Lemmas
String.length_eq_list_length : ∀ (l : List Char), (String.ofList l).length = l.length
-- Mathlib.Data.Set.Countable
Set.exists_seq_iSup_eq_top_iff_countable : ∀ {α : Type u} [inst : CompleteLattice α] {p : α → Prop},
  (∃ x, p x) → ((∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤) ↔ ∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.algebraMap_mem : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (S : StarSubalgebra R A) (r : R),
  (algebraMap R A) r ∈ S
-- Mathlib.Data.Fin.Basic
Fin.natCast_mono : ∀ {n a b : ℕ}, b ≤ n → a ≤ b → ↑a ≤ ↑b
-- Mathlib.Algebra.Notation.Lemmas
one_lt_ite : ∀ {α : Type u_1} [inst : One α] {p : Prop} [inst_1 : Decidable p] {a b : α} [inst_2 : LT α],
  1 < a → 1 < b → 1 < if p then a else b
-- Mathlib.Order.Hom.PowersetCard
Set.powersetCard.ofFinEmbEquiv_symm_apply : ∀ {n : ℕ} {I : Type u_1} [inst : LinearOrder I] (s : ↑(Set.powersetCard I n)),
  Set.powersetCard.ofFinEmbEquiv.symm s = (↑s).orderEmbOfFin ⋯
-- Mathlib.Data.List.Perm.Basic
List.eq_map_comp_perm : ∀ {α : Type u_1} {β : Type u_2} (f : α → β),
  (Relation.Comp (fun x1 x2 => x1 = List.map f x2) fun x1 x2 => x1.Perm x2) = fun x1 x2 => x1.Perm (List.map f x2)
-- Mathlib.FieldTheory.SplittingField.Construction
/-- Any splitting field is isomorphic to `SplittingFieldAux f`.  -/
Polynomial.IsSplittingField.algEquiv : {K : Type v} →
  (L : Type w) →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] → (f : Polynomial K) → [h : Polynomial.IsSplittingField K L f] → L ≃ₐ[K] f.SplittingField
-- Batteries.Data.Fin.Lemmas
Fin.isSome_findSomeRev?_of_isSome : ∀ {n : ℕ} {α : Type u_1} {i : Fin n} {f : Fin n → Option α}, (f i).isSome = true → (Fin.findSomeRev? f).isSome = true
-- Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
_private.Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind.0.NumberField.Ideal.primesOverSpanEquivMonicFactorsModAux : {p : ℕ} →
  [inst : Fact (Nat.Prime p)] →
    (A : Polynomial ℤ) →
      { Q //
          Q ∈ UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Ideal.Quotient.mk (Ideal.span {↑p})) A) } ≃
        ↥(UniqueFactorizationMonoid.normalizedFactors (Polynomial.map (Int.castRingHom (ZMod p)) A)).toFinset
-- Mathlib.CategoryTheory.Enriched.Limits.HasConicalPullbacks
/-- `HasConicalPullback f g` represents the mere existence of a conical limit cone for the pair
of morphisms `f : X ⟶ Z` and `g : Y ⟶ Z`  -/
CategoryTheory.Enriched.HasConicalPullback : (V : Type u') →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u} →
        [inst_2 : CategoryTheory.Category.{v, u} C] →
          [CategoryTheory.EnrichedOrdinaryCategory V C] → {X Y Z : C} → (X ⟶ Z) → (Y ⟶ Z) → Prop
-- Mathlib.Algebra.Homology.DerivedCategory.Fractions
/-- Any morphism `f : Q.obj X ⟶ Q.obj Y` in the derived category
with `X` strictly `≥ a` and `≤ b`, and `Y` strictly `≥ a`
can be written as `f = inv (Q.map s) ≫ Q.map g` with `s : X' ⟶ X`
a quasi-isomorphism with `X'` strictly `≥ a` and `≤ b`, and `g : X' ⟶ Y`.  -/
DerivedCategory.right_fac_of_isStrictlyLE_of_isStrictlyGE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {X Y : CochainComplex C ℤ} (a b : ℤ) [X.IsStrictlyGE a] [X.IsStrictlyLE b]
  [Y.IsStrictlyGE a] (f : DerivedCategory.Q.obj X ⟶ DerivedCategory.Q.obj Y),
  ∃ X',
    ∃ (_ : X'.IsStrictlyGE a) (_ : X'.IsStrictlyLE b),
      ∃ s,
        ∃ (x : CategoryTheory.IsIso (DerivedCategory.Q.map s)),
          ∃ g,
            f =
              CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (DerivedCategory.Q.map s))
                (DerivedCategory.Q.map g)
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- `f` composed with `rightRetraction` is `leftRetraction` composed with `ι`  -/
CategoryTheory.IsSplitEqualizer.top_rightRetraction_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {ι : W ⟶ X}
  (self : CategoryTheory.IsSplitEqualizer f g ι) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp self.rightRetraction h) =
    CategoryTheory.CategoryStruct.comp self.leftRetraction (CategoryTheory.CategoryStruct.comp ι h)
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
CategoryTheory.LocalizerMorphism.isLocalizedEquivalence_of_functorial_right_resolutions : ∀ {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₂)
  {ρ : CategoryTheory.Functor C₂ C₁} (i : CategoryTheory.Functor.id C₂ ⟶ ρ.comp Φ.functor),
  (∀ (X₂ : C₂), W₂ (i.app X₂)) →
    W₁ = W₂.inverseImage Φ.functor →
      ∀ [Φ.functor.Full] [Φ.functor.Faithful] [W₂.HasTwoOutOfThreeProperty], Φ.IsLocalizedEquivalence
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.add_lt_add_of_le_of_lt : ∀ {α : Type u} [inst : Add α] {w x y z : WithBot α} [inst_1 : Preorder α] [AddLeftStrictMono α] [AddRightMono α],
  w ≠ ⊥ → w ≤ y → x < z → w + x < y + z
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.Hom.comm : ∀ {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.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  {X Y : CategoryTheory.Triangulated.SpectralObject C ι} (self : X.Hom Y) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
  CategoryTheory.CategoryStruct.comp (X.δ f g)
      ((CategoryTheory.shiftFunctor C 1).map (self.hom.app (CategoryTheory.ComposableArrows.mk₁ f))) =
    CategoryTheory.CategoryStruct.comp (self.hom.app (CategoryTheory.ComposableArrows.mk₁ g)) (Y.δ f g)
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
/-- The measure that will decrease during the induction in the `C : R → R[X]` case of
Chevalley's theorem with complexity bound.  -/
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.degree : {R : Type u_2} →
  [inst : CommRing R] → {n : ℕ} → ChevalleyThm.PolynomialC.InductionObj✝ R n → ChevalleyThm.PolynomialC.DegreeType✝ n
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instZero.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β],
  ContinuousMap.instZero = { zero := ContinuousMap.const α 0 }
-- Mathlib.Algebra.Group.NatPowAssoc
NatPowAssoc.mk : ∀ {M : Type u_2} [inst : MulOneClass M] [inst_1 : Pow M ℕ],
  (∀ (k n : ℕ) (x : M), x ^ (k + n) = x ^ k * x ^ n) → (∀ (x : M), x ^ 0 = 1) → (∀ (x : M), x ^ 1 = x) → NatPowAssoc M
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- The all-ones column vector multiplied with a column stochastic matrix is 1.  -/
Matrix.one_vecMul_of_mem_colStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R},
  M ∈ Matrix.colStochastic R n → Matrix.vecMul 1 M = 1
-- Mathlib.Analysis.Normed.Lp.ProdLp
/-- The `L^p` product of two isometric equivalences.  -/
IsometryEquiv.withLpProdCongr : (p : ENNReal) →
  {α : Type u_2} →
    {β : Type u_3} →
      {α' : Type u_5} →
        {β' : Type u_6} →
          [hp : Fact (1 ≤ p)] →
            [inst : PseudoEMetricSpace α] →
              [inst_1 : PseudoEMetricSpace β] →
                [inst_2 : PseudoEMetricSpace α'] →
                  [inst_3 : PseudoEMetricSpace β'] → α ≃ᵢ α' → β ≃ᵢ β' → WithLp p (α × β) ≃ᵢ WithLp p (α' × β')
-- Mathlib.LinearAlgebra.RootSystem.CartanMatrix
RootPairing.Base.apply_mem_range_root_of_cartanMatrixEq : ∀ {ι : 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] [CharZero R] [IsDomain R] [Finite ι]
  {ι₂ : Type u_6} {M₂ : Type u_7} {N₂ : Type u_8} [inst_8 : AddCommGroup M₂] [inst_9 : Module R M₂]
  [inst_10 : AddCommGroup N₂] [inst_11 : Module R N₂] {P : RootPairing ι R M N} [P.IsRootSystem]
  [inst_13 : P.IsCrystallographic] [P.IsReduced] (b : P.Base) {P₂ : RootPairing ι₂ R M₂ N₂}
  [inst_15 : P₂.IsCrystallographic] (b₂ : P₂.Base) (e : ↥b.support ≃ ↥b₂.support) (f : M ≃ₗ[R] M₂),
  (∀ (i : ↥b.support), f (P.root ↑i) = P₂.root ↑(e i)) →
    ∀ m ∈ Set.range ⇑P.root,
      (∀ (i j : ↥b.support), b₂.cartanMatrix (e i) (e j) = b.cartanMatrix i j) → f m ∈ Set.range ⇑P₂.root
-- Mathlib.Algebra.Group.Action.Defs
/-- `VAdd` version of `zero_add_eq_id`  -/
zero_vadd_eq_id : ∀ (M : Type u_1) {α : Type u_5} [inst : AddMonoid M] [inst_1 : AddAction M α], (fun x => 0 +ᵥ x) = id
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_sub : ∀ {α : Type u_1} {M : Type u_8} {G : Type u_12} [inst : Zero M] [inst_1 : SubtractionCommMonoid G] {f : α →₀ M}
  {h₁ h₂ : α → M → G}, (f.sum fun a b => h₁ a b - h₂ a b) = f.sum h₁ - f.sum h₂
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
ContinuousLinearMap.comp_memLp : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {𝕜 : Type u_6} {𝕜' : Type u_7}
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' F] {σ : 𝕜 →+* 𝕜'} [RingHomIsometric σ] (L : E →SL[σ] F) (f : ↥(MeasureTheory.Lp E p μ)),
  MeasureTheory.MemLp (⇑L ∘ ↑↑f) p μ
-- Mathlib.FieldTheory.Galois.Basic
/-- If `H` is a normal Subgroup of `Gal(L / K)`, then `fixedField H` is Galois over `K`.  -/
IsGalois.of_fixedField_normal_subgroup : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [IsGalois K L]
  (H : Subgroup Gal(L/K)) [hn : H.Normal], IsGalois K ↥(IntermediateField.fixedField H)
-- Mathlib.RingTheory.Algebraic.Integral
/-- A field extension is algebraic if it is finite.  -/
Algebra.IsAlgebraic.of_finite : ∀ (R : Type u_3) (A : Type u_4) [inst : CommRing R] [Nontrivial R] [inst_2 : Ring A] [inst_3 : Algebra R A]
  [Module.Finite R A], Algebra.IsAlgebraic R A
-- Mathlib.Data.Finite.Defs
/-- **Alias** of the reverse direction of `Set.infinite_coe_iff`. -/
Set.Infinite.to_subtype : ∀ {α : Type u} {s : Set α}, s.Infinite → Infinite ↑s
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- The natural equivalence between linear maps from `M` to `N`
and `1`-multilinear alternating maps from `M` to `N`.  -/
AlternatingMap.ofSubsingleton : (R : Type u_1) →
  [inst : Semiring R] →
    (M : Type u_2) →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          (N : Type u_3) →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] → {ι : Type u_7} → [Subsingleton ι] → ι → (M →ₗ[R] N) ≃ M [⋀^ι]→ₗ[R] N
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.HoldsForLocalizationAway.containsIdentities : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P) →
    RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => P
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueMul.to_mulOpposite : ∀ {G : Type u_1} [inst : Mul G] {A B : Finset G} {a0 b0 : G},
  UniqueMul A B a0 b0 →
    UniqueMul (Finset.map { toFun := MulOpposite.op, inj' := ⋯ } B)
      (Finset.map { toFun := MulOpposite.op, inj' := ⋯ } A) (MulOpposite.op b0) (MulOpposite.op a0)
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.truncFinset_monomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {s : Finset (σ →₀ ℕ)} {x : σ →₀ ℕ} (r : R),
  x ∈ s → (MvPowerSeries.truncFinset R s) ((MvPowerSeries.monomial x) r) = (MvPolynomial.monomial x) r
-- Mathlib.NumberTheory.PythagoreanTriples
_private.Mathlib.NumberTheory.PythagoreanTriples.0.coprime_sq_sub_mul_of_even_odd : ∀ {m n : ℤ}, m.gcd n = 1 → m % 2 = 0 → n % 2 = 1 → (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.associator_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y)) {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C}
  (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ
        (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ f₁ f₂) f₃)
      (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ Y₁ Y₂ Y₃).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ X₁ X₂ X₃).hom
      (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ f₁
        (CategoryTheory.CartesianMonoidalCategory.ofChosenFiniteProducts.tensorHom ℬ f₂ f₃))
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatMk_g : ∀ {R : Type u} [inst : Ring R] {X₁ X₂ X₃ : Type v} [inst_1 : AddCommGroup X₁] [inst_2 : AddCommGroup X₂]
  [inst_3 : AddCommGroup X₃] [inst_4 : Module R X₁] [inst_5 : Module R X₂] [inst_6 : Module R X₃] (f : X₁ →ₗ[R] X₂)
  (g : X₂ →ₗ[R] X₃) (hfg : g ∘ₗ f = 0), (CategoryTheory.ShortComplex.moduleCatMk f g hfg).g = ModuleCat.ofHom g
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPullback.isoIsPullback.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : C} (X Y : C) {Z : C} {fst fst_1 : P ⟶ X}
  (e_fst : fst = fst_1) {snd snd_1 : P ⟶ Y} (e_snd : snd = snd_1) {f f_1 : X ⟶ Z} (e_f : f = f_1) {g g_1 : Y ⟶ Z}
  (e_g : g = g_1) {P' : C} {fst' fst'_1 : P' ⟶ X} (e_fst' : fst' = fst'_1) {snd' snd'_1 : P' ⟶ Y}
  (e_snd' : snd' = snd'_1) (h : CategoryTheory.IsPullback fst snd f g) (h' : CategoryTheory.IsPullback fst' snd' f g),
  CategoryTheory.IsPullback.isoIsPullback X Y h h' = CategoryTheory.IsPullback.isoIsPullback X Y ⋯ ⋯
-- Mathlib.Data.Num.ZNum
ZNum.zneg_bitm1 : ∀ (n : ZNum), -n.bitm1 = (-n).bit1
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Finite
Set.finite_smul_set : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {a : G} {s : Set α}, (a • s).Finite ↔ s.Finite
-- Mathlib.GroupTheory.Coprod.Basic
AddEquiv.coprodAssoc_symm_apply_inr_inr : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddMonoid M] [inst_1 : AddMonoid N] [inst_2 : AddMonoid P]
  (x : P), (AddEquiv.coprodAssoc M N P).symm (AddMonoid.Coprod.inr (AddMonoid.Coprod.inr x)) = AddMonoid.Coprod.inr x
-- Mathlib.CategoryTheory.Limits.Bicones
CategoryTheory.Bicone.right.sizeOf_spec : ∀ {J : Type u₁} [inst : SizeOf J], sizeOf CategoryTheory.Bicone.right = 1
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Alt.applyFVarSubst : Lean.Meta.FVarSubst → Lean.Meta.Match.Alt → Lean.Meta.Match.Alt
-- Init.Control.Lawful.Instances
StateT.run_liftWith : ∀ {m : Type u → Type u_1} {σ α : Type u} [inst : Monad m] [LawfulMonad m]
  (f : ({β : Type u} → StateT σ m β → m (stM m (StateT σ m) β)) → m α) (s : σ),
  (liftWith f).run s = (fun x => (x, s)) <$> f fun {β} x => x.run s
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.adicAbv_intCast_le_one`.

---

The `v`-adic absolute value of an integer is `≤ 1`.  -/
NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_one : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] (n : ℤ), (NumberField.HeightOneSpectrum.adicAbv K v) ↑n ≤ 1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The 1st differential in the complex of inhomogeneous chains of `A : Rep k G`, as a
`k`-linear map `(G² →₀ A) → (G →₀ A)`. It is defined by
`a·(g₁, g₂) ↦ ρ_A(g₁⁻¹)(a)·g₂ - a·g₁g₂ + a·g₁`.  -/
groupHomology.d₂₁ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → ModuleCat.of k (G × G →₀ ↑A) ⟶ ModuleCat.of k (G →₀ ↑A)
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
AlgebraicGeometry.instHasRingHomPropertyLocallyOfFiniteTypeFiniteType : AlgebraicGeometry.HasRingHomProperty @AlgebraicGeometry.LocallyOfFiniteType fun {R S} [CommRing R] [CommRing S] =>
  RingHom.FiniteType
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.partition_snd : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : (a : α) → β a → Bool}, (Std.DTreeMap.Raw.partition f t).2.WF
-- Mathlib.RingTheory.Ideal.Colon
Ideal.annihilator_quotient : ∀ {R : Type u_1} [inst : Ring R] {I : Ideal R} [I.IsTwoSided], Module.annihilator R (R ⧸ I) = I
-- Std.Http.Data.Body.Length
/-- Checks if the `Length` is a fixed size.
 -/
Std.Http.Body.Length.isFixed : Std.Http.Body.Length → Bool
-- Lean.Elab.PatternVar
_private.Lean.Elab.PatternVar.0.Lean.Elab.Term.CollectPatternVars.collect.processCtorApp : Lean.Syntax → Lean.Elab.Term.CollectPatternVars.M Lean.Syntax
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arcsin_mem_Icc : ∀ (x : ℝ), Real.arcsin x ∈ Set.Icc (-(Real.pi / 2)) (Real.pi / 2)
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.inr_φ_fst : ∀ {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.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.φ f g)
        CategoryTheory.Limits.biprod.fst) =
    -CategoryTheory.CategoryStruct.id Y
-- Mathlib.Computability.DFA
DFA.mk.injEq : ∀ {α : Type u} {σ : Type v} (step : σ → α → σ) (start : σ) (accept : Set σ) (step_1 : σ → α → σ) (start_1 : σ)
  (accept_1 : Set σ),
  ({ step := step, start := start, accept := accept } = { step := step_1, start := start_1, accept := accept_1 }) =
    (step = step_1 ∧ start = start_1 ∧ accept = accept_1)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₂_id_comp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{u, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C),
  groupHomology.mapCycles₂ (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) =
    CategoryTheory.CategoryStruct.comp (groupHomology.mapCycles₂ (MonoidHom.id G) φ)
      (groupHomology.mapCycles₂ (MonoidHom.id G) ψ)
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
/-- **Alias** of `AlgebraicGeometry.LocallyOfFiniteType.finiteType_appLE`. -/
AlgebraicGeometry.Scheme.Hom.finiteType_appLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.LocallyOfFiniteType f] {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V →
        ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).FiniteType
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_erase : ∀ {M : Type u_5} [inst : CommMonoid M] {s : Multiset M} {a : M} [inst_1 : DecidableEq M],
  a ∈ s → a * (s.erase a).prod = s.prod
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- For `f : α →ᵤ[𝔖] β`, where `𝔖 : Set (Set α)` is nonempty and directed, `𝓝 f` admits the
family `{g | ∀ x ∈ S, (f x, g x) ∈ V}` for `S ∈ 𝔖` and `V ∈ 𝓑` as a filter basis, for any basis
`𝓑` of `𝓤 β`.  -/
UniformOnFun.hasBasis_nhds_of_basis : ∀ (α : Type u_1) (β : Type u_2) {ι : Type u_4} [inst : UniformSpace β] (𝔖 : Set (Set α)) (f : UniformOnFun α β 𝔖),
  𝔖.Nonempty →
    DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖 →
      ∀ {p : ι → Prop} {s : ι → Set (β × β)},
        (uniformity β).HasBasis p s →
          (nhds f).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => {g | (g, f) ∈ UniformOnFun.gen 𝔖 Si.1 (s Si.2)}
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : ChainComplex C ℕ) {Δ Δ' Δ'' : SimplexCategory} (i' : Δ'' ⟶ Δ') (i : Δ' ⟶ Δ) [inst_2 : CategoryTheory.Mono i']
  [inst_3 : CategoryTheory.Mono i],
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i)
      (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i') =
    AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K (CategoryTheory.CategoryStruct.comp i' i)
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.join_nil : ∀ {α : Type u}, Stream'.WSeq.nil.join = Stream'.WSeq.nil
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_alter_of_beq_eq_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  m.WF → (k == k') = false → (m.alter k f).contains k' = m.contains k'
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.comp_whiskerLeft_symm : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'),
  CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η)
        (CategoryTheory.Bicategory.associator f g h').hom)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.isoMk_inv_right : ∀ {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 Y : CategoryTheory.Comma L₁ R₁} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right)
  (h :
    autoParam
      (CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom =
        CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom))
      CategoryTheory.Comma.isoMk._auto_1),
  (CategoryTheory.Comma.isoMk l r h).inv.right = r.inv