mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.coe_sup : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s t : TopologicalSpace.NonemptyCompacts α), ↑(s ⊔ t) = ↑s ∪ ↑t
-- Lean.Elab.DefView
/-- Elaboration result.  -/
Lean.Elab.BodyProcessedSnapshot.value : Lean.Elab.BodyProcessedSnapshot → Lean.Expr
-- Mathlib.Topology.EMetricSpace.Basic
/-- The product of two emetric spaces, with the max distance, is an extended
metric spaces. We make sure that the uniform structure thus constructed is the one
corresponding to the product of uniform spaces, to avoid diamond problems.  -/
Prod.emetricSpaceMax : {β : Type v} → {γ : Type w} → [EMetricSpace γ] → [EMetricSpace β] → EMetricSpace (γ × β)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.mul : Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.delete_iff : ∀ {α : outParam (Type u)} {β : Type v} [self : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] (c : β)
  (l l' : Std.Sat.Literal α),
  l' ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList (Std.Tactic.BVDecide.LRAT.Internal.Clause.delete c l) ↔
    l' ≠ l ∧ l' ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
tangentBundleCore_coordChange_achart : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] (x x' z : M),
  (tangentBundleCore I M).coordChange (achart H x) (achart H x') z =
    fderivWithin 𝕜 (↑(extChartAt I x') ∘ ↑(extChartAt I x).symm) (Set.range ↑I) (↑(extChartAt I x) z)
-- Mathlib.Algebra.Algebra.Subalgebra.Directed
Subalgebra.iSupLift_inclusion : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {ι : Type u_4} [inst_5 : Nonempty ι] (K : ι → Subalgebra R A)
  {dir : Directed (fun x1 x2 => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₐ[R] B}
  {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (Subalgebra.inclusion h)} {T : Subalgebra R A} {hT : T ≤ iSup K}
  {i : ι} (x : ↥(K i)) (h : K i ≤ T), (Subalgebra.iSupLift K dir f hf T hT) ((Subalgebra.inclusion h) x) = (f i) x
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- A side of a right-angled triangle divided by the cosine of the adjacent angle equals the
hypotenuse.  -/
EuclideanGeometry.dist_div_cos_angle_of_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
    p₁ = p₂ ∨ p₃ ≠ p₂ → dist p₃ p₂ / Real.cos (EuclideanGeometry.angle p₂ p₃ p₁) = dist p₁ p₃
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.instHasModelBitVecOfNatNat : HasModel✝ Int32 (BitVec 32)
-- Mathlib.CategoryTheory.Limits.Shapes.SingleObj
CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints_symm_apply_coe : ∀ {M : Type v} [inst : Monoid M] (J : CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u))
  (p : ↑(MulAction.fixedPoints M (J.obj (CategoryTheory.SingleObj.star M)))) (x : CategoryTheory.SingleObj M),
  ↑((CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints J).symm p) x = ↑p
-- Mathlib.Geometry.Diffeology.Basic
/-- The D-topology of the diffeology. This is included as part of the data in order to give
control over what the D-topology is defeq to. See also note [forgetful inheritance].  -/
DiffeologicalSpace.dTopology : {X : Type u_1} → [self : DiffeologicalSpace X] → TopologicalSpace X
-- Mathlib.RingTheory.MvPowerSeries.Equiv
PowerSeries.subst_toMvPowerSeries : ∀ {σ : Type u_2} {τ : Type u_3} {R : Type u_4} [inst : CommRing R] {f : PowerSeries R} {i : σ}
  {a : σ → MvPowerSeries τ R},
  MvPowerSeries.HasSubst a → MvPowerSeries.subst a ((PowerSeries.toMvPowerSeries i) f) = PowerSeries.subst (a i) f
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenCoend.ι_desc : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenCoendsOfShape J C] {X : C} (f : (j : J) → (F.obj (Opposite.op j)).obj j ⟶ X)
  (hf :
    ∀ ⦃i j : J⦄ (g : i ⟶ j),
      CategoryTheory.CategoryStruct.comp ((F.map g.op).app i) (f i) =
        CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map g) (f j))
  (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenCoend.ι F j)
      (CategoryTheory.Limits.chosenCoend.desc f hf) =
    f j
-- Mathlib.Analysis.Normed.Ring.Basic
List.nnnorm_prod : ∀ {α : Type u_2} [inst : SeminormedRing α] [NormOneClass α] [NormMulClass α] (l : List α),
  ‖l.prod‖₊ = (List.map nnnorm l).prod
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
continuousMultilinearCurryLeftEquiv_apply : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : ContinuousMultilinearMap 𝕜 Ei G) (x : Ei 0)
  (v : (i : Fin n) → Ei i.succ), (((continuousMultilinearCurryLeftEquiv 𝕜 Ei G) f) x) v = f (Fin.cons x v)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.snd_inl : ∀ {R : Type u_1} (A : Type u_2) [inst : Zero A] (r : R), (Unitization.inl r).toProd.2 = 0
-- Std.Http.Protocol.H1
/-- Consumes close-delimited body bytes.

When socket EOF is observed (`noMoreInput` + atEnd), closes body; otherwise it
either emits available bytes or requests more data.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.parseCloseDelimitedBody : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir × Option Std.Http.Protocol.H1.PulledChunk × Bool
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.swap_map : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] (f : M →+ M') (g : N →+ N') (x : AddMonoid.Coprod M N),
  (AddMonoid.Coprod.swap M' N') ((AddMonoid.Coprod.map f g) x) =
    (AddMonoid.Coprod.map g f) ((AddMonoid.Coprod.swap M N) x)
