mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.Step.cons_not : ∀ {α : Type u} {L : List (α × Bool)} {x : α} {b : Bool}, FreeGroup.Red.Step ((x, b) :: (x, !b) :: L) L
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.get_bind_map_set : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  {α : Type u_1} (f : σ → PUnit.{u_1 + 1} → α),
  (do
      let s ← get
      f s <$> set s) =
    do
    let __do_lift ← get
    pure (f __do_lift PUnit.unit)
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
/-- If an additive monoid `M` continuously acts on an R₁ topological space `X`,
`g` is an element of `M` such that its natural multiples are dense in `M`,
and `μ` is a finite inner regular measure on `X` which is ergodic with respect to the action of `M`,
then the vector addition of `g` is an ergodic map.  -/
ergodic_vadd_of_denseRange_nsmul : ∀ {X : Type u_2} [inst : TopologicalSpace X] [R1Space X] [inst_2 : MeasurableSpace X] [BorelSpace X] {M : Type u_3}
  [inst_4 : AddMonoid M] [inst_5 : TopologicalSpace M] [inst_6 : AddAction M X] [ContinuousVAdd M X] {g : M},
  (DenseRange fun x => x • g) →
    ∀ (μ : MeasureTheory.Measure X) [MeasureTheory.IsFiniteMeasure μ] [μ.InnerRegular] [ErgodicVAdd M X μ],
      Ergodic (fun x => g +ᵥ x) μ
-- Mathlib.FieldTheory.Finite.Basic
/-- If `L/K` is an algebraic extension of a finite field, the Frobenius `K`-algebra endomorphism
of `L` is an automorphism.  -/
FiniteField.frobeniusAlgEquivOfAlgebraic : (K : Type u_1) →
  [inst : Field K] →
    [Fintype K] → (L : Type u_3) → [inst_2 : Field L] → [inst_3 : Algebra K L] → [Algebra.IsAlgebraic K L] → Gal(L/K)
-- Mathlib.Data.List.DropRight
List.rtakeWhile_concat : ∀ {α : Type u_1} (p : α → Bool) (l : List α) (x : α),
  List.rtakeWhile p (l ++ [x]) = if p x = true then List.rtakeWhile p l ++ [x] else []
-- Mathlib.Analysis.Convex.Jensen
/-- Concave **strict Jensen inequality**.

If the function is strictly concave, the weights are strictly positive and the indexed family of
points is non-constant, then Jensen's inequality is strict.

See also `StrictConcaveOn.map_sum_eq_iff`.  -/
StrictConcaveOn.lt_map_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConcaveOn 𝕜 s f →
    (∀ i ∈ t, 0 < w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) → (∃ j ∈ t, ∃ k ∈ t, p j ≠ p k) → ∑ i ∈ t, w i • f (p i) < f (∑ i ∈ t, w i • p i)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.pushToken : Lean.SourceInfo → String → Bool → Lean.PrettyPrinter.FormatterM Unit
-- Qq.ForLean.ReduceEval
Lean.Meta.instReduceEvalLiteral_qq : Lean.Meta.ReduceEval Lean.Literal
-- Lean.Elab.DefView
Lean.Elab.HeaderProcessedSnapshot.mk.sizeOf_spec : ∀ (toSnapshot : Lean.Language.Snapshot) (view : Lean.Elab.DefViewElabHeaderData) (state : Lean.Elab.Term.SavedState)
  (tacStx? : Option Lean.Syntax) (tacSnap? : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot))
  (bodyStx : Lean.Syntax) (bodySnap : Lean.Language.SnapshotTask (Option Lean.Elab.BodyProcessedSnapshot))
  (moreSnaps : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)),
  sizeOf
      { toSnapshot := toSnapshot, view := view, state := state, tacStx? := tacStx?, tacSnap? := tacSnap?,
        bodyStx := bodyStx, bodySnap := bodySnap, moreSnaps := moreSnaps } =
    1 + sizeOf toSnapshot + sizeOf view + sizeOf state + sizeOf tacStx? + sizeOf tacSnap? + sizeOf bodyStx +
        sizeOf bodySnap +
      sizeOf moreSnaps
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Predicate stating that a match for a given pattern is never a proper suffix of another match.

