mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_congr : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] {p : MvPolynomial σ R}
  (f : R →+* S₁) (g₁ g₂ : σ → S₁),
  (∀ {i : σ} {c : σ →₀ ℕ}, i ∈ c.support → MvPolynomial.coeff c p ≠ 0 → g₁ i = g₂ i) →
    MvPolynomial.eval₂ f g₁ p = MvPolynomial.eval₂ f g₂ p
-- Mathlib.FieldTheory.Finite.Polynomial
MvPolynomial.map_restrict_dom_evalₗ : ∀ (K : Type u_1) (σ : Type u_2) [inst : Field K] [inst_1 : Fintype K] [Finite σ],
  Submodule.map (MvPolynomial.evalₗ K σ) (MvPolynomial.restrictDegree σ K (Fintype.card K - 1)) = ⊤
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.foldrM_eq_foldrM_toArray : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {δ : Type w} {m : Type w → Type w'} [inst : Monad m]
  [LawfulMonad m] {f : α → δ → m δ} {init : δ}, Std.TreeSet.Raw.foldrM f init t = Array.foldrM f init t.toArray
-- Mathlib.Data.Sign.Defs
SignType.nonpos_iff_ne_one : ∀ {a : SignType}, a ≤ 0 ↔ a ≠ 1
-- Std.Do.WP.Sound
/-- Pure-proposition soundness for `ExceptT.run`, generalizing `Except.of_wp_eq`.  -/
Std.Do.ExceptT.of_wp_run : ∀ {m : Type u → Type u_1} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Do.WP m Std.Do.PostShape.pure]
  [Std.Do.WPSound m Std.Do.PostShape.pure] [inst_4 : MonadAttach m] [LawfulMonadAttach m] {ε α : Type u}
  {prog : ExceptT ε m α} {x : Except ε α} (P : Except ε α → Prop),
  MonadAttach.CanReturn prog.run x →
    (⊢ₛ (Std.Do.wp prog).apply (fun a => ⌜P (Except.ok a)⌝, fun e => ⌜P (Except.error e)⌝, PUnit.unit)) → P x
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValueD_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [EquivBEq α] {f : α → β → Option γ} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k k' : α} {fallback : γ},
      Std.Internal.List.getKey? k l = some k' →
        Std.Internal.List.getValueD k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l)
            fallback =
          ((Std.Internal.List.getValue? k l).bind fun x => f k' x).getD fallback
-- Mathlib.Tactic.Simps.Basic
/-- name for this projection used in the structure definition  -/
Simps.ParsedProjectionData.strName : Simps.ParsedProjectionData → Lean.Name
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.disjointUnion_symm_apply : ∀ {α : Type u_1} {β : Type u_2} (e e' : PartialEquiv α β) (hs : Disjoint e.source e'.source)
  (ht : Disjoint e.target e'.target) [inst : (x : α) → Decidable (x ∈ e.source)]
  [inst_1 : (y : β) → Decidable (y ∈ e.target)], ↑(e.disjointUnion e' hs ht).symm = e.target.piecewise ↑e.symm ↑e'.symm
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.insert k v)[k]? = some v
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_add_product : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t : Finset α},
  Finset.image (fun x => x.1 + x.2) (s ×ˢ t) = s + t
-- Mathlib.Algebra.Field.Subfield.Basic
/-- Restriction of a ring homomorphism to its range interpreted as a subfield.  -/
RingHom.rangeRestrictField : {K : Type u} → {L : Type v} → [inst : DivisionRing K] → [inst_1 : DivisionRing L] → (f : K →+* L) → K →+* ↥f.fieldRange
-- Mathlib.Data.List.Chain
/-- If `a` and `b` are related by the reflexive transitive closure of `r`, then there is an
`r`-chain starting from `a` and ending on `b`.
 -/
List.exists_isChain_ne_nil_of_relationReflTransGen : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α},
  Relation.ReflTransGen r a b → ∃ l, ∃ (hl : l ≠ []), List.IsChain r l ∧ l.head hl = a ∧ l.getLast hl = b
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instAdd.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_5} [inst : (i : ι) → Add (M i)], Pi.instAdd = { add := fun f g i => f i + g i }
-- Mathlib.Topology.Compactness.Lindelof
eq_closed_inter_nat : ∀ {X : Type u} [inst : TopologicalSpace X] [HereditarilyLindelofSpace X] {ι : Type u_2} [Nonempty ι] (C : ι → Set X),
  (∀ (i : ι), IsClosed (C i)) → ∃ k, ⋂ n, C (k n) = ⋂ i, C i