-- Mathlib.Data.Int.Bitwise
Int.bodd_add_div2 : ∀ (n : ℤ), (bif n.bodd then 1 else 0) + 2 * n.div2 = n
-- Mathlib.Data.Set.Insert
Set.Nonempty.eq_zero : ∀ {α : Type u_1} [Subsingleton α] [inst : Zero α] {s : Set α}, s.Nonempty → s = {0}
-- Mathlib.Order.SuccPred.Relation
/-- **Alias** of `transGen_of_pred_of_refl`.

---

`(n, m)` is in the transitive closure of a reflexive relation `~` if `i ~ pred i` and
`pred i ~ i` for all `i` between `n` and `m`.  -/
transGen_of_pred_of_reflexive : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α] (r : α → α → Prop) {n m : α}
  [Std.Refl r],
  (∀ i ∈ Set.Ioc m n, r i (Order.pred i)) → (∀ i ∈ Set.Ioc n m, r (Order.pred i) i) → Relation.TransGen r n m
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Inhabited α] {f : (a : α) → β a → Bool}
  {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey! k (List.filter (fun p => f p.fst p.snd) l) =
      ((Std.Internal.List.getKey? k l).pfilter fun x h => f x (Std.Internal.List.getValueCast x l ⋯)).get!
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.lt_iff : ∀ {α : Type u} [inst : LT α] [inst_1 : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α] {a b : α},
  a < b ↔ Std.PRange.UpwardEnumerable.LT a b
-- Mathlib.Analysis.Calculus.MeanValue
/-- General fencing theorem for continuous functions with an estimate on the derivative.
Let `f` and `B` be continuous functions on `[a, b]` such that

* `f a ≤ B a`;
* `B` has derivative `B'` everywhere on `ℝ`;
* `f` has right derivative `f'` at every point of `[a, b)`;
* we have `f' x < B' x` whenever `f x = B x`.

Then `f x ≤ B x` everywhere on `[a, b]`.  -/
image_le_of_deriv_right_lt_deriv_boundary : ∀ {f f' : ℝ → ℝ} {a b : ℝ},
  ContinuousOn f (Set.Icc a b) →
    (∀ x ∈ Set.Ico a b, HasDerivWithinAt f (f' x) (Set.Ici x) x) →
      ∀ {B B' : ℝ → ℝ},
        f a ≤ B a →
          (∀ (x : ℝ), HasDerivAt B (B' x) x) →
            (∀ x ∈ Set.Ico a b, f x = B x → f' x < B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → f x ≤ B x
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.trans_ofSet : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : Set Y} (hs : IsOpen s),
  e.trans (OpenPartialHomeomorph.ofSet s hs) = e.restr (↑e ⁻¹' s)
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsInt.neg_to_eq : ∀ {α : Type u_1} [inst : Ring α] {n : ℕ} {a a' : α}, Mathlib.Meta.NormNum.IsInt a (Int.negOfNat n) → ↑n = a' → a = -a'
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- If `g : ℝ → ℝ` is periodic with period `T > 0` and `0 < ∫ x in 0..T, g x`, then
`t ↦ ∫ x in 0..t, g x` tends to `∞` as `t` tends to `∞`.  -/
Function.Periodic.tendsto_atTop_intervalIntegral_of_pos : ∀ {T : ℝ} {g : ℝ → ℝ},
  Function.Periodic g T →
    0 < ∫ (x : ℝ) in 0..T, g x → 0 < T → Filter.Tendsto (fun t => ∫ (x : ℝ) in 0..t, g x) Filter.atTop Filter.atTop
-- Mathlib.Tactic.DeriveCountable
/-- Generic step of the injectivity argument, pops the head of the pairs.
Used in the recursive steps where we need to supply an additional injectivity argument.
 -/
Mathlib.Deriving.Countable.cons_eq_imp : ∀ {p : Prop} {a b a' b' : ℕ}, (a = a' → b = b' → p) → Nat.pair a b = Nat.pair a' b' → p
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.insertMany_list_singleton : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {k : α} {v : β k},
  m.insertMany [⟨k, v⟩] = m.insert k v
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- A factorisation of a morphism `f = e ≫ m`, with `m` monic.  -/
CategoryTheory.Limits.MonoFactorisation.m_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (self : CategoryTheory.Limits.MonoFactorisation f), CategoryTheory.Mono self.m
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapCoconePrecompose_hom_hom : ∀ {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] (H : CategoryTheory.Functor C D)
  {F G : CategoryTheory.Functor J C} {α : G ⟶ F} {c : CategoryTheory.Limits.Cocone F},
  H.mapCoconePrecompose.hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
-- Mathlib.Analysis.Normed.Group.Basic
norm_mul_eq_norm_right : ∀ {E : Type u_5} [inst : SeminormedGroup E] {x : E} (y : E), ‖x‖ = 0 → ‖x * y‖ = ‖y‖
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insertIfNew k v).maxKey? = some (t.maxKey?.elim k fun k' => if cmp k' k = Ordering.lt then k else k')
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblXYZ_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 = Q 0 * P 2 →
            P 1 * Q 2 ≠ W.negY Q * P 2 →
              W.dblXYZ P =
                W.dblZ P •
                  ![W.toAffine.addX (P 0 / P 2) (Q 0 / Q 2)
                      (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)),
                    W.toAffine.addY (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2)
                      (W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2)),
                    1]
-- Mathlib.Dynamics.TopologicalEntropy.NetEntropy
Dynamics.netEntropyInfEntourage_le_coverEntropyInfEntourage : ∀ {X : Type u_1} {U : SetRel X X} (T : X → X) (F : Set X),
  Dynamics.netEntropyInfEntourage T F U ≤ Dynamics.coverEntropyInfEntourage T F U
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.maxEntry!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited ((a : α) × β a)], t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.maxEntry! = t₂.maxEntry!
-- Mathlib.Analysis.RCLike.Basic
RCLike.ratCast_re : ∀ {K : Type u_1} [inst : RCLike K] (q : ℚ), RCLike.re ↑q = ↑q
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.exists_of_res_zero_of_qcqs : ∀ {X : AlgebraicGeometry.Scheme} {U : TopologicalSpace.Opens ↥X},
  IsCompact U.carrier →
    IsQuasiSeparated U.carrier →
      ∀ {f s : ↑(X.presheaf.obj (Opposite.op U))},
        TopCat.Presheaf.restrictOpen f (X.basicOpen s) ⋯ = 0 → ∃ n, s ^ n * f = 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
AddHom.withBotMap_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N), ⇑f.withBotMap = WithBot.map ⇑f
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_attach_eq_prod_dite : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : Fintype ι] (s : Finset ι) (f : ↥s → M)
  [inst_2 : DecidablePred fun x => x ∈ s], ∏ i ∈ s.attach, f i = ∏ i, if h : i ∈ s then f ⟨i, h⟩ else 1
-- Mathlib.Data.Rel
SetRel.core_subset_core : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β} {t₁ t₂ : Set β}, t₁ ⊆ t₂ → R.core t₁ ⊆ R.core t₂
-- Mathlib.Analysis.Normed.Group.Uniform
AntilipschitzWith.add_sub_lipschitzWith : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {Kf Kg : NNReal}
  {f g : α → E}, AntilipschitzWith Kf f → LipschitzWith Kg (g - f) → Kg < Kf⁻¹ → AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g
-- Aesop.Script.SScript
Aesop.Script.SScript.takeNConsecutiveFocusAndSolve? : Array Aesop.Script.SScript → ℕ → Aesop.Script.SScript → Option (Array Aesop.Script.SScript × Aesop.Script.SScript)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getD_eq_getD_get? : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {a : α} {fallback : β}, Std.DHashMap.Raw.Const.getD m a fallback = (Std.DHashMap.Raw.Const.get? m a).getD fallback
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.endRingEquiv_apply : ∀ {R : Type u} [inst : Ring R] (M : ModuleCat R) (f : M.Hom M), M.endRingEquiv f = f.hom
-- Init.Grind.Ring.Field
Lean.Grind.Field.of_mul_eq_zero : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] {a b : α}, a * b = 0 → a = 0 ∨ b = 0
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.zero_left : ∀ {o : Ordinal.{u_1}}, o ≠ 0 → Ordinal.CNF 0 o = [(0, o)]
-- Std.Data.DTreeMap.Raw.Basic
/-- Retrieves the key from the mapping that matches `a`. Ensures that such a mapping exists by
requiring a proof of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the map.
 -/
Std.DTreeMap.Raw.getKey : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → (t : Std.DTreeMap.Raw α β cmp) → (a : α) → a ∈ t → α
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.InducedCategory.homAddEquiv_symm_apply_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  {F : D → C} {X Y : CategoryTheory.InducedCategory C F} (f : F X ⟶ F Y),
  (CategoryTheory.InducedCategory.homAddEquiv.symm f).hom = f
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
/-- The category of closed subschemes is contravariantly equivalent
to the lattice of ideal sheaves.  -/
AlgebraicGeometry.IsClosedImmersion.overEquivIdealSheafData : (X : AlgebraicGeometry.Scheme) →
  (CategoryTheory.MorphismProperty.Over @AlgebraicGeometry.IsClosedImmersion ⊤ X)ᵒᵖ ≌ X.IdealSheafData
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.FiniteCyclic
Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_toFun : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : CommGroup G] [inst_2 : Fintype G] (A : Rep.{u, u, u} k G) (g : G)
  (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) (a : ↑A) (x : MonoidAlgebra k G),
  (Rep.Hom.hom ((ModuleCat.Hom.hom ((Rep.FiniteCyclicGroup.homResolutionIso A g hg).inv.f i)) a)) x =
    x.coeff.sum fun x r => r • (A.ρ x) a
-- Init.Data.Sum.Lemmas
Sum.getRight_eq_iff : ∀ {β : Type u_1} {b : β} {α : Type u_2} {x : α ⊕ β} (h : x.isRight = true), x.getRight h = b ↔ x = Sum.inr b
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.nonsingular_negAdd : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F},
  W.Nonsingular x₁ y₁ →
    W.Nonsingular x₂ y₂ →
      ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂) →
        W.Nonsingular (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_filter_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {f : (a : α) → β a → Bool}
  {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.containsKey k (List.filter (fun p => f p.fst p.snd) l) = true ↔
      ∃ (h : Std.Internal.List.containsKey k l = true), f k (Std.Internal.List.getValueCast k l h) = true)
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.instBicategory : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] →
      CategoryTheory.Bicategory (CategoryTheory.CatEnrichedOrdinary C)
