mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_symm_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))}
  (a : { a // ↑(NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet a) ∈ ↑↑J }),
  ↑((NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv K J).symm a) = ↑↑a
-- Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic
SimpleGraph.UnitDistEmbedding.bot_p : ∀ {V : Type u_1} {E : Type u_3} [inst : MetricSpace E] (p : V ↪ E), (SimpleGraph.UnitDistEmbedding.bot p).p = p
-- Mathlib.Algebra.Order.Ring.Canonical
tsub_mul : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R] [inst_3 : Sub R]
  [OrderedSub R] [Std.Total fun x1 x2 => x1 ≤ x2] [AddLeftReflectLE R] [MulRightMono R] (a b c : R),
  (a - b) * c = a * c - b * c
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.aroots_X_sub_C : ∀ {S : Type v} {T : Type w} [inst : CommRing T] [inst_1 : CommRing S] [inst_2 : IsDomain S] [inst_3 : Algebra T S]
  (r : T), (Polynomial.X - Polynomial.C r).aroots S = {(algebraMap T S) r}
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylor_pow : ∀ {R : Type u_1} [inst : CommSemiring R] (r : R) (f : Polynomial R) (n : ℕ),
  (Polynomial.taylor r) (f ^ n) = (Polynomial.taylor r) f ^ n
-- Mathlib.Geometry.Manifold.Algebra.Monoid
ContMDiff.nsmul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3} [inst_1 : TopologicalSpace H]
  {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_5}
  [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G]
  {E' : Type u_6} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7}
  [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_8} [inst_11 : TopologicalSpace M]
  [inst_12 : ChartedSpace H' M] {g : M → G}, ContMDiff I' I n g → ∀ (m : ℕ), ContMDiff I' I n fun x => m • g x
-- Init.Data.List.Lemmas
List.flatten_eq_singleton_iff : ∀ {α : Type u_1} {xs : List (List α)} {y : α},
  xs.flatten = [y] ↔ ∃ as bs, xs = as ++ [y] :: bs ∧ (∀ l ∈ as, l = []) ∧ ∀ l ∈ bs, l = []
-- Mathlib.Analysis.SpecificLimits.Basic
tsum_geometric_inv_two : ∑' (n : ℕ), 2⁻¹ ^ n = 2
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_max! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {hc : t.max! ∈ t}, t.get t.max! hc = t.max!
-- Mathlib.LinearAlgebra.GeneralLinearGroup.Basic
LinearMap.GeneralLinearGroup.toLinearEquiv_inv : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : LinearMap.GeneralLinearGroup R M), f⁻¹.toLinearEquiv = f.toLinearEquiv⁻¹
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.zero_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x y : M),
  (0 x) y = 0
-- Init.Data.Int.Gcd
Int.gcd_le_natAbs_left : ∀ {a : ℤ} (b : ℤ), a ≠ 0 → a.gcd b ≤ a.natAbs
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.instConcreteCategoryRingHomCarrier : CategoryTheory.ConcreteCategory RingCat fun R S => ↑R →+* ↑S
-- Init.Prelude
/-- The `BitVec` with value `i`, given a proof that `i < 2^w`.  -/
BitVec.ofNatLT : {w : ℕ} → (i : ℕ) → i < 2 ^ w → BitVec w
-- Init.Data.Vector.Attach
Vector.pmap_map : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} {n : ℕ} {p : β → Prop} {g : (b : β) → p b → γ} {f : α → β}
  {xs : Vector α n} (H : ∀ a ∈ Vector.map f xs, p a),
  Vector.pmap g (Vector.map f xs) H = Vector.pmap (fun a h => g (f a) h) xs ⋯
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitInfo.imp.inj : ∀ {e : Lean.Expr} {h : e.isForall = true} {source : Lean.Meta.Grind.SplitSource} {e_1 : Lean.Expr}
  {h_1 : e_1.isForall = true} {source_1 : Lean.Meta.Grind.SplitSource},
  Lean.Meta.Grind.SplitInfo.imp e h source = Lean.Meta.Grind.SplitInfo.imp e_1 h_1 source_1 →
    e = e_1 ∧ source = source_1
