mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- Given `F : Jᵒᵖ ⥤ J ⥤ C`, this property asserts the existence of the end of `F`.  -/
CategoryTheory.Limits.HasEnd : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] → CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C) → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- A limit cone for `X : Discrete α ⥤ C` that is given
by `∏ᶜ (fun j => X.obj (Discrete.mk j))`.  -/
CategoryTheory.Limits.Pi.cone : {α : Type w₂} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) →
        [CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] → CategoryTheory.Limits.Cone X
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
/-- The inclusion of the bounded derived category.  -/
DerivedCategory.Bounded.ι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → CategoryTheory.Functor (DerivedCategory.Bounded C) (DerivedCategory C)
-- Batteries.Data.Char.AsciiCasing
Char.isUpper_toLower_eq_false : ∀ (c : Char), c.toLower.isUpper = false
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.ofArrows.fac_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {I : Type u_1} {X : C} {Y : I → C} {f : (i : I) → Y i ⟶ X}
  {W : C} {g : W ⟶ X} (hg : (CategoryTheory.Sieve.ofArrows Y f).arrows g) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Sieve.ofArrows.h hg)
      (CategoryTheory.CategoryStruct.comp (f (CategoryTheory.Sieve.ofArrows.i hg)) h) =
    CategoryTheory.CategoryStruct.comp g h
-- Mathlib.Data.Finset.Defs
Finset.coe_subset : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, ↑s₁ ⊆ ↑s₂ ↔ s₁ ⊆ s₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.CommSq.cone_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z} (s : CategoryTheory.CommSq f g h i), s.cone.fst = f
-- Mathlib.Analysis.Complex.Convex
/-- If opposite corners of a rectangle are contained in a convex set, the whole rectangle is.  -/
Complex.Convex.rectangle_subset : ∀ {U : Set ℂ},
  Convex ℝ U →
    ∀ {z w : ℂ}, z ∈ U → w ∈ U → ↑z.re + ↑w.im * Complex.I ∈ U → ↑w.re + ↑z.im * Complex.I ∈ U → z.Rectangle w ⊆ U
-- Mathlib.Data.List.Basic
List.IsSuffix.idxOf_le : ∀ {α : Type u} {l₁ l₂ : List α} [inst : BEq α] [LawfulBEq α],
  l₁ <:+ l₂ → ∀ (a : α), List.idxOf a l₂ ≤ l₂.length - l₁.length + List.idxOf a l₁
-- Init.Meta.Defs
Lean.Name.replacePrefix : Lean.Name → Lean.Name → Lean.Name → Lean.Name
-- Batteries.Data.AssocList
/-- `O(n)`. Returns true if every entry in the list satisfies `p`.  -/
Batteries.AssocList.all : {α : Type u_1} → {β : Type u_2} → (α → β → Bool) → Batteries.AssocList α β → Bool
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
CategoryTheory.Idempotents.app_idem_assoc : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Functor J C))
  (X : J) {Z : C} (h : P.X.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.p.app X) (CategoryTheory.CategoryStruct.comp (P.p.app X) h) =
    CategoryTheory.CategoryStruct.comp (P.p.app X) h
-- Init.Data.Vector.Lemmas
/-- Variant of `replicate_succ` that prepends `a` at the beginning of the vector.  -/
Vector.replicate_succ' : ∀ {n : ℕ} {α : Type u_1} {a : α}, Vector.replicate (n + 1) a = Vector.cast ⋯ (#v[a] ++ Vector.replicate n a)
-- Std.Data.DTreeMap.Internal.Lemmas
/-- A variant of `contains_of_contains_insertMany_list` used in `get_insertMany_list`.  -/
Std.DTreeMap.Internal.Impl.Const.contains_of_contains_insertMany_list' : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α] (h : t.WF) {l : List (α × β)} {k : α},
  Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.Const.insertMany t l ⋯) = true →
    List.findSomeRev?
          (fun x =>
            match x with
            | (a, b) => if compare a k = Ordering.eq then some b else none)
          l =
        none →
      Std.DTreeMap.Internal.Impl.contains k t = true