-- Mathlib.Topology.Separation.Hausdorff
DiscreteTopology.toT2Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [DiscreteTopology X], T2Space X
-- Init.Data.UInt.BasicAux
/-- Converts a `UInt32` into the corresponding `Fin UInt32.size`.  -/
UInt32.toFin : UInt32 → Fin UInt32.size
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncLTGELTSelfToGELT : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : EInt),
  CategoryTheory.IsIso (t.eTruncLTGELTSelfToGELT a b)
-- Mathlib.Algebra.GroupWithZero.Equiv
MulEquiv.toMonoidWithZeroHom_inj : ∀ {G : Type u_1} {H : Type u_2} [inst : MulZeroOneClass G] [inst_1 : MulZeroOneClass H] {f g : G ≃* H},
  f.toMonoidWithZeroHom = g.toMonoidWithZeroHom ↔ f = g
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.pointwise_smul_toAddSubmonoid : ∀ {M : Type u_1} {R : Type u_3} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] (a : M)
  (S : Ideal R), (Function.Surjective fun r => a • r) → (a • S).toAddSubmonoid = a • S.toAddSubmonoid
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.min_eq_or : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {p q : (a : α) × β a}, p ⊓ q = p ∨ p ⊓ q = q
-- Mathlib.Probability.Decision.Risk.Countable
ProbabilityTheory.bayesRisk_countable' : ∀ {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ}
  [Countable 𝓨] [MeasurableSingletonClass 𝓨],
  Measurable ℓ →
    ProbabilityTheory.bayesRisk ℓ P π =
      ⨅ κ, ⨅ (_ : ProbabilityTheory.IsMarkovKernel κ), ∑' (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y * ((P θ).bind ⇑κ) {y} ∂π