-- Mathlib.Order.Category.LinOrd
_private.Mathlib.Order.Category.LinOrd.0.LinOrd.Hom.mk.sizeOf_spec : ∀ {X Y : LinOrd} (hom' : ↑X →o ↑Y), sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_18 : HAdd Std.Time.Minute.Offset Std.Time.Nanosecond.Offset Std.Time.Nanosecond.Offset
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.productiveRel_of_fst : ∀ {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : Std.Iterator α₁ m β]
  [inst_2 : Std.Iterator α₂ m β] [inst_3 : Std.Iterators.Productive α₁ m] [inst_4 : Std.Iterators.Productive α₂ m]
  {it₁ it₁' : Std.IterM m β} {it₂ : Std.IterM m β},
  it₁'.finitelyManySkips.Rel it₁.finitelyManySkips →
    Std.Iterators.Types.Append.ProductiveRel α₁ α₂ m β (it₁'.append it₂) (it₁.append it₂)
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.ker_projectionL : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q), (↑(p.projectionL q h)).ker = q
-- Mathlib.Order.Disjoint
IsComplemented.sup : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {a b : α},
  IsComplemented a → IsComplemented b → IsComplemented (a ⊔ b)
-- ProofWidgets.Component.Basic
/-- A component is a widget module with a `default` or named export which is a
[React component](https://react.dev/learn/your-first-component). Every component definition must
be annotated with `@[widget_module]`. This makes it possible for the infoview to load the component.

## Execution environment

The JS environment in which components execute provides a fixed set of libraries accessible via
direct `import`, notably
[`@leanprover/infoview`](https://www.npmjs.com/package/@leanprover/infoview).
All [React contexts](https://react.dev/learn/passing-data-deeply-with-context) exported from
`@leanprover/infoview` are usable from components.

## Lean encoding of props

`Props` is the Lean representation of the type `JsProps` of
[React props](https://react.dev/learn/passing-props-to-a-component)
that the component expects.
The export of the module specified in `«export»` should then have type
`(props: JsProps & { pos: DocumentPosition, children: React.ReactNode }) => React.ReactNode`
where `DocumentPosition` is defined in `@leanprover/infoview`.
`Props` is expected to have a `Lean.Server.RpcEncodable` instance
specifying how to encode props as JSON.

Note that by defining a `Component Props` with a specific JS implementation,
you are *asserting* that `Props` is a correct representation of `JsProps`.  -/
ProofWidgets.Component : Type → Type
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.centralizer_le : ∀ {R : Type u_1} [inst : NonUnitalRing R] (s t : Set R),
  s ⊆ t → NonUnitalSubring.centralizer t ≤ NonUnitalSubring.centralizer s
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.image_preimage : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂) (s : Set P₂), ⇑e '' ⇑e ⁻¹' s = s
-- Mathlib.RingTheory.Ideal.GoingUp
Ideal.comap_ne_bot_of_integral_mem : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {I : Ideal S} [inst_2 : Algebra R S]
  [Nontrivial R] [IsDomain S] {x : S}, x ≠ 0 → x ∈ I → IsIntegral R x → Ideal.comap (algebraMap R S) I ≠ ⊥
-- Lean.Meta.Closure
/-- Create an auxiliary definition with the given name, type and value.
The parameters `type` and `value` may contain free and meta variables.
A "closure" is computed, and a term of the form `name.{u_1 ... u_n} t_1 ... t_m` is
returned where `u_i`s are universe parameters and metavariables `type` and `value` depend on,
and `t_j`s are free and meta variables `type` and `value` depend on.  -/
Lean.Meta.mkAuxDefinition : Lean.Name → Lean.Expr → Lean.Expr → optParam Bool false → optParam Bool true → optParam Bool true → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.coeff_iterate_derivative : ∀ {R : Type u} [inst : Semiring R] {k : ℕ} (p : Polynomial R) (m : ℕ),
  ((⇑Polynomial.derivative)^[k] p).coeff m = (m + k).descFactorial k • p.coeff (m + k)
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.reindexFinsetRange_apply : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) [inst_3 : Fintype ι] [inst_4 : DecidableEq M] (x : ↥(Finset.image (⇑b) Finset.univ)),
  b.reindexFinsetRange x = ↑x
-- Mathlib.Condensed.Discrete.Colimit
/-- `isColimitLocallyConstantPresheaf` in the case of `S.asLimit`.  -/
LightCondensed.isColimitLocallyConstantPresheafDiagram : (X : Type u) →
  (S : LightProfinite) →
    CategoryTheory.Limits.IsColimit
      ((LightCondensed.locallyConstantPresheaf X).mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.FinMeasAdditive.smul_measure_iff : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} {T : Set α → β}
  [inst : AddMonoid β] (c : ENNReal),
  c ≠ 0 → c ≠ ⊤ → (MeasureTheory.FinMeasAdditive (c • μ) T ↔ MeasureTheory.FinMeasAdditive μ T)
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.instPerfectField : ∀ (K : Type u) [inst : Field K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p],
  PerfectField (PerfectClosure K p)
-- Mathlib.Topology.Algebra.Monoid
Specializes.pow : ∀ {M : Type u_6} [inst : Monoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M] {a b : M},
  a ⤳ b → ∀ (n : ℕ), (a ^ n) ⤳ (b ^ n)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitesimal_inv_of_infinite : ∀ {x : ℝ*}, x.Infinite → x⁻¹.Infinitesimal
-- Mathlib.RingTheory.Bialgebra.Equiv
/-- Reinterpret an element of a type of bialgebra equivalences as a bialgebra equivalence.  -/
BialgEquivClass.toBialgEquiv : {F : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Semiring B] →
              [inst_3 : Algebra R A] →
                [inst_4 : Algebra R B] →
                  [inst_5 : CoalgebraStruct R A] →
                    [inst_6 : CoalgebraStruct R B] →
                      [inst_7 : EquivLike F A B] → [BialgEquivClass F R A B] → F → A ≃ₐc[R] B
-- Mathlib.CategoryTheory.Category.TwoP
/-- The functor from `Pointed` to `TwoP` which adds a first point.  -/
pointedToTwoPSnd : CategoryTheory.Functor Pointed TwoP
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.constantsOn.eq_1 : ∀ (α : Type u'),
  FirstOrder.Language.constantsOn α =
    { Functions := FirstOrder.Language.constantsOnFunc α, Relations := fun x => Empty }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- the pushout cocone is a colimit  -/
CategoryTheory.BicartesianSq.isColimit' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z} (self : CategoryTheory.BicartesianSq f g h i),
  Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk h i ⋯))
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_3 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w : ℕ) (lhsExpr : Std.Tactic.BVDecide.BVExpr w)
  (op : Std.Tactic.BVDecide.BVBinOp) (rhsExpr : Std.Tactic.BVDecide.BVExpr w)
  (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, lhsExpr.bin op rhsExpr with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_1 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_3 w lhsExpr op rhsExpr
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
/-- A multivariate polynomial is `Monic` with respect to a monomial order
if its leading coefficient (for that monomial order) is 1.  -/
MonomialOrder.Monic : {σ : Type u_1} → MonomialOrder σ → {R : Type u_2} → [inst : CommSemiring R] → MvPolynomial σ R → Prop
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitEpi.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} [inst_1 : SizeOf C] (section_ : Y ⟶ X)
  (id :
    autoParam (CategoryTheory.CategoryStruct.comp section_ f = CategoryTheory.CategoryStruct.id Y)
      CategoryTheory.SplitEpi.id._autoParam),
  sizeOf { section_ := section_, id := id } = 1 + sizeOf section_ + sizeOf id
-- Mathlib.Algebra.Star.StarRingHom
/-- `NonUnitalStarRingHomClass F A B` states that `F` is a type of non-unital ⋆-ring homomorphisms.
You should also extend this typeclass when you extend `NonUnitalStarRingHom`.  -/
NonUnitalStarRingHomClass : (F : Type u_1) →
  (A : outParam (Type u_2)) →
    (B : outParam (Type u_3)) →
      [inst : NonUnitalNonAssocSemiring A] →
        [Star A] →
          [inst_2 : NonUnitalNonAssocSemiring B] →
            [Star B] → [inst_4 : FunLike F A B] → [NonUnitalRingHomClass F A B] → Prop
-- Init.Data.List.MapIdx
List.mapIdx_nil : ∀ {α : Type u_1} {β : Type u_2} {f : ℕ → α → β}, List.mapIdx f [] = []
-- Mathlib.Algebra.ContinuedFractions.Translations
_private.Mathlib.Algebra.ContinuedFractions.Translations.0.GenContFract.contsAux.match_1.eq_2 : ∀ {K : Type u_1} (motive : Option (GenContFract.Pair K) → Sort u_2) (gp : GenContFract.Pair K)
  (h_1 : Unit → motive none) (h_2 : (gp : GenContFract.Pair K) → motive (some gp)),
  (match some gp with
    | none => h_1 ()
    | some gp => h_2 gp) =
    h_2 gp
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.mul_const_eq : ∀ {α : Type u_1} {b c : α} [inst : Mul α], b = c → ∀ (a : α), a * b = a * c
-- Init.Data.Int.Order
Int.min_eq_right : ∀ {a b : ℤ}, b ≤ a → min a b = b
-- Mathlib.Algebra.Algebra.Defs
Algebra.commute_algebraMap_right : ∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R) (x : A),
  Commute x ((algebraMap R A) r)
-- Mathlib.Analysis.Real.Sqrt
Real.abs_le_sqrt : ∀ {x y : ℝ}, x ^ 2 ≤ y → |x| ≤ √y
-- Mathlib.Algebra.Group.Commute.Basic
pow_inv_comm : ∀ {G : Type u_1} [inst : Group G] (a : G) (m n : ℕ), a⁻¹ ^ m * a ^ n = a ^ n * a⁻¹ ^ m
-- Mathlib.Algebra.IsPrimePow
/-- `n` is a prime power if there is a prime `p` and a positive natural `k` such that `n` can be
written as `p^k`.  -/
IsPrimePow : {R : Type u_1} → [CommMonoidWithZero R] → R → Prop
-- Mathlib.Data.Finset.Lattice.Fold
Finset.apply_sup'_eq_sup'_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup γ] {s : Finset β}
  (H : s.Nonempty) {f : β → α} (g : α → γ), (∀ (x y : α), g (x ⊔ y) = g x ⊔ g y) → g (s.sup' H f) = s.sup' H (g ∘ f)
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.relations.Winv₁ : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (w : X ⟶ Y) (hw : W w),
  CategoryTheory.Localization.Construction.relations W
    (CategoryTheory.CategoryStruct.comp (CategoryTheory.Localization.Construction.ψ₁ W w)
      (CategoryTheory.Localization.Construction.ψ₂ W w hw))
    (CategoryTheory.CategoryStruct.id (CategoryTheory.Localization.Construction.ιPaths W X))
-- Mathlib.Data.FunLike.Group
FunLike.coeMulHom.eq_1 : ∀ (F : Type u_1) (α : Type u_2) (β : Type u_3) [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : Mul β]
  [inst_3 : IsMulApply F α β], FunLike.coeMulHom F α β = { toFun := fun f => ⇑f, map_mul' := ⋯ }
-- Mathlib.Tactic.ErwQuestion
/-- Checks that the input `Expr` represents a proof produced by `(e)rw` and returns the types of the
LHS of the equality being written (one from the target, the other from the lemma used).
These will be defeq, but not necessarily reducibly so.
 -/
Mathlib.Tactic.Erw?.extractRewriteEq : Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Lean.Environment
/-- The main branch that initiated adding a declaration, i.e. `AddConstAsyncResult.mainEnv`.

This is the more common case and true for e.g. all accesses from attributes.
 -/
Lean.AsyncBranch.mainEnv : Lean.AsyncBranch
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.uset.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId} {i : ℕ} {y : Lean.FVarId} {k : Lean.Compiler.LCNF.Code pu}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_9} {fvarId_1 : Lean.FVarId}
  {i_1 : ℕ} {y_1 : Lean.FVarId} {k_1 : Lean.Compiler.LCNF.Code pu}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_9},
  Lean.Compiler.LCNF.Code.uset fvarId i y k h = Lean.Compiler.LCNF.Code.uset fvarId_1 i_1 y_1 k_1 h_1 →
    fvarId = fvarId_1 ∧ i = i_1 ∧ y = y_1 ∧ k = k_1
