mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Http.Internal.Char
/-- field-vchar = VCHAR
; ASCII-only variant (no obs-text).
 -/
Std.Http.Internal.Char.fieldVchar : Char → Bool
-- Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel
CategoryTheory.Limits.CokernelCofork.isColimitMapBifunctor.hom_ext : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C] {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁}
  {c₁ : CategoryTheory.Limits.CokernelCofork f₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁) {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  {c₂ : CategoryTheory.Limits.CokernelCofork f₂} (hc₂ : CategoryTheory.Limits.IsColimit c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) [(F.obj c₁.pt).PreservesZeroMorphisms]
  [F.PreservesZeroMorphisms]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₂ 0) (F.obj c₁.pt)]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0) (F.flip.obj Y₂)] {T : C}
  {f g : (F.obj c₁.pt).obj c₂.pt ⟶ T},
  CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.Limits.Cofork.π c₁)).app Y₂)
        (CategoryTheory.CategoryStruct.comp ((F.obj c₁.pt).map (CategoryTheory.Limits.Cofork.π c₂)) f) =
      CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.Limits.Cofork.π c₁)).app Y₂)
        (CategoryTheory.CategoryStruct.comp ((F.obj c₁.pt).map (CategoryTheory.Limits.Cofork.π c₂)) g) →
    f = g
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtPlace_mixedSpaceOfRealSpace : ∀ {K : Type u_1} [inst : Field K] {x : NumberField.mixedEmbedding.realSpace K} {w : NumberField.InfinitePlace K},
  0 ≤ x w → (NumberField.mixedEmbedding.normAtPlace w) (NumberField.mixedEmbedding.mixedSpaceOfRealSpace x) = x w
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.algebra₂ : (R : Type u_1) →
  [inst : CommRing R] →
    {A : Type u} →
      {B : Type u_2} →
        [inst_1 : CommRing A] →
          [inst_2 : Algebra R A] →
            [inst_3 : CommRing B] →
              [inst_4 : Algebra A B] →
                (D : Algebra.Smooth.DescentAux✝ A B) → Algebra (↥(Algebra.Smooth.DescentAux.subalgebra✝ R D)) B
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.instInhabitedSigmaQuotedConstMkStr1NilLevelExSumNat : Inhabited ((e : Q(ℕ)) × Mathlib.Tactic.Ring.Common.ExSumNat e)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
measurable_id' : ∀ {α : Type u_1} {x : MeasurableSpace α}, Measurable fun a => a
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.arsinh.eq_1 : ∀ (x : ℝ), Real.arsinh x = Real.log (x + √(1 + x ^ 2))
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.instInhabited : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → Inhabited (CategoryTheory.Mon C)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- Restrictions scalars along equal ring homomorphisms are naturally isomorphic.  -/
ModuleCat.restrictScalarsCongr : {R : Type u₁} →
  {S : Type u₂} →
    [inst : Ring R] →
      [inst_1 : Ring S] → {f g : R →+* S} → f = g → (ModuleCat.restrictScalars f ≅ ModuleCat.restrictScalars g)
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.Rel.smul : ∀ {R : Type u} {X : Type v} [inst : CommRing R] (t : R) {a b : FreeNonUnitalNonAssocAlgebra R X},
  FreeLieAlgebra.Rel R X a b → FreeLieAlgebra.Rel R X (t • a) (t • b)
-- Mathlib.CategoryTheory.Galois.Basic
/-- `F` preserves quotients by finite groups (G5).  -/
CategoryTheory.PreGaloisCategory.FiberFunctor.preservesQuotientsByFiniteGroups : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} {inst_1 : CategoryTheory.PreGaloisCategory C}
  {F : CategoryTheory.Functor C FintypeCat} [self : CategoryTheory.PreGaloisCategory.FiberFunctor F] (G : Type u₂)
  [inst_2 : Group G] [Finite G], CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.SingleObj G) F
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.irreducibleSpace_iff_isPrime_nilradical : ∀ {R : Type u} [inst : CommSemiring R], IrreducibleSpace (PrimeSpectrum R) ↔ (nilradical R).IsPrime
-- Init.Sym.Lemmas
Lean.Sym.Int.lt_eq_true : ∀ (a b : ℤ), decide (a < b) = true → (a < b) = True
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.exists : ∀ {α : Type u} {p : Multiplicative α → Prop}, (∃ a, p a) ↔ ∃ a, p (Multiplicative.ofAdd a)
-- Lean.Parser.Extension
Lean.Parser.addBuiltinTrailingParser : Lean.Name → Lean.Name → Lean.Parser.TrailingParser → ℕ → IO Unit
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_right_le_mk_add_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk b ≤ ArchimedeanClass.mk (a + b) ↔ ArchimedeanClass.mk b ≤ ArchimedeanClass.mk a
-- Mathlib.Analysis.InnerProductSpace.Adjoint
Unitary.norm_map : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] (u : ↥(unitary (H →L[𝕜] H))) (x : H), ‖↑u x‖ = ‖x‖
-- Mathlib.Order.Defs.Unbundled
LowerSet.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : LE α] [inst_1 : SizeOf α] (carrier : Set α) (lower' : IsLowerSet carrier),
  sizeOf { carrier := carrier, lower' := lower' } = 1
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.sum_repr_mul_repr : ∀ {ι : Type u_10} {R : Type u_14} {M : Type u_15} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (b : Module.Basis ι R M) {ι' : Type u_17} [inst_3 : Fintype ι'] (b' : Module.Basis ι' R M)
  (x : M) (i : ι), ∑ j, (b.repr (b' j)) i * (b'.repr x) j = (b.repr x) i
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.induction_on : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} {motive : HNNExtension G A B φ → Prop}
  (x : HNNExtension G A B φ),
  (∀ (g : G), motive (HNNExtension.of g)) →
    motive HNNExtension.t →
      (∀ (x y : HNNExtension G A B φ), motive x → motive y → motive (x * y)) →
        (∀ (x : HNNExtension G A B φ), motive x → motive x⁻¹) → motive x
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.mem_sSup_iff : ∀ {α : Type u_1} [inst : LE α] {S : Set (LowerSet α)} {a : α}, a ∈ sSup S ↔ ∃ s ∈ S, a ∈ s
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfOrdArgs.lt_iff : ∀ {α : Type u} (self : Std.Packages.LinearPreorderOfOrdArgs α),
  let this := self.ord;
  let this_1 := self.le;
  have this_2 := ⋯;
  let this_3 := self.lt;
  ∀ (a b : α), a < b ↔ compare a b = Ordering.lt
-- Mathlib.Algebra.Order.CauSeq.Basic
/-- `CauSeq β abv` is the type of `β`-valued Cauchy sequences, with respect to the absolute value
function `abv`.  -/
CauSeq : {α : Type u_3} →
  [inst : Field α] → [inst_1 : LinearOrder α] → [IsStrictOrderedRing α] → (β : Type u_4) → [Ring β] → (β → α) → Type u_4
-- Mathlib.RingTheory.AlgebraTower
Module.Basis.smulTower'_repr_mk : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid A]
  [inst_3 : Module R S] [inst_4 : Module S A] [inst_5 : Module R A] [inst_6 : IsScalarTower R S A] {ι : Type u_5}
  {ι' : Type u_6} (b : Module.Basis ι R S) (c : Module.Basis ι' S A) (x : A) (i : ι') (j : ι),
  ((b.smulTower' c).repr x) (i, j) = (b.repr ((c.repr x) i)) j
-- Mathlib.Util.ParseCommand
/-- `#parse parserFnId => str` allows to capture parsing exceptions.
`parserFnId` is the identifier of a `ParserFn` and `str` is the string that
`parserFnId` should parse.

If the parse is successful, then the output is logged;
if the parse is successful, then the output is captured in an exception.

In either case, `#guard_msgs` can then be used to capture the resulting parsing errors.

For instance, `#parse` can be used as follows
```lean
/-- error: <input>:1:3: Stacks tags must be exactly 4 characters -/
#guard_msgs in #parse Mathlib.Stacks.stacksTagFn => "A05"
```
 -/
Mathlib.GuardExceptions.parseCmd : Lean.ParserDescr
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
/-- If `f : G → H` is a multiplicative homomorphism between two monoids, then
`mapDomain f` is an algebra homomorphism between their monoid algebras.  -/
SkewMonoidAlgebra.mapDomainAlgHom : {G : Type u_2} →
  [inst : Monoid G] →
    (k : Type u_6) →
      (A : Type u_7) →
        [inst_1 : CommSemiring k] →
          [inst_2 : Semiring A] →
            [inst_3 : Algebra k A] →
              {H : Type u_8} →
                {F : Type u_9} →
                  [inst_4 : Monoid H] →
                    [inst_5 : FunLike F G H] →
                      [MonoidHomClass F G H] →
                        [inst_7 : MulSemiringAction G A] →
                          [inst_8 : MulSemiringAction H A] →
                            [inst_9 : SMulCommClass G k A] →
                              [inst_10 : SMulCommClass H k A] →
                                {f : F} →
                                  (∀ (a : G) (x : A), a • x = f a • x) →
                                    SkewMonoidAlgebra A G →ₐ[k] SkewMonoidAlgebra A H
-- Mathlib.Data.Finset.SDiff
Finset.instGeneralizedBooleanAlgebra : {α : Type u_1} → [DecidableEq α] → GeneralizedBooleanAlgebra (Finset α)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_erase!_eq_iff_not_compare_eq_minKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α},
      (Std.DTreeMap.Internal.Impl.erase! k t).minKey? = t.minKey? ↔
        ∀ {km : α}, t.minKey? = some km → ¬compare k km = Ordering.eq
-- Mathlib.Analysis.Asymptotics.SpecificAsymptotics
pow_div_pow_eventuallyEq_atBot : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {p q : ℕ},
  (fun x => x ^ p / x ^ q) =ᶠ[Filter.atBot] fun x => x ^ (↑p - ↑q)
-- Plausible.Gen
/-- Lift `Random.random` to the `Gen` monad.  -/
Plausible.Gen.chooseAny : (α : Type u) → [Plausible.Random Id α] → Plausible.Gen α
-- Mathlib.Topology.Algebra.Valued.NormedValued
NormedField.instRankOneNNRealValuation : {K : Type u_2} → [inst : NontriviallyNormedField K] → [inst_1 : IsUltrametricDist K] → NormedField.valuation.RankOne
-- Mathlib.Tactic.GCongr.Core
/-- Mark `declName` with the `gcongr` attribute.  -/
Mathlib.Tactic.GCongr.addGCongrLemma : Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Action.Basic
Action.hom_injective : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G},
  Function.Injective Action.Hom.hom
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.instDecidableEqQuotientAddSubgroupOfDecidablePredMem : {α : Type u_1} → [inst : AddGroup α] → (s : AddSubgroup α) → [DecidablePred fun x => x ∈ s] → DecidableEq (α ⧸ s)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_inr : ∀ (R : Type u) {M : Type v} [inst : Zero R] (m : M), (TrivSqZeroExt.inr m).snd = m
-- Lean.Meta.Match.Basic
Lean.Meta.Match.AltLHS : Type
-- Mathlib.GroupTheory.Finiteness
Monoid.fg_def : ∀ {M : Type u_1} [inst : Monoid M], Monoid.FG M ↔ ⊤.FG
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.mk.congr_simp : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (toList toList_1 : List ((i : ι) × M i))
  (e_toList : toList = toList_1) (ne_one : ∀ l ∈ toList, l.snd ≠ 1)
  (chain_ne : List.IsChain (fun l l' => l.fst ≠ l'.fst) toList),
  { toList := toList, ne_one := ne_one, chain_ne := chain_ne } = { toList := toList_1, ne_one := ⋯, chain_ne := ⋯ }
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
/-- The subscheme associated to the pullback ideal sheaf is isomorphic to the fibred product.  -/
AlgebraicGeometry.Scheme.IdealSheafData.comapIso : {X Y : AlgebraicGeometry.Scheme} →
  (I : Y.IdealSheafData) → (f : X ⟶ Y) → (I.comap f).subscheme ≅ CategoryTheory.Limits.pullback f I.subschemeι
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval_map : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁) (p : MvPolynomial σ R), (MvPolynomial.eval g) ((MvPolynomial.map f) p) = MvPolynomial.eval₂ f g p
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
/-- The special-value formula `Γ(1/2) = √π`, which is equivalent to the Gaussian integral.  -/
Real.Gamma_one_half_eq : Real.Gamma (1 / 2) = √Real.pi
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
AbsoluteValue.LiesOver.congr_simp : ∀ {K : Type u_3} {L : Type u_4} {S : Type u_5} [inst : CommRing K] [inst_1 : IsSimpleRing K] [inst_2 : CommRing L]
  [inst_3 : Algebra K L] [inst_4 : PartialOrder S] [inst_5 : Nontrivial L] [inst_6 : Semiring S]
  (w w_1 : AbsoluteValue L S), w = w_1 → ∀ (v v_1 : AbsoluteValue K S), v = v_1 → w.LiesOver v = w_1.LiesOver v_1
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_symm_eq_iff : ∀ {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₂}
  {τ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair τ₁₂ τ₂₁] [inst_7 : RingHomInvPair τ₂₁ τ₁₂] {p : Submodule R M}
  (e : M ≃ₛₗ[τ₁₂] M₂) {K : Submodule R₂ M₂}, Submodule.map (↑e.symm) K = p ↔ Submodule.map (↑e) p = K
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.faithfulSMul : ∀ (S : Type u_2) [inst : CommSemiring S] (R : Type u_4) [inst_1 : CommRing R] [NoZeroDivisors R] [inst_3 : Algebra R S]
  (P : Ideal R) [hp : P.IsPrime] [IsLocalization.AtPrime S P], FaithfulSMul R S
-- Mathlib.NumberTheory.LSeries.PrimesInAP
Nat.frequently_atTop_prime_and_modEq : ∀ {q a : ℕ}, q ≠ 0 → a.Coprime q → ∃ᶠ (p : ℕ) in Filter.atTop, Nat.Prime p ∧ p ≡ a [MOD q]
-- Mathlib.Data.Rat.Lemmas
Rat.isSquare_iff : ∀ {q : ℚ}, IsSquare q ↔ IsSquare q.num ∧ IsSquare q.den
-- Init.Prelude
/-- `a % b` computes the remainder upon dividing `a` by `b`. See `HMod`.  -/
Mod.mod : {α : Type u} → [self : Mod α] → α → α → α
-- Mathlib.Data.Int.Bitwise
_private.Mathlib.Data.Int.Bitwise.0.Int.bitwise.match_1.eq_2 : ∀ (motive : ℤ → ℤ → Sort u_1) (m n : ℕ) (h_1 : (m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n))
  (h_2 : (m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) (h_3 : (m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n))
  (h_4 : (m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)),
  (match Int.ofNat m, Int.negSucc n with
    | Int.ofNat m, Int.ofNat n => h_1 m n
    | Int.ofNat m, Int.negSucc n => h_2 m n
    | Int.negSucc m, Int.ofNat n => h_3 m n
    | Int.negSucc m, Int.negSucc n => h_4 m n) =
    h_2 m n
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.zmod_cast_comp_toZModPow : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (m n : ℕ) (h : m ≤ n),
  (ZMod.castHom ⋯ (ZMod (p ^ m))).comp (PadicInt.toZModPow n) = PadicInt.toZModPow m
-- Mathlib.RingTheory.Algebraic.Integral
instIsPushoutFractionRingPolynomial : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [alg : Algebra.IsAlgebraic R S] [inst_3 : IsDomain S] [inst_4 : FaithfulSMul R S],
  Algebra.IsPushout R (FractionRing (Polynomial R)) S (FractionRing (Polynomial S))
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- If there exists a surjective equivariant map `α →ₑ[σ] β`
then pretransitivity descends from `n ↪ α` to `n ↪ β`.

The subtlety is that if it is not injective, this map does not induce
an equivariant map from `n ↪ α` to `n ↪ β`.  -/
MulAction.IsPretransitive.of_embedding : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {H : Type u_3} {β : Type u_4}
  [inst_2 : Group H] [inst_3 : MulAction H β] {σ : G → H} {f : α →ₑ[σ] β} {n : Type u_5},
  Function.Surjective ⇑f → ∀ [MulAction.IsPretransitive G (n ↪ α)], MulAction.IsPretransitive H (n ↪ β)
-- Mathlib.Topology.Sheaves.Abelian
/-- Exactness can be checked on stalks for complexes of sheaves.  -/
TopCat.Sheaf.exact_iff_stalkFunctor_map_exact : ∀ {C : Type v} [inst : CategoryTheory.Category.{u, v} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  [inst_2 : CategoryTheory.Limits.HasLimits C] {FC : C → C → Type u_1} {CC : C → Type u}
  [inst_3 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [instCC : CategoryTheory.ConcreteCategory C FC]
  [inst_4 : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget C)]
  [inst_5 : CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget C)] [inst_6 : CategoryTheory.Abelian C]
  {X : TopCat} (S : CategoryTheory.ShortComplex (TopCat.Sheaf C X)),
  S.Exact ↔ ∀ (x : ↑X), (S.map ((TopCat.Sheaf.forget C X).comp (TopCat.Presheaf.stalkFunctor C x))).Exact
-- Init.Data.UInt.Lemmas
BitVec.ofNat_uInt8ToNat : ∀ (n : UInt8), BitVec.ofNat 8 n.toNat = n.toBitVec
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max?_bind_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp], t.max?.bind t.get? = t.max?
-- Mathlib.Data.Nat.Bits
Nat.bit0_bits : ∀ (n : ℕ), n ≠ 0 → (2 * n).bits = false :: n.bits
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.Spec.residue_residueFieldIso_hom : ∀ (R : CommRingCat) (x : ↥(AlgebraicGeometry.Spec R)),
  CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.Spec R).residue x)
      (AlgebraicGeometry.Scheme.Spec.residueFieldIso R x).hom =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.stalkIso R x).hom
      (CommRingCat.ofHom (algebraMap (Localization.AtPrime x.asIdeal) x.asIdeal.ResidueField))
-- Mathlib.Data.Complex.Basic
Complex.normSq.eq_1 : Complex.normSq =
  { toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := Complex.normSq._proof_1,
    map_one' := Complex.normSq._proof_2, map_mul' := ⋯ }
-- Lean.Compiler.LCNF.Types
_private.Lean.Compiler.LCNF.Types.0.Lean.Compiler.LCNF.toLCNFType.visitApp : Lean.Expr → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.conjugateEquiv_apply : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ l₂ : c ⟶ d} {r₁ r₂ : d ⟶ c}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (α : l₂ ⟶ l₁),
  (CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₂) α =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor r₁).inv
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Bicategory.mateEquiv adj₁ adj₂)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor l₂).hom
            (CategoryTheory.CategoryStruct.comp α (CategoryTheory.Bicategory.rightUnitor l₁).inv)))
        (CategoryTheory.Bicategory.leftUnitor r₂).hom)
-- Mathlib.Algebra.Group.Action.Opposite
MulOpposite.instIsScalarTower : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M N] [inst_1 : SMul M α] [inst_2 : SMul N α]
  [IsScalarTower M N α], IsScalarTower M N αᵐᵒᵖ
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyIsoSc'_inv_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology],
  CategoryTheory.CategoryStruct.comp (K.homologyIsoSc' i j k hi hk).inv (K.homologyι j) =
    CategoryTheory.CategoryStruct.comp (K.sc' i j k).homologyι (K.opcyclesIsoSc' i j k hi hk).inv
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKeyGE!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.Equiv t₂ → t₁.getKeyGE! k = t₂.getKeyGE! k
-- Init.Data.Vector.Lemmas
Vector.back.congr_simp : ∀ {n : ℕ} {α : Type u_1} [inst : NeZero n] (xs xs_1 : Vector α n), xs = xs_1 → xs.back = xs_1.back
-- Mathlib.LinearAlgebra.Matrix.Permutation
/-- The trace of a permutation matrix equals the number of fixed points.  -/
Matrix.trace_permutation : ∀ {n : Type u_1} {R : Type u_2} [inst : DecidableEq n] (σ : Equiv.Perm n) [inst_1 : Fintype n]
  [inst_2 : AddCommMonoidWithOne R], (Equiv.Perm.permMatrix R σ).trace = ↑(Function.fixedPoints ⇑σ).ncard
-- Mathlib.Data.Finsupp.Basic
Finsupp.finite_range : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M), (Set.range ⇑f).Finite
-- Std.Data.TreeSet.Basic
/-- Support for the `for` loop construct in `do` blocks. The iteration happens in ascending
order.
 -/
Std.TreeSet.forIn : {α : Type u} →
  {cmp : α → α → Ordering} →
    {δ : Type w} → {m : Type w → Type w₂} → [Monad m] → (α → δ → m (ForInStep δ)) → δ → Std.TreeSet α cmp → m δ
-- Mathlib.Data.Fintype.Defs
Fintype.decidableEqEmbeddingFintype : {α : Type u_1} → {β : Type u_2} → [DecidableEq β] → [Fintype α] → DecidableEq (α ↪ β)
-- Mathlib.Algebra.Homology.ComplexShape
/-- There is at most one nonzero differential to `X j`.  -/
ComplexShape.prev_eq : ∀ {ι : Type u_1} (self : ComplexShape ι) {i i' j : ι}, self.Rel i j → self.Rel i' j → i = i'
-- Lean.Parser.Module.Syntax
/-- Parser for a Lean module. We never actually run this parser but instead use the imperative definitions in the parent module that
return the same syntax tree structure, but add error recovery. Still, it is helpful to have a `Parser` definition
for it in order to auto-generate helpers such as the pretty printer.  -/
Lean.Parser.Module.module : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Triangulated.Generators
/-- An object property `P` is called a classical generator, if every object can be reached
from objects in `P` by shifts, binary products, retracts and extensions.  -/
CategoryTheory.ObjectProperty.IsClassicalTriangulatedGenerator : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [CategoryTheory.Pretriangulated C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomainRingHom_comp : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} {O : Type u_8} [inst : Semiring R] [inst_1 : Monoid M]
  [inst_2 : Monoid N] [inst_3 : Monoid O] (f : N →* O) (g : M →* N),
  MonoidAlgebra.mapDomainRingHom R (f.comp g) =
    (MonoidAlgebra.mapDomainRingHom R f).comp (MonoidAlgebra.mapDomainRingHom R g)
-- Mathlib.Probability.Kernel.Composition.MapComap
/-- Define a `Kernel β γ` from a `Kernel (α × β) γ` by taking the comap of `fun b ↦ (a, b)` for
a given `a : α`.  -/
ProbabilityTheory.Kernel.sectR : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        {γ : Type u_4} →
          {mγ : MeasurableSpace γ} → ProbabilityTheory.Kernel (α × β) γ → α → ProbabilityTheory.Kernel β γ
-- Batteries.Data.String.Lemmas
String.map_eq_empty_iff : ∀ (s : String) (f : Char → Char), String.Legacy.map f s = "" ↔ s = ""
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.asIsoHomologyι_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hg : S.g = 0) [inst_2 : S.HasHomology], (S.asIsoHomologyι hg).hom = S.homologyι
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instInvolutiveNeg : {α : Type u_1} → [InvolutiveNeg α] → InvolutiveNeg (Lex α)
-- Mathlib.GroupTheory.IsSubnormal
/-- A characterisation of satisfying `IsSubnormal` in terms of chains of additive
subgroups, each normal in the following one.

The sequence stabilises once it reaches `⊤`, which is guaranteed at the asserted `n`.  -/
AddSubgroup.IsSubnormal.isSubnormal_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G},
  H.IsSubnormal ↔ ∃ n f, Monotone f ∧ (∀ (i : ℕ), ((f i).addSubgroupOf (f (i + 1))).Normal) ∧ f 0 = H ∧ f n = ⊤
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.getKeyD_eq_getKeyDₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β)
  (a fallback : α), m.getKeyD a fallback = m.getKeyDₘ a fallback