mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey?_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (Std.DTreeMap.Const.insertMany t l).getKey? k = t.getKey? k
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.instCoeCommMonCat.eq_1 : CommGrpCat.instCoeCommMonCat = { coe := (CategoryTheory.forget₂ CommGrpCat CommMonCat).obj }
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
PresheafOfModules.Submodule.instPartialOrder : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → {M : PresheafOfModules R} → PartialOrder M.Submodule
-- Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
OrderDual.mulRightMono : ∀ {α : Type u} [inst : LE α] [inst_1 : Mul α] [c : MulRightMono α], MulRightMono αᵒᵈ
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.instIteratorLoopIdSearchStep : {s : String.Slice} → Std.IteratorLoop (String.Slice.Pattern.ForwardSliceSearcher s) Id Id
-- Batteries.Data.Fin.Lemmas
/-- **Alias** of `Fin.isSome_find?_iff`. -/
Fin.find?_isSome_iff : ∀ {n : ℕ} {p : Fin n → Bool}, (Fin.find? p).isSome = true ↔ ∃ i, p i = true
-- Mathlib.CategoryTheory.Functor.Const
CategoryTheory.Functor.constCompWhiskeringLeftIso_inv_app_app : ∀ (J : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  {D : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D] (F : CategoryTheory.Functor J D) (X : C) (X_1 : J),
  ((CategoryTheory.Functor.constCompWhiskeringLeftIso J F).inv.app X).app X_1 = CategoryTheory.CategoryStruct.id X
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.forallBoundedTelescopeImp : {α : Type} → Lean.Expr → Option ℕ → (Array Lean.Expr → Lean.Expr → Lean.MetaM α) → Bool → Bool → Lean.MetaM α
-- Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
AlgebraicTopology.DoldKan.homotopyPToId_eventually_constant : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) {q n : ℕ},
  n < q →
    (AlgebraicTopology.DoldKan.homotopyPToId X (q + 1)).hom n (n + 1) =
      (AlgebraicTopology.DoldKan.homotopyPToId X q).hom n (n + 1)