-- Mathlib.Order.SuccPred.Basic
/-- A constructor for `SuccOrder α` for `α` a linear order.  -/
SuccOrder.ofCore : {α : Type u_1} →
  [inst : LinearOrder α] →
    (succ : α → α) →
      (∀ {a : α}, ¬IsMax a → ∀ (b : α), a < b ↔ succ a ≤ b) → (∀ (a : α), IsMax a → succ a = a) → SuccOrder α
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.isOrthogonal_symm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i j : ι),
  P.IsOrthogonal i j ↔ P.IsOrthogonal j i
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.SheafedSpace.GlueData.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (toGlueData : CategoryTheory.GlueData (AlgebraicGeometry.SheafedSpace C))
  (f_open : ∀ (i j : toGlueData.J), AlgebraicGeometry.SheafedSpace.IsOpenImmersion (toGlueData.f i j))
  (toGlueData_1 : CategoryTheory.GlueData (AlgebraicGeometry.SheafedSpace C))
  (f_open_1 : ∀ (i j : toGlueData_1.J), AlgebraicGeometry.SheafedSpace.IsOpenImmersion (toGlueData_1.f i j)),
  ({ toGlueData := toGlueData, f_open := f_open } = { toGlueData := toGlueData_1, f_open := f_open_1 }) =
    (toGlueData = toGlueData_1)
-- Mathlib.MeasureTheory.Measure.Prokhorov
/-- **Alias** of `isCompact_setOfPred_finiteMeasure_le_of_compactSpace`.

---

In a compact space, the set of finite measures with mass at most `C` is compact.  -/
isCompact_setOf_finiteMeasure_le_of_compactSpace : ∀ (E : Type u_1) [inst : MeasurableSpace E] [inst_1 : TopologicalSpace E] [T2Space E] [inst_3 : BorelSpace E]
  [CompactSpace E] (C : NNReal), IsCompact {μ | μ.mass ≤ C}