-- Mathlib.Algebra.Module.Equiv.Basic
Units.toLinearMap_mulLeftLinearEquiv : ∀ {R : Type u_9} {A : Type u_10} [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] (u : Aˣ), ↑((Units.mulLeftLinearEquiv R A) u) = LinearMap.mulLeft R ↑u
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
Matrix.charpoly.univ_coeff_eval₂Hom : ∀ {R : Type u_1} {S : Type u_2} (n : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] (f : R →+* S) (M : n × n → S) (i : ℕ),
  (MvPolynomial.eval₂Hom f M) ((Matrix.charpoly.univ R n).coeff i) = (Matrix.of (Function.curry M)).charpoly.coeff i
-- Mathlib.NumberTheory.FunctionField
/-- **Alias** of `RatFunc.inftyValuation_apply`. -/
FunctionField.inftyValuation_apply : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)] {x : RatFunc F},
  (RatFunc.inftyValuation F) x = RatFunc.inftyValuationDef F x
-- Mathlib.FieldTheory.Minpoly.MinpolyDiv
natDegree_minpolyDiv_lt : ∀ {R : Type u_2} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
  IsIntegral R x → ∀ [Nontrivial S], (minpolyDiv R x).natDegree < (minpoly R x).natDegree
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.limZero_congr : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f g : CauSeq β abv}, f ≈ g → (f.LimZero ↔ g.LimZero)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_union_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} [inst_1 : Inhabited (β k)],
  Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.union m₂ ⋯ ⋯).get! k = m₁.get! k
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.closure_iUnion : ∀ {M : Type u_1} [inst : MulOneClass M] {ι : Sort u_4} (s : ι → Set M),
  Submonoid.closure (⋃ i, s i) = ⨆ i, Submonoid.closure (s i)
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.isGLB_sInf : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (T : Set (CategoryTheory.Pretopology C)), IsGLB T (sInf T)
-- Mathlib.RingTheory.Ideal.Pure
/-- [Stacks Tag 04PS](https://stacks.math.columbia.edu/tag/04PS) ((5) => (7)) -/
Ideal.le_ker_atPrime_of_forall_exists_eq_mul : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R},
  (∀ x ∈ I, ∃ y ∈ I, x = x * y) →
    ∀ {p : Ideal R} [inst_1 : p.IsPrime], I ≤ p → I ≤ RingHom.ker (algebraMap R (Localization.AtPrime p))
-- Mathlib.Analysis.Convex.Visible
/-- All points of the convex hull of a set `s` visible from a point `x ∉ convexHull ℝ s` lie in the
convex hull of such points that actually lie in `s`.

Note that the converse does not hold.  -/
IsVisible.mem_convexHull_isVisible : ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] {s : Set V} {x y : V},
  x ∉ (convexHull ℝ) s →
    y ∈ (convexHull ℝ) s →
      IsVisible ℝ ((convexHull ℝ) s) x y → y ∈ (convexHull ℝ) {z | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x z}
-- Init.Prelude
/-- Applies a function to the current state that both computes a new state and a value. The new state
replaces the current state, and the value is returned.

It is equivalent to `do let (a, s) := f (← get); set s; pure a`. However, using `modifyGet` may
lead to higher performance because it doesn't add a new reference to the state value. Additional
references can inhibit in-place updates of data.
 -/
MonadStateOf.modifyGet : {σ : semiOutParam (Type u)} → {m : Type u → Type v} → [self : MonadStateOf σ m] → {α : Type u} → (σ → α × σ) → m α
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedAddMonoid.ext_iff : ∀ {α : Type u_2} {M : Type u_3} [inst : AddMonoid M] {rels : FreeAddMonoid α → FreeAddMonoid α → Prop}
  {φ ψ : PresentedAddMonoid rels →+ M},
  φ = ψ ↔ ∀ (x : α), φ (PresentedAddMonoid.of rels x) = ψ (PresentedAddMonoid.of rels x)
-- Mathlib.Data.Seq.Computation
Computation.liftRel_of_mem : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} {a : α} {b : β} {ca : Computation α} {cb : Computation β},
  a ∈ ca → b ∈ cb → R a b → Computation.LiftRel R ca cb
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.push : Option Lean.Grind.AC.Seq → Lean.Grind.AC.Var → Option Lean.Grind.AC.Seq
-- Mathlib.RingTheory.Derivation.Basic
Derivation.mk_coe : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] (f : A →ₗ[R] M)
  (h₁ : f 1 = 0) (h₂ : ∀ (a b : A), f (a * b) = a • f b + b • f a),
  ⇑{ toLinearMap := f, map_one_eq_zero' := h₁, leibniz' := h₂ } = ⇑f