-- Mathlib.Logic.Function.CompTypeclasses
CompTriple.IsId.mk : ∀ {M : Type u_1} {σ : M → M}, σ = id → CompTriple.IsId σ
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.lt_natCast_add_one_iff`. -/
ENat.lt_coe_add_one_iff : ∀ {m : ℕ∞} {n : ℕ}, m < ↑n + 1 ↔ m ≤ ↑n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSignatureHelpOptions.fromJson : Lean.Json → Except String Lean.Lsp.SignatureHelpOptions
-- Mathlib.Logic.Equiv.Defs
Equiv.funUnique_symm_apply : ∀ (α : Sort u) (β : Sort u_1) [inst : Unique α], ⇑(Equiv.funUnique α β).symm = uniqueElim
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- A short complex `S` has left homology when there exists a `S.LeftHomologyData`  -/
CategoryTheory.ShortComplex.HasLeftHomology : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.ShortComplex C → Prop
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.inclRightFull : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D],
  (CategoryTheory.Join.inclRight C D).Full
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.algebraMap_apply' : ∀ (Γ : Type u_1) {R : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring Γ] [inst_2 : PartialOrder Γ]
  [inst_3 : IsStrictOrderedRing Γ] {S : Type u_4} [inst_4 : CommSemiring S] [inst_5 : Algebra S (PowerSeries R)]
  (x : S), (algebraMap S (HahnSeries Γ R)) x = (HahnSeries.ofPowerSeries Γ R) ((algebraMap S (PowerSeries R)) x)
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.down_mk : ∀ {α : Type u_2} [inst : Add α] [inst_1 : IsRightCancelAdd α] [inst_2 : One α] (j i : α),
  i + 1 = j → (ComplexShape.down α).Rel j i
-- Mathlib.Topology.Category.CompHausLike.Limits
CompHausLike.finiteCoproduct.ι_injective : ∀ {P : TopCat → Prop} {α : Type w} [inst : Finite α] (X : α → CompHausLike P)
  [inst_1 : CompHausLike.HasExplicitFiniteCoproduct X] (a : α),
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (CompHausLike.finiteCoproduct.ι X a))
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.prod_mono : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] ⦃s₁ s₂ : Subsemiring R⦄,
  s₁ ≤ s₂ → ∀ ⦃t₁ t₂ : Subsemiring S⦄, t₁ ≤ t₂ → s₁.prod t₁ ≤ s₂.prod t₂
-- Mathlib.Algebra.Lie.Classical
/-- A matrix transforming the bilinear form defined by the matrix `JB` into an
almost-split-signature diagonal matrix.

It looks like this as a `(2l+1) x (2l+1)` matrix of blocks:

```
[ 1 0  0 ]
[ 0 1 -1 ]
[ 0 1  1 ]
```

where sizes of the blocks are:

```
[`1 x 1` `1 x l` `1 x l`]
[`l x 1` `l x l` `l x l`]
[`l x 1` `l x l` `l x l`]
```  -/
LieAlgebra.Orthogonal.PB : (l : Type u_4) → (R : Type u₂) → [DecidableEq l] → [CommRing R] → Matrix (Unit ⊕ l ⊕ l) (Unit ⊕ l ⊕ l) R
-- Mathlib.Order.CompleteLattice.Defs
/-- **Alias** of the forward direction of `isLUB_iff_sSup_eq`. -/
IsLUB.sSup_eq : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α}, IsLUB s a → sSup s = a
-- Mathlib.Testing.Plausible.Functions
/-- Data structure specifying a total function using a list of pairs
and a default value returned when the input is not in the domain of
the partial function.

`mapToSelf f` encodes `x ↦ f x` when `x ∈ f` and `x ↦ x`,
i.e. `x` to itself, otherwise.

We use `Σ` to encode mappings instead of `×` because we
rely on the association list API defined in `Mathlib/Data/List/Sigma.lean`.
 -/
Plausible.InjectiveFunction : Type u → Type u
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.Algebra.lift_apply : ∀ {R : Type u_1} {ι : Type u_2} [inst : Preorder ι] (G : ι → Type u_3) {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  (f : (x x_1 : ι) → (h : x ≤ x_1) → T h) [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : CommSemiring R]
  [inst_5 : (i : ι) → Semiring (G i)] [inst_6 : (i : ι) → Algebra R (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] [inst_8 : Nonempty ι] (P : Type u_7)
  [inst_9 : Semiring P] [inst_10 : Algebra R P] (g : (i : ι) → G i →ₐ[R] P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) (z : DirectLimit G f),
  (DirectLimit.Algebra.lift G f P g Hg) z = DirectLimit.lift f (fun x1 x2 => (g x1) x2) ⋯ z
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.instHasHomologyUnopOfOpposite : ∀ {ι : Type u_1} (V : Type u_2) [inst : CategoryTheory.Category.{v_1, u_2} V] (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (K : HomologicalComplex Vᵒᵖ c) (i : ι) [K.HasHomology i],
  K.unop.HasHomology i
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.toSubmonoid_strictMono : ∀ {R : Type u} [inst : NonAssocRing R], StrictMono fun s => s.toSubmonoid
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
/-- The map `composableArrows₅ hS₁ i j hij ⟶ composableArrows₅ hS₂ i j hij` of exact
sequences induced by a morphism `φ : S₁ ⟶ S₂` between short exact short complexes of
homological complexes.  -/
HomologicalComplex.HomologySequence.mapComposableArrows₅ : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        {c : ComplexShape ι} →
          {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} →
            (S₁ ⟶ S₂) →
              (hS₁ : S₁.ShortExact) →
                (hS₂ : S₂.ShortExact) →
                  (i j : ι) →
                    (hij : c.Rel i j) →
                      HomologicalComplex.HomologySequence.composableArrows₅ hS₁ i j hij ⟶
                        HomologicalComplex.HomologySequence.composableArrows₅ hS₂ i j hij
-- Std.Time.Date.Unit.Month
/-- The ordinal value representing the month of October.
 -/
Std.Time.Month.Ordinal.october : Std.Time.Month.Ordinal
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : CompleteLattice γ] {g : CompleteLatticeHom β γ} {f₁ f₂ : CompleteLatticeHom α β},
  Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Scheme.Etale.forget_obj_hom : ∀ (X : AlgebraicGeometry.Scheme) (Y : X.Etale), ((AlgebraicGeometry.Scheme.Etale.forget X).obj Y).hom = Y.hom
-- Mathlib.Algebra.Ring.Prod
/-- Given semirings `R`, `S`, the natural projection homomorphism from `R × S` to `S`.  -/
RingHom.snd : (R : Type u_1) → (S : Type u_3) → [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → R × S →+* S
-- Mathlib.CategoryTheory.Triangulated.Functor
/-- The canonical isomorphism `(F ⋙ G).mapTriangle ≅ F.mapTriangle ⋙ G.mapTriangle`.  -/
CategoryTheory.Functor.mapTriangleCompIso : {C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            [inst_3 : CategoryTheory.HasShift C ℤ] →
              [inst_4 : CategoryTheory.HasShift D ℤ] →
                [inst_5 : CategoryTheory.HasShift E ℤ] →
                  (F : CategoryTheory.Functor C D) →
                    [inst_6 : F.CommShift ℤ] →
                      (G : CategoryTheory.Functor D E) →
                        [inst_7 : G.CommShift ℤ] → (F.comp G).mapTriangle ≅ F.mapTriangle.comp G.mapTriangle
-- Mathlib.Algebra.Lie.Ideal
LieIdeal.inclusion_injective : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I₁ I₂ : LieIdeal R L}
  (h : I₁ ≤ I₂), Function.Injective ⇑(LieIdeal.inclusion h)
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.addMonoidalFunctorComp_isMonoidal : ∀ {M : Type u} [inst : AddMonoid M] {N : Type u'} [inst_1 : AddMonoid N] {K : Type u} [inst_2 : AddMonoid K]
  (F : M →+ N) (G : N →+ K), CategoryTheory.NatTrans.IsMonoidal (CategoryTheory.Discrete.addMonoidalFunctorComp F G).hom
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.instPartialOrder : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {I : Ideal R} → PartialOrder (I.Filtration M)
-- Mathlib.Logic.Encodable.Basic
/-- An encodable type is equivalent to the range of its encoding function.  -/
Encodable.equivRangeEncode : (α : Type u_3) → [inst : Encodable α] → α ≃ ↑(Set.range Encodable.encode)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁ \ t₂).size + (t₁ ∩ t₂).size = t₁.size
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
/-- The non-zero fractional ideal `⟨X - x, Y - y⟩` of `F(W)` for some `x` and `y` in `F`.  -/
WeierstrassCurve.Affine.CoordinateRing.XYIdeal' : {F : Type u} →
  [inst : Field F] →
    {W : WeierstrassCurve.Affine F} →
      {x y : F} → W.Nonsingular x y → (FractionalIdeal (nonZeroDivisors W.CoordinateRing) W.FunctionField)ˣ
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.mk''_eq_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p : Submodule R M}
  (x : M), Quotient.mk'' x = Submodule.Quotient.mk x
-- Mathlib.Analysis.Normed.Group.Quotient
/-- `S.normedMk` agrees with `QuotientAddGroup.mk' S`.  -/
AddSubgroup.normedMk.apply : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] (S : AddSubgroup M) (m : M),
  S.normedMk m = (QuotientAddGroup.mk' S) m
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.maxD_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.maxD fallback ∈ t
-- Mathlib.Algebra.Quandle
/-- The associativity of a unital shelf comes for free.
 -/
UnitalShelf.assoc : ∀ {S : Type u_1} [inst : UnitalShelf S] (x y z : S), Shelf.act (Shelf.act x y) z = Shelf.act x (Shelf.act y z)
-- Mathlib.CategoryTheory.Limits.Cones
/-- Functoriality is functorial.  -/
CategoryTheory.Limits.Cocone.functorialityCompFunctoriality : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            {E : Type u₅} →
              [inst_3 : CategoryTheory.Category.{v₅, u₅} E] →
                (F : CategoryTheory.Functor J C) →
                  (G : CategoryTheory.Functor C D) →
                    (H : CategoryTheory.Functor D E) →
                      (CategoryTheory.Limits.Cocone.functoriality F G).comp
                          (CategoryTheory.Limits.Cocone.functoriality (F.comp G) H) ≅
                        CategoryTheory.Limits.Cocone.functoriality F (G.comp H)
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- `n + 1` points are affinely independent if and only if their
`vectorSpan` has dimension `n`.  -/
affineIndependent_iff_finrank_vectorSpan_eq : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] (p : ι → P) {n : ℕ},
  Fintype.card ι = n + 1 → (AffineIndependent k p ↔ Module.finrank k ↥(vectorSpan k (Set.range p)) = n)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKeyD_erase_eq_of_not_compare_maxKeyD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k fallback : α},
      (t.erase k).isEmpty = false →
        ¬cmp k (t.maxKeyD fallback) = Ordering.eq → (t.erase k).maxKeyD fallback = t.maxKeyD fallback
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.nrRealPlaces_eq_one_of_finrank_eq_one : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K],
  Module.finrank ℚ K = 1 → NumberField.InfinitePlace.nrRealPlaces K = 1
