mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.mk.injEq : ∀ {ι : Type u_5} {B : Type u_6} [inst : TopologicalSpace B] {F : Type u_7} [inst_1 : TopologicalSpace F]
  (baseSet : ι → Set B) (isOpen_baseSet : ∀ (i : ι), IsOpen (baseSet i)) (indexAt : B → ι)
  (mem_baseSet_at : ∀ (x : B), x ∈ baseSet (indexAt x)) (coordChange : ι → ι → B → F → F)
  (coordChange_self : ∀ (i : ι), ∀ x ∈ baseSet i, ∀ (v : F), coordChange i i x v = v)
  (continuousOn_coordChange :
    ∀ (i j : ι), ContinuousOn (fun p => coordChange i j p.1 p.2) ((baseSet i ∩ baseSet j) ×ˢ Set.univ))
  (coordChange_comp :
    ∀ (i j k : ι),
      ∀ x ∈ baseSet i ∩ baseSet j ∩ baseSet k, ∀ (v : F), coordChange j k x (coordChange i j x v) = coordChange i k x v)
  (baseSet_1 : ι → Set B) (isOpen_baseSet_1 : ∀ (i : ι), IsOpen (baseSet_1 i)) (indexAt_1 : B → ι)
  (mem_baseSet_at_1 : ∀ (x : B), x ∈ baseSet_1 (indexAt_1 x)) (coordChange_1 : ι → ι → B → F → F)
  (coordChange_self_1 : ∀ (i : ι), ∀ x ∈ baseSet_1 i, ∀ (v : F), coordChange_1 i i x v = v)
  (continuousOn_coordChange_1 :
    ∀ (i j : ι), ContinuousOn (fun p => coordChange_1 i j p.1 p.2) ((baseSet_1 i ∩ baseSet_1 j) ×ˢ Set.univ))
  (coordChange_comp_1 :
    ∀ (i j k : ι),
      ∀ x ∈ baseSet_1 i ∩ baseSet_1 j ∩ baseSet_1 k,
        ∀ (v : F), coordChange_1 j k x (coordChange_1 i j x v) = coordChange_1 i k x v),
  ({ baseSet := baseSet, isOpen_baseSet := isOpen_baseSet, indexAt := indexAt, mem_baseSet_at := mem_baseSet_at,
        coordChange := coordChange, coordChange_self := coordChange_self,
        continuousOn_coordChange := continuousOn_coordChange, coordChange_comp := coordChange_comp } =
      { baseSet := baseSet_1, isOpen_baseSet := isOpen_baseSet_1, indexAt := indexAt_1,
        mem_baseSet_at := mem_baseSet_at_1, coordChange := coordChange_1, coordChange_self := coordChange_self_1,
        continuousOn_coordChange := continuousOn_coordChange_1, coordChange_comp := coordChange_comp_1 }) =
    (baseSet = baseSet_1 ∧ indexAt = indexAt_1 ∧ coordChange = coordChange_1)
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
/-- Evaluation of a multivariate power series at `f` at a point `a : σ → S`.

It coincides with the evaluation of `f` as a polynomial if `f` is the coercion of a polynomial.
Otherwise, it is only relevant if `φ` is continuous and `HasEval a`.  -/
MvPowerSeries.eval₂ : {σ : Type u_1} →
  {R : Type u_2} →
    [inst : CommRing R] →
      [UniformSpace R] →
        {S : Type u_3} → [inst_2 : CommRing S] → [UniformSpace S] → (R →+* S) → (σ → S) → MvPowerSeries σ R → S