This implies that the notion of reverse match and longest reverse match coincide.
 -/
String.Slice.Pattern.Model.NoSuffixPatternModel : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.Model.PatternModel pat] → Prop
-- Batteries.Data.BitVec.Lemmas
/-- **Alias** of `BitVec.getLsb_ofFnBE`. -/
BitVec.getLsb'_ofFnBE : ∀ {n : ℕ} (f : Fin n → Bool) (i : Fin n), (BitVec.ofFnBE f).getLsb i = f i.rev
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.mul_le_right : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {x y : ↑(Set.Icc 0 1)},
  x * y ≤ y
-- Mathlib.Data.FunLike.Ring
/-- A `FunLike` type with `(f + g) x = f x + g x` and `(f * g) x = f (g x)` is a `Ring` if `α` is a
`Ring`.  -/
FunLike.ring : {F : Type u_1} →
  {α : Type u_2} →
    [inst : FunLike F α α] →
      [inst_1 : Zero F] →
        [inst_2 : One F] →
          [inst_3 : Mul F] →
            [inst_4 : Add F] →
              [inst_5 : Neg F] →
                [inst_6 : Sub F] →
                  [inst_7 : AddCommGroup α] →
                    [IsZeroApply F α α] →
                      [IsAddApply F α α] →
                        [IsOneApplyEqSelf F α] →
                          [IsMulApplyEqComp F α] →
                            [IsNegApply F α α] →
                              [IsSubApply F α α] →
                                [inst_14 : SMul ℕ F] →
                                  [IsSMulApply ℕ F α α] →
                                    [inst_16 : SMul ℤ F] →
                                      [IsSMulApply ℤ F α α] →
                                        [AddMonoidHomClass F α α] →
                                          [inst_19 : NatCast F] →
                                            [IsNatCastApply F α] → [inst_21 : IntCast F] → [IsIntCastApply F α] → Ring F
-- Init.Data.Dyadic.Basic
_private.Init.Data.Dyadic.Basic.0.Rat.toDyadic.match_1.splitter : (motive : ℤ → Sort u_1) →
  (prec : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((n : ℕ) → motive (Int.negSucc n)) → motive prec
-- Mathlib.Algebra.Star.StarRingHom
/-- Transitivity of `StarRingEquiv`.  -/
StarRingEquiv.trans : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      [inst : Add A] →
        [inst_1 : Add B] →
          [inst_2 : Mul A] →
            [inst_3 : Mul B] →
              [inst_4 : Star A] →
                [inst_5 : Star B] →
                  [inst_6 : Add C] → [inst_7 : Mul C] → [inst_8 : Star C] → (A ≃⋆+* B) → (B ≃⋆+* C) → A ≃⋆+* C
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for division of `BitVec`s.  -/
BitVec.reduceDiv : Lean.Meta.Simp.DSimproc
-- Mathlib.FieldTheory.IsPerfectClosure
/-- If `i : K →+* L` is `p`-radical, then for any reduced ring `M` of exponential characteristic
`p`, the map `(L →+* M) → (K →+* M)` induced by `i` is injective.
A special case of `IsPRadical.injective_comp_of_pNilradical_eq_bot`
and a generalization of `IsPurelyInseparable.injective_comp_algebraMap`.  -/
IsPRadical.injective_comp : ∀ {K : Type u_1} {L : Type u_2} (M : Type u_3) [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (p : ℕ) [ExpChar M p] [IsPRadical i p] [IsReduced M], Function.Injective fun f => f.comp i
-- Mathlib.RingTheory.FinitePresentation
/-- If `A` is a finitely presented `R`-algebra, then `MvPolynomial (Fin n) A` is finitely presented
as `R`-algebra.  -/
Algebra.FinitePresentation.mvPolynomial_of_finitePresentation : ∀ {R : Type w₁} {A : Type w₂} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Algebra.FinitePresentation R A] (ι : Type v) [Finite ι], Algebra.FinitePresentation R (MvPolynomial ι A)
-- Mathlib.Analysis.Meromorphic.Basic
Meromorphic.const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_4} [inst_3 : NormedRing R] [inst_4 : Module R E] [IsBoundedSMul R E]
  {f : 𝕜 → E} [SMulCommClass 𝕜 R E], Meromorphic f → ∀ (c : R), Meromorphic (c • f)
