mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.baseChange_a₆ : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R) (S : Type s) [inst_1 : CommRing S]
  [inst_2 : Algebra R S], (W.baseChange S).a₆ = (algebraMap R S) W.a₆
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- The heterobasic version of `map` coincides with the regular version.  -/
TensorProduct.AlgebraTensorModule.map_eq : ∀ {R : Type uR} {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : AddCommMonoid P] [inst_6 : Module R P] [inst_7 : AddCommMonoid Q] [inst_8 : Module R Q] (f : M →ₗ[R] P)
  (g : N →ₗ[R] Q), TensorProduct.AlgebraTensorModule.map f g = TensorProduct.map f g
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.find_size : ∀ (self : Batteries.UnionFind) (x : Fin self.size), (self.find x).fst.size = self.size
-- Mathlib.Topology.Baire.BaireMeasurable
BaireMeasurableSet.sInter : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set (Set α)},
  s.Countable → (∀ t ∈ s, BaireMeasurableSet t) → BaireMeasurableSet (⋂₀ s)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.coeFn_finsetSum : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {ι : Type u_6} (s : Finset ι) (f : ι → ↥(MeasureTheory.Lp E p μ)),
  ↑↑(∑ i ∈ s, f i) =ᵐ[μ] ∑ i ∈ s, ↑↑(f i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_le_size_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k}, t.size ≤ (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.size
-- Init.Control.Basic
instToBoolBool : ToBool Bool
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.π_comp_H2Iso_hom_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↑(groupHomology.cycles A 2)),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.H2Iso A).hom)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.π A 2)) x) =
    (groupHomology.shortComplexH2 A).moduleCatToCycles.range.mkQ
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.isoCycles₂ A).hom) x)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.pushforward.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (E : CategoryTheory.PreZeroHypercover X),
  CategoryTheory.PreZeroHypercover.pushforward f E =
    { I₀ := E.I₀, X := E.X, f := fun i => CategoryTheory.CategoryStruct.comp (E.f i) f }
-- Mathlib.NumberTheory.Dioph
IsPoly.const : ∀ {α : Type u_1} (n : ℤ), IsPoly fun x => n
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
/-- A Jordan decomposition of a measurable space is a pair of mutually singular,
finite measures.  -/
MeasureTheory.JordanDecomposition : (α : Type u_2) → [MeasurableSpace α] → Type u_2
-- Mathlib.Topology.Constructions
/-- A map out of a sum type is continuous if its restriction to each summand is.  -/
continuous_sigma : ∀ {X : Type u} {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] [inst_1 : TopologicalSpace X]
  {f : Sigma σ → X}, (∀ (i : ι), Continuous fun a => f ⟨i, a⟩) → Continuous f
-- Init.System.IO
/-- A representation of “the real world” that's used in `IO` monads to ensure that `IO` actions are not
reordered.
 -/
IO.RealWorld : Type
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.toFullSubcategory_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X : P.FullSubcategory}
  (Q : HomotopicalAlgebra.Precylinder X.obj) (hQ : P Q.I),
  (Q.toFullSubcategory hQ).π = CategoryTheory.ObjectProperty.homMk Q.π
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.FG.countable_hom : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (N : Type u_2) [inst_1 : L.Structure N] [Countable N],
  FirstOrder.Language.Structure.FG L M → Countable (L.Hom M N)
-- Mathlib.Data.List.AList
AList.extract_eq_lookup_erase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (s : AList β),
  AList.extract a s = (AList.lookup a s, AList.erase a s)
-- Mathlib.Computability.RecursiveIn
Nat.RecursiveIn.succ : ∀ {O : Set (ℕ →. ℕ)}, Nat.RecursiveIn O ↑Nat.succ
-- Lean.Message
Lean.MessageData.compose.sizeOf_spec : ∀ (a a_1 : Lean.MessageData), sizeOf (a.compose a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.map_update_smul : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) (v : ι → M)
  [inst_5 : DecidableEq ι] (i : ι) (r : R) (x : M), f (Function.update v i (r • x)) = r • f (Function.update v i x)
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.insert.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (a : α) (b : β a) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.insert ⟨{ size := size, buckets := buckets }, hm⟩ a b =
    match Std.DHashMap.Internal.mkIdx buckets.size hm (hash a) with
    | ⟨i, h⟩ =>
      let bkt := buckets[i];
      if Std.DHashMap.Internal.AssocList.contains a bkt = true then
        let buckets' := buckets.uset i Std.DHashMap.Internal.AssocList.nil h;
        ⟨{ size := size, buckets := buckets'.uset i (Std.DHashMap.Internal.AssocList.replace a b bkt) ⋯ }, ⋯⟩
      else
        have size' := size + 1;
        let buckets' := buckets.uset i (Std.DHashMap.Internal.AssocList.cons a b bkt) h;
        Std.DHashMap.Internal.Raw₀.expandIfNecessary ⟨{ size := size', buckets := buckets' }, ⋯⟩
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ} {k k' : α} {fallback : γ},
  t.WF → t.getKey? k = some k' → (Std.TreeMap.Raw.map f t).getD k fallback = (Option.map (f k') t[k]?).getD fallback