-- Mathlib.CategoryTheory.Galois.Topology
/-- `Aut F` is equipped with the by the embedding into `∀ X, Aut (F.obj X)` induced embedding.  -/
CategoryTheory.PreGaloisCategory.instTopologicalSpaceAutFunctorFintypeCat : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) → TopologicalSpace (CategoryTheory.Aut F)
-- Mathlib.Order.Preorder.Chain
IsChain.diff : ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, IsChain r s → IsChain r (s \ t)
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasFDerivWithinAt_comp_sub : ∀ {𝕜 : 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}
  {f' : E →L[𝕜] F} {x : E} {s : Set E} (a : E),
  HasFDerivWithinAt (fun x => f (x - a)) f' s x ↔ HasFDerivWithinAt f f' (-a +ᵥ s) (x - a)
-- Mathlib.RepresentationTheory.Rep.Res
/-- The instances above show that the restriction functor `res φ : Rep R G ⥤ Rep R H`
preserves and reflects exactness.  -/
Rep.res_map_exact : ∀ {G : Type v1} {H : Type v2} [inst : Monoid G] [inst_1 : Monoid H] (f : H →* G) {k : Type u} [inst_2 : CommRing k]
  (S : CategoryTheory.ShortComplex (Rep.{w, u, v1} k G)), (S.map (Rep.resFunctor f)).Exact ↔ S.Exact
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
CompactCoherentification.continuousOn_mk_comp_iff_of_Compact : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {A : Set X},
  IsCompact A → ∀ {f : X → Y}, ContinuousOn (⇑(CompactCoherentification.mk Y) ∘ f) A ↔ ContinuousOn f A
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getKey! (t.minKeyD fallback) = t.minKeyD fallback
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
AddOpposite.dist_op : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] (x y : α), dist (AddOpposite.op x) (AddOpposite.op y) = dist x y
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} [inst_3 : HasDerivedCategory C] {n : ℕ}
  {α β : CategoryTheory.Abelian.Ext X Y n}, α = β ↔ α.hom = β.hom
-- Init.Data.Option.Attach
_private.Init.Data.Option.Attach.0.Option.instDecidableEq.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (val : α) (h_1 : Unit → motive none)
  (h_2 : (val : α) → motive (some val)),
  (match some val with
    | none => h_1 ()
    | some val => h_2 val) =
    h_2 val
-- Init.Data.Nat.Lcm
Nat.gcd_mul_lcm : ∀ (m n : ℕ), m.gcd n * m.lcm n = m * n
-- Plausible.Gen
/-- Create an `Array` of examples using `x`. The size is controlled
by the size parameter of `Gen`.  -/
Plausible.Gen.arrayOf : {α : Type u} → Plausible.Gen α → Plausible.Gen (Array α)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_filter_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k k' : α},
  m.getKey? k = some k' → (Std.ExtHashMap.filter f m)[k]? = Option.filter (fun x => f k' x) m[k]?
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.c₆_of_isShortNF_of_char_three : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] [CharP R 3], W.c₆ = 0
-- Mathlib.Topology.Category.Compactum
/-- The adjunction between `free` and `forget`.  -/
Compactum.adj : Compactum.free ⊣ Compactum.forget
-- Init.Core
Except.error.inj : ∀ {ε : Type u} {α : Type v} {a a_1 : ε}, Except.error a = Except.error a_1 → a = a_1
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.support_expand : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (φ : MvPowerSeries σ R),
  Function.support ((MvPowerSeries.expand p hp) φ) = (fun x => p • x) '' Function.support φ
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.pullbackCoverOfRight_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C}
  [inst_1 : J.IsStableUnderBaseChange] {Y : C} (E : J.ZeroHypercover Y) {X Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.HasPullback f g]
  [inst_3 : ∀ (i : E.I₀), CategoryTheory.Limits.HasPullback (E.f i) (CategoryTheory.Limits.pullback.snd f g)],
  (E.pullbackCoverOfRight f g).toPreZeroHypercover = E.pullbackCoverOfRight f g
-- Mathlib.Algebra.Module.Torsion.Basic
/-- A module where every element is `a`-torsion for all `a` in `s`.  -/
Module.IsTorsionBySet : (R : Type u_1) → (M : Type u_2) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Set R → Prop
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonFoldingRange : Lean.ToJson Lean.Lsp.FoldingRange
-- Mathlib.Analysis.Complex.Periodic
Function.Periodic.cuspFunction_add : ∀ {h : ℝ} {f g : ℂ → ℂ},
  ContinuousAt (Function.Periodic.cuspFunction h f) 0 →
    ContinuousAt (Function.Periodic.cuspFunction h g) 0 →
      Function.Periodic.cuspFunction h (f + g) = Function.Periodic.cuspFunction h f + Function.Periodic.cuspFunction h g
-- Mathlib.Order.RelIso.Basic
RelIso.relIsoCongr_apply : ∀ {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop}
  {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₁ : r₁ ≃r s₁),
  (e₁.relIsoCongr e₂) f₁ = (e₁.symm.trans f₁).trans e₂