-- Init.Data.Nat.Div.Basic
Nat.div_eq_of_eq_mul_right : ∀ {n m k : ℕ}, 0 < n → m = n * k → m / n = k
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.norm_nonzero_of_not_equiv_zero : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {f : PadicSeq p}, ¬f ≈ 0 → f.norm ≠ 0
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
LinearIsometryEquiv.toLinearEquiv_rTensor : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f : E ≃ₗᵢ[𝕜] F),
  (LinearIsometryEquiv.rTensor G f).toLinearEquiv = LinearEquiv.rTensor G f.toLinearEquiv
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Node.brecOn.eq : ∀ {α : Type u} {β : Type v} {motive_1 : Lean.PersistentHashMap.Node α β → Sort u_1}
  {motive_2 : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Sort u_1}
  {motive_3 : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) → Sort u_1}
  {motive_4 : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β) → Sort u_1}
  (t : Lean.PersistentHashMap.Node α β) (F_1 : (t : Lean.PersistentHashMap.Node α β) → t.below → motive_1 t)
  (F_2 :
    (t : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
      Lean.PersistentHashMap.Node.below_1 t → motive_2 t)
  (F_3 :
    (t : List (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
      Lean.PersistentHashMap.Node.below_2 t → motive_3 t)
  (F_4 :
    (t : Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) →
      Lean.PersistentHashMap.Node.below_3 t → motive_4 t),
  t.brecOn F_1 F_2 F_3 F_4 = F_1 t (Lean.PersistentHashMap.Node.brecOn.go t F_1 F_2 F_3 F_4).2
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f * g) x = f x * g x` is a left cancel semigroup if `β` is a
left cancel semigroup.  -/
FunLike.leftCancelSemigroup : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Mul F] → [inst_2 : LeftCancelSemigroup β] → [IsMulApply F α β] → LeftCancelSemigroup F
-- Mathlib.Algebra.Order.Archimedean.Basic
/-- Every x greater than or equal to 1 is between two successive
natural-number powers of every y greater than one.  -/
exists_nat_pow_near : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [Archimedean R] [ExistsAddOfLE R]
  {x y : R}, 1 ≤ x → 1 < y → ∃ n, y ^ n ≤ x ∧ x < y ^ (n + 1)
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.forget_createsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J GrpCat) → CategoryTheory.CreatesLimit F (CategoryTheory.forget GrpCat)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.coeFnAddMonoidHom.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddZeroClass Y],
  LocallyConstant.coeFnAddMonoidHom = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.summable_weierstrassPSummand : ∀ (L : PeriodPair) (z x : ℂ),
  (∀ (l : ↥L.lattice), ‖z - x‖ < ‖↑l - x‖) →
    Summable (Function.uncurry fun b c => L.weierstrassPSummand x b c * (z - x) ^ b)
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
Manifold.LiftSourceTargetPropertyAt.domChart_mem_maximalAtlas : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop}
  (h : Manifold.LiftSourceTargetPropertyAt I J n f x P), h.domChart ∈ IsManifold.maximalAtlas I n M
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The natural isomorphism arising from `mapForget_eq`.  -/
CategoryTheory.Over.mapForget : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X Y : T} →
      (f : X ⟶ Y) → (CategoryTheory.Over.map f).comp (CategoryTheory.Over.forget Y) ≅ CategoryTheory.Over.forget X
-- Mathlib.Order.Filter.Map
Filter.mem_comap_iff : ∀ {α : Type u_1} {β : Type u_2} {f : Filter β} {m : α → β},
  Function.Injective m → Set.range m ∈ f → ∀ {S : Set α}, S ∈ Filter.comap m f ↔ m '' S ∈ f
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
_private.Mathlib.Algebra.ContinuedFractions.Computation.Basic.0.GenContFract.IntFractPair.stream.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cyclesIso_hom_i_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cyclesIso_hom_i._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cyclesIso_hom_i._auto_3) {Z : C}
  (h : (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₂) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).hom
      (CategoryTheory.CategoryStruct.comp (X.iCycles f₁ f₂ n₁) h) =
    CategoryTheory.CategoryStruct.comp (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).iCycles h
-- Mathlib.NumberTheory.GaussSum
/-- Replacing `ψ` by `mulShift ψ a` and multiplying the Gauss sum by `χ a` does not change it.  -/
gaussSum_mulShift : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] (χ : MulChar R R')
  (ψ : AddChar R R') (a : Rˣ), χ ↑a * gaussSum χ (ψ.mulShift ↑a) = gaussSum χ ψ
-- Aesop.Tree.RunMetaM
Aesop.Rapp.runMetaMModifyingParentState : {m : Type → Type} → [Monad m] → [MonadLiftT Lean.MetaM m] → [MonadFinally m] → {α : Type} → m α → Aesop.Rapp → m α
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.empty_mul : ∀ {α : Type u_2} [inst : Mul α] {s : Set α}, ∅ * s = ∅
-- Init.Data.Nat.Lemmas
Nat.add_mod_mod : ∀ (m n k : ℕ), (m + n % k) % k = (m + n) % k
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- If x is in `pinGroup Q`, then `(ι Q).range` is closed under twisted conjugation. The reverse
statement presumably being true only in finite dimensions.  -/
pinGroup.conjAct_smul_range_ι : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ},
  ↑x ∈ pinGroup Q → ∀ [Invertible 2], ConjAct.toConjAct x • (CliffordAlgebra.ι Q).range = (CliffordAlgebra.ι Q).range
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_erase_eq_sub : ∀ {ι : Type u_1} {G : Type u_3} {s : Finset ι} [inst : AddCommGroup G] [inst_1 : DecidableEq ι] {f : ι → G} {a : ι},
  a ∈ s → ∑ x ∈ s.erase a, f x = ∑ x ∈ s, f x - f a
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} {α β : F ⟶ G} (h : α = β),
  CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq h =
    CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq h
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.posPart.eq_1 : ∀ {α : Type u_1} {E : Type u_2} [inst : LinearOrder E] [inst_1 : Zero E] [inst_2 : MeasurableSpace α]
  (f : MeasureTheory.SimpleFunc α E), f.posPart = MeasureTheory.SimpleFunc.map (fun b => max b 0) f
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Suggest merging two adjacent `rw` tactics if that also solves the goal.  -/
Mathlib.TacticAnalysis.rwMerge : Mathlib.TacticAnalysis.Config
-- Mathlib.Data.Finsupp.ToDFinsupp
finsuppEquivDFinsupp_apply : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero M] [inst_2 : (m : M) → Decidable (m ≠ 0)],
  ⇑finsuppEquivDFinsupp = Finsupp.toDFinsupp
-- Mathlib.Order.Category.BddDistLat
BddDistLat.dual_map : ∀ {X Y : BddDistLat} (f : X ⟶ Y),
  BddDistLat.dual.map f = BddDistLat.ofHom (BoundedLatticeHom.dual (BddDistLat.Hom.hom f))
-- Init.Data.BitVec.Lemmas
/-- Sign extending to a width smaller than the starting width is a truncation.  -/
BitVec.signExtend_eq_setWidth_of_le : ∀ {w : ℕ} (x : BitVec w) {v : ℕ}, v ≤ w → BitVec.signExtend v x = BitVec.setWidth v x
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.coe_center : ∀ (R : Type u) [inst : NonAssocRing R], ↑(Subring.center R) = Set.center R
-- Std.Data.HashMap.RawLemmas
/-- Variant of `getElem!_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.HashMap.Raw.getElem!_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] [inst_4 : Inhabited γ] {f : α → β → γ} {k : α} (h : m.WF),
  (Std.HashMap.Raw.map f m)[k]! = (Option.pmap (fun v h => f (m.getKey k h) v) m[k]? ⋯).get!
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.namespaceId.injEq : ∀ (stx stx_1 : Lean.Syntax),
  (Lean.Elab.CompletionInfo.namespaceId stx = Lean.Elab.CompletionInfo.namespaceId stx_1) = (stx = stx_1)
-- Mathlib.Combinatorics.Hypergraph.Basic
/-- The edge set  -/
Hypergraph.edgeSet : {α : Type u_4} → Hypergraph α → Set (Set α)
-- Mathlib.Combinatorics.Quiver.SingleObj
/-- Type tag on `Unit` used to define single-object quivers.  -/
Quiver.SingleObj : Type u_1 → Type
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.insertMany!_empty_list_nil : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α},
  ↑(Std.DTreeMap.Internal.Impl.empty.insertMany! []) = Std.DTreeMap.Internal.Impl.empty