-- Mathlib.Testing.Plausible.Functions
_private.Mathlib.Testing.Plausible.Functions.0.List.dlookup.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : List (Sigma β) → Sort u_3) (a' : α) (b : β a') (l : List (Sigma β))
  (h_1 : Unit → motive []) (h_2 : (a' : α) → (b : β a') → (l : List (Sigma β)) → motive (⟨a', b⟩ :: l)),
  (match ⟨a', b⟩ :: l with
    | [] => h_1 ()
    | ⟨a', b⟩ :: l => h_2 a' b l) =
    h_2 a' b l
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_smul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (c : ℝ) (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.variance (c • X) μ = c ^ 2 * ProbabilityTheory.variance X μ
-- Mathlib.RingTheory.Binomial
Ring.smeval_ascPochhammer_succ_neg : ∀ (n : ℕ), (ascPochhammer ℕ (n + 1)).smeval (-↑n) = 0
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- The pullback of the top object in `MonoOver Y`
is (isomorphic to) the top object in `MonoOver X`.  -/
CategoryTheory.MonoOver.pullbackTop : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasPullbacks C] → (f : X ⟶ Y) → (CategoryTheory.MonoOver.pullback f).obj ⊤ ≅ ⊤
-- Mathlib.Topology.MetricSpace.Cover
Metric.IsCover.empty : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ε : NNReal} {N : Set X}, Metric.IsCover ε ∅ N
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.id_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.HomologyData),
  (CategoryTheory.ShortComplex.HomologyMapData.id h).right = CategoryTheory.ShortComplex.RightHomologyMapData.id h.right
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnriched.comp_eq : ∀ {C : Type u_1} [inst : CategoryTheory.EnrichedCategory CategoryTheory.Cat C] {X Y Z : CategoryTheory.CatEnriched C}
  (f : X ⟶ Y) (g : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f g = (CategoryTheory.eComp CategoryTheory.Cat X Y Z).toFunctor.obj (f, g)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_union_eq_right : ∀ {ι : Type u_1} {M : Type u_4} {s₁ s₂ : Finset ι} [inst : CommMonoid M] {f : ι → M} [inst_1 : DecidableEq ι],
  (∀ a ∈ s₁, a ∉ s₂ → f a = 1) → ∏ a ∈ s₁ ∪ s₂, f a = ∏ a ∈ s₂, f a
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.denote_go_eq_divRec_q : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (assign : α → Bool) (curr : ℕ)
  (lhs rhs rbv qbv : BitVec w) (n d q r : aig.RefVec w) (wn wr : ℕ),
  (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := n.get idx hidx }⟧ = lhs.getLsbD idx) →
    (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := d.get idx hidx }⟧ = rhs.getLsbD idx) →
      (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := q.get idx hidx }⟧ = qbv.getLsbD idx) →
        (∀ (idx : ℕ) (hidx : idx < w), ⟦assign, { aig := aig, ref := r.get idx hidx }⟧ = rbv.getLsbD idx) →
          ∀ (idx : ℕ) (hidx : idx < w),
            ⟦assign,
                { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig curr n d wn wr q r).aig,
                  ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig curr n d wn wr q r).q.get idx hidx }⟧ =
              (BitVec.divRec curr { n := lhs, d := rhs } { wn := wn, wr := wr, q := qbv, r := rbv }).q.getLsbD idx
-- Mathlib.Order.RelSeries
RelSeries.take_length : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)), (p.take i).length = ↑i
-- Mathlib.Tactic.CategoryTheory.Coherence
/-- Coherence tactic for monoidal categories.  -/
Mathlib.Tactic.Coherence.monoidalCoherence : Lean.MVarId → Lean.Elab.TermElabM Unit