-- Init.Try
/-- If `name` is `true`, all functions in the same namespace are considered for function induction, unfolding, etc.  -/
Lean.Try.Config.name : Lean.Try.Config → Bool
-- Mathlib.Order.RelIso.Basic
RelEmbedding.mk.inj : ∀ {α : Type u_5} {β : Type u_6} {r : α → α → Prop} {s : β → β → Prop} {toEmbedding : α ↪ β}
  {map_rel_iff' : ∀ {a b : α}, s (toEmbedding a) (toEmbedding b) ↔ r a b} {toEmbedding_1 : α ↪ β}
  {map_rel_iff'_1 : ∀ {a b : α}, s (toEmbedding_1 a) (toEmbedding_1 b) ↔ r a b},
  { toEmbedding := toEmbedding, map_rel_iff' := map_rel_iff' } =
      { toEmbedding := toEmbedding_1, map_rel_iff' := map_rel_iff'_1 } →
    toEmbedding = toEmbedding_1
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Multipliable.of_nat_of_neg : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] {f : ℤ → G},
  (Multipliable fun n => f ↑n) → (Multipliable fun n => f (-↑n)) → Multipliable f
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
TopCat.stdSimplexHomeomorphI_vertex_zero : TopCat.stdSimplexHomeomorphI (stdSimplex.vertex 0) = 0
-- Mathlib.GroupTheory.Nilpotent
/-- Abelian groups have nilpotency class at most one.  -/
CommGroup.nilpotencyClass_le_one : ∀ {G : Type u_2} [inst : CommGroup G], Group.nilpotencyClass G ≤ 1
-- Init.Data.List.Nat.Range
List.getLast?_range' : ∀ {s n : ℕ}, (List.range' s n).getLast? = if n = 0 then none else some (s + n - 1)
-- Mathlib.Analysis.Rat.NatSqrt.Real
Nat.realSqrt_mem_Ico : ∀ (x : ℕ) {prec : ℕ}, 0 < prec → √↑x ∈ Set.Ico (↑(x.ratSqrt prec)) (↑(x.ratSqrt prec) + 1 / ↑prec)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.preimage_mul_right_singleton : ∀ {α : Type u_2} [inst : Group α] {a b : α}, {b}.preimage (fun x => x * a) ⋯ = {b * a⁻¹}
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_lt_sub_left : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] [AddRightStrictMono α] {a b : α},
  a < b → ∀ (c : α), c - b < c - a
-- Init.Data.Option.Monadic
_private.Init.Data.Option.Monadic.0.Option.instForIn'InferInstanceMembershipOfMonad.match_1.eq_2 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (r : β) (h_1 : (r : β) → motive (ForInStep.done r))
  (h_2 : (r : β) → motive (ForInStep.yield r)),
  (match ForInStep.yield r with
    | ForInStep.done r => h_1 r
    | ForInStep.yield r => h_2 r) =
    h_2 r
-- Init.Data.String.Defs
String.Pos.Raw.IsValidForSlice.isValid_offsetBy : ∀ {s : String.Slice} {p : String.Pos.Raw},
  String.Pos.Raw.IsValidForSlice s p → String.Pos.Raw.IsValid s.str (p.offsetBy s.startInclusive.offset)
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.iic_incl_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {X Y : C} {f : X ⟶ Y} [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  (c : CategoryTheory.TransfiniteCompositionOfShape J f) (j : J) (i : ↑(Set.Iic j)),
  (c.iic j).incl.app i = c.F.map (CategoryTheory.homOfLE ⋯)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqPoly.beq.eq_1 : ∀ (a b : ℤ),
  Lean.Grind.CommRing.instBEqPoly.beq (Lean.Grind.CommRing.Poly.num a) (Lean.Grind.CommRing.Poly.num b) = (a == b)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.isoSpec_hom_appTop : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  AlgebraicGeometry.Scheme.Hom.appTop hU.isoSpec.hom =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).hom
      U.topIso.inv
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.X_pow_card_pow_sub_X_ne_zero : ∀ (K' : Type u_3) [inst : Field K'] {p n : ℕ}, n ≠ 0 → 1 < p → Polynomial.X ^ p ^ n - Polynomial.X ≠ 0
-- Mathlib.FieldTheory.IsRealClosed.Basic
IsRealClosed.isSquare_neg_of_not_isSquare : ∀ {R : Type u} [inst : Field R] [IsRealClosed R] {x : R}, ¬IsSquare x → IsSquare (-x)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k a fallback : α} {v : β},
      (t.insertIfNew k v).getKeyD a fallback = if cmp k a = Ordering.eq ∧ k ∉ t then k else t.getKeyD a fallback
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- The equivalence between `Matrix m n A` and `CStarMatrix m n A`.  -/
CStarMatrix.ofMatrix : {m : Type u_7} → {n : Type u_8} → {A : Type u_9} → Matrix m n A ≃ CStarMatrix m n A
-- Mathlib.MeasureTheory.Function.UnifTight
/-- **Vitali's convergence theorem** (non-finite measure version).

