mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ConcreteCategory.Elementwise
CategoryTheory.Limits.colimit.ι_desc_apply : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F] (c : CategoryTheory.Limits.Cocone F)
  (j : J) {F_1 : C → C → Type uF} {carrier : C → Type w}
  {instFunLike : (X Y : C) → FunLike (F_1 X Y) (carrier X) (carrier Y)} [inst_3 : CategoryTheory.ConcreteCategory C F_1]
  (x : carrier (F.obj j)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.desc F c))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x) =
    (CategoryTheory.ConcreteCategory.hom (c.ι.app j)) x
-- Init.Data.Array.Attach
/-- Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
`Array {x // P x}` is the same as the input `Array α`.
 -/
_private.Init.Data.Array.Attach.0.Array.attachWithImpl : {α : Type u_1} → (xs : Array α) → (P : α → Prop) → (∀ x ∈ xs, P x) → Array { x // P x }
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabOmission : Lean.Elab.Term.TermElab
-- Mathlib.RingTheory.Valuation.RankOne
Valuation.RankOne.mk : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : Ring R] →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] →
        {v : Valuation R Γ₀} → [toRankLeOne : v.RankLeOne] → [toIsNontrivial : v.IsNontrivial] → v.RankOne
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.CoconeMorphism.inv_hom_id : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cocone F} (f : c ≅ d),
  CategoryTheory.CategoryStruct.comp f.inv.hom f.hom.hom = CategoryTheory.CategoryStruct.id d.pt
-- Mathlib.Algebra.Module.Pi
/-- A special case of `Pi.module` for non-dependent types. Lean struggles to elaborate
definitions elsewhere in the library without this.  -/
Pi.Function.module : (I : Type u) →
  (α : Type u_1) → (β : Type u_2) → [inst : Semiring α] → [inst_1 : AddCommMonoid β] → [Module α β] → Module α (I → β)
-- Mathlib.Topology.Sets.CompactOpenCovered
IsCompactOpenCovered.empty : ∀ {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [inst : (i : ι) → TopologicalSpace (X i)],
  IsCompactOpenCovered f ∅
-- Mathlib.Data.Real.Basic
Real.cauchy_intCast : ∀ (z : ℤ), (↑z).cauchy = ↑z
-- Mathlib.RingTheory.Ideal.Height
/-- In a nontrivial commutative ring `R`, the supremum of heights of all ideals is equal to the
Krull dimension of `R`.  -/
Ideal.sup_height_eq_ringKrullDim : ∀ {R : Type u_1} [inst : CommRing R] [Nontrivial R], ↑(⨆ I, ⨆ (_ : I ≠ ⊤), I.height) = ringKrullDim R
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.foldlM_eq_foldlM_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ},
  Std.DTreeMap.foldlM (fun d a x => f d a) init t = List.foldlM f init t.keys
-- Mathlib.Algebra.GroupWithZero.Units.Lemmas
/-- A monoid homomorphism between groups with zeros sending `0` to `0` sends `a⁻¹` to `(f a)⁻¹`.  -/
map_inv₀ : ∀ {G₀ : Type u_3} {G₀' : Type u_5} {F : Type u_6} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero G₀']
  [inst_2 : FunLike F G₀ G₀'] [MonoidWithZeroHomClass F G₀ G₀'] (f : F) (a : G₀), f a⁻¹ = (f a)⁻¹
-- Mathlib.Algebra.Group.Commute.Defs
Commute.self_pow : ∀ {M : Type u_2} [inst : Monoid M] (a : M) (n : ℕ), Commute a (a ^ n)
-- Mathlib.Analysis.InnerProductSpace.Laplacian
bilinearIteratedFDerivTwo.eq_1 : ∀ (𝕜 : 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] (f : E → F)
  (x : E), bilinearIteratedFDerivTwo 𝕜 f x = ContinuousLinearMap.toLinearMap₁₂ (fderiv 𝕜 (fderiv 𝕜 f) x)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get!_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], (t₁ ∪ t₂).get! k = t₂.getD k (t₁.get! k)
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Ring
/-- **Pentagonal number theorem**, assuming appropriate multipliability and summability.

