mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
IsometryEquiv.mk.congr_simp : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (toEquiv toEquiv_1 : α ≃ β)
  (e_toEquiv : toEquiv = toEquiv_1) (isometry_toFun : Isometry toEquiv.toFun),
  { toEquiv := toEquiv, isometry_toFun := isometry_toFun } = { toEquiv := toEquiv_1, isometry_toFun := ⋯ }
-- Mathlib.FieldTheory.AxGrothendieck
Sum.map.eq_1 : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} (f : α → α') (g : β → β'),
  Sum.map f g = Sum.elim (Sum.inl ∘ f) (Sum.inr ∘ g)
-- Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
MeasureTheory.eLpNorm'_sum_le : ∀ {α : Type u_1} {ε' : Type u_4} {m : MeasurableSpace α} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddCommMonoid ε'] {q : ℝ} {μ : MeasureTheory.Measure α} [ContinuousAdd ε'] {ι : Type u_5}
  {f : ι → α → ε'} {s : Finset ι},
  (∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ) →
    1 ≤ q → MeasureTheory.eLpNorm' (∑ i ∈ s, f i) q μ ≤ ∑ i ∈ s, MeasureTheory.eLpNorm' (f i) q μ
-- Mathlib.Algebra.Order.Group.MinMax
min_inv_inv' : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] (a b : α), min a⁻¹ b⁻¹ = (max a b)⁻¹
-- Qq.Match
Qq.Impl.«term_qq_match_←_|_In_» : Lean.ParserDescr
-- Mathlib.Topology.Sober
TopologicalSpace.IsOpenCover.quasiSober_iff_forall : ∀ {α : Type u_1} [inst : TopologicalSpace α] {ι : Type u_3} {U : ι → TopologicalSpace.Opens α},
  TopologicalSpace.IsOpenCover U → (QuasiSober α ↔ ∀ (i : ι), QuasiSober ↥(U i))
-- Init.Data.Array.Basic
List.mem_toArray : ∀ {α : Type u} {a : α} {l : List α}, a ∈ l.toArray ↔ a ∈ l
-- Mathlib.SetTheory.Cardinal.SchroederBernstein
/-- The cardinals are totally ordered. See
`Cardinal.conditionallyCompleteLinearOrderBot` for (one of) the lattice
instance.  -/
Function.Embedding.total : ∀ (α : Type u) (β : Type v), Nonempty (α ↪ β) ∨ Nonempty (β ↪ α)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_insertList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst toInsert).contains k = false →
    Std.Internal.List.getValueCast? k (Std.Internal.List.insertList l toInsert) = Std.Internal.List.getValueCast? k l
-- Mathlib.Algebra.DirectSum.Module
DirectSum.coe_congrAddEquiv : ∀ {ι : Type u_2} {N : ι → Type u_3} [inst : (i : ι) → AddCommMonoid (N i)] {P : ι → Type u_4}
  [inst_1 : (i : ι) → AddCommMonoid (P i)] (u : (i : ι) → N i ≃+ P i),
  ⇑(DirectSum.congrAddEquiv u).toAddMonoidHom = ⇑(DirectSum.map fun i => (u i).toAddMonoidHom)
-- Mathlib.Topology.Bases
/-- A set `s` is in the neighbourhood of `a` iff there is some basis set `t`, which
contains `a` and is itself contained in `s`.  -/
TopologicalSpace.IsTopologicalBasis.mem_nhds_iff : ∀ {α : Type u} [t : TopologicalSpace α] {a : α} {s : Set α} {b : Set (Set α)},
  TopologicalSpace.IsTopologicalBasis b → (s ∈ nhds a ↔ ∃ t ∈ b, a ∈ t ∧ t ⊆ s)
-- Mathlib.Algebra.BigOperators.Intervals
/-- Telescopic sum over `Fin`.  -/
Fin.sum_Iic_sub : ∀ {M : Type u_3} [inst : AddCommGroup M] {n : ℕ} (a : Fin n) (f : Fin (n + 1) → M),
  ∑ i ≤ a, (f i.succ - f i.castSucc) = f a.succ - f 0