-- Mathlib.Algebra.Free
FreeMagma.lift_comp_of' : ∀ {α : Type u} {β : Type v} [inst : Mul β] (f : FreeMagma α →ₙ* β), FreeMagma.lift (⇑f ∘ FreeMagma.of) = f
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_zero : 0⁻¹ = ⊤
-- Mathlib.Analysis.Complex.Trigonometric
Complex.exp_eq_exp_re_mul_sin_add_cos : ∀ (x : ℂ), Complex.exp x = Complex.exp ↑x.re * (Complex.cos ↑x.im + Complex.sin ↑x.im * Complex.I)
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_two_assoc : ∀ {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₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ : C₁} {X₂ Y₂ : C₂} {X₃ : C₃}
  (f₂ : X₂ ⟶ Y₂) (g : (F.obj X₁).obj Y₂ ⟶ X₃) {Z : C₂} (h : (G.obj (Opposite.op X₁)).obj X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (adj₂.homEquiv (CategoryTheory.CategoryStruct.comp ((F.obj X₁).map f₂) g)) h =
    CategoryTheory.CategoryStruct.comp f₂ (CategoryTheory.CategoryStruct.comp (adj₂.homEquiv g) h)
-- Mathlib.LinearAlgebra.LinearDisjoint
Submodule.LinearDisjoint.injective : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N → Function.Injective ⇑(M.mulMap N)
-- Mathlib.MeasureTheory.Function.AEEqFun
ContinuousMap.toAEEqFunAddHom.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) [inst_1 : TopologicalSpace α]
  [inst_2 : BorelSpace α] [inst_3 : TopologicalSpace β] [inst_4 : SecondCountableTopologyEither α β]
  [inst_5 : TopologicalSpace.PseudoMetrizableSpace β] [inst_6 : AddGroup β] [inst_7 : IsTopologicalAddGroup β],
  ContinuousMap.toAEEqFunAddHom μ = { toFun := ContinuousMap.toAEEqFun μ, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Order.Floor.Ring
Int.floor_natCast : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (n : ℕ), ⌊↑n⌋ = ↑n
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instInhabitedZoneRules : Inhabited Std.Time.TimeZone.ZoneRules
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.pairingIn_threeShortAddTwoLong_left : ∀ {ι : 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] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2] [Finite ι] [CharZero R] [IsDomain R] (i : ι),
  P.pairingIn ℤ (RootPairing.EmbeddedG2.threeShortAddTwoLong P) i =
    3 * P.pairingIn ℤ (RootPairing.EmbeddedG2.short P) i + 2 * P.pairingIn ℤ (RootPairing.EmbeddedG2.long P) i
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.valuation_mul : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {x y : ℚ_[p]}, x ≠ 0 → y ≠ 0 → (x * y).valuation = x.valuation + y.valuation
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsSimpleAddGroup.prime_card : ∀ {α : Type u_1} [inst : AddCommGroup α] [IsSimpleAddGroup α], Nat.Prime (Nat.card α)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.eqLhs : Bool → Lean.Meta.Grind.EMatchTheoremKind
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
/-- `S[X] ⊗[R] R[Y] ≃ S[X, Y]`  -/
MvPolynomial.tensorEquivSum : (R : Type u) →
  [inst : CommSemiring R] →
    (σ : Type u_1) →
      (ι : Type u_2) →
        (S : Type u_3) →
          [inst_1 : CommSemiring S] →
            [inst_2 : Algebra R S] → TensorProduct R (MvPolynomial σ S) (MvPolynomial ι R) ≃ₐ[S] MvPolynomial (σ ⊕ ι) S
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalCStarAlgebra.toNormedSpace : {A : Type u_1} → [self : NonUnitalCStarAlgebra A] → NormedSpace ℂ A
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- A pushout cone is a colimit cocone in `Cᵒᵖ` if and only if the corresponding pullback cone
in `C` is a limit cone.  -/
CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitUnop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : Cᵒᵖ} →
      {f : X ⟶ Y} →
        {g : X ⟶ Z} →
          (c : CategoryTheory.Limits.PushoutCocone f g) →
            CategoryTheory.Limits.IsColimit c ≃ CategoryTheory.Limits.IsLimit c.unop
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.coe_map : ∀ {α : Type u_1} (n : ℕ) {β : Type u_2} (f : α ↪ β) (s : ↑(Set.powersetCard α n)),
  ↑(Set.powersetCard.map n f s) = ⇑f '' ↑s