$$ \prod_{n = 0}^{\infty} (1 - x^{n + 1}) =
\sum_{k=0}^{\infty} (-1)^k \left(x^{k(3k+1)/2} - x^{(k+1)(3k+2)/2}\right) $$  -/
Pentagonal.tprod_one_sub_pow : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] [T2Space R] {x : R},
  IsTopologicallyNilpotent x →
    (∀ (k : ℕ), Summable fun n => x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1))) →
      (∀ (k : ℕ), Multipliable fun n => 1 - x ^ (n + k + 1)) →
        (Summable fun k => (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))) →
          Filter.Tendsto
              (fun k =>
                (-1) ^ (k + 1) * x ^ ((k + 1) * (3 * k + 4) / 2) *
                  ∑' (n : ℕ), x ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - x ^ (k + i + 1)))
              Filter.atTop (nhds 0) →
            ∏' (n : ℕ), (1 - x ^ (n + 1)) = ∑' (k : ℕ), (-1) ^ k * (x ^ pentagonal (-↑k) - x ^ pentagonal (↑k + 1))
-- Mathlib.RingTheory.ZariskisMainTheorem
IsLocalization.Away.mapₐ.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_5} [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {B : Type u_6}
  [inst_3 : CommSemiring B] [inst_4 : Algebra R B] (Aₚ : Type u_7) [inst_5 : CommSemiring Aₚ] [inst_6 : Algebra A Aₚ]
  [inst_7 : Algebra R Aₚ] [inst_8 : IsScalarTower R A Aₚ] (Bₚ : Type u_8) [inst_9 : CommSemiring Bₚ]
  [inst_10 : Algebra B Bₚ] [inst_11 : Algebra R Bₚ] [inst_12 : IsScalarTower R B Bₚ] (f f_1 : A →ₐ[R] B) (e_f : f = f_1)
  (a a_1 : A) (e_a : a = a_1) [inst_13 : IsLocalization.Away a Aₚ] [inst_14 : IsLocalization.Away (f a) Bₚ],
  IsLocalization.Away.mapₐ Aₚ Bₚ f a = IsLocalization.Away.mapₐ Aₚ Bₚ f_1 a_1
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.rootSpan_eq_top_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Field R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [P.IsAnisotropic], P.rootSpan R = ⊤ ↔ P.corootSpan R = ⊤
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.Collector.saveFunInd : Lean.Expr → Lean.Meta.FunIndInfo → Array Lean.Expr → Lean.Meta.FunInd.Collector.M Unit
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.mem_finiteRange_iff_hasFiniteRange : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : CommRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [IsNoetherianRing K] {f : V →ₗ[K] V₂},
  f ∈ LinearMap.finiteRange K V V₂ ↔ f.HasFiniteRange
-- Lean.InternalExceptionId
/-- Convert internal exception id into the message "internal exception #<idx>" -/
Lean.InternalExceptionId.toString : Lean.InternalExceptionId → String
-- Mathlib.Algebra.CharP.Subring
CharP.subsemiring : ∀ (R : Type u) [inst : Semiring R] (p : ℕ) [CharP R p] (S : Subsemiring R), CharP (↥S) p
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.isMonicOfDegree_sub_add_two : ∀ {R : Type u_1} [inst : Ring R] [Nontrivial R] (a b : R),
  (Polynomial.X ^ 2 - Polynomial.C a * Polynomial.X + Polynomial.C b).IsMonicOfDegree 2
-- Mathlib.Order.Booleanisation
/-- The top element of `Booleanisation α` is the complement of the bottom element of `α`.  -/
Booleanisation.instTop : {α : Type u_1} → [GeneralizedBooleanAlgebra α] → Top (Booleanisation α)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_abs_right : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {f : α → E} {l : Filter α} {u : α → ℝ},
  (f =o[l] fun x => |u x|) ↔ f =o[l] u
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  [inst : Inhabited β] {f : Option β → Option β}, (m.alter k f)[k]! = (f m[k]?).get!
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- Given a `PushoutObjObj` of `f₁ : Arrow C₁` and `f₂ : Arrow C₂`, a `PushoutObjObj` of `f₁'` and
`f₂ : Arrow C₂`, and an isomorphism `f₁ ≅ f₁'`, this defines an isomorphism of the induced
pushout maps.  -/
CategoryTheory.Functor.PushoutObjObj.ι_iso_of_iso_left : {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₃)} →
              {f₁ f₁' : CategoryTheory.Arrow C₁} →
                {f₂ : CategoryTheory.Arrow C₂} →
                  (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) →
                    (sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom) →
                      (f₁ ≅ f₁') → (CategoryTheory.Arrow.mk sq₁₂.ι ≅ CategoryTheory.Arrow.mk sq₁₂'.ι)
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netEntropyEntourage_le_coverEntropyEntourage : ∀ {X : Type u_1} {U : SetRel X X} (T : X → X) (F : Set X),
  Dynamics.netEntropyEntourage T F U ≤ Dynamics.coverEntropyEntourage T F U
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multiequalizer.lift_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasMultiequalizer I] (W : C)
  (k : (a : J.L) → W ⟶ I.left a)
  (h :
    ∀ (b : J.R),
      CategoryTheory.CategoryStruct.comp (k (J.fst b)) (I.fst b) =
        CategoryTheory.CategoryStruct.comp (k (J.snd b)) (I.snd b))
  (a : J.L) {Z : C} (h_1 : I.left a ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.lift I W k h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multiequalizer.ι I a) h_1) =
    CategoryTheory.CategoryStruct.comp (k a) h_1