-- Std.Do.SPred.DerivedLaws
/-- Expresses that the conjunction of `P` and `Q` is equivalent to `spred(P ∧ Q)`, but potentially
simpler.
 -/
Std.Do.SPred.Tactic.SimpAnd : {σs : List (Type u)} → Std.Do.SPred σs → Std.Do.SPred σs → outParam (Std.Do.SPred σs) → Prop
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.WideSubcategory.instBraidedCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (P : CategoryTheory.MorphismProperty C) →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : CategoryTheory.BraidedCategory C] →
          [inst_3 : P.IsStableUnderBraiding] → CategoryTheory.BraidedCategory (CategoryTheory.WideSubcategory P)
-- Mathlib.Data.TwoPointing
TwoPointing.mk.sizeOf_spec : ∀ {α : Type u_3} [inst : SizeOf α] (toProd : α × α) (fst_ne_snd : toProd.1 ≠ toProd.2),
  sizeOf { toProd := toProd, fst_ne_snd := fst_ne_snd } = 1 + sizeOf toProd
-- Mathlib.Computability.Encoding
Computability.Γ'.bit : Bool → Computability.Γ'
-- Init.System.IO
/-- Reads the entire remaining contents of the file handle as a UTF-8-encoded string. An exception is
thrown if the contents are not valid UTF-8.

The underlying file is not automatically closed, and subsequent reads from the handle may block
and/or return data.
 -/
IO.FS.Handle.readToEnd : IO.FS.Handle → IO String
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.A_three : CartanMatrix.A 3 = !![2, -1, 0; -1, 2, -1; 0, -1, 2]
-- Mathlib.Computability.EpsilonNFA
εNFA.start_one : ∀ {α : Type u} {σ : Type v}, εNFA.start 1 = Set.univ
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg.cons_iff : ∀ {hd : ℝ} {tl : Tactic.ComputeAsymptotics.UnitMonomial},
  Tactic.ComputeAsymptotics.UnitMonomial.FirstNonzeroIsNeg (hd :: tl) ↔ hd < 0 ∨ hd = 0 ∧ tl.FirstNonzeroIsNeg
-- Mathlib.Data.Set.Lattice
Set.biUnion_empty : ∀ {α : Type u_1} {β : Type u_2} (s : α → Set β), ⋃ x ∈ ∅, s x = ∅
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.instHasZeroObject : ∀ {R : Type u} [inst : Semiring R], CategoryTheory.Limits.HasZeroObject (SemimoduleCat R)
-- Init.Data.String.Lemmas.Basic
String.Slice.Pos.copy_inj : ∀ {s : String.Slice} {p₁ p₂ : s.Pos}, p₁.copy = p₂.copy ↔ p₁ = p₂
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftRingHom_apply_ofFractionRing_mk : ∀ {L : Type u_2} {R : Type u_3} [inst : Field L] [inst_1 : CommRing R] (φ : Polynomial R →+* L)
  (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors L)) (n : Polynomial R)
  (d : ↥(nonZeroDivisors (Polynomial R))),
  (RatFunc.liftRingHom φ hφ) { toFractionRing := Localization.mk n d } = φ n / φ ↑d
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.map_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  (self : PresheafOfModules R) {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z),
  self.map (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (self.map f)
      (CategoryTheory.CategoryStruct.comp ((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f))).map (self.map g))
        ((ModuleCat.restrictScalarsComp' (RingCat.Hom.hom (R.map f)) (RingCat.Hom.hom (R.map g))
                (RingCat.Hom.hom (R.map (CategoryTheory.CategoryStruct.comp f g))) ⋯).inv.app
          (self.obj Z)))
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_of_mk_nonneg : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x : K}
  (f : ArchimedeanClass.FiniteResidueField K →+*o ℝ) (h : 0 ≤ ArchimedeanClass.mk x),
  ArchimedeanClass.stdPart x = f (ArchimedeanClass.FiniteResidueField.mk (ArchimedeanClass.FiniteElement.mk x h))