A sequence of functions `f` converges to `g` in Lp
if and only if it is uniformly integrable, uniformly tight and converges to `g` in measure.  -/
MeasureTheory.tendstoInMeasure_iff_tendsto_Lp : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup β] {μ : MeasureTheory.Measure α}
  {p : ENNReal} {f : ℕ → α → β} {g : α → β},
  1 ≤ p →
    p ≠ ⊤ →
      (∀ (n : ℕ), MeasureTheory.MemLp (f n) p μ) →
        MeasureTheory.MemLp g p μ →
          (MeasureTheory.TendstoInMeasure μ f Filter.atTop g ∧
              MeasureTheory.UnifIntegrable f p μ ∧ MeasureTheory.UnifTight f p μ ↔
            Filter.Tendsto (fun n => MeasureTheory.eLpNorm (f n - g) p μ) Filter.atTop (nhds 0))
-- Mathlib.MeasureTheory.Group.Arithmetic
aemeasurable_const_vadd_iff : ∀ {β : Type u_5} {α : Type u_6} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace α] {f : α → β}
  {μ : MeasureTheory.Measure α} {G : Type u_7} [inst_2 : AddGroup G] [inst_3 : AddAction G β] [MeasurableConstVAdd G β]
  (c : G), AEMeasurable (fun x => c +ᵥ f x) μ ↔ AEMeasurable f μ
-- Mathlib.Logic.Function.Basic
Function.FactorsThrough.extend_apply : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {g : α → γ},
  Function.FactorsThrough g f → ∀ (e' : β → γ) (a : α), Function.extend f g e' (f a) = g a
-- Init.Data.Int.Order
Int.min_comm : ∀ (a b : ℤ), min a b = min b a
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.TensorSigns.ε'_succ : ∀ {I : Type u_7} {inst : AddMonoid I} {c : ComplexShape I} [self : c.TensorSigns] (p q : I),
  c.Rel p q → (ComplexShape.TensorSigns.ε' c) q = -(ComplexShape.TensorSigns.ε' c) p
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.ker.lift_apply_coe : ∀ {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] (f : NormedAddGroupHom V₁ V₂)
  (g : NormedAddGroupHom V₂ V₃) (h : g.comp f = 0) (v : V₁), ↑((NormedAddGroupHom.ker.lift f g h) v) = f v
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.toList_roc : ∀ {α : Type u} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α fun x => Unit),
  t.Ordered →
    ∀ (lowerBound upperBound : α),
      Std.Slice.toList (Std.Roc.Sliceable.mkSlice t lowerBound<...=upperBound) =
        List.filter (fun e => decide ((compare e lowerBound).isGT = true ∧ (compare e upperBound).isLE = true)) t.keys
-- Mathlib.Geometry.Euclidean.MongePoint
Affine.Simplex.mongePointWeightsWithCircumcenter.eq_2 : ∀ (n : ℕ),
  Affine.Simplex.mongePointWeightsWithCircumcenter n Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex =
    -2 / ↑(n + 1)
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_natCast_p_sub_one : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], ‖↑(p - 1)‖ = 1
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.vanishingIdeal.eq_1 : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] {𝒜 : ℕ → σ}
  [inst_3 : GradedRing 𝒜] (t : Set (ProjectiveSpectrum 𝒜)),
  ProjectiveSpectrum.vanishingIdeal t = ⨅ x ∈ t, x.asHomogeneousIdeal
