mathlib-initiative/mathlib-types huggingface dataset:
-- Plausible.Sampleable
/-- `#sample type`, where `type` has an instance of `SampleableExt`, prints ten random
values of type `type` using an increasing size parameter.

```lean
#sample Nat
-- prints
-- 0
-- 0
-- 2
-- 24
-- 64
-- 76
-- 5
-- 132
-- 8
-- 449
-- or some other sequence of numbers

#sample List Int
-- prints
-- []
-- [1, 1]
-- [-7, 9, -6]
-- [36]
-- [-500, 105, 260]
-- [-290]
-- [17, 156]
-- [-2364, -7599, 661, -2411, -3576, 5517, -3823, -968]
-- [-643]
-- [11892, 16329, -15095, -15461]
-- or whatever
```
 -/
Plausible.«command#sample_» : Lean.ParserDescr
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.mulSingle_one : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → One (M i)] [inst_1 : DecidableEq ι] (i : ι), Pi.mulSingle i 1 = 1
-- Mathlib.Analysis.Calculus.Deriv.Inv
deriv_inv'' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'}, DifferentiableAt 𝕜 c x → c x ≠ 0 → deriv c⁻¹ x = -deriv c x / c x ^ 2
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {fallback : β}, k ∉ m₂ → (m₁ \ m₂).getD k fallback = m₁.getD k fallback
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.mk.injEq : ∀ {α : Type} (tries : Array (Lean.Meta.LazyDiscrTree.Trie α))
  (roots : Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex)
  (tries_1 : Array (Lean.Meta.LazyDiscrTree.Trie α))
  (roots_1 : Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex),
  ({ tries := tries, roots := roots } = { tries := tries_1, roots := roots_1 }) = (tries = tries_1 ∧ roots = roots_1)
-- Init.Data.BitVec.Lemmas
BitVec.toNat_sshiftRight'_of_msb_false : ∀ {w : ℕ} {x y : BitVec w}, x.msb = false → (x.sshiftRight' y).toNat = x.toNat >>> y.toNat
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.enoughProjectives_of_enoughInjectives_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.EnoughInjectives Cᵒᵖ],
  CategoryTheory.EnoughProjectives C
-- Mathlib.Topology.Order.SuccPred
PredOrder.accPt_principal : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α] [PredOrder α] [NoMinOrder α]
  {a : α} {s : Set α}, AccPt a (Filter.principal s) ↔ ¬IsMax a ∧ ∀ (b : α), a < b → (s ∩ Set.Ioo a b).Nonempty