-- Mathlib.Analysis.Seminorm
/-- **Alias** of `FunLike.coe_add`. -/
Seminorm.coe_add : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Add F] [inst_2 : Add β]
  [IsAddApply F α β] (f g : F), ⇑(f + g) = ⇑f + ⇑g
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
Units.one_le_inv : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ), 1 ≤ ↑u⁻¹ ↔ ↑u ≤ 1
-- Lean.Parser.Do
Lean.Parser.Term.doReassignArrow.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.zsmul_neg_iff : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.IntModule M] [Lean.Grind.OrderedAdd M]
  [inst_4 : LT M] [Std.LawfulOrderLT M] (k : ℤ) {a : M}, a < 0 → (k • a < 0 ↔ 0 < k)
-- Mathlib.Analysis.InnerProductSpace.TwoDim
/-- Auxiliary construction for `Orientation.rightAngleRotation`, rotation by 90 degrees in an
oriented real inner product space of dimension 2.  -/
Orientation.rightAngleRotationAux₂ : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] → [Fact (Module.finrank ℝ E = 2)] → Orientation ℝ E (Fin 2) → E →ₗᵢ[ℝ] E
-- Lean.Meta.Hint
/-- A widget for a clickable link (or icon) that inserts text into the document at a given position.

The props to this widget are of the following form:
```json
{
  "range": {
    "start": {"line": 100, "character": 0},
    "end":   {"line": 100, "character": 5}
  },
  "suggestion": "hi",
  "acceptSuggestionProps": {
    "kind": "text",
    "hoverText": "Displayed on hover",
    "linkText": "Displayed as the text of the link"
  }
}
```
... or the following form, where `codiconName` is one of the icons at
https://microsoft.github.io/vscode-codicons/dist/codicon.html and `gaps` determines
whether there are clickable spaces surrounding the icon:
```json
{
  "range": {
    "start": {"line": 100, "character": 0},
    "end":   {"line": 100, "character": 5}
  },
  "suggestion": "hi",
  "acceptSuggestionProps": {
    "kind": "icon",
    "hoverText": "Displayed on hover",
    "codiconName": "search",
    "gaps": true
  }
}
```

Note: we cannot add the `builtin_widget_module` attribute here because that would require importing
`Lean.Widget.UserWidget`, which in turn imports much of `Lean.Elab` -- the module where we want to
be able to use this widget. Instead, we register the attribute post-hoc when we declare the regular
"Try This" widget in `Lean.Meta.Tactic.TryThis`.
 -/
Lean.Meta.Hint.textInsertionWidget : Lean.Widget.Module
-- Mathlib.GroupTheory.Sylow
IsPGroup.toSylow_coe : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [inst_1 : Fact (Nat.Prime p)] {P : Subgroup G} (hP1 : IsPGroup p ↥P)
  (hP2 : ¬p ∣ P.index), ↑(hP1.toSylow hP2) = P
-- Mathlib.CategoryTheory.Quotient.Preadditive
/-- The preadditive structure on the category `Quotient r` when `r` is compatible
with the addition.  -/
CategoryTheory.Quotient.preadditive : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (r : HomRel C) →
        [CategoryTheory.Congruence r] →
          (∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)) →
            CategoryTheory.Preadditive (CategoryTheory.Quotient r)
-- ProofWidgets.Util
/-- Transform an action `x : m α` into an action `m (n α)` that
- saves the current context/state of `m`; and
- returns an action `y : n α` that would use the saved context/state if run.
  Note that because `y` no longer has access to `m`'s state,
  any `StateT` changes that it makes when you run it later will be discarded.  -/