-- Mathlib.Algebra.Regular.Opposite
isAddRegular_unop : ∀ {R : Type u_1} [inst : Add R] {a : Rᵃᵒᵖ}, IsAddRegular (AddOpposite.unop a) ↔ IsAddRegular a
-- Mathlib.Algebra.Polynomial.Div
Polynomial.add_modByMonic : ∀ {R : Type u} [inst : CommRing R] {q : Polynomial R} (p₁ p₂ : Polynomial R), (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iter.toArray.eq_1 : ∀ {α β : Type w} [inst : Std.Iterator α Id β] (it : Std.Iter β), it.toArray = it.toIterM.toArray.run
-- Mathlib.Data.Nat.Prime.Defs
Nat.minFac_eq : ∀ (n : ℕ), n.minFac = if 2 ∣ n then 2 else n.minFacAux 3
-- Mathlib.Data.Nat.MaxPowDiv
Nat.maxPowDvdDiv.eq_1 : ∀ (p n : ℕ), p.maxPowDvdDiv n = if H : 1 < p ∧ n ≠ 0 then Nat.maxPowDvdDiv.go n p H else (0, n)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.iteratedDerivWithin_cos_Icc : ∀ (n : ℕ) {a b : ℝ},
  a < b → ∀ {x : ℝ}, x ∈ Set.Icc a b → iteratedDerivWithin n Real.cos (Set.Icc a b) x = iteratedDeriv n Real.cos x
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.mk.inj : ∀ {R : Type u} {S : Type v} {ι : Type w} {inst : CommRing R} {inst_1 : CommRing S} {inst_2 : Algebra R S}
  {P : Algebra.Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} {inst_3 : CommRing R'}
  {inst_4 : CommRing S'} {inst_5 : Algebra R' S'} {P' : Algebra.Generators R' S' ι'} {inst_6 : Algebra S S'}
  {val : ι → P'.Ring} {aeval_val : ∀ (i : ι), (MvPolynomial.aeval P'.val) (val i) = (algebraMap S S') (P.val i)}
  {val_1 : ι → P'.Ring} {aeval_val_1 : ∀ (i : ι), (MvPolynomial.aeval P'.val) (val_1 i) = (algebraMap S S') (P.val i)},
  { val := val, aeval_val := aeval_val } = { val := val_1, aeval_val := aeval_val_1 } → val = val_1
-- Mathlib.Data.Fin.Tuple.Curry
Function.OfArity.curry_two_eq_curry : ∀ {α β : Type u} (f : (Fin 2 → α) → β), Function.OfArity.curry f = Function.curry (f ∘ ⇑(finTwoArrowEquiv α).symm)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_hom_inv_whiskerRight_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) (k : c ⟶ d)
  {Z : a ⟶ d} (h_1 : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g k) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η.hom k))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η.inv k)) h_1) =
    h_1
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2.stepAux.eq_1 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [inst : DecidableEq K] (x : σ)
  (x_1 : (k : K) → List (Γ k)) (k : K) (f : σ → Γ k) (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2.stepAux (Turing.TM2.Stmt.push k f q) x x_1 = Turing.TM2.stepAux q x (Function.update x_1 k (f x :: x_1 k))
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.equiv_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} (h : IsTensorProduct f) (x : TensorProduct R M₁ M₂),
  h.equiv x = (TensorProduct.lift f) x
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Context.mk.injEq : ∀ (m returnType : Lean.Syntax) (uvars : Array Lean.Elab.Term.Do.Var) (kind : Lean.Elab.Term.Do.ToTerm.Kind)
  (m_1 returnType_1 : Lean.Syntax) (uvars_1 : Array Lean.Elab.Term.Do.Var) (kind_1 : Lean.Elab.Term.Do.ToTerm.Kind),
  ({ m := m, returnType := returnType, uvars := uvars, kind := kind } =
      { m := m_1, returnType := returnType_1, uvars := uvars_1, kind := kind_1 }) =
    (m = m_1 ∧ returnType = returnType_1 ∧ uvars = uvars_1 ∧ kind = kind_1)