-- Lean.Meta.Sym.Simp.SimpM
/-- Read-only context for the simplifier.  -/
Lean.Meta.Sym.Simp.Context : Type
-- Init.Data.BitVec.Basic
/-- Returns the `i`th least significant bit.
 -/
BitVec.getLsb : {w : ℕ} → BitVec w → Fin w → Bool
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- A function `f` that is injective on adjacent vertices in a graph `G`
(equivalently `f` is a valid `W`-coloring of `G`, or `G ≤ comap ⊤ f`)
is a homomorphism from `G` to the mapped graph.  -/
SimpleGraph.Hom.map : {V : Type u_1} →
  {W : Type u_2} → (f : V → W) → (G : SimpleGraph V) → (∀ {u v : V}, G.Adj u v → f u ≠ f v) → G →g SimpleGraph.map f G
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.add_univ : ∀ {α : Type u_2} [inst : AddGroup α] {s : Set α}, s.Nonempty → s + Set.univ = Set.univ
-- Lean.DocString.Types
/-- A description list that associates explanatory text with shorter items.
 -/
Lean.Doc.Block.dl : {i : Type u} → {b : Type v} → Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Lean.Doc.Block i b
-- Mathlib.Data.Set.MulAntidiagonal
Set.mem_mulAntidiagonal : ∀ {α : Type u_1} [inst : Mul α] {s t : Set α} {a : α} {x : α × α},
  x ∈ s.mulAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 * x.2 = a
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- The `SpecialLinearGroup` analogue of
`Matrix.Pivot.exists_list_transvec_mul_diagonal_mul_list_transvec`:
every element of `SL(ι, F)` is a product of transvections,
a diagonal matrix of determinant `1`, and transvections.  -/
Matrix.SpecialLinearGroup.exists_list_transvec_mul_diagonal_mul_list_transvec : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  (M : Matrix.SpecialLinearGroup ι F),
  ∃ L L' D,
    ∃ (hD : (Matrix.diagonal D).det = 1),
      M =
        (List.map Matrix.TransvectionStruct.toSpecialLinearGroup L).prod * ⟨Matrix.diagonal D, hD⟩ *
          (List.map Matrix.TransvectionStruct.toSpecialLinearGroup L').prod
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeNegAssignment.eq_4 : Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned.removeNegAssignment =
  Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ne_empty_of_erase_ne_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  t.erase k ≠ ∅ → t ≠ ∅
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso_hom_app_snd_fst : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {A' : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] {B : Type u} [inst_2 : CategoryTheory.Category.{v, u} B]
  (T : Type u_3) [inst_3 : CategoryTheory.Category.{v_3, u_3} T] (X : CategoryTheory.Functor ((A ⊕ A') ⊕ T) B),
  ((CategoryTheory.Sum.associativityFunctorEquivNaturalityFunctorIso T).hom.app X).2.1 =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Sum.inl_ A' T).whiskerLeft
        ((CategoryTheory.Sum.inr_ A (A' ⊕ T)).associator (CategoryTheory.sum.inverseAssociator A A' T) X).inv)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Sum.inl_ A' T).associator
            ((CategoryTheory.Sum.inr_ A (A' ⊕ T)).comp (CategoryTheory.sum.inverseAssociator A A' T)) X).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight (CategoryTheory.sum.inlCompInrCompInverseAssociator A A' T).hom X)
          ((CategoryTheory.Sum.inr_ A A').associator (CategoryTheory.Sum.inl_ (A ⊕ A') T) X).hom))
-- Mathlib.Logic.Equiv.Sum
/-- Sum with `IsEmpty` is equivalent to the original type.  -/
Equiv.sumEmpty : (α : Type u_9) → (β : Type u_10) → [IsEmpty β] → α ⊕ β ≃ α
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.IsReduced.mk : ∀ {X : AlgebraicGeometry.Scheme},
  autoParam (∀ (U : X.Opens), IsReduced ↑(X.presheaf.obj (Opposite.op U)))
      AlgebraicGeometry.IsReduced.component_reduced._autoParam →
    AlgebraicGeometry.IsReduced X
-- Mathlib.Computability.TuringMachine.Tape
Turing.BlankRel.refl : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (l : List Γ), Turing.BlankRel l l
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCocones.mk.inj : ∀ {J : Type u_1} {K : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} J}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} K} {C : Type u_3} {inst_2 : CategoryTheory.Category.{v_3, u_3} C}
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} {obj : (j : J) → CategoryTheory.Limits.Cocone (F.obj j)}
  {map : {j j' : J} → (f : j ⟶ j') → obj j ⟶ (CategoryTheory.Limits.Cocone.precompose (F.map f)).obj (obj j')}
  {id :
    autoParam (∀ (j : J), (map (CategoryTheory.CategoryStruct.id j)).hom = CategoryTheory.CategoryStruct.id (obj j).pt)
      CategoryTheory.Limits.DiagramOfCocones.id._autoParam}
  {comp :
    autoParam
      (∀ {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃),
        (map (CategoryTheory.CategoryStruct.comp f g)).hom = CategoryTheory.CategoryStruct.comp (map f).hom (map g).hom)
      CategoryTheory.Limits.DiagramOfCocones.comp._autoParam}
  {obj_1 : (j : J) → CategoryTheory.Limits.Cocone (F.obj j)}
  {map_1 : {j j' : J} → (f : j ⟶ j') → obj_1 j ⟶ (CategoryTheory.Limits.Cocone.precompose (F.map f)).obj (obj_1 j')}
  {id_1 :
    autoParam
      (∀ (j : J), (map_1 (CategoryTheory.CategoryStruct.id j)).hom = CategoryTheory.CategoryStruct.id (obj_1 j).pt)
      CategoryTheory.Limits.DiagramOfCocones.id._autoParam}
  {comp_1 :
    autoParam
      (∀ {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃),
        (map_1 (CategoryTheory.CategoryStruct.comp f g)).hom =
          CategoryTheory.CategoryStruct.comp (map_1 f).hom (map_1 g).hom)
      CategoryTheory.Limits.DiagramOfCocones.comp._autoParam},
  { obj := obj, map := map, id := id, comp := comp } = { obj := obj_1, map := map_1, id := id_1, comp := comp_1 } →
    obj = obj_1 ∧ map ≍ map_1
-- Mathlib.Control.Functor
Functor.Comp.instPure : {F : Type u → Type w} → {G : Type v → Type u} → [Applicative F] → [Applicative G] → Pure (Functor.Comp F G)
-- Mathlib.GroupTheory.Sylow
/-- If `H` is a subgroup of `G` of cardinality `p ^ n`, then the cardinality of the
normalizer of `H` is congruent mod `p ^ (n + 1)` to the cardinality of `G`.  -/
Sylow.card_normalizer_modEq_card : ∀ {G : Type u} [inst : Group G] [Finite G] {p n : ℕ} [hp : Fact (Nat.Prime p)] {H : Subgroup G},
  Nat.card ↥H = p ^ n → Nat.card ↥(Subgroup.normalizer ↑H) ≡ Nat.card G [MOD p ^ (n + 1)]
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstr.mk.inj : ∀ {lhs rhs : Lean.Grind.AC.Seq} {h : Lean.Meta.Grind.AC.EqCnstrProof} {id : ℕ} {lhs_1 rhs_1 : Lean.Grind.AC.Seq}
  {h_1 : Lean.Meta.Grind.AC.EqCnstrProof} {id_1 : ℕ},
  { lhs := lhs, rhs := rhs, h := h, id := id } = { lhs := lhs_1, rhs := rhs_1, h := h_1, id := id_1 } →
    lhs = lhs_1 ∧ rhs = rhs_1 ∧ h = h_1 ∧ id = id_1
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderTriple.inv_le_inv : ∀ (p q r : ENNReal) [p.HolderTriple q r], p⁻¹ ≤ r⁻¹
-- Mathlib.Geometry.Convex.Cone.Basic
/-- Top is less than or equal to the linear span of a generating convex cone.  -/
ConvexCone.IsGenerating.top_le_span : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {C : ConvexCone R M}, C.IsGenerating → ⊤ ≤ Submodule.span R ↑C
-- Mathlib.Data.Nat.SuccPred
/-- **Alias** of the forward direction of `Fin.covBy_iff`. -/
CovBy.coe_fin : ∀ {n : ℕ} {a b : Fin n}, a ⋖ b → ↑a ⋖ ↑b
-- Init.Data.List.MinMax
List.isSome_max?_of_mem : ∀ {α : Type u_1} {l : List α} [inst : Max α] {a : α}, a ∈ l → l.max?.isSome = true
-- Lean.Meta.Match.AltTelescopes
_private.Lean.Meta.Match.AltTelescopes.0.Lean.Meta.Match.forallAltVarsTelescope.isNamedPatternProof : Lean.Expr → Lean.Expr → Bool
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.map_obj_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ G)
  (X : CategoryTheory.Grothendieck F),
  ((CategoryTheory.Grothendieck.map α).obj X).fiber = (α.app X.base).toFunctor.obj X.fiber
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
_private.Mathlib.Topology.UniformSpace.UniformConvergenceTopology.0.UniformOnFun.«term𝒰(_,_,_)» : Lean.ParserDescr
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.denote.match_1.eq_2 : ∀ (motive : Int.Internal.Linear.Poly → Sort u_1) (k : ℤ) (v : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly)
  (h_1 : (k : ℤ) → motive (Int.Internal.Linear.Poly.num k))
  (h_2 :
    (k : ℤ) →
      (v : Int.Internal.Linear.Var) → (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.add k v p)),
  (match Int.Internal.Linear.Poly.add k v p with
    | Int.Internal.Linear.Poly.num k => h_1 k
    | Int.Internal.Linear.Poly.add k v p => h_2 k v p) =
    h_2 k v p
-- Mathlib.GroupTheory.Congruence.Defs
/-- The quotient of an `AddCommMagma` by an additive congruence relation is
an `AddCommMagma`.  -/
AddCon.addCommMagma : {M : Type u_4} → [inst : AddCommMagma M] → (c : AddCon M) → AddCommMagma c.Quotient
-- Init.System.ST
instSTWorldEST : {ε σ : Type} → STWorld σ (EST ε σ)
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.iCycles_δ : ∀ {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 k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.iCycles_δ._auto_1),
  CategoryTheory.CategoryStruct.comp (X.iCycles f g n₀) (X.δ f g n₀ n₁ hn₁) = 0
-- Aesop.Tree.AddRapp
Aesop.getGoalsToCopy : Aesop.UnorderedArraySet Lean.MVarId → Aesop.GoalRef → Aesop.TreeM (Array Aesop.GoalRef)
-- Mathlib.LinearAlgebra.TensorProduct.Basis
TensorProduct.sum_tmul_basis_left_eq_zero : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (ℬ : Module.Basis ι R M) (b : ι →₀ N),
  (b.sum fun i n => ℬ i ⊗ₜ[R] n) = 0 → b = 0
-- Mathlib.RingTheory.Algebraic.Basic
IsAlgebraic.algebraMap : ∀ {R : Type u} {S : Type u_1} {A : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R A] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [IsScalarTower R S A] {a : S},
  IsAlgebraic R a → IsAlgebraic R ((algebraMap S A) a)
-- Init.Data.SInt.Lemmas
ISize.ofIntLE_bitVecToInt : ∀ (n : BitVec System.Platform.numBits), ISize.ofIntLE n.toInt ⋯ ⋯ = ISize.ofBitVec n
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.forM_eq_forM_keysArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → m PUnit.{w + 1}}, (forM t fun a => f a.fst) = Array.forM f t.keysArray
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.epi_image_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f] [E : CategoryTheory.Epi f],
  CategoryTheory.Epi (CategoryTheory.Limits.image.ι f)
-- Mathlib.NumberTheory.FactorisationProperties
Nat.infinite_odd_deficient : {n | Odd n ∧ n.Deficient}.Infinite
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.ProjectivePresentation.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} [inst_1 : SizeOf C] (p : C)
  [projective : CategoryTheory.Projective p] (f : p ⟶ X) [epi : CategoryTheory.Epi f],
  sizeOf { p := p, projective := projective, f := f, epi := epi } =
    1 + sizeOf p + sizeOf projective + sizeOf f + sizeOf epi
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfp_zero : Ordinal.nfp 0 = id
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- A lower hemicontinuous function intersected with a function with an open graph is lower
hemicontinuous.  -/
LowerHemicontinuous.inter_hasOpenCGraph : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f g : α → Set β},
  LowerHemicontinuous f → HasOpenCGraph g → LowerHemicontinuous fun x => f x ∩ g x