-- Lean.Data.Lsp.Basic
Lean.Lsp.MarkupKind : Type
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitClosedBall.coe_pow : ∀ {𝕜 : Type u_1} [inst : SeminormedRing 𝕜] [inst_1 : NormOneClass 𝕜] (x : ↑(Metric.closedBall 0 1)) (n : ℕ),
  ↑(x ^ n) = ↑x ^ n
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_isNonloop_iff : ∀ {α : Type u_1} {M : Matroid α} {e : α} {D : Set α}, (M.delete D).IsNonloop e ↔ M.IsNonloop e ∧ e ∉ D
-- Mathlib.Topology.Order
IndiscreteTopology.isClosed_iff : ∀ {α : Type u_1} {t₂ : TopologicalSpace α} [IndiscreteTopology α] (C : Set α), IsClosed C ↔ C = ∅ ∨ C = Set.univ
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.pOpcycles_extendOpcyclesIso_inv_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'}
  (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : (K.extend e).HasHomology j'] {Z : C}
  (h : (K.extend e).opcycles j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.pOpcycles j)
      (CategoryTheory.CategoryStruct.comp (K.extendOpcyclesIso e hj').inv h) =
    CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').inv
      (CategoryTheory.CategoryStruct.comp ((K.extend e).pOpcycles j') h)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
_private.Mathlib.RingTheory.PowerSeries.WeierstrassPreparation.0.PowerSeries.IsWeierstrassDivisorAt.seq.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((k : ℕ) → motive k.succ) → motive x
-- Mathlib.Data.List.TakeDrop
/-- Compared to `drop_take_append_drop`, the order of summands is swapped.  -/
List.drop_take_append_drop' : ∀ {α : Type u} (x : List α) (m n : ℕ), List.take n (List.drop m x) ++ List.drop (n + m) x = List.drop m x
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
/-- A correspondence `f : α → Set β` is lower hemicontinuous if and only if its *lower inverse*
(i.e., `u : Set β ↦ (f ⁻¹' (Iic uᶜ))ᶜ`, note that `f ⁻¹' (Iic u) = {x | (f x ∩ u).Nonempty}`)
sends open sets to open sets.  -/
lowerHemicontinuous_iff_isOpen_compl_preimage_Iic_compl : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} [inst_1 : TopologicalSpace β],
  LowerHemicontinuous f ↔ ∀ (u : Set β), IsOpen u → IsOpen (f ⁻¹' Set.Iic uᶜ)ᶜ
-- Mathlib.LinearAlgebra.Orientation
/-- The value of `Orientation.map` when the index type has cardinality equal to the finite
dimension, in terms of `f.det`.  -/
Orientation.map_eq_det_inv_smul : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : Fintype ι] [FiniteDimensional R M]
  (x : Orientation R M ι) (f : M ≃ₗ[R] M),
  Fintype.card ι = Module.finrank R M → (Orientation.map ι f) x = (LinearEquiv.det f)⁻¹ • x
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- The heterobasic version of `rid` coincides with the regular version.  -/
TensorProduct.AlgebraTensorModule.rid_eq_rid : ∀ (R : Type uR) (M : Type uM) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  TensorProduct.AlgebraTensorModule.rid R R M = TensorProduct.rid R M
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.π_of_isColimit : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {t : CategoryTheory.Limits.Bicone f}
  (ht : CategoryTheory.Limits.IsColimit t.toCocone) (j : J),
  t.π j = ht.desc (CategoryTheory.Limits.Cofan.mk (f j) fun j' => if h : j' = j then CategoryTheory.eqToHom ⋯ else 0)
-- Init.Data.String.Basic
String.Slice.replaceStart : (s : String.Slice) → s.Pos → String.Slice
-- Mathlib.Logic.Unique
/-- If the domain of a surjective function is a subsingleton, then the codomain is a subsingleton as
well.  -/
Function.Surjective.subsingleton : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} [Subsingleton α], Function.Surjective f → Subsingleton β
-- Mathlib.RingTheory.Coprime.Lemmas
/-- **Alias** of the reverse direction of `Nat.isCoprime_iff_coprime`. -/
Nat.Coprime.isCoprime : ∀ {m n : ℕ}, m.Coprime n → IsCoprime ↑m ↑n
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.isEmpty_eq_isEmpty_toIterM : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.IteratorLoop α Id Id] {it : Std.Iter β},
  it.isEmpty = it.toIterM.isEmpty.run.down
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
/-- The free groupoid construction on a category as a functor.  -/
CategoryTheory.Grpd.free : CategoryTheory.Functor CategoryTheory.Cat CategoryTheory.Grpd
-- Mathlib.Logic.Equiv.Basic
/-- If a proposition holds for all elements, then the subtype is
equivalent to the original type.  -/
Equiv.subtypeUnivEquiv : {α : Sort u_9} → {p : α → Prop} → (∀ (x : α), p x) → Subtype p ≃ α
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of `MonoidAlgebra.coeff_mul_single_apply`. -/
MonoidAlgebra.mul_single_apply : ∀ {R : Type u_1} {G : Type u_3} [inst : Semiring R] [inst_1 : Group G] (x : MonoidAlgebra R G) (r : R) (g h : G),
  (x * MonoidAlgebra.single g r).coeff h = x.coeff (h * g⁻¹) * r
-- Mathlib.Analysis.Matrix.Normed
Matrix.linfty_opNorm_diagonal : ∀ {m : Type u_3} {α : Type u_5} [inst : Fintype m] [inst_1 : SeminormedAddCommGroup α] [inst_2 : DecidableEq m]
  (v : m → α), ‖Matrix.diagonal v‖ = ‖v‖
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Functor
/-- The inverse functor used to establish the equivalence `grothendieckPrecompFunctorEquivalence`
between the Grothendieck construction on `CostructuredArrow.functor` and the comma category.  -/
CategoryTheory.CostructuredArrow.commaToGrothendieckPrecompFunctor : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (L : CategoryTheory.Functor C D) →
              (R : CategoryTheory.Functor E D) →
                CategoryTheory.Functor (CategoryTheory.Comma L R)
                  (CategoryTheory.Grothendieck (R.comp (CategoryTheory.CostructuredArrow.functor L)))
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
/-- Eta-expanded form of `MeasureTheory.condExp_zero` -/
MeasureTheory.condExp_fun_zero : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E], μ[fun x => 0 | m] = fun x => 0
-- Mathlib.Data.Finset.PImage
Finset.pimage_empty : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α →. β} [inst_1 : (x : α) → Decidable (f x).Dom],
  Finset.pimage f ∅ = ∅