-- Mathlib.Data.Finset.Image
Finset.mem_map_equiv : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {f : α ≃ β} {b : β}, b ∈ Finset.map f.toEmbedding s ↔ f.symm b ∈ s
-- Mathlib.Tactic.Convert
_private.Mathlib.Tactic.Convert.0.instEvalExprExpensiveConfig.evalExpr : Lean.Expr → Lean.MetaM Convert.ExpensiveConfig
-- Mathlib.Control.Monad.Cont
LawfulMonadCont.toLawfulMonad : ∀ {m : Type u → Type v} {inst : Monad m} {inst_1 : MonadCont m} [self : LawfulMonadCont m], LawfulMonad m
-- Mathlib.Analysis.Asymptotics.AsymptoticEquivalent
Asymptotics.transIsEquivalentIsEquivalent : {α : Type u_1} →
  {β : Type u_2} →
    [inst : NormedAddCommGroup β] →
      {l : Filter α} → Trans (Asymptotics.IsEquivalent l) (Asymptotics.IsEquivalent l) (Asymptotics.IsEquivalent l)
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.coe_toHomeomorph_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n),
  ⇑h.toHomeomorph.symm = ⇑h.symm
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
/-- `cofan₁` is colimit  -/
HomotopicalAlgebra.AttachCells.isColimit₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type t} →
      {A B : α → C} →
        {g : (a : α) → A a ⟶ B a} →
          {X₁ X₂ : C} →
            {f : X₁ ⟶ X₂} → (self : HomotopicalAlgebra.AttachCells g f) → CategoryTheory.Limits.IsColimit self.cofan₁
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
/-- Auxiliary definition for `ofCocone`.  -/
CategoryTheory.SmallObject.SuccStruct.ofCocone.objIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u} →
      [inst_1 : LinearOrder J] →
        {j : J} →
          {F : CategoryTheory.Functor (↑(Set.Iio j)) C} →
            (c : CategoryTheory.Limits.Cocone F) →
              (i : J) → (hi : i < j) → CategoryTheory.SmallObject.SuccStruct.ofCocone.obj c i ≅ F.obj ⟨i, hi⟩
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_re_zero_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), RCLike.re (inner 𝕜 x 0) = 0
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.rename_toMvPowerSeries : ∀ {R : Type u_1} {σ : Type u_2} {τ : Type u_3} [inst : CommSemiring R] (f : σ → τ) [inst_1 : Filter.TendstoCofinite f]
  (a : σ) (p : PowerSeries R),
  (MvPowerSeries.rename f) ((PowerSeries.toMvPowerSeries a) p) = (PowerSeries.toMvPowerSeries (f a)) p
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.Indep.of_delete : ∀ {α : Type u_1} {M : Matroid α} {I D : Set α}, (M.delete D).Indep I → M.Indep I
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Construct a morphism between whiskered extensions.  -/
CategoryTheory.Bicategory.LeftExtension.whiskerHom : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          {s t : CategoryTheory.Bicategory.LeftExtension f g} →
            (s ⟶ t) → {x : B} → (h : c ⟶ x) → s.whisker h ⟶ t.whisker h
-- Mathlib.Data.Finset.Lattice.Lemmas
Finset.inter_insert_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {s₁ s₂ : Finset α} {a : α}, a ∉ s₁ → s₁ ∩ insert a s₂ = s₁ ∩ s₂
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
IntermediateField.isSplittingField_iff : ∀ {K : Type v} {L : Type w} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {p : Polynomial K}
  {F : IntermediateField K L},
  Polynomial.IsSplittingField K (↥F) p ↔
    (Polynomial.map (algebraMap K ↥F) p).Splits ∧ F = IntermediateField.adjoin K (p.rootSet L)