-- Mathlib.Topology.Algebra.Monoid
addMonoidHomOfMemClosureRangeCoe_apply : ∀ {M₁ : Type u_6} {M₂ : Type u_7} [inst : TopologicalSpace M₂] [inst_1 : T2Space M₂] [inst_2 : AddZeroClass M₁]
  [inst_3 : AddZeroClass M₂] [inst_4 : ContinuousAdd M₂] {F : Type u_8} [inst_5 : FunLike F M₁ M₂]
  [inst_6 : AddMonoidHomClass F M₁ M₂] (f : M₁ → M₂) (hf : f ∈ closure (Set.range fun f x => f x)),
  ⇑(addMonoidHomOfMemClosureRangeCoe f hf) = f
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.instCoeSortType : CoeSort SemiNormedGrp (Type u_1)
-- Mathlib.Algebra.CharP.Defs
ExpChar.zero : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R], ExpChar R 1
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_div : ∀ (a b : UInt8), (a / b).toUInt16 = a.toUInt16 / b.toUInt16
-- Mathlib.Algebra.Order.Ring.Unbundled.Rat
Rat.instSemilatticeInf : SemilatticeInf ℚ
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.range_eq_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)} (p : F' ⟶ F)
  [CategoryTheory.Epi p], CategoryTheory.Subfunctor.range p = ⊤
-- Mathlib.Tactic.NormNum.Basic
Mathlib.Meta.NormNum.isInt_add : ∀ {α : Type u_1} [inst : Ring α] {f : α → α → α} {a b : α} {a' b' c : ℤ},
  f = HAdd.hAdd →
    Mathlib.Meta.NormNum.IsInt a a' →
      Mathlib.Meta.NormNum.IsInt b b' → a'.add b' = c → Mathlib.Meta.NormNum.IsInt (f a b) c
-- Init.Data.SInt.Lemmas
ISize.minValue_le_toInt : ∀ (x : ISize), ISize.minValue.toInt ≤ x.toInt
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.isPositive_self_comp_adjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (S : E →L[𝕜] F),
  (S ∘SL ContinuousLinearMap.adjoint S).IsPositive
-- Mathlib.Data.Num.Basic
/-- The predecessor of a `ZNum`.  -/
ZNum.pred : ZNum → ZNum
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_insertManyIfNewUnit!_list_of_not_mem_of_mem : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] [inst : Inhabited α],
  t.WF →
    ∀ {l : List α} {k k' : α},
      compare k k' = Ordering.eq →
        k ∉ t →
          List.Pairwise (fun a b => ¬compare a b = Ordering.eq) l →
            k ∈ l → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)).getKey! k' = k
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- Let `μ` be a σ-finite left invariant measure on `G`. Then `μ` is equal to the
additive Haar measure defined by `K₀` iff `μ K₀ = 1`.  -/
MeasureTheory.Measure.addHaarMeasure_eq_iff : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [SecondCountableTopology G]
  (K₀ : TopologicalSpace.PositiveCompacts G) (μ : MeasureTheory.Measure G) [MeasureTheory.SigmaFinite μ]
  [μ.IsAddLeftInvariant], MeasureTheory.Measure.addHaarMeasure K₀ = μ ↔ μ ↑K₀ = 1
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.le_max!_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  k ∈ t → (cmp k t.max!).isLE = true
-- Mathlib.Combinatorics.Enumerative.Composition
/-- The composition made of blocks all of size `1`.  -/
Composition.ones : (n : ℕ) → Composition n
-- Mathlib.Topology.Sets.Closeds
/-- `TopologicalSpace.Closeds.compl` as an `OrderIso` to the order dual of
`TopologicalSpace.Opens α`.  -/
TopologicalSpace.Closeds.complOrderIso : (α : Type u_2) → [inst : TopologicalSpace α] → TopologicalSpace.Closeds α ≃o (TopologicalSpace.Opens α)ᵒᵈ
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.gciMapComap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ⇑f),
  AddSubmonoid.gciMapComap hf = ⋯.toGaloisCoinsertion ⋯
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.cmp.match_1.eq_6 : ∀ (motive : PosNum → PosNum → Sort u_1) (a b : PosNum) (h_1 : Unit → motive PosNum.one PosNum.one)
  (h_2 : (x : PosNum) → motive x PosNum.one) (h_3 : (x : PosNum) → motive PosNum.one x)
  (h_4 : (a b : PosNum) → motive a.bit0 b.bit0) (h_5 : (a b : PosNum) → motive a.bit0 b.bit1)
  (h_6 : (a b : PosNum) → motive a.bit1 b.bit0) (h_7 : (a b : PosNum) → motive a.bit1 b.bit1),
  (match a.bit1, b.bit0 with
    | PosNum.one, PosNum.one => h_1 ()
    | x, PosNum.one => h_2 x
    | PosNum.one, x => h_3 x
    | a.bit0, b.bit0 => h_4 a b
    | a.bit0, b.bit1 => h_5 a b
    | a.bit1, b.bit0 => h_6 a b
    | a.bit1, b.bit1 => h_7 a b) =
    h_6 a b
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.homologyDataIdId_right_p : ∀ {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.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j : ι} (f : i ⟶ j) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.homologyDataIdId._auto_3),
  (X.homologyDataIdId f n₀ n₁ n₂ hn₁ hn₂).right.p =
    CategoryTheory.CategoryStruct.id ((X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f))
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.ext_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {m₁ m₂ : Std.ExtHashSet α},
  (∀ (k : α), k ∈ m₁ ↔ k ∈ m₂) → m₁ = m₂