-- Mathlib.Analysis.Calculus.FDeriv.Prod
differentiableWithinAt_snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {p : E × F}
  {s : Set (E × F)}, DifferentiableWithinAt 𝕜 Prod.snd s p
-- Mathlib.Algebra.Homology.HomologicalComplex
ChainComplex.mkHom_f_succ_succ : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (P Q : ChainComplex V ℕ) (zero : P.X 0 ⟶ Q.X 0) (one : P.X 1 ⟶ Q.X 1)
  (one_zero_comm : CategoryTheory.CategoryStruct.comp one (Q.d 1 0) = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero)
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X n ⟶ Q.X n) ×'
            (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×'
              CategoryTheory.CategoryStruct.comp f' (Q.d (n + 1) n) =
                CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f) →
        (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
          CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 2) (n + 1)) =
            CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst)
  (n : ℕ),
  (P.mkHom Q zero one one_zero_comm succ).f (n + 2) =
    (succ n ⟨(P.mkHom Q zero one one_zero_comm succ).f n, ⟨(P.mkHom Q zero one one_zero_comm succ).f (n + 1), ⋯⟩⟩).fst
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryGT?.go.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (best : Option ((a : α) × β a))
  (a : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.getEntryGT?.go k best a =
    match a with
    | Std.DTreeMap.Internal.Impl.leaf => best
    | Std.DTreeMap.Internal.Impl.inner size ky y l r =>
      match compare k ky with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.getEntryGT?.go k (some ⟨ky, y⟩) l
      | x => Std.DTreeMap.Internal.Impl.getEntryGT?.go k best r
-- Batteries.Data.Fin.Coding
Fin.decodeSigma.eq_2 : ∀ (n_2 : ℕ) (f_2 : Fin (n_2 + 1) → ℕ) (x_2 : ℕ) (hx : x_2 < Fin.sum f_2),
  Fin.decodeSigma f_2 ⟨x_2, hx⟩ =
    if hx0 : x_2 < f_2 0 then ⟨0, ⟨x_2, hx0⟩⟩
    else
      have hxf := ⋯;
      match Fin.decodeSigma (fun x => f_2 x.succ) ⟨x_2 - f_2 0, hxf⟩ with
      | ⟨⟨i, hi⟩, y⟩ => ⟨⟨i + 1, ⋯⟩, y⟩
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.coe_fstL : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : Semiring 𝕜] [inst_3 : AddCommGroup α] [inst_4 : AddCommGroup β] [inst_5 : Module 𝕜 α] [inst_6 : Module 𝕜 β],
  ↑(WithLp.fstL p 𝕜 α β) = WithLp.fstₗ p 𝕜 α β