-- Batteries.Data.List.Basic
List.IsChain.brecOn : ∀ {α : Type u_1} {R : α → α → Prop} {motive : (a : List α) → List.IsChain R a → Prop} {a : List α}
  (t : List.IsChain R a), (∀ (a : List α) (t : List.IsChain R a), List.IsChain.below t → motive a t) → motive a t
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)}
  {he : (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.isEmpty = false},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.maxKey he = k ↔
    (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (compare k' k).isLE = true
-- Mathlib.RingTheory.MatrixAlgebra
MatrixEquivTensor.invFun_add : ∀ (n : Type u_3) (R : Type u_5) (A : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n] (M N : Matrix n n A),
  MatrixEquivTensor.invFun n R A (M + N) = MatrixEquivTensor.invFun n R A M + MatrixEquivTensor.invFun n R A N
-- Mathlib.Algebra.Ring.Units
Units.neg_divp : ∀ {α : Type u} [inst : Monoid α] [inst_1 : HasDistribNeg α] (a : α) (u : αˣ), -(a /ₚ u) = -a /ₚ u
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Zero.new : {α : Type} → BaseIO (Std.CloseableChannel.Zero✝ α)
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
  (𝒱 : (i : 𝒰.I₀) → (CategoryTheory.Limits.pullback f (𝒰.f i)).OpenCover)
  [∀ (i : 𝒰.I₀), AlgebraicGeometry.IsAffine (𝒰.X i)]
  [∀ (i : 𝒰.I₀) (j : (𝒱 i).I₀), AlgebraicGeometry.IsAffine ((𝒱 i).X j)],
  AlgebraicGeometry.IsClosedImmersion
    (CategoryTheory.Limits.pullback.diagonal f ∣_ AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange f 𝒰 𝒱)
-- Mathlib.Topology.Algebra.Group.Basic
continuousAt_zpow : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] (x : G) (z : ℤ),
  ContinuousAt (fun x => x ^ z) x
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.image_eq_target_inter_inv_preimage : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : Set X}, s ⊆ e.source → ↑e '' s = e.target ∩ ↑e.symm ⁻¹' s
-- Mathlib.Order.Filter.Cofinite
Filter.Tendsto.exists_forall_ge : ∀ {α : Type u_2} {β : Type u_3} [Nonempty α] [inst : LinearOrder β] {f : α → β},
  Filter.Tendsto f Filter.cofinite Filter.atBot → ∃ a₀, ∀ (a : α), f a ≤ f a₀
-- Lean.Structure
_private.Lean.Structure.0.Lean.StructureState.map : Lean.StructureState✝ → Lean.PersistentHashMap Lean.Name Lean.StructureInfo
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.inner_rightAngleRotation_swap : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), inner ℝ x (o.rightAngleRotation y) = -inner ℝ (o.rightAngleRotation x) y
-- Mathlib.Data.Fin.Tuple.Basic
Fin.append_left_snoc : ∀ {n m : ℕ} {α : Sort u_2} (xs : Fin n → α) (x : α) (ys : Fin m → α),
  Fin.append (Fin.snoc xs x) ys = Fin.append xs (Fin.cons x ys) ∘ Fin.cast ⋯
-- Mathlib.Data.Finset.Grade
Finset.covBy_iff_exists_cons : ∀ {α : Type u_1} {s t : Finset α}, s ⋖ t ↔ ∃ a, ∃ (ha : a ∉ s), Finset.cons a s ha = t
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.Kernel.indep_limsup_self : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω}
  {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} {β : Type u_4}
  {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι},
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.Kernel.iIndep s κ μα →
      (∀ (t : Set ι), p t → tᶜ ∈ f) →
        Directed (fun x1 x2 => x1 ⊆ x2) ns →
          (∀ (a : β), p (ns a)) →
            (∀ (n : ι), ∃ a, n ∈ ns a) → ProbabilityTheory.Kernel.Indep (Filter.limsup s f) (Filter.limsup s f) κ μα