-- Lean.Declaration
Lean.TheoremVal : Type
-- Mathlib.RingTheory.LinearDisjoint
/-- If `{ a_i }` is an `R`-basis of `A`, if `{ b_j }` is an `R`-basis of `B`,
such that the family `{ a_i * b_j }` in `S` is `R`-linearly independent,
then `A` and `B` are linearly disjoint.  -/
Subalgebra.LinearDisjoint.of_basis_mul : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (A B : Subalgebra R S)
  {κ : Type u_1} {ι : Type u_2} (a : Module.Basis κ R ↥A) (b : Module.Basis ι R ↥B),
  (LinearIndependent R fun i => ↑(a i.1) * ↑(b i.2)) → A.LinearDisjoint B
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.combine'.eq_def : ∀ (fuel : ℕ) (p₁ p₂ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.combine' fuel p₁ p₂ =
    match fuel with
    | 0 => p₁.append p₂
    | fuel.succ =>
      match p₁, p₂ with
      | Int.Internal.Linear.Poly.num k₁, Int.Internal.Linear.Poly.num k₂ => Int.Internal.Linear.Poly.num (k₁ + k₂)
      | Int.Internal.Linear.Poly.num k₁, Int.Internal.Linear.Poly.add a x p =>
        Int.Internal.Linear.Poly.add a x (Int.Internal.Linear.Poly.combine' fuel (Int.Internal.Linear.Poly.num k₁) p)
      | Int.Internal.Linear.Poly.add a x p, Int.Internal.Linear.Poly.num k₂ =>
        Int.Internal.Linear.Poly.add a x (Int.Internal.Linear.Poly.combine' fuel p (Int.Internal.Linear.Poly.num k₂))
      | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ =>
        bif Nat.beq x₁ x₂ then
          have a := a₁ + a₂;
          bif a == 0 then Int.Internal.Linear.Poly.combine' fuel p₁ p₂
          else Int.Internal.Linear.Poly.add a x₁ (Int.Internal.Linear.Poly.combine' fuel p₁ p₂)
        else
          bif Nat.blt x₂ x₁ then
            Int.Internal.Linear.Poly.add a₁ x₁
              (Int.Internal.Linear.Poly.combine' fuel p₁ (Int.Internal.Linear.Poly.add a₂ x₂ p₂))
          else
            Int.Internal.Linear.Poly.add a₂ x₂
              (Int.Internal.Linear.Poly.combine' fuel (Int.Internal.Linear.Poly.add a₁ x₁ p₁) p₂)
-- Mathlib.Algebra.Homology.HomologicalComplex
CochainComplex.mk_X_2 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂) (s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0)
  (succ :
    (S : CategoryTheory.ShortComplex V) →
      (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' CategoryTheory.CategoryStruct.comp S.g d₂ = 0),
  (CochainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).X 2 = X₂
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.ofHom_s : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C) {X Y : C}
  (f : X ⟶ Y) [inst_1 : W.ContainsIdentities],
  (CategoryTheory.MorphismProperty.LeftFraction.ofHom W f).s = CategoryTheory.CategoryStruct.id Y
-- Mathlib.Analysis.SpecialFunctions.Pochhammer
/-- `descPochhammer ℝ n` is convex on `[n-1, ∞)`.  -/
convexOn_descPochhammer_eval : ∀ (n : ℕ), ConvexOn ℝ (Set.Ici (↑n - 1)) fun x => Polynomial.eval x (descPochhammer ℝ n)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.continuousOn_cos : ∀ {s : Set ℝ}, ContinuousOn Real.cos s
-- Mathlib.Order.WithBot
WithTop.instUniqueOfIsEmpty : {α : Type u_1} → [IsEmpty α] → Unique (WithTop α)
-- Mathlib.Order.KrullDimension
Order.height_le_of_krullDim_preimage_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : PartialOrder β] {m : ℕ} (f : α →o β),
  (∀ (x : β), Order.krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m) → ∀ (x : α), Order.height x ≤ (↑m + 1) * Order.height (f x) + ↑m
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.IterM.step_flatMapAfter : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [inst_3 : Std.Iterator α₂ m γ] {f : β → Std.IterM m γ} {it₁ : Std.IterM m β} {it₂ : Option (Std.IterM m γ)},
  (Std.IterM.flatMapAfter f it₁ it₂).step =
    match it₂ with
    | none => do
      let __do_lift ← it₁.step
      match __do_lift.inflate with
        | ⟨Std.IterStep.yield it₁' b, h⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.flatMapAfter f it₁' (some (f b))) ⋯))
        | ⟨Std.IterStep.skip it₁', h⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.flatMapAfter f it₁' none) ⋯))
        | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
    | some it₂ => do
      let __do_lift ← it₂.step
      match __do_lift.inflate with
        | ⟨Std.IterStep.yield it₂' out, h⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (Std.IterM.flatMapAfter f it₁ (some it₂')) out ⋯))
        | ⟨Std.IterStep.skip it₂', h⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.flatMapAfter f it₁ (some it₂')) ⋯))
        | ⟨Std.IterStep.done, h⟩ =>
          pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.IterM.flatMapAfter f it₁ none) ⋯))
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.ext_iff : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p q : Submodule R M},
  p = q ↔ ∀ (x : M), x ∈ p ↔ x ∈ q