MonadSaveCtx.saveCtxM : {m : Type → Type} → {n : outParam (Type → Type)} → [self : MonadSaveCtx m n] → {α : Type} → m α → m (n α)
-- Mathlib.Analysis.Matrix.Normed
Matrix.norm_diagonal : ∀ {n : Type u_4} {α : Type u_5} [inst : Fintype n] [inst_1 : SeminormedAddCommGroup α] [inst_2 : DecidableEq n]
  (v : n → α), ‖Matrix.diagonal v‖ = ‖v‖
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
Topology.RelCWComplex.Subcomplex.finiteDimensional_subcomplex_of_finiteDimensional : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D]
  [Topology.RelCWComplex.FiniteDimensional C] (E : Topology.RelCWComplex.Subcomplex C),
  Topology.RelCWComplex.FiniteDimensional ↑E
-- Init.Grind.Ring.Envelope
_private.Init.Grind.Ring.Envelope.0.Lean.Grind.Ring.OfSemiring.mk_lt_mk : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [inst_5 : Lean.Grind.OrderedAdd α] {a₁ a₂ b₁ b₂ : α},
  Lean.Grind.Ring.OfSemiring.Q.mk (a₁, a₂) < Lean.Grind.Ring.OfSemiring.Q.mk (b₁, b₂) ↔ a₁ + b₂ < a₂ + b₁
-- Mathlib.Topology.EMetricSpace.Defs
/-- `EDist α` means that `α` is equipped with an extended distance.  -/
EDist : Type u_2 → Type u_2
-- Mathlib.LinearAlgebra.SpecialLinearGroup
/-- The canonical isomorphism from `SL(n, R)` to the special linear group of the module `n → R`.  -/
Matrix.SpecialLinearGroup.toLin'_equiv : {R : Type u_1} →
  [inst : CommRing R] →
    {n : Type u_3} →
      [inst_1 : Fintype n] → [inst_2 : DecidableEq n] → Matrix.SpecialLinearGroup n R ≃* SpecialLinearGroup R (n → R)
-- Mathlib.Order.Bounded
Set.bounded_lt_Ioo : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), Set.Bounded (fun x1 x2 => x1 < x2) (Set.Ioo a b)
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instMax.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G],
  FiniteIndexNormalAddSubgroup.instMax =
    {
      max := fun U V =>
        let __Subgroup := U.toAddSubgroup ⊔ V.toAddSubgroup;
        { toAddSubgroup := __Subgroup, isNormal' := ⋯, isFiniteIndex' := ⋯ } }
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.covariance_self : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ},
  AEMeasurable X μ → ProbabilityTheory.covariance X X μ = ProbabilityTheory.variance X μ
-- Mathlib.Analysis.Convex.Strong
UniformConvexOn.neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {φ : ℝ → ℝ} {s : Set E} {f : E → ℝ},
  UniformConvexOn s φ f → UniformConcaveOn s φ (-f)
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.Indep.cardinalMk_le_cRank : ∀ {α : Type u} {M : Matroid α} {I : Set α}, M.Indep I → Cardinal.mk ↑I ≤ M.cRank
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
_private.Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf.0.CategoryTheory.Precoverage.SmallConstruction.Witness.eval.match_1.splitter : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    {K : CategoryTheory.Precoverage C} →
      (ι : C → Type (max u_1 u_2)) →
        (motive : (x : C) → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι x → Sort u_3) →
          (x : C) →
            (x_1 : CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι x) →
              ((X : C) → (i : ι X) → motive X (CategoryTheory.Precoverage.SmallConstruction.Witness.base✝ X i)) →
                ((x Y : C) →
                    (f : x ⟶ Y) →
                      (i : CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι Y) →
                        motive x (CategoryTheory.Precoverage.SmallConstruction.Witness.restrict✝ f i)) →
                  ((x : C) →
                      (R : CategoryTheory.Presieve x) →
                        (hR : R ∈ K.coverings x) →
                          (h :
                              ⦃W : C⦄ →
                                (r : W ⟶ x) → R r → CategoryTheory.Precoverage.SmallConstruction.Witness✝ K ι W) →
                            motive x (CategoryTheory.Precoverage.SmallConstruction.Witness.amalgamate✝ hR h)) →
                    motive x x_1
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.mem_of_closed' : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α}, IsClosed s → ∀ {a : α}, a ∈ s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range
StarSubalgebra.ofClass.congr_simp : ∀ {S : Type u_6} {R : Type u_7} {A : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : StarRing R] [inst_4 : StarRing A] [inst_5 : StarModule R A] [inst_6 : SetLike S A]
  [inst_7 : SubsemiringClass S A] [inst_8 : SMulMemClass S R A] [inst_9 : StarMemClass S A] (s s_1 : S),
  s = s_1 → StarSubalgebra.ofClass s = StarSubalgebra.ofClass s_1
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- The set of leading terms of non-zero polynomials within a set `B` is equal to the set of
leading terms of all polynomials within `B`, excluding zero.
 -/