-- Mathlib.Topology.Neighborhoods
subset_interior_iff_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {s V : Set X}, s ⊆ interior V ↔ ∀ x ∈ s, V ∈ nhds x
-- Mathlib.RingTheory.Localization.BaseChange
/-- The isomorphism `Rₘ ⊗[R] S ≃ₐ[Rₘ] Sₘ`.  -/
Localization.tensorRightAlgEquiv : {R : Type u_10} →
  [inst : CommRing R] →
    (M : Submonoid R) →
      (S : Type u_12) →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            TensorProduct R (Localization M) S ≃ₐ[Localization M] Localization (Algebra.algebraMapSubmonoid S M)
-- Mathlib.Order.WithBot
WithTop.instOrderTop : {α : Type u_1} → [inst : LE α] → OrderTop (WithTop α)
-- Mathlib.Data.Multiset.Defs
Multiset.mem_of_subset : ∀ {α : Type u_1} {s t : Multiset α} {a : α}, s ⊆ t → a ∈ s → a ∈ t
-- Init.Data.UInt.Lemmas
USize.add_eq_right : ∀ {a b : USize}, a + b = b ↔ a = 0
-- Mathlib.Analysis.Normed.Group.Pointwise
ball_one_mul_singleton : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E), Metric.ball 1 δ * {x} = Metric.ball x δ
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.instInhabitedState.default : Lean.Elab.Term.CollectPatternVars.State
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
/-- This lemma states that given some finite set of vertices, of which at least one is in the
support of a given walk, one of them is the first to be encountered. This consequence is encoded
as the set of vertices, restricted to those in the support, except for the first, being empty.
You could interpret this as being `takeUntilSet`, but defining this is slightly involved due to
not knowing what the final vertex is. This could be done by defining a function to obtain the
first encountered vertex and then use that to define `takeUntilSet`. That direction could be
worthwhile if this concept is used more widely.  -/
SimpleGraph.Walk.exists_mem_support_mem_erase_mem_support_takeUntil_eq_empty : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v : V} {p : G.Walk u v} (s : Finset V),
  {x ∈ s | x ∈ p.support}.Nonempty →
    ∃ x ∈ s, ∃ (hx : x ∈ p.support), {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅
-- Mathlib.Tactic.CrossRefAttribute
/-- `traceCrossRefs db verbose` prints the cross-references of database `db` and
inlines the declaration types if `verbose` is `true`.  -/
Mathlib.CrossRef.traceCrossRefs : Mathlib.CrossRef.Database → optParam Bool false → Lean.Elab.Command.CommandElabM Unit
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.subtheoryModel_models : ∀ {L : FirstOrder.Language} {T : L.Theory} (M : T.ModelType) {T' : L.Theory} (h : T' ⊆ T), ↑(M.subtheoryModel h) ⊨ T
-- Mathlib.NumberTheory.LSeries.Nonvanishing
/-- The trivial zero at `s = -2` of the zeta function gives that `F (-2) = 0`.
This is used later to obtain a contradiction.  -/
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.BadChar.F_neg_two : ∀ {N : ℕ} [inst : NeZero N] (B : DirichletCharacter.BadChar✝ N), DirichletCharacter.BadChar.F✝ B ↑(-2) = 0
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
/-- The explicit left homology data of a short complex of modules that is
given by a kernel and a quotient given by the `LinearMap` API. The projections to `K` and `H` are
not simp lemmas because the generic lemmas about `LeftHomologyData` are more useful here.  -/
CategoryTheory.ShortComplex.moduleCatLeftHomologyData : {R : Type u} → [inst : Ring R] → (S : CategoryTheory.ShortComplex (ModuleCat R)) → S.LeftHomologyData
-- Mathlib.Algebra.Group.Graph
AddMonoidHom.graph_toAddSubmonoid : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (f : G →+ H),
  f.graph.toAddSubmonoid = f.mgraph
-- Mathlib.Topology.ContinuousMap.Basic
ContinuousMap.piMap_apply : ∀ {I : Type u_5} {X : I → Type u_7} {Y : I → Type u_8} [inst : (i : I) → TopologicalSpace (X i)]
  [inst_1 : (i : I) → TopologicalSpace (Y i)] (f : (i : I) → C(X i, Y i)) (a : (i : I) → X i) (i : I),
  (ContinuousMap.piMap f) a i = (f i) (a i)
-- Batteries.Data.Nat.Bitwise.Lemmas
Nat.xor_xor_cancel_left : ∀ (x y : ℕ), x ^^^ (x ^^^ y) = y
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.evenKernel_def : ∀ (a x : ℝ),
  ↑(HurwitzZeta.evenKernel (↑a) x) =
    Complex.exp (-↑Real.pi * ↑a ^ 2 * ↑x) * jacobiTheta₂ (↑a * Complex.I * ↑x) (Complex.I * ↑x)
-- Mathlib.Data.List.Rotate
List.IsRotated.reverse : ∀ {α : Type u} {l l' : List α}, l ~r l' → l.reverse ~r l'.reverse
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Real.isPiSystem_Ioo_rat : IsPiSystem (⋃ a, ⋃ b, ⋃ (_ : a < b), {Set.Ioo ↑a ↑b})
-- Lean.Elab.Do.Legacy
/-- Syntax to reference the monad associated with the do notation.  -/
Lean.Elab.Term.Do.ToTerm.Context.m : Lean.Elab.Term.Do.ToTerm.Context → Lean.Syntax
-- Mathlib.RingTheory.MatrixPolynomialAlgebra
Polynomial.eval₂AlgHom.congr_simp : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f f_1 : A →ₐ[R] B) (e_f : f = f_1) (b b_1 : B) (e_b : b = b_1)
  (hf : ∀ (a : A), Commute (f a) b), Polynomial.eval₂AlgHom f b hf = Polynomial.eval₂AlgHom f_1 b_1 ⋯
-- Mathlib.Tactic.GRewrite.Elab
/-- Apply the `grewrite` tactic to a local hypothesis.  -/
_private.Mathlib.Tactic.GRewrite.Elab.0.Mathlib.Tactic.GRewrite.grewriteLocalDecl : Lean.Syntax → Bool → Lean.FVarId → Mathlib.Tactic.GRewrite.Config → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.w_app_assoc : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] {S S' : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X}
  (φ : S ⟶ S') (x : X) {Z : B} (h : G.obj (S'.snd.obj x) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (φ.fst.app x)) (CategoryTheory.CategoryStruct.comp (S'.iso.hom.app x) h) =
    CategoryTheory.CategoryStruct.comp (S.iso.hom.app x) (CategoryTheory.CategoryStruct.comp (G.map (φ.snd.app x)) h)
-- Lean.LibrarySuggestions.Basic
Lean.LibrarySuggestions.librarySuggestionsExt : Lean.SimplePersistentEnvExtension Lean.Name (Option Lean.Name)
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.basisDivisor_self : ∀ {F : Type u_1} [inst : Field F] {x : F}, Lagrange.basisDivisor x x = 0
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Initialize.0.Lean.Meta.RefinedDiscrTree.ImportErrorData.errors : Lean.Meta.RefinedDiscrTree.ImportErrorData✝ → IO.Ref (Array Lean.Meta.RefinedDiscrTree.ImportFailure✝)
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.v_def : ∀ (K : Type u_1) [inst : Field K] {x : RatFunc K},
  Valued.v x = (IsDedekindDomain.HeightOneSpectrum.valuation (RatFunc K) (Polynomial.idealX K)) x
-- Mathlib.Analysis.LocallyConvex.Polar
StrongDual.polar_singleton : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] {E : Type u_5} [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] {a : E}, StrongDual.polar 𝕜 {a} = {x | ‖x a‖ ≤ 1}
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
QuadraticMap.PosDef.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {R₂ : Type u} [inst : CommSemiring R₂] [inst_1 : AddCommMonoid M] [inst_2 : Module R₂ M]
  [inst_3 : PartialOrder N] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] (Q₂ : QuadraticMap R₂ M N),
  Q₂.PosDef = ∀ (x : M), x ≠ 0 → 0 < Q₂ x