-- Batteries.Lean.LawfulMonadLift
instLawfulMonadLiftBaseIOEIO_batteries : ∀ {ε : Type}, LawfulMonadLift BaseIO (EIO ε)
-- Mathlib.Algebra.Category.Ring.Basic
CommRingCat.ofHom_apply : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) (r : R),
  (CategoryTheory.ConcreteCategory.hom (CommRingCat.ofHom f)) r = f r
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
quasispectrum.not_isUnit_mem : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalRing A] [inst_2 : Module R A] (a : A)
  {r : R}, ¬IsUnit r → r ∈ quasispectrum R a
-- Init.Data.String.OrderInstances
String.Pos.instTotalLe : ∀ {s : String}, Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.Combinatorics.Additive.Energy
Finset.le_addEnergy_self : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Add α] {s : Finset α}, s.card ^ 2 ≤ s.addEnergy s
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
measurableSet_frontier : ∀ {α : Type u_1} {s : Set α} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α],
  MeasurableSet (frontier s)
-- Mathlib.Order.SuccPred.Basic
Order.pred_succ_iterate_of_not_isMax : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [inst_2 : PredOrder α] (i : α) (n : ℕ),
  ¬IsMax (Order.succ^[n - 1] i) → Order.pred^[n] (Order.succ^[n] i) = i
-- Mathlib.Data.Fintype.Card
Fintype.card_pos_iff : ∀ {α : Type u_1} [inst : Fintype α], 0 < Fintype.card α ↔ Nonempty α
-- Lean.Meta.Tactic.Grind.CasesMatch
_private.Lean.Meta.Tactic.Grind.CasesMatch.0.Lean.Meta.Grind.casesMatch.updateTags : Lean.MVarId → Array Lean.Expr → Lean.MetaM Unit
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteProfiniteContinuousMap : CategoryTheory.HasForget₂ ProfiniteAddGrp.{u_1} Profinite
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_eq_some_getD_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {a : α} {fallback : β a}, t.contains a = true → t.get? a = some (t.getD a fallback)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Ioc₀ : ∀ {G₀ : Type u_2} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {c : G₀} (a b : G₀),
  0 < c → (fun x => c * x) ⁻¹' Set.Ioc a b = Set.Ioc (a / c) (b / c)
-- Mathlib.Algebra.Category.Grp.Limits
/-- The chosen cone is a limit cone.
(Generally, you'll just want to use `limit.cone F`.)  -/
GrpCat.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J GrpCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget GrpCat)).sections] →
        CategoryTheory.Limits.IsLimit (GrpCat.limitCone F)