-- Lean.Message
Lean.MessageData.ofGoal.inj : ∀ {a a_1 : Lean.MVarId}, Lean.MessageData.ofGoal a = Lean.MessageData.ofGoal a_1 → a = a_1
-- Mathlib.Analysis.Normed.Ring.Basic
/-- If `α` is a seminormed ring with `‖1‖ = 1`, then `‖a ^ n‖ ≤ ‖a‖ ^ n`.
See also `norm_pow_le'`.  -/
norm_pow_le : ∀ {α : Type u_2} [inst : SeminormedRing α] [NormOneClass α] (a : α) (n : ℕ), ‖a ^ n‖ ≤ ‖a‖ ^ n
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_erase : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {k a fallback : α}, (m.erase k).getKeyD a fallback = if (k == a) = true then fallback else m.getKeyD a fallback
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoState.mk.sizeOf_spec : ∀ (enabled : Bool) (assignment : Lean.PersistentHashMap Lean.MVarId Lean.Elab.InfoTree)
  (lazyAssignment : Lean.PersistentHashMap Lean.MVarId (Task Lean.Elab.InfoTree))
  (trees : Lean.PersistentArray Lean.Elab.InfoTree),
  sizeOf { enabled := enabled, assignment := assignment, lazyAssignment := lazyAssignment, trees := trees } =
    1 + sizeOf enabled + sizeOf assignment + sizeOf lazyAssignment + sizeOf trees
-- Init.Data.Bool
Bool.and_or_inj_left_iff : ∀ {m x y : Bool}, (m && x) = (m && y) ∧ (m || x) = (m || y) ↔ x = y
-- Mathlib.Order.Bounds.Basic
SemilatticeSup.ofIsLUB.eq_1 : ∀ {α : Type u_1} [inst : PartialOrder α] (sup : α → α → α) (isLUB_pair : ∀ (a b : α), IsLUB {a, b} (sup a b)),
  SemilatticeSup.ofIsLUB sup isLUB_pair =
    { toPartialOrder := inst, sup := sup, le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯ }
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.Subcomplex.instEpiToOfSimplex : ∀ {X : SSet} {n : ℕ} (x : X.obj (Opposite.op { len := n })), CategoryTheory.Epi (SSet.Subcomplex.toOfSimplex x)
-- Init.PropLemmas
Decidable.iff_not_comm : ∀ {a b : Prop} [Decidable a] [Decidable b], (a ↔ ¬b) ↔ (b ↔ ¬a)
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun.congr_simp : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type v} [inst_2 : Field K] [inst_3 : Algebra R K]
  [inst_4 : IsFractionRing R K] (v v_1 : IsDedekindDomain.HeightOneSpectrum R),
  v = v_1 → ∀ (x x_1 : Kˣ), x = x_1 → v.valuationOfNeZeroToFun x = v_1.valuationOfNeZeroToFun x_1
-- Mathlib.CategoryTheory.Limits.Types.Coequalizers
CategoryTheory.Limits.Types.coequalizerIso_π_comp_hom : ∀ {X Y : Type u} (f g : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g)
      (CategoryTheory.Limits.Types.coequalizerIso f g).hom =
    TypeCat.ofHom
      (Function.Coequalizer.mk ⇑(CategoryTheory.ConcreteCategory.hom f) ⇑(CategoryTheory.ConcreteCategory.hom g))