-- Mathlib.Data.Fin.Tuple.Curry
Function.OfArity.curry_uncurry : ∀ {α β : Type u} {n : ℕ} (f : Function.OfArity α β n), Function.OfArity.curry f.uncurry = f
-- Mathlib.Data.Set.Subset
Set.subset_preimage_val_image_val_iff : ∀ {α : Type u_2} {A : Set α} {D E : Set ↑A}, D ⊆ Subtype.val ⁻¹' Subtype.val '' E ↔ D ⊆ E
-- Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Mathlib.Tactic.Monoidal.naturality_whiskerLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {p f g h pf pfg : C} {η : g ≅ h} (η_f : CategoryTheory.MonoidalCategoryStruct.tensorObj p f ≅ pf)
  (η_fg : CategoryTheory.MonoidalCategoryStruct.tensorObj pf g ≅ pfg)
  (η_fh : CategoryTheory.MonoidalCategoryStruct.tensorObj pf h ≅ pfg),
  CategoryTheory.MonoidalCategory.whiskerLeftIso pf η ≪≫ η_fh = η_fg →
    CategoryTheory.MonoidalCategory.whiskerLeftIso p (CategoryTheory.MonoidalCategory.whiskerLeftIso f η) ≪≫
        Mathlib.Tactic.Monoidal.normalizeIsoComp η_f η_fh =
      Mathlib.Tactic.Monoidal.normalizeIsoComp η_f η_fg