-- Mathlib.Logic.Embedding.Basic
Equiv.refl_toEmbedding : ∀ {α : Type u_1}, (Equiv.refl α).toEmbedding = Function.Embedding.refl α
-- Mathlib.Algebra.Order.Group.Synonym
isRightRegular_toLex : ∀ {α : Type u_1} [inst : Monoid α] {a : α}, IsRightRegular (toLex a) ↔ IsRightRegular a
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
/-- The inverse trivialization of the tangent space can be expressed in terms of the tangent bundle
core. To write it as the manifold derivative of `(extChartAt I b₀).symm`, see
`TangentBundle.symmL_trivializationAt`.

Use with care as it abuses the defeq `TangentSpace I b = E`.  -/
TangentBundle.symmL_trivializationAt_eq_core : ∀ {𝕜 : 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] {b₀ b : M},
  b ∈ (chartAt H b₀).source →
    Bundle.Trivialization.symmL 𝕜 (trivializationAt E (TangentSpace I) b₀) b =
      (tangentBundleCore I M).coordChange (achart H b₀) (achart H b) b
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.instReprError.repr : Std.Internal.Parsec.Error → ℕ → Std.Format
-- Lean.Meta.Tactic.Rfl
/-- Environment extensions for `refl` lemmas  -/
Lean.Meta.Rfl.reflExt : Lean.SimpleScopedEnvExtension (Lean.Name × Array Lean.Meta.DiscrTree.Key) (Lean.Meta.DiscrTree Lean.Name)
-- Mathlib.SetTheory.Ordinal.Exponential
/-- `0 ^ a = 1` if `a = 0` and `0 ^ a = 0` otherwise.  -/
Ordinal.zero_opow' : ∀ (a : Ordinal.{u_1}), 0 ^ a = 1 - a
-- Init.Data.Fin.Basic
/-- Replaces a value with its difference from the largest value in the type.

Considering the values of `Fin n` as a sequence `0`, `1`, …, `n-2`, `n-1`, `Fin.rev` finds the
corresponding element of the reversed sequence. In other words, it maps `0` to `n-1`, `1` to `n-2`,
..., and `n-1` to `0`.

Examples:
 * `(5 : Fin 6).rev = (0 : Fin 6)`
 * `(0 : Fin 6).rev = (5 : Fin 6)`
 * `(2 : Fin 5).rev = (2 : Fin 5)`
 -/
Fin.rev : {n : ℕ} → Fin n → Fin n
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.functor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i)
  [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 :
    ∀ {X S : C} (πX : X ⟶ S),
      CategoryTheory.Limits.HasColimitsOfShape
        (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C]
  {π₁ π₂ : CategoryTheory.Arrow C} (τ : π₁ ⟶ π₂),
  (CategoryTheory.SmallObject.functor f).map τ =
    CategoryTheory.Arrow.homMk (CategoryTheory.SmallObject.functorMap f τ) (CategoryTheory.Arrow.Hom.right τ) ⋯
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.mem_functorPushforward_iff_of_full_of_faithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] {X Y : C} (R : CategoryTheory.Sieve X) (f : Y ⟶ X),
  CategoryTheory.Presieve.functorPushforward F R.arrows (F.map f) ↔ R.arrows f
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.isPreconnected_Icc : ∀ {α : Type u_1} [inst : TopologicalSpace α] {K L : TopologicalSpace.NonemptyCompacts α},
  IsPreconnected ↑L → IsPreconnected (Set.Icc K L)
-- Std.Http.Data.URI.Basic
Std.Http.URI.instInhabitedBuilder : Inhabited Std.Http.URI.Builder
-- Mathlib.Data.Prod.Basic
Function.Bijective.prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ},
  Function.Bijective f → Function.Bijective g → Function.Bijective (Prod.map f g)
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
IsTranscendenceBasis.of_isAlgebraic_adjoin_image_compl : ∀ {ι : Type u} {R : Type u_1} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [FaithfulSMul R S] [NoZeroDivisors S] (i j : ι) (v : ι → S),
  (IsTranscendenceBasis R fun x => v ↑x) →
    IsAlgebraic (↥(Algebra.adjoin R (v '' {j}ᶜ))) (v j) → IsTranscendenceBasis R fun x => v ↑x