MonomialOrder.image_leadingTerm_sdiff_singleton_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (B : Set (MvPolynomial σ R)),
  m.leadingTerm '' (B \ {0}) = m.leadingTerm '' B \ {0}
-- Mathlib.Order.GaloisConnection.Defs
GaloisConnection.l_u_l_eq_l' : ∀ {α : Type u} {β : Type v} [inst : PartialOrder α] [inst_1 : Preorder β] {u : α → β} {l : β → α},
  GaloisConnection l u → l ∘ u ∘ l = l
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.ins.match_3.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 : (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.red a y b))
  (h_3 :
    (a : RBTree.RBNode α) → (y : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a y b)),
  (match RBTree.RBNode.nil with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node RBTree.RBColor.red a y b => h_2 a y b
    | RBTree.RBNode.node RBTree.RBColor.black a y b => h_3 a y b) =
    h_1 ()
-- Mathlib.Algebra.Group.Subgroup.Basic
MonoidHom.prodMap_comap_prod : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {G' : Type u_8} {N' : Type u_9} [inst_2 : Group G']
  [inst_3 : Group N'] (f : G →* N) (g : G' →* N') (S : Subgroup N) (S' : Subgroup N'),
  Subgroup.comap (f.prodMap g) (S.prod S') = (Subgroup.comap f S).prod (Subgroup.comap g S')
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.le_order_smul : ∀ {R : Type u_3} {V : Type u_8} [inst : Zero V] [inst_1 : SMulZeroClass R V] {Γ : Type u_9} [inst_2 : Zero Γ]
  [inst_3 : LinearOrder Γ] (r : R) (x : HahnSeries Γ V), r • x ≠ 0 → x.order ≤ (r • x).order
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_ofBool : ∀ {i : ℕ} (b : Bool), (BitVec.ofBool b).getMsbD i = (decide (i = 0) && b)
-- Mathlib.Algebra.Group.Subsemigroup.Basic
Subsemigroup.gi.eq_1 : ∀ (M : Type u_1) [inst : Mul M], Subsemigroup.gi M = GaloisConnection.toGaloisInsertion ⋯ ⋯
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.le_functorPullback_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X : C} (R : CategoryTheory.Presieve X),
  R ≤ CategoryTheory.Presieve.functorPullback F (CategoryTheory.Presieve.map F R)
-- Mathlib.NumberTheory.Divisors
Nat.eq_properDivisors_of_subset_of_sum_eq_sum : ∀ {n : ℕ} {s : Finset ℕ}, s ⊆ n.properDivisors → ∑ x ∈ s, x = ∑ x ∈ n.properDivisors, x → s = n.properDivisors
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.step_filterMapM.match_1.eq_2 : ∀ {β β' : Type u_1} {n : Type u_1 → Type u_2} {f : β → n (Option β')} [inst : MonadAttach n] (out : β)
  (motive : Subtype (MonadAttach.CanReturn (f out)) → Sort u_3) (out' : β')
  (hf : MonadAttach.CanReturn (f out) (some out')) (h_1 : (hf : MonadAttach.CanReturn (f out) none) → motive ⟨none, hf⟩)
  (h_2 : (out' : β') → (hf : MonadAttach.CanReturn (f out) (some out')) → motive ⟨some out', hf⟩),
  (match ⟨some out', hf⟩ with
    | ⟨none, hf⟩ => h_1 hf
    | ⟨some out', hf⟩ => h_2 out' hf) =
    h_2 out' hf
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.exists_Polynomial_intValuation_lt : ∀ {K : Type u_2} [inst : Field K] (F : PowerSeries K) (η : (WithZero (Multiplicative ℤ))ˣ),
  ∃ P, (PowerSeries.idealX K).intValuation (F - ↑P) < ↑η
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.coe_orderIsoOfPrime_apply_coe : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (I : Ideal R)
  [hI : I.IsPrime] [inst_3 : IsLocalization.AtPrime S I] (a : { p // p.IsPrime }),
  ↑↑((IsLocalization.AtPrime.orderIsoOfPrime S I) a) = ⇑(algebraMap R S) ⁻¹' ↑↑a
-- Std.Data.TreeMap.Raw.Basic
/-- Carries out a monadic action on each mapping in the tree map in ascending order.  -/
Std.TreeMap.Raw.forM : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {m : Type w → Type w₂} → [Monad m] → (α → β → m PUnit.{w + 1}) → Std.TreeMap.Raw α β cmp → m PUnit.{w + 1}
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.insertMin.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (l' : Std.DTreeMap.Internal.Impl α β)
  (motive : Std.DTreeMap.Internal.Impl.Tree α β (1 + l'.size) → Sort u_3) (l'' : Std.DTreeMap.Internal.Impl α β)
  (hl''₁ : l''.Balanced) (hl''₂ : l''.size = 1 + l'.size)
  (h_1 :
    (l'' : Std.DTreeMap.Internal.Impl α β) →
      (hl''₁ : l''.Balanced) →
        (hl''₂ : l''.size = 1 + l'.size) → motive { impl := l'', balanced_impl := hl''₁, size_impl := hl''₂ }),
  (match { impl := l'', balanced_impl := hl''₁, size_impl := hl''₂ } with
    | { impl := l'', balanced_impl := hl''₁, size_impl := hl''₂ } => h_1 l'' hl''₁ hl''₂) =
    h_1 l'' hl''₁ hl''₂
-- Mathlib.Data.W.Constructions
_private.Mathlib.Data.W.Constructions.0.WType.ofNat.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive Nat.zero) (h_2 : (n : ℕ) → motive n.succ),
  (match Nat.zero with
    | Nat.zero => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.GroupTheory.Solvable
Group.IsSolvable.commutator_lt_of_ne_bot : ∀ {G : Type u_1} [inst : Group G] [Group.IsSolvable G] {H : Subgroup G}, H ≠ ⊥ → ⁅H, H⁆ < H
-- Mathlib.Data.Matrix.Diagonal
Matrix.diag_zero : ∀ {n : Type u_3} {α : Type v} [inst : Zero α], Matrix.diag 0 = 0
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
RingHom.IsStableUnderBaseChange.pullback_fst_appTop : ∀ (P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop),
  (RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
      ∀ {X Y S : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] [AlgebraicGeometry.IsAffine Y]
        [AlgebraicGeometry.IsAffine S] (f : X ⟶ S) (g : Y ⟶ S),
        P (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop g)) →
          P (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop (CategoryTheory.Limits.pullback.fst f g)))
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_erase_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).size ≤ t.size
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_minD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {fallback : α}, t.contains (t.minD fallback) = true
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
/-- Returns `.true` if `c` is satisfied by the current partial model,
`.undef` if `c` contains unassigned variables, and `.false` otherwise.
 -/
Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.satisfied : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr → Lean.Meta.Grind.GoalM Lean.LBool
-- Mathlib.NumberTheory.MulChar.Duality
MulChar.apply_mulCharEquiv : ∀ {M : Type u_1} {R : Type u_2} [inst : CommMonoid M] [inst_1 : CommRing R] [inst_2 : Finite M]
  [inst_3 : HasEnoughRootsOfUnity R (Monoid.exponent Mˣ)] (χ : MulChar M R) (η : MulChar (MulChar M R) R),
  χ ↑((MulChar.mulCharEquiv M R) η) = η χ
-- Mathlib.Data.Multiset.Replicate
Multiset.replicate_one : ∀ {α : Type u_1} (a : α), Multiset.replicate 1 a = {a}
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  (t₁ ∪ t₂).isEmpty = (t₁.isEmpty && t₂.isEmpty)
-- Lean.Parser.Do
Lean.Parser.Term.doExpr.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.instSetLike : {X : Type u_1} →
  [t : TopologicalSpace X] →
    {C D : Set X} → [inst : Topology.RelCWComplex C D] → SetLike (Topology.RelCWComplex.Subcomplex C) X
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- A partial linear map that contains every element in a directed set of
`HahnEmbedding.Partial`.  -/
HahnEmbedding.Partial.sSupFun : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      {R : Type u_3} →
                        [inst_9 : AddCommGroup R] →
                          [inst_10 : LinearOrder R] →
                            [inst_11 : Module K R] →
                              {seed : HahnEmbedding.Seed K M R} →
                                {c : Set (HahnEmbedding.Partial seed)} →
                                  DirectedOn (fun x1 x2 => x1 ≤ x2) c →
                                    M →ₗ.[K] Lex (HahnSeries (FiniteArchimedeanClass M) R)