-- Mathlib.Data.Nat.Digits.Defs
/-- (Impl.) An auxiliary definition for `digits`, to help get the desired definitional unfolding.  -/
Nat.digitsAux0 : ℕ → List ℕ
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.isIso_of_bijective_of_isClosedMap : ∀ {X Y : TopCat} (f : X ⟶ Y),
  Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f) →
    IsClosedMap ⇑(CategoryTheory.ConcreteCategory.hom f) → CategoryTheory.IsIso f
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
/-- The two-variable Jacobi theta function is periodic in `z` with period 1.  -/
jacobiTheta₂_add_left : ∀ (z τ : ℂ), jacobiTheta₂ (z + 1) τ = jacobiTheta₂ z τ
-- Lean.Elab.Command
Lean.Elab.Command.addUnivLevel : Lean.Syntax → Lean.Elab.Command.CommandElabM Unit
-- Init.Grind.Ordered.Field
Lean.Grind.Field.IsOrdered.mul_inv_lt_iff_mul_lt_of_neg : ∀ {R : Type u} [inst : Lean.Grind.Field R] [inst_1 : LE R] [inst_2 : LT R] [Std.LawfulOrderLT R]
  [inst_4 : Std.IsLinearOrder R] [Lean.Grind.OrderedRing R] (a c : R) {b : R}, b < 0 → (a * b⁻¹ < c ↔ c * b < a)
-- Mathlib.Data.Fintype.Shrink
Shrink.instFintype : {α : Type u} → [inst : Fintype α] → Fintype (Shrink.{v, u} α)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.exists_sup_ge : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup β] [inst_1 : OrderBot β] [WellFoundedGT β] (f : α → β),
  ∃ t, ∀ (a : α), f a ≤ t.sup f
-- Mathlib.Tactic.NormNum.Ineq
Mathlib.Meta.NormNum.isNat_le_false : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [CharZero α] {a b : α} {a' b' : ℕ},
  Mathlib.Meta.NormNum.IsNat a a' → Mathlib.Meta.NormNum.IsNat b b' → a'.ble b' = false → ¬a ≤ b
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- If a function is integrable on a set `s` and vanishes everywhere on its complement,
then it is integrable.  -/
MeasureTheory.IntegrableOn.integrable_of_forall_notMem_eq_zero : ∀ {α : Type u_1} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α} {ε' : Type u_7}
  [inst : TopologicalSpace ε'] [inst_1 : ENormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε'] {f : α → ε'},
  MeasureTheory.IntegrableOn f s μ → (∀ x ∉ s, f x = 0) → MeasureTheory.Integrable f μ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {km : α}, t.minKey? = some km → t.getKey! km = km
-- Lean.Meta.Tactic.Backtrack
Lean.Meta.Tactic.Backtrack.BacktrackConfig.mk.injEq : ∀ (maxDepth : ℕ) (proc : List Lean.MVarId → List Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId)))
  (suspend : Lean.MVarId → Lean.MetaM Bool) (discharge : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId)))
  (commitIndependentGoals : Bool) (maxDepth_1 : ℕ)
  (proc_1 : List Lean.MVarId → List Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId)))
  (suspend_1 : Lean.MVarId → Lean.MetaM Bool) (discharge_1 : Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId)))
  (commitIndependentGoals_1 : Bool),
  ({ maxDepth := maxDepth, proc := proc, suspend := suspend, discharge := discharge,
        commitIndependentGoals := commitIndependentGoals } =
      { maxDepth := maxDepth_1, proc := proc_1, suspend := suspend_1, discharge := discharge_1,
        commitIndependentGoals := commitIndependentGoals_1 }) =
    (maxDepth = maxDepth_1 ∧
      proc = proc_1 ∧ suspend = suspend_1 ∧ discharge = discharge_1 ∧ commitIndependentGoals = commitIndependentGoals_1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.variableChange_a₆ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R),
  (C • W).a₆ = ↑C.u⁻¹ ^ 6 * (W.a₆ + C.r * W.a₄ + C.r ^ 2 * W.a₂ + C.r ^ 3 - C.t * W.a₃ - C.t ^ 2 - C.r * C.t * W.a₁)