-- Mathlib.Data.Finset.Max
Finset.ofDual_min' : ∀ {α : Type u_2} [inst : LinearOrder α] {s : Finset αᵒᵈ} (hs : s.Nonempty),
  OrderDual.ofDual (s.min' hs) = (Finset.image (⇑OrderDual.ofDual) s).max' ⋯
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
Valued.cauchy_iff : ∀ {R : Type u} [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀]
  {F : Filter R},
  Cauchy F ↔
    F.NeBot ∧
      ∀ (γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ),
        ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, Valued.v.restrict (y - x) < ↑γ
-- Std.Data.Internal.List.Associative
Std.Internal.List.pairwise_fst_eq_false_map_toProd : ∀ {α : Type u} [inst : BEq α] {β : Type v} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    List.Pairwise (fun a b => (a.1 == b.1) = false) (List.map (fun x => (x.fst, x.snd)) l)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- The **lower Lebesgue integral** of a function `f` with respect to a measure `μ`.  -/
MeasureTheory.«term∫⁻_,_∂_» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.isRightDerivedFunctor_iff_of_iso : ∀ {C : Type u_1} {D : Type u_3} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  {RF RF' : CategoryTheory.Functor D H} {F : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : F ⟶ L.comp RF) (α' : F ⟶ L.comp RF') (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  (e : RF ≅ RF'),
  CategoryTheory.CategoryStruct.comp α (L.whiskerLeft e.hom) = α' →
    (RF.IsRightDerivedFunctor α W ↔ RF'.IsRightDerivedFunctor α' W)
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- Constructor for natural transformations between functors from `V.HomotopyCategory`.  -/
SSet.Truncated.HomotopyCategory.mkNatTrans : {V : SSet.Truncated 2} →
  {D : Type u_1} →
    [inst : CategoryTheory.Category.{v_1, u_1} D] →
      {F G : CategoryTheory.Functor V.HomotopyCategory D} →
        (φ :
            (x : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })) →
              F.obj (SSet.Truncated.HomotopyCategory.mk x) ⟶ G.obj (SSet.Truncated.HomotopyCategory.mk x)) →
          autoParam
              (∀ ⦃x y : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })⦄
                (e : SSet.Truncated.Edge x y),
                CategoryTheory.CategoryStruct.comp (F.map (SSet.Truncated.HomotopyCategory.homMk e)) (φ y) =
                  CategoryTheory.CategoryStruct.comp (φ x) (G.map (SSet.Truncated.HomotopyCategory.homMk e)))
              _auto_135✝ →
            (F ⟶ G)