-- Mathlib.Data.Sigma.Basic
Sigma.forall : ∀ {α : Type u_1} {β : α → Type u_4} {p : (a : α) × β a → Prop},
  (∀ (x : (a : α) × β a), p x) ↔ ∀ (a : α) (b : β a), p ⟨a, b⟩
-- Mathlib.Topology.Homotopy.HomotopyGroup
GenLoop.fromLoop_coe : ∀ {N : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {x : X} [inst_1 : DecidableEq N] (i : N)
  (p : LoopSpace (↑(GenLoop { j // j ≠ i } X x)) GenLoop.const),
  ↑(GenLoop.fromLoop i p) =
    ({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp p.toContinuousMap).uncurry.comp ↑(Cube.splitAt i)
-- Mathlib.Data.Set.Basic
Set.ne_univ_iff_exists_notMem : ∀ {α : Type u_1} (s : Set α), s ≠ Set.univ ↔ ∃ a, a ∉ s
-- Mathlib.RingTheory.Extension.Presentation.Submersive
/-- If `P` is a pre-submersive presentation of `S` over `R` and `T` is an `R`-algebra, we
obtain a natural pre-submersive presentation of `T ⊗[R] S` over `T`.  -/
Algebra.PreSubmersivePresentation.baseChange : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              (T : Type u_1) →
                [inst_3 : CommRing T] →
                  [inst_4 : Algebra R T] →
                    Algebra.PreSubmersivePresentation R S ι σ →
                      Algebra.PreSubmersivePresentation T (TensorProduct R T S) ι σ
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instIsUniformAddGroup : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F], IsUniformAddGroup (SchwartzMap E F)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.IsCut.gt_trans : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x y : α} [RBTree.RBNode.IsCut cmp cut]
  [Std.TransCmp cmp], cmp x y = Ordering.lt → cut y = Ordering.gt → cut x = Ordering.gt
-- Mathlib.Algebra.Category.Grp.Limits
/-- If `J` is `u`-small, `GrpCat.{u}` has limits of shape `J`.  -/
GrpCat.hasLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.HasLimitsOfShape J GrpCat
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.toBilinForm_inj : ∀ {𝕜 : Type u_2} {E : Type u_5} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] (L₁ L₂ : E →L[𝕜] E →L[𝕜] 𝕜), L₁.toBilinForm = L₂.toBilinForm ↔ L₁ = L₂
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.faithful_map₂ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B}
  {F : CategoryTheory.Functor C A} {G : CategoryTheory.Functor D B} (α : F.comp U ⟶ S.comp G) (β : G.obj T ⟶ V)
  [F.Faithful], (CategoryTheory.CostructuredArrow.map₂ α β).Faithful
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.epi₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles, T.mor₂ = 0 → CategoryTheory.Epi T.mor₁
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.CMExtension.algebraMap_equivMaximalRealSubfield_symm_apply : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : NumberField.IsTotallyReal F] [inst_2 : Field K]
  [inst_3 : CharZero K] [inst_4 : Algebra.IsIntegral ℚ K] [inst_5 : NumberField.IsTotallyComplex K]
  [inst_6 : Algebra F K] [inst_7 : Algebra.IsQuadraticExtension F K] (x : ↥(NumberField.maximalRealSubfield K)),
  (algebraMap F K) ((NumberField.CMExtension.equivMaximalRealSubfield F K).symm x) =
    (algebraMap (↥(NumberField.maximalRealSubfield K)) K) x
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.awayToAwayRight_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] (x : R) [inst_4 : IsLocalization.Away x S] (y : R) [inst_5 : Algebra R P]
  [inst_6 : IsLocalization.Away (x * y) P] (a : R),
  (IsLocalization.Away.awayToAwayRight x y) ((algebraMap R S) a) = (algebraMap R P) a
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.ne_one : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M}, IsPrimitiveRoot ζ k → 1 < k → ζ ≠ 1
-- Mathlib.SetTheory.Ordinal.FundamentalSequence
Ordinal.IsFundamentalSequence.strict_mono : ∀ {a o : Ordinal.{u}} {f : (b : Ordinal.{u}) → b < o → Ordinal.{u}},
  a.IsFundamentalSequence o f → ∀ {i j : Ordinal.{u}} (hi : i < o) (hj : j < o), i < j → f i hi < f j hj
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.baseChange_addXYZ : ∀ {R : Type r} {S : Type s} {A : Type u} {B : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : CommRing B] {W' : WeierstrassCurve.Jacobian R} [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B) (P Q : Fin 3 → A), (W'.baseChange B).addXYZ (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ (W'.baseChange A).addXYZ P Q
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.registerMVarErrorInfo : Lean.Elab.Term.MVarErrorInfo → Lean.Elab.TermElabM Unit
-- Mathlib.Analysis.Real.Cardinality
Cardinal.cantorFunctionAux_true : ∀ {c : ℝ} {f : ℕ → Bool} {n : ℕ}, f n = true → Cardinal.cantorFunctionAux c f n = c ^ n
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- Sum of finitely many `term`s.  -/
ZetaAsymptotics.termSum : ℝ → ℕ → ℝ
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.Tendsto.const_mul : ∀ {α : Type u_2} {f : Filter α} {m : α → EReal} {a b : EReal},
  Filter.Tendsto m f (nhds b) → a ≠ ⊥ ∨ b ≠ 0 → a ≠ ⊤ ∨ b ≠ 0 → Filter.Tendsto (fun b => a * m b) f (nhds (a * b))
-- Mathlib.Data.FinEnum
List.mem_pi_toList : ∀ {α : Type u_1} [inst : FinEnum α] {β : α → Type u_2} [inst_1 : (a : α) → FinEnum (β a)] (xs : List α)
  (f : (a : α) → a ∈ xs → β a), f ∈ xs.pi fun x => FinEnum.toList (β x)
-- Mathlib.FieldTheory.IsAlgClosed.Basic
/-- If `k` is algebraically closed, then every irreducible polynomial over `k` is linear.
 -/
IsAlgClosed.degree_eq_one_of_irreducible : ∀ (k : Type u) [inst : Field k] [IsAlgClosed k] {p : Polynomial k}, Irreducible p → p.degree = 1