-- Mathlib.Analysis.Complex.Conformal
/-- In cases where the **Cauchy-Riemann Equation** guarantees complex differentiability at `x`, the
complex derivative equals `ContinuousLinearMap.complexOfReal` of the real derivative.
 -/
HasFDerivWithinAt.complexOfReal : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} {s : Set ℂ}
  {f' : ℂ →L[ℝ] E},
  HasFDerivWithinAt f f' s x → ∀ (h₂ : f' Complex.I = Complex.I • f' 1), HasFDerivWithinAt f (f'.complexOfReal h₂) s x
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.piecewise'_apply_left : ∀ {X : Type u_1} {Z : Type u_3} [inst : TopologicalSpace X] {C₀ C₁ C₂ : Set X} (h₀ : C₀ ⊆ C₁ ∪ C₂) (h₁ : IsClosed C₁)
  (h₂ : IsClosed C₂) (f₁ : LocallyConstant (↑C₁) Z) (f₂ : LocallyConstant (↑C₂) Z)
  [inst_1 : DecidablePred fun x => x ∈ C₁] (hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩) (x : ↑C₀)
  (hx : ↑x ∈ C₁), (LocallyConstant.piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₁ ⟨↑x, hx⟩
-- 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.Logic.Relation
Relation.TransGen.trans_left : ∀ {α : Type u_1} {r : α → α → Prop} {a b c : α},
  Relation.TransGen r a b → Relation.ReflTransGen r b c → Relation.TransGen r a c
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.coreToInt.sizeOf_spec : ∀ (e : Lean.Expr) (pos : Bool) (toIntThm : Lean.Expr) (lhs rhs : Int.Internal.Linear.Expr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.coreToInt e pos toIntThm lhs rhs) =
    1 + sizeOf e + sizeOf pos + sizeOf toIntThm + sizeOf lhs + sizeOf rhs
-- Aesop.Forward.RuleInfo
Aesop.instInhabitedSlot : Inhabited Aesop.Slot
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.homFamily_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.MorphismProperty C) (f : ↑P.toSet),
  P.homFamily f = (↑f).hom