-- Batteries.Data.Fin.Coding
/-- Decode `Bool` from `Fin 2`.  -/
Fin.decodeBool : Fin 2 → Bool
-- Init.System.IO
/-- Flushes the output buffer associated with the handle, writing any unwritten data to the associated
output device.
 -/
IO.FS.Handle.flush : IO.FS.Handle → IO Unit
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- The disjoint union of two `C^n` manifolds modelled on `(E, H)`
is a `C^n` manifold modelled on `(E, H)`.  -/
IsManifold.disjointUnion : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {M : Type u_4} [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {M' : Type u_5}
  [inst_6 : TopologicalSpace M'] [inst_7 : ChartedSpace H M'] [hM : IsManifold I n M] [hM' : IsManifold I n M'],
  IsManifold I n (M ⊕ M')
-- Mathlib.Data.List.DropRight
List.rdropWhile_singleton : ∀ {α : Type u_1} (p : α → Bool) (x : α), List.rdropWhile p [x] = if p x = true then [] else [x]
-- Mathlib.Topology.Constructions.SumProd
/-- Continuous functions on products are continuous in their first argument  -/
Continuous.curry_left : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X × Y → Z}, Continuous f → ∀ {y : Y}, Continuous fun x => f (x, y)
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.mkBEqCached.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.BinaryInput),
  aig.mkBEqCached input =
    ((aig.mkGateCached (input.invert false true)).aig.mkGateCached ((input.cast ⋯).invert true false)).aig.mkGateCached
      { lhs := ((aig.mkGateCached (input.invert false true)).ref.cast ⋯).not,
        rhs :=
          ((aig.mkGateCached (input.invert false true)).aig.mkGateCached ((input.cast ⋯).invert true false)).ref.not }
-- Mathlib.Order.Filter.Pointwise
Filter.neBot_neg_iff : ∀ {α : Type u_2} [inst : Neg α] {f : Filter α}, (-f).NeBot ↔ f.NeBot
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.forIn'_eq_forIn'_toIterM : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type w → Type w''} [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] {γ : Type w} {it : Std.Iter β} {init : γ}
  {f : (out : β) → out ∈ it → γ → m (ForInStep γ)},
  forIn' it init f = forIn' it.toIterM init fun out h acc => f out ⋯ acc
-- Lean.Compiler.IR.Format
Lean.IR.formatAlt : (Lean.IR.FnBody → Std.Format) → ℕ → Lean.IR.Alt → Std.Format
-- Lean.Setup
/-- Load a `ModuleSetup` from a JSON file.  -/
Lean.ModuleSetup.load : System.FilePath → IO Lean.ModuleSetup