-- Init.Data.String.Lemmas.IsEmpty
String.eq_empty_iff_forall_eq : ∀ {s : String}, s = "" ↔ ∀ (p q : s.Pos), p = q
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.fold.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode α) →
      (Unit → motive RBTree.RBNode.nil) →
        ((c : RBTree.RBColor) →
            (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)) →
          motive x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_eq_getEntry? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.getKey? a l = Option.map (fun x => x.fst) (Std.Internal.List.getEntry? a l)
-- Mathlib.RingTheory.Radical.NatInt
Int.radical_natCast : ∀ {n : ℕ}, UniqueFactorizationMonoid.radical ↑n = ↑(UniqueFactorizationMonoid.radical n)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- An epimorphism in `SimplexCategory` must decrease lengths  -/
SimplexCategory.len_le_of_epi : ∀ {x y : SimplexCategory} (f : x ⟶ y) [CategoryTheory.Epi f], y.len ≤ x.len
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.quasiSeparatedSpace_of_isAffine : ∀ (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X], QuasiSeparatedSpace ↥X
-- Mathlib.Data.Sym.Basic
/-- Fill a term `m : Sym α (n - i)` with `i` copies of `a` to obtain a term of `Sym α n`.
This is a convenience wrapper for `m.append (replicate i a)` that adjusts the term using
`Sym.cast`.  -/
Sym.fill : {α : Type u_1} → {n : ℕ} → α → (i : Fin (n + 1)) → Sym α (n - ↑i) → Sym α n
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.Rel.lie_self : ∀ {R : Type u} {X : Type v} [inst : CommRing R] (a : FreeNonUnitalNonAssocAlgebra R X), FreeLieAlgebra.Rel R X (a * a) 0
-- Mathlib.Order.Interval.Multiset
Multiset.right_mem_Ioc : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, b ∈ Multiset.Ioc a b ↔ a < b