-- Mathlib.Data.Rat.Defs
Rat.nontrivial : Nontrivial ℚ
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.instIsTriangulatedHomotopyCategoryIntUpQh : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C], DerivedCategory.Qh.IsTriangulated
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
TopologicalSpace.IsCompletelyMetrizableSpace.complete : ∀ {X : Type u_3} {t : TopologicalSpace X} [self : TopologicalSpace.IsCompletelyMetrizableSpace X],
  ∃ m, PseudoMetricSpace.toUniformSpace.toTopologicalSpace = t ∧ CompleteSpace X
-- Mathlib.Algebra.Lie.Basic
/-- An equivalence of Lie algebras (denoted as `L₁ ≃ₗ⁅R⁆ L₂`) is a morphism
which is also a linear equivalence.
We could instead define an equivalence to be a morphism which is also a (plain) equivalence.
However, it is more convenient to define via linear equivalence to get `.toLinearEquiv` for free.  -/
LieEquiv : (R : Type u) →
  (L : Type v) →
    (L' : Type w) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] → [LieAlgebra R L] → [inst_3 : LieRing L'] → [LieAlgebra R L'] → Type (max v w)
-- Lean.Elab.Tactic.Try
Lean.Elab.Tactic.Try.observing : {α : Type} → Lean.Elab.Tactic.Try.TryTacticM α → Lean.Elab.Tactic.Try.TryTacticM (Lean.Elab.Tactic.Try.TacticResult α)
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.MemSobolev.mono : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : InnerProductSpace ℂ F] [inst_7 : CompleteSpace F] {s s' : ℝ},
  s' ≤ s →
    ∀ {f : TemperedDistribution E F}, TemperedDistribution.MemSobolev s 2 f → TemperedDistribution.MemSobolev s' 2 f
-- Lean.Data.Lsp.CodeActions
/-- Contains additional diagnostic information about the context in which a code action is run.

[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#codeActionContext)  -/
Lean.Lsp.CodeActionContext : Type
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
/-- A strongly co-Cartesian arrow lying over an isomorphism is an isomorphism.  -/
CategoryTheory.Functor.IsStronglyCocartesian.isIso_of_base_isIso : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCocartesian f φ]
  [CategoryTheory.IsIso f], CategoryTheory.IsIso φ
-- Init.Data.Array.Lemmas
Array.setIfInBounds_eq_of_size_le : ∀ {α : Type u_1} {xs : Array α} {i : ℕ}, xs.size ≤ i → ∀ {a : α}, xs.setIfInBounds i a = xs
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.brecOn.go : {pu : Lean.Compiler.LCNF.Purity} →
  {motive_1 : Lean.Compiler.LCNF.Alt pu → Sort u} →
    {motive_2 : Lean.Compiler.LCNF.FunDecl pu → Sort u} →
      {motive_3 : Lean.Compiler.LCNF.Cases pu → Sort u} →
        {motive_4 : Lean.Compiler.LCNF.Code pu → Sort u} →
          {motive_5 : Array (Lean.Compiler.LCNF.Alt pu) → Sort u} →
            {motive_6 : List (Lean.Compiler.LCNF.Alt pu) → Sort u} →
              (t : Lean.Compiler.LCNF.Alt pu) →
                ((t : Lean.Compiler.LCNF.Alt pu) → t.below → motive_1 t) →
                  ((t : Lean.Compiler.LCNF.FunDecl pu) → t.below → motive_2 t) →
                    ((t : Lean.Compiler.LCNF.Cases pu) → t.below → motive_3 t) →
                      ((t : Lean.Compiler.LCNF.Code pu) → t.below → motive_4 t) →
                        ((t : Array (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_1 t → motive_5 t) →
                          ((t : List (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_2 t → motive_6 t) →
                            motive_1 t ×' t.below
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.union_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp}, t₁.union t₂ = t₁ ∪ t₂
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.map_natCast_star : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : NonAssocSemiring α] [inst_2 : StarRing α] (d : ℕ),
  (↑d).map star = ↑d
-- Init.Data.SInt.Lemmas
Int32.zero_lt_one : 0 < 1