-- Mathlib.Order.Defs.LinearOrder
compare_iff : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α) {o : Ordering}, compare a b = o ↔ o.Compares a b
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.Const.alter.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.Combinatorics.SimpleGraph.Metric
/-- The distance between two vertices is the length of the shortest walk between them.
If no such walk exists, this uses the junk value of `0`.
 -/
SimpleGraph.dist : {V : Type u_1} → SimpleGraph V → V → V → ℕ
-- Init.Data.Fin.Lemmas
Fin.is_le' : ∀ {n : ℕ} {a : Fin n}, ↑a ≤ n
-- Init.Prelude
/-- Division of natural numbers, discarding the remainder. Division by `0` returns `0`. Usually accessed
via the `/` operator.

This operation is sometimes called “floor division.”

This function is overridden at runtime with an efficient implementation. This definition is
the logical model.

Examples:
 * `21 / 3 = 7`
 * `21 / 5 = 4`
 * `0 / 22 = 0`
 * `5 / 0 = 0`
 -/
Nat.div : ℕ → ℕ → ℕ
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.add_neg_mul''' : ∀ {w : ℕ} {x y : BitVec w}, ~~~(y * x + x) + 1#w = ~~~y * x
-- Mathlib.Topology.Defs.Basic
WithTopology.ext_iff : ∀ {X : Type u_1} {t : TopologicalSpace X} {x y : WithTopology X t}, x = y ↔ x.ofTopology = y.ofTopology
-- Init.System.ST
ST.Ref.mk.injEq : ∀ {σ α : Type} (ref : ST.RefPointed.type) (h : Nonempty α) (ref_1 : ST.RefPointed.type) (h_1 : Nonempty α),
  ({ ref := ref, h := h } = { ref := ref_1, h := h_1 }) = (ref = ref_1)
-- Init.Data.Order.PackageFactories
/-- This structure contains all the data needed to create a `LinearOrderPackage α` instance. Its fields
are automatically provided if possible. For the detailed rules how the fields are inferred, see
`LinearOrderPackage.ofLE`.
 -/
Std.Packages.LinearOrderOfLEArgs : Type u → Type u
-- Mathlib.CategoryTheory.Localization.Prod
CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift.eq_1 : ∀ {C₁ : Type u₁} {C₂ : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {E : Type u₅} [inst_2 : CategoryTheory.Category.{v₅, u₅} E]
  (F : CategoryTheory.Functor (C₁ × C₂) E) (hF : (W₁.prod W₂).IsInvertedBy F) [inst_3 : W₁.ContainsIdentities]
  [inst_4 : W₂.ContainsIdentities],
  CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift F hF =
    CategoryTheory.Functor.uncurry.obj
      (CategoryTheory.Localization.Construction.lift
          (CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.prodLift₁ F hF).flip ⋯).flip
-- Mathlib.RingTheory.Valuation.ValuativeRel.Trivial
ValuativeRel.trivialRel_eq_ofValuation_one : ∀ {R Γ : Type} [inst : Ring R] [inst_1 : DecidableEq R] [inst_2 : IsDomain R]
  [inst_3 : LinearOrderedCommGroupWithZero Γ], ValuativeRel.trivialRel = ValuativeRel.ofValuation 1
-- Init.Data.Hashable
instHashableArray : {α : Type u_1} → [Hashable α] → Hashable (Array α)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Limits.Cone.overPost_π_app : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {D : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone D)
  (j : J) (k : CategoryTheory.Over j), (c.overPost j).π.app k = CategoryTheory.Over.homMk (c.π.app k.left) ⋯
-- Mathlib.CategoryTheory.Sites.CoverPreserving
CategoryTheory.compatiblePreservingOfFlat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (K : CategoryTheory.GrothendieckTopology D) (G : CategoryTheory.Functor C D) [CategoryTheory.RepresentablyFlat G],
  CategoryTheory.CompatiblePreserving K G
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Expr.denote.match_1.eq_3 : ∀ (motive : Int.Internal.Linear.Expr → Sort u_1) (a : Int.Internal.Linear.Expr)
  (h_1 : (a b : Int.Internal.Linear.Expr) → motive (a.add b))
  (h_2 : (a b : Int.Internal.Linear.Expr) → motive (a.sub b)) (h_3 : (a : Int.Internal.Linear.Expr) → motive a.neg)
  (h_4 : (k : ℤ) → motive (Int.Internal.Linear.Expr.num k))
  (h_5 : (v : Int.Internal.Linear.Var) → motive (Int.Internal.Linear.Expr.var v))
  (h_6 : (k : ℤ) → (e : Int.Internal.Linear.Expr) → motive (Int.Internal.Linear.Expr.mulL k e))
  (h_7 : (e : Int.Internal.Linear.Expr) → (k : ℤ) → motive (e.mulR k)),
  (match a.neg with
    | a.add b => h_1 a b
    | a.sub b => h_2 a b
    | a.neg => h_3 a
    | Int.Internal.Linear.Expr.num k => h_4 k
    | Int.Internal.Linear.Expr.var v => h_5 v
    | Int.Internal.Linear.Expr.mulL k e => h_6 k e
    | e.mulR k => h_7 e k) =
    h_3 a
-- Mathlib.Order.Atoms
Pi.isCoatomistic : ∀ {ι : Type u_4} {π : ι → Type u} [inst : (i : ι) → CompleteLattice (π i)] [∀ (i : ι), IsCoatomistic (π i)],
  IsCoatomistic ((i : ι) → π i)
-- Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence
/-- The naturality for the inverse.  -/
Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality.mkNaturalityInv : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality m] →
    Mathlib.Tactic.BicategoryLike.NormalizedHom →
      Mathlib.Tactic.BicategoryLike.NormalizedHom →
        Mathlib.Tactic.BicategoryLike.Mor₁ →
          Mathlib.Tactic.BicategoryLike.Mor₁ →
            Mathlib.Tactic.BicategoryLike.Mor₂Iso →
              Mathlib.Tactic.BicategoryLike.Mor₂Iso → Mathlib.Tactic.BicategoryLike.Mor₂Iso → Lean.Expr → m Lean.Expr
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram.IsTerminal.mk.inj : ∀ {J : Type w} {inst : CategoryTheory.SmallCategory J} {κ : Cardinal.{w}}
  {D : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.Diagram J κ} {e : J}
  {prop_id : D.W (CategoryTheory.CategoryStruct.id e)} {lift : {j : J} → D.P j → (j ⟶ e)}
  {hlift : ∀ {j : J} (hj : D.P j), D.W (lift hj)} {uniq : ∀ {j : J} (hj : D.P j) {φ : j ⟶ e}, D.W φ → lift hj = φ}
  {comm : ∀ {i j : J} (f : i ⟶ j) (hf : D.W f), CategoryTheory.CategoryStruct.comp f (lift ⋯) = lift ⋯}
  {prop_id_1 : D.W (CategoryTheory.CategoryStruct.id e)} {lift_1 : {j : J} → D.P j → (j ⟶ e)}
  {hlift_1 : ∀ {j : J} (hj : D.P j), D.W (lift_1 hj)}
  {uniq_1 : ∀ {j : J} (hj : D.P j) {φ : j ⟶ e}, D.W φ → lift_1 hj = φ}
  {comm_1 : ∀ {i j : J} (f : i ⟶ j) (hf : D.W f), CategoryTheory.CategoryStruct.comp f (lift_1 ⋯) = lift_1 ⋯},
  { prop_id := prop_id, lift := lift, hlift := hlift, uniq := uniq, comm := comm } =
      { prop_id := prop_id_1, lift := lift_1, hlift := hlift_1, uniq := uniq_1, comm := comm_1 } →
    lift = lift_1
-- Mathlib.LinearAlgebra.FreeModule.ModN
ModN.instFinite : ∀ {G : Type u_1} [inst : AddCommGroup G] {n : ℕ} [NeZero n] [Module.Free ℤ G] [Module.Finite ℤ G], Finite (ModN G n)
-- Mathlib.Data.Finset.Prod
Finset.product_union : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t t' : Finset β} [inst : DecidableEq α] [inst_1 : DecidableEq β],
  s ×ˢ (t ∪ t') = s ×ˢ t ∪ s ×ˢ t'