-- Mathlib.Algebra.Ring.Int.Parity
Int.ne_of_odd_add : ∀ {m n : ℤ}, Odd (m + n) → m ≠ n
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.multinomial_cons : ∀ {α : Type u_1} {s : Finset α} {a : α} (ha : a ∉ s) (f : α → ℕ),
  Nat.multinomial (Finset.cons a s ha) f = (f a + ∑ i ∈ s, f i).choose (f a) * Nat.multinomial s f
-- Mathlib.Algebra.Order.CompleteField
/-- `inducedMap` as an `OrderRingHom`.  -/
ConditionallyCompleteLinearOrderedField.inducedOrderRingHom : (α : Type u_2) →
  (β : Type u_3) →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [IsStrictOrderedRing α] →
          [inst_3 : Field β] →
            [inst_4 : ConditionallyCompleteLinearOrder β] → [IsStrictOrderedRing β] → [Archimedean α] → α →+*o β
-- Mathlib.Order.Filter.AtTopBot.Archimedean
Int.comap_cast_atTop : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R] [Archimedean R],
  Filter.comap Int.cast Filter.atTop = Filter.atTop
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.startsWith_eq_forwardPatternStartsWith : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String.Slice},
  s.startsWith pat = String.Slice.Pattern.ForwardPattern.startsWith pat s
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.sub_eq_zero : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {a b : α}, a ≠ ⊤ → (b - a = 0 ↔ b = a)
-- Lean.Meta.Coe
/-- Coerces `expr` to a type.  -/
Lean.Meta.coerceToSort? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {a : α} {h' : t[a]?.isSome = true}, t[a]?.get h' = t[a]
-- Std.Do.WP.SimpLemmas
Std.Do.WP.restoreM_StateT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α σ : Type u} {Q : Std.Do.PostCond α (Std.Do.PostShape.arg σ ps)}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (x : m (α × σ)),
  (Std.Do.wp (MonadControl.restoreM x)).apply Q = fun x_1 =>
    (Std.Do.wp x).apply
      (fun x =>
        match x with
        | (a, s) => Q.1 a s,
        Q.2)
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.mul_nat_iff : ∀ {p x : ℝ} {n : ℕ}, n ≠ 0 → (LiouvilleWith p (x * ↑n) ↔ LiouvilleWith p x)
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
/-- The pushout under the initial object is the coproduct  -/
isCoproductOfIsInitialIsPushout : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          (h : W ⟶ X) →
            (k : W ⟶ Y) →
              (H₁ : CategoryTheory.Limits.IsInitial W) →
                CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk f g ⋯) →
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk f g)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insert k v).minKey? = some (t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k')
-- Mathlib.Logic.Equiv.Basic
/-- Note: the "obvious" statement `(piCongrLeft' P e).symm g a = g (e a)` doesn't typecheck: the
LHS would have type `P a` while the RHS would have type `P (e.symm (e a))`. This lemma is a way
around it in the case where `a` is of the form `e.symm b`, so we can use `g b` instead of
`g (e (e.symm b))`.  -/
Equiv.piCongrLeft'_symm_apply_apply : ∀ {α : Sort u_1} {β : Sort u_4} (P : α → Sort u_9) (e : α ≃ β) (g : (b : β) → P (e.symm b)) (b : β),
  (Equiv.piCongrLeft' P e).symm g (e.symm b) = g b
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.BlockMem.instNontrivial : ∀ (G : Type u_1) [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] [Nontrivial X] (a : X),
  Nontrivial (MulAction.BlockMem G a)
-- Mathlib.Data.ZMod.Basic
ZMod.lift_coe : ∀ (n : ℕ) {A : Type u_2} [inst : AddGroup A] (f : { f // f ↑n = 0 }) (x : ℤ), ((ZMod.lift n) f) ↑x = ↑f x
-- Mathlib.Topology.Algebra.Module.Equiv
/-- `ContinuousLinearEquivClass F σ M M₂` asserts `F` is a type of bundled continuous
`R`-linear equivs `M → M₂`. This is an abbreviation for
`ContinuousSemilinearEquivClass F (RingHom.id R) M M₂`.  -/
ContinuousLinearEquivClass : (F : Type u_1) →
  (R : outParam (Type u_2)) →
    [inst : Semiring R] →
      (M : outParam (Type u_3)) →
        [TopologicalSpace M] →
          [inst_2 : AddCommMonoid M] →
            (M₂ : outParam (Type u_4)) →
              [TopologicalSpace M₂] →
                [inst_4 : AddCommMonoid M₂] → [Module R M] → [Module R M₂] → [EquivLike F M M₂] → Prop
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Basic.0.Std.Tactic.BVDecide.BVExpr.toString.match_1.eq_7 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w w_1 n : ℕ) (expr : Std.Tactic.BVDecide.BVExpr w_1)
  (h : w = w_1 * n) (h_1 : (w idx : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var idx))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_4 :
    (w : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) → (rhs : Std.Tactic.BVDecide.BVExpr w) → motive w (lhs.bin op rhs))
  (h_5 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (operand : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op operand))
  (h_6 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_7 :
    (w w_2 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_2) →
        (h : w = w_2 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, Std.Tactic.BVDecide.BVExpr.replicate n expr h with
    | w, Std.Tactic.BVDecide.BVExpr.var idx => h_1 w idx
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_3 len w start expr
    | w, lhs.bin op rhs => h_4 w lhs op rhs
    | w, Std.Tactic.BVDecide.BVExpr.un op operand => h_5 w op operand
    | w, lhs.append rhs h => h_6 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_7 w w_2 n expr h
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_7 w w_1 n expr h
-- Mathlib.Data.Fintype.EquivFin
Equiv.embeddingEquivOfFinite_symm_apply_apply : ∀ (α : Type u_4) [inst : Finite α] (e : α ≃ α) (a : α), ((Equiv.embeddingEquivOfFinite α).symm e) a = e a
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.interSmallerFn.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (kv' : (a : α) × β a)
  (h_1 : (kv' : (a : α) × β a) → motive (some kv')) (h_2 : Unit → motive none),
  (match some kv' with
    | some kv' => h_1 kv'
    | none => h_2 ()) =
    h_1 kv'
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.Hom.comp.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  {M N K : CategoryTheory.Mat_ C} (f : M.Hom N) (g : N.Hom K) (i : M.ι) (k : K.ι),
  f.comp g i k = ∑ j, CategoryTheory.CategoryStruct.comp (f i j) (g j k)
-- Std.Sat.AIG.LawfulVecOperator
Std.Sat.AIG.LawfulVecOperator.denote_input_entry : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Std.Sat.AIG α → ℕ → Type}
  {f : {len : ℕ} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len}
  [Std.Sat.AIG.LawfulVecOperator α β fun {len} => f] {len : ℕ} {assign : α → Bool} (entry : Std.Sat.AIG.Entrypoint α)
  {input : β entry.aig len} {h : entry.ref.gate < (f entry.aig input).aig.decls.size},
  ⟦assign,
      { aig := (f entry.aig input).aig, ref := { gate := entry.ref.gate, invert := entry.ref.invert, hgate := h } }⟧ =
    ⟦assign, entry⟧
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Embedding.toHom_inj : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f g : L.Embedding M N}, f.toHom = g.toHom ↔ f = g
-- Mathlib.Topology.Algebra.Order.Group
/-- In a linearly ordered additive group, the integer multiples of an element are
dense iff they are the whole group.  -/
denseRange_zsmul_iff_surjective : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [inst_2 : LinearOrder G] [IsOrderedAddMonoid G]
  [OrderTopology G] {a : G}, (DenseRange fun x => x • a) ↔ Function.Surjective fun x => x • a
-- Batteries.Tactic.Lint.Basic
Batteries.Tactic.Lint.Linter.mk : (Lean.Name → Lean.MetaM (Option Lean.MessageData)) →
  Lean.MessageData → Lean.MessageData → Bool → Batteries.Tactic.Lint.Linter
-- Std.Time.Format.Modifier
Std.Time.Modifier.S.sizeOf_spec : ∀ (presentation : Std.Time.Fraction), sizeOf (Std.Time.Modifier.S presentation) = 1 + sizeOf presentation
-- Mathlib.Algebra.Category.MonCat.Limits
CommMonCat.forget_createsLimits : CategoryTheory.CreatesLimits (CategoryTheory.forget MonCat)
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.level_one' : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n), n = 1 → χ = 1
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.functor_map : ∀ (k G : Type u) [inst : CommRing k] [inst_1 : Group G] (n : ℕ) {A B : Rep.{u, u, u} k G} (φ : A ⟶ B),
  (groupHomology.functor k G n).map φ = groupHomology.map (MonoidHom.id G) φ n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.π_snd : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {X₃ Y₃ : C₃}
  {f₃ : X₃ ⟶ Y₃} (self : G.PullbackObjObj f₁ f₃),
  CategoryTheory.CategoryStruct.comp self.π self.snd = (G.obj (Opposite.op Y₁)).map f₃
-- Lean.Parser.Attr
Lean.Parser.Attr.externEntry : Lean.Parser.Parser
-- Mathlib.Analysis.InnerProductSpace.Spectrum
_private.Mathlib.Analysis.InnerProductSpace.Spectrum.0.LinearMap.IsSymmetric.unsortedEigenvalues.eq_1 : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E] {n : ℕ} (hT : T.IsSymmetric) (hn : Module.finrank 𝕜 E = n)
  (i : Fin n),
  LinearMap.IsSymmetric.unsortedEigenvalues✝ hT hn i =
    RCLike.re (↑T (DirectSum.IsInternal.subordinateOrthonormalBasisIndex hn ⋯ i ⋯))
-- Mathlib.Algebra.Free
Magma.AssocQuotient.lift_comp_of : ∀ {α : Type u} [inst : Mul α] {β : Type v} [inst_1 : Semigroup β] (f : α →ₙ* β),
  (Magma.AssocQuotient.lift f).comp Magma.AssocQuotient.of = f
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.hComp_assoc_heq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C]
  {a b c d : CategoryTheory.CatEnrichedOrdinary C} {f f' : a ⟶ b} {g g' : b ⟶ c} {h h' : c ⟶ d} (η : f ⟶ f')
  (θ : g ⟶ g') (κ : h ⟶ h'),
  CategoryTheory.CatEnrichedOrdinary.hComp (CategoryTheory.CatEnrichedOrdinary.hComp η θ) κ ≍
    CategoryTheory.CatEnrichedOrdinary.hComp η (CategoryTheory.CatEnrichedOrdinary.hComp θ κ)
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- The upper shadow of a set family `𝒜` is all sets we can get by adding one element to any set in
`𝒜`, and the (`k` times) iterated upper shadow (`upShadow^[k]`) is all sets we can get by adding
`k` elements from any set in `𝒜`.  -/
FinsetFamily.«term∂⁺» : Lean.ParserDescr
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- The left-translation shift is continuous.  -/
SymbolicDynamics.FullShift.continuous_mulShift : ∀ {A : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : TopologicalSpace A] (g : G),
  Continuous (SymbolicDynamics.FullShift.mulShift g)
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.IsBase.cardinalMk_le_cRank : ∀ {α : Type u} {M : Matroid α} {B : Set α}, M.IsBase B → Cardinal.mk ↑B ≤ M.cRank
-- Mathlib.RepresentationTheory.FinGroupCharZero
/-- If `G` is finite and its order is nonzero in the field `k`, then every object of
`FDRep k G` is injective.
 -/
FDRep.instInjectiveOfNeZeroCastCard : ∀ {k : Type u} [inst : Field k] {G : Type u} [Finite G] [inst_2 : Group G] [NeZero ↑(Nat.card G)] (V : FDRep k G),
  CategoryTheory.Injective V
-- Mathlib.Algebra.RingQuot
RingQuot.Rel.add_left : ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} ⦃a b c : R⦄, RingQuot.Rel r a b → RingQuot.Rel r (a + c) (b + c)
-- Mathlib.Topology.EMetricSpace.Diam
/-- The extended diameter of a singleton vanishes  -/
Metric.ediam_singleton : ∀ {X : Type u_2} {x : X} [inst : PseudoEMetricSpace X], Metric.ediam {x} = 0
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.prod.inr_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.inr X Y) CategoryTheory.Limits.prod.snd =
    CategoryTheory.CategoryStruct.id Y
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.norm_domDomCongr : ∀ (𝕜 : Type u) {ι : Type v} {ι' : Type v'} (G : Type wG) (G' : Type wG') [inst : Fintype ι] [inst_1 : Fintype ι']
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
  [inst_5 : NormedAddCommGroup G'] [inst_6 : NormedSpace 𝕜 G'] (σ : ι ≃ ι')
  (f : ContinuousMultilinearMap 𝕜 (fun x => G) G'), ‖ContinuousMultilinearMap.domDomCongr σ f‖ = ‖f‖
-- Mathlib.Combinatorics.Schnirelmann
/-- If `k` is omitted from the set, its Schnirelmann density is upper bounded by `1 - k⁻¹`.
 -/
schnirelmannDensity_le_of_notMem : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] {k : ℕ}, k ∉ A → schnirelmannDensity A ≤ 1 - (↑k)⁻¹
-- Mathlib.Algebra.GCDMonoid.Basic
dvd_antisymm_of_normalize_eq : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] [IsLeftCancelMulZero α] {a b : α},
  normalize a = a → normalize b = b → a ∣ b → b ∣ a → a = b
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.addGroup : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {N : Type u_6} →
                              [inst_7 : TopologicalSpace N] →
                                [inst_8 : ChartedSpace H N] →
                                  {n : WithTop ℕ∞} →
                                    {G : Type u_10} →
                                      [inst_9 : AddGroup G] →
                                        [inst_10 : TopologicalSpace G] →
                                          [inst_11 : ChartedSpace H' G] →
                                            [LieAddGroup I' n G] → AddGroup (ContMDiffMap I I' N G n)
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
/-- The space of affine maps between two normed spaces is linearly isometric to the product of the
codomain with the space of linear maps, by taking the value of the affine map at `(0 : V)` and the
linear part.  -/
ContinuousAffineMap.decompLinearIsometryEquiv : (𝕜 : Type u_1) →
  (R : Type u_2) →
    (V : Type u_3) →
      (W : Type u_4) →
        [inst : SeminormedAddCommGroup V] →
          [inst_1 : SeminormedAddCommGroup W] →
            [inst_2 : NontriviallyNormedField 𝕜] →
              [inst_3 : NormedSpace 𝕜 V] →
                [inst_4 : NormedSpace 𝕜 W] →
                  [inst_5 : Ring R] →
                    [inst_6 : Module R W] →
                      [inst_7 : ContinuousConstSMul R W] →
                        [inst_8 : SMulCommClass 𝕜 R W] → (V →ᴬ[𝕜] W) ≃ₗᵢ[R] W × (V →L[𝕜] W)
-- Aesop.Stats.Basic
Aesop.instMonadStatsReaderT : {m : Type → Type} → {α : Type} → [Aesop.MonadStats m] → Aesop.MonadStats (ReaderT α m)
-- Mathlib.Algebra.Group.Idempotent
IsIdempotentElem.iff_eq_one_of_isUnit : ∀ {M : Type u_1} [inst : Monoid M] {a : M}, IsUnit a → (IsIdempotentElem a ↔ a = 1)