mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Tree.AddRapp
/-- Adds a new rapp and its subgoals. If the rapp assigns mvars, all relevant
goals containing these mvars are copied as children of the rapp as well. If
the rapp drops mvars, these are treated as assigned mvars, in the sense that
the same goals are copied as if the dropped mvar had been assigned.

Note that adding a rapp may prove the parent goal, but this function does not
make the necessary changes. So after calling it, you should check whether the
rapp's parent goal is proven and mark it accordingly.
 -/
Aesop.addRapp : Aesop.AddRapp → Aesop.TreeM Aesop.RappRef
-- Init.Data.UInt.Basic
instXorOpUInt64 : XorOp UInt64
-- Std.Data.Iterators.Producers.Monadic.Array
Std.Iterators.Types.ArrayIterator.mk.inj : ∀ {α : Type w} {array : Array α} {pos : ℕ} {array_1 : Array α} {pos_1 : ℕ},
  { array := array, pos := pos } = { array := array_1, pos := pos_1 } → array = array_1 ∧ pos = pos_1
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulDysonETransform_fst : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommGroup α] (e : α) (x : Finset α × Finset α),
  (Finset.mulDysonETransform e x).1 = x.1 ∪ e • x.2
-- Mathlib.RingTheory.HopfAlgebra.Convolution
/-- The antipode of a commutative Hopf algebra as an algebra hom.  -/
HopfAlgebra.antipodeAlgHom : (R : Type u_1) →
  (A : Type u_2) → [inst : CommSemiring R] → [inst_1 : CommSemiring A] → [inst_2 : HopfAlgebra R A] → A →ₐ[R] A
-- Mathlib.MeasureTheory.Measure.Real
/-- **Alias** of `MeasureTheory.measureReal_sdiff'`. -/
MeasureTheory.measureReal_diff' : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet t →
    autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_sdiff'._auto_1 →
      autoParam (μ t ≠ ⊤) MeasureTheory.measureReal_sdiff'._auto_3 → μ.real (s \ t) = μ.real (s ∪ t) - μ.real t
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_range_eq_of_injective : ∀ {α : Type u} {β : Type v} {f : α → β},
  Function.Injective f → Cardinal.lift.{u, v} (Cardinal.mk ↑(Set.range f)) = Cardinal.lift.{v, u} (Cardinal.mk α)
-- Mathlib.Algebra.Group.Defs
/-- Multiplication is right cancellative (i.e. right regular).  -/
IsRightCancelMul.mul_right_cancel : ∀ {G : Type u} {inst : Mul G} [self : IsRightCancelMul G] (a : G), IsRightRegular a
-- Mathlib.Data.NNRat.Defs
instSubNNRat : Sub ℚ≥0
-- Mathlib.Algebra.Group.Defs
/-- An `AddMonoid` is an `AddSemigroup` with an element `0` such that `0 + a = a + 0 = a`.  -/
AddMonoid : Type u → Type u
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.applyPartition.go.match_1.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) →
    (x = Ordering.lt → motive Ordering.lt) →
      (x = Ordering.eq → motive Ordering.eq) → (x = Ordering.gt → motive Ordering.gt) → motive x
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_mul_cos_add_sin_mul_I_sub : ∀ {r : ℝ},
  0 < r →
    ∀ (θ : ℝ),
      (↑r * (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I)).arg - θ = 2 * Real.pi * ↑⌊(Real.pi - θ) / (2 * Real.pi)⌋
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.hasHomology_of_hasCokernel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) (Z : C) [CategoryTheory.Limits.HasCokernel f],
  { X₁ := X, X₂ := Y, X₃ := Z, f := f, g := 0, zero := ⋯ }.HasHomology
-- Mathlib.LinearAlgebra.Projectivization.Subspace
Projectivization.Subspace.subset_span_trans : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {S T U : Set (Projectivization K V)},
  S ⊆ ↑(Projectivization.Subspace.span T) →
    T ⊆ ↑(Projectivization.Subspace.span U) → S ⊆ ↑(Projectivization.Subspace.span U)
-- Mathlib.NumberTheory.Dioph
Dioph.ex1_dioph : ∀ {α : Type u} {S : Set (Option α → ℕ)}, Dioph S → Dioph {v | ∃ x, Option.elim' x v ∈ S}
-- Mathlib.NumberTheory.FactorisationProperties
Nat.deficient_two : Nat.Deficient 2
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.instToString : {w : ℕ} → ToString (Std.Tactic.BVDecide.BVExpr w)
-- Mathlib.Order.Heyting.Basic
/-- Transfer `GeneralizedHeytingAlgebra` across an `Equiv`.  -/
Equiv.generalizedHeytingAlgebra : {α : Type u_2} → {β : Type u_3} → α ≃ β → [GeneralizedHeytingAlgebra β] → GeneralizedHeytingAlgebra α
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
AnalyticAt.differentiableWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}
  {s : Set E}, AnalyticAt 𝕜 f x → DifferentiableWithinAt 𝕜 f s x
-- Mathlib.Topology.Algebra.UniformMulAction
MulOpposite.uniformContinuousConstSMul : ∀ {M : Type v} {X : Type x} [inst : UniformSpace X] [inst_1 : SMul M X] [UniformContinuousConstSMul M X],
  UniformContinuousConstSMul M Xᵐᵒᵖ
-- Mathlib.Topology.MetricSpace.Defs
dist_ofDual : ∀ {X : Type u_1} [inst : Dist X] (a b : Xᵒᵈ), dist (OrderDual.ofDual a) (OrderDual.ofDual b) = dist a b
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.le_unzero_iff : ∀ {α : Type u_1} [inst : LE α] {y : WithZero α} {a : α} (hy : y ≠ 0), a ≤ WithZero.unzero hy ↔ ↑a ≤ y
-- Init.Data.Array.Basic
/-- Counts the number of elements in the array `as` that satisfy the Boolean predicate `p`.

Examples:
* `#[1, 2, 3, 4, 5].countP (· % 2 == 0) = 2`
* `#[1, 2, 3, 4, 5].countP (· < 5) = 4`
* `#[1, 2, 3, 4, 5].countP (· > 5) = 0`
 -/
Array.countP : {α : Type u} → (α → Bool) → Array α → ℕ
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.eq_bot_or_top : ∀ {α : Type u_2} [inst : TopologicalSpace α] [IndiscreteTopology α] (U : TopologicalSpace.Opens α), U = ⊥ ∨ U = ⊤
-- Init.System.IOError
IO.Error.noFileOrDirectory.sizeOf_spec : ∀ (filename : String) (osCode : UInt32) (details : String),
  sizeOf (IO.Error.noFileOrDirectory filename osCode details) = 1 + sizeOf filename + sizeOf osCode + sizeOf details
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSet_iff_meas_biInter : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : ι → Set Ω},
  (∀ (i : ι), MeasurableSet (f i)) →
    (ProbabilityTheory.Kernel.iIndepSet f κ μ ↔
      ∀ (s : Finset ι), ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ s, f i) = ∏ i ∈ s, (κ a) (f i))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.union_eq : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β}, m₁.union m₂ = m₁ ∪ m₂
-- Std.Http.Data.URI.Basic
Std.Http.URI.Host.name.inj : ∀ {name name_1 : Std.Http.URI.DomainName}, Std.Http.URI.Host.name name = Std.Http.URI.Host.name name_1 → name = name_1
-- Lean.Parser.Term
/-- `binrel% r a b` elaborates `r a b` as a binary relation using the type propagation protocol in `Lean.Elab.Extra`.  -/
Lean.Parser.Term.binrel : Lean.Parser.Parser
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.constAlter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α],
  m₁.WF →
    m₂.WF →
      ∀ (k : α) (f : Option β → Option β),
        m₁.Equiv m₂ → (Std.DHashMap.Raw.Const.alter m₁ k f).Equiv (Std.DHashMap.Raw.Const.alter m₂ k f)
-- Mathlib.Algebra.BigOperators.ModEq
Nat.ModEq.multisetSum_map : ∀ {α : Type u_1} {n : ℕ} {f g : α → ℕ} {s : Multiset α},
  (∀ x ∈ s, f x ≡ g x [MOD n]) → (Multiset.map f s).sum ≡ (Multiset.map g s).sum [MOD n]
-- Mathlib.Topology.Irreducible
instPreirreducibleSpaceOfIndiscreteTopology : ∀ {X : Type u_1} [inst : TopologicalSpace X] [IndiscreteTopology X], PreirreducibleSpace X
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.map_top : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), ⊤.map f = ⊤
-- Mathlib.Algebra.Order.Group.Equiv
ofLexAddEquiv.eq_1 : ∀ (α : Type u_1) [inst : Add α], ofLexAddEquiv α = { toEquiv := ofLex, map_add' := ⋯ }
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.cRank_eq_iSup_cardinalMk_indep : ∀ {α : Type u} {M : Matroid α}, M.cRank = ⨆ I, Cardinal.mk ↑↑I
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.ae_comp_iff : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} {p : β → Prop},
  MeasurableSet {z | p z} → ((∀ᵐ (z : β) ∂μ.bind ⇑κ, p z) ↔ ∀ᵐ (y : α) ∂μ, ∀ᵐ (z : β) ∂κ y, p z)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
CategoryTheory.Precoverage.locallyCoverDense_of_map_functorPullback_mem : ∀ {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_3, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_4} D] (F : CategoryTheory.Functor C D) (K : CategoryTheory.Precoverage D)
  [K.HasIsos] [K.IsStableUnderBaseChange] [K.IsStableUnderComposition] [K.HasPullbacks],
  (∀ {S : C} {R : CategoryTheory.Presieve (F.obj S)},
      R ∈ K.coverings (F.obj S) →
        CategoryTheory.Presieve.map F (CategoryTheory.Presieve.functorPullback F R) ∈ K.coverings (F.obj S)) →
    F.LocallyCoverDense K.toGrothendieck
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.isHenstock_single_iff : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {x : ι → ℝ} (hJ : J ≤ I) (h : x ∈ BoxIntegral.Box.Icc I),
  (BoxIntegral.TaggedPrepartition.single I J hJ x h).IsHenstock ↔ x ∈ BoxIntegral.Box.Icc J
-- Mathlib.Data.Set.Function
Set.InjOn.mem_image_iff : ∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {f : α → β} {x : α},
  Set.InjOn f s → s₁ ⊆ s → x ∈ s → (f x ∈ f '' s₁ ↔ x ∈ s₁)
-- Mathlib.Analysis.Calculus.FDeriv.Pow
hasFDerivAt_pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  (n : ℕ) {x : 𝔸},
  HasFDerivAt (fun x => x ^ n)
    (∑ i ∈ Finset.range n, MulOpposite.op (x ^ i) • x ^ (n.pred - i) • ContinuousLinearMap.id 𝕜 𝔸) x
-- Std.Http.Protocol.H1.Event
Std.Http.Protocol.H1.instInhabitedEvent : {a : Std.Http.Protocol.H1.Direction} → Inhabited (Std.Http.Protocol.H1.Event a)
-- Lean.Server.FileWorker.RequestHandling
_private.Lean.Server.FileWorker.RequestHandling.0.Lean.Server.FileWorker.handleDocumentSymbol.toDocumentSymbols : Lean.FileMap →
  List Lean.Syntax →
    Array Lean.Lsp.DocumentSymbol →
      List Lean.Server.FileWorker.NamespaceEntry → Lean.Server.RequestM (Array Lean.Lsp.DocumentSymbol)
-- Lean.Parser.Term.Basic
Lean.Parser.Term.structInstLVal.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Analytic.Composition
/-- If two functions `g` and `f` have power series `q` and `p` respectively at `f x` and `x`, within
two sets `s` and `t` such that `f` maps `s` to `t`, then `g ∘ f` admits the power
series `q.comp p` at `x` within `s`.  -/
HasFPowerSeriesWithinAt.comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {g : F → G} {f : E → F} {q : FormalMultilinearSeries 𝕜 F G}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {t : Set F} {s : Set E},
  HasFPowerSeriesWithinAt g q t (f x) →
    HasFPowerSeriesWithinAt f p s x → Set.MapsTo f s t → HasFPowerSeriesWithinAt (g ∘ f) (q.comp p) s x
-- Mathlib.Data.PFunctor.Multivariate.M
/-- `n`-ary M-type for `P`  -/
MvPFunctor.M : {n : ℕ} → MvPFunctor.{u} (n + 1) → TypeVec.{u} n → Type u
-- Mathlib.Data.Nat.Factorization.Defs
Nat.factorizationEquiv_symm_apply_coe : ∀ (x : { f // ∀ p ∈ f.support, Nat.Prime p }), ↑(Nat.factorizationEquiv.symm x) = (↑x).prod fun x1 x2 => x1 ^ x2
-- Lean.Syntax
_private.Lean.Syntax.0.Lean.Syntax.findStack?.go : (Lean.Syntax → Bool) → (Lean.Syntax → Bool) → Lean.Syntax.Stack → Lean.Syntax → Option Lean.Syntax.Stack
-- Mathlib.GroupTheory.Index
AddSubgroup.nsmul_mem_of_relIndex_ne_zero_of_dvd : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G},
  H.relIndex K ≠ 0 → ∀ {a : G}, a ∈ K → ∀ {n : ℕ}, (∀ (m : ℕ), 0 < m → m ≤ H.relIndex K → m ∣ n) → n • a ∈ H ⊓ K
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.count_self : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α]
  [inst_2 : DecidableEq (Associates α)] [inst_3 : (p : Associates α) → Decidable (Irreducible p)] [Nontrivial α]
  {p : Associates α}, Irreducible p → p.count p.factors = 1
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.ext_iff : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] {f g : M →ₙ+ N}, f = g ↔ ∀ (x : M), f x = g x
-- Mathlib.LinearAlgebra.AffineSpace.Slope
slope_comm : ∀ {k : Type u_1} {E : Type u_2} {PE : Type u_3} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
  [inst_3 : AddTorsor E PE] (f : k → PE) (a b : k), slope f a b = slope f b a
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- A simple graph `G` is inducingly contained in a simple graph `H` if there exists an induced
subgraph of `H` isomorphic to `G`. This is denoted by `G ⊴ H`.  -/
SimpleGraph.IsIndContained : {V : Type u_1} → {W : Type u_2} → SimpleGraph V → SimpleGraph W → Prop
-- Std.Http.Data.Response
Std.Http.Response.instInhabitedHead.default : Std.Http.Response.Head
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `derivWithin_const_smul_field`.

---

A variant of `derivWithin_const_smul` without differentiability assumption when the scalar
multiplication is by division ring elements.  -/
derivWithin_const_smul' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} {𝕝 : Type u_3} [inst_3 : DivisionSemiring 𝕝] [inst_4 : Module 𝕝 F]
  [SMulCommClass 𝕜 𝕝 F] [ContinuousConstSMul 𝕝 F] (c : 𝕝) (f : 𝕜 → F), derivWithin (c • f) s x = c • derivWithin f s x
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- **Alias** of `Left.mul_pos`.

---

Assumes left covariance.  -/
mul_pos : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : Preorder α] [PosMulStrictMono α], 0 < a → 0 < b → 0 < a * b
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The monoidal functor sending a type `H` with a `G`-action to the induced `k`-linear
`G`-representation on `k[H].`  -/
Rep.linearization : (k : Type u) →
  (G : Type v) →
    [inst : CommRing k] → [inst_1 : Monoid G] → CategoryTheory.Functor (Action (Type w) G) (Rep.{max w u, u, v} k G)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapAddMon_obj_addMon_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] (A : CategoryTheory.AddMon C),
  CategoryTheory.AddMonObj.zero =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (F.map CategoryTheory.AddMonObj.zero)
-- Mathlib.Analysis.Normed.Affine.Isometry
LinearIsometry.toAffineIsometry_toAffineMap : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : SeminormedAddCommGroup V₂] [inst_4 : NormedSpace 𝕜 V₂] (f : V →ₗᵢ[𝕜] V₂),
  f.toAffineIsometry.toAffineMap = f.toAffineMap
-- Mathlib.Algebra.Order.AddGroupWithTop
WithTop.LinearOrderedAddCommGroup.top_sub : ∀ {G : Type u_1} [inst : AddCommGroup G] (x : WithTop G), ⊤ - x = ⊤
-- Mathlib.Algebra.Ring.Parity
Dvd.dvd.even : ∀ {α : Type u_2} [inst : Semiring α] {a b : α}, a ∣ b → Even a → Even b
-- Mathlib.GroupTheory.Subgroup.Centralizer
/-- If all the elements of a set `s` commute, then `closure s` is an additive commutative group.  -/
AddSubgroup.isAddCommutative_closure : ∀ {G : Type u_1} [inst : AddGroup G] {k : Set G},
  (∀ x ∈ k, ∀ y ∈ k, x + y = y + x) → IsAddCommutative ↥(AddSubgroup.closure k)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Without this lemma, `limit.hom_ext` would be applied, but the goal would involve terms
in `Discrete β` rather than `β` itself.  -/
CategoryTheory.Limits.Pi.hom_ext : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f] {X : C} (g₁ g₂ : X ⟶ ∏ᶜ f),
  (∀ (b : β),
      CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Pi.π f b) =
        CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Pi.π f b)) →
    g₁ = g₂
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.subset_compl_iff_disjoint_left : ∀ {α : Type u_1} {s t : Finset α} [inst : Fintype α] [inst_1 : DecidableEq α], s ⊆ tᶜ ↔ Disjoint t s
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.cast_trans : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {i j k : ℕ}
  (h : i = j) (h' : j = k), TensorPower.cast R M h ≪≫ₗ TensorPower.cast R M h' = TensorPower.cast R M ⋯
-- Std.Data.ByteSlice
instSliceableByteSliceNat_1 : Std.Rco.Sliceable ByteSlice ℕ ByteSlice
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.fixingSubgroup.eq_1 : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (K : IntermediateField F E),
  K.fixingSubgroup = fixingSubgroup Gal(E/F) ↑K
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.leftUnitor_hom_hom : ∀ (X : SFinKer), (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom.hom = ProbabilityTheory.Kernel.id.map Prod.snd
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.comapDomain_zero : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N) (hf : Function.Injective f),
  AddMonoidAlgebra.comapDomain f hf 0 = 0
-- Lean.SubExpr
Lean.SubExpr.Pos.append : Lean.SubExpr.Pos → Lean.SubExpr.Pos → Lean.SubExpr.Pos
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.map_id_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
  CategoryTheory.Limits.coprod.map (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) =
    CategoryTheory.CategoryStruct.id (X ⨿ Y)
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.GlobalPreprocessor.mk.injEq : ∀ (toPreprocessorBase : Mathlib.Tactic.Linarith.PreprocessorBase)
  (transform : List Lean.Expr → Lean.MetaM (List Lean.Expr))
  (toPreprocessorBase_1 : Mathlib.Tactic.Linarith.PreprocessorBase)
  (transform_1 : List Lean.Expr → Lean.MetaM (List Lean.Expr)),
  ({ toPreprocessorBase := toPreprocessorBase, transform := transform } =
      { toPreprocessorBase := toPreprocessorBase_1, transform := transform_1 }) =
    (toPreprocessorBase = toPreprocessorBase_1 ∧ transform = transform_1)
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
/-- A zero object is a left unit for categorical coproduct.  -/
CategoryTheory.Limits.zeroCoprodIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → (X : C) → 0 ⨿ X ≅ X
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.coe_smul : ∀ {G : Type u_4} [inst : Group G] {H : Subgroup G} (g h : ↥H), ↑(ConjAct.toConjAct g • h) = ConjAct.toConjAct ↑g • ↑h
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.Comma.costructuredArrowSndAdjunction_counit_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (b : B) (X : CategoryTheory.CostructuredArrow L (R.obj b)),
  (CategoryTheory.Comma.costructuredArrowSndAdjunction L R b).counit.app X =
    CategoryTheory.CostructuredArrow.homMk (CategoryTheory.CategoryStruct.id X.left) ⋯
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.refl_symm : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Mul α], (OrderMonoidIso.refl α).symm = OrderMonoidIso.refl α
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- **Alias** of `ModularForm.qExpansion_neg`. -/
ModularFormClass.qExpansion_neg : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ},
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ (f : F) [ModularFormClass F Γ k], UpperHalfPlane.qExpansion h (-⇑f) = -UpperHalfPlane.qExpansion h ⇑f
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
CompactConvergenceCLM.instContinuousEvalConst : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F],
  ContinuousEvalConst (CompactConvergenceCLM σ E F) E F
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation_var : ∀ (R : Type u) [inst : CommRing R] (n : ℕ) (M : Type u_1) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (m : (exteriorPower.presentation.relations R (Fin n) M).G),
  (exteriorPower.presentation R n M).var m = (exteriorPower.ιMulti R n) m
-- Mathlib.Analysis.Complex.OpenMapping
/-- Corollary to the open mapping theorem: A holomorphic function whose imaginary part is constant is
itself constant.
 -/
AnalyticOnNhd.eq_const_add_im_mul_I_of_re_eq_const : ∀ {f : ℂ → ℂ} {U : Set ℂ} {c₀ : ℝ},
  AnalyticOnNhd ℂ f U → (∀ x ∈ U, (f x).im = c₀) → IsOpen U → IsConnected U → ∃ c, ∀ x ∈ U, f x = ↑c + ↑c₀ * Complex.I
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.shortComplexFunctor'_obj_g : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i j k : ι) (K : HomologicalComplex C c),
  ((HomologicalComplex.shortComplexFunctor' C c i j k).obj K).g = K.d j k
-- Std.Async.Select
/-- Swap out the `IO.Promise` within the `Waiter`. Note that the part which determines whether the
`Waiter` is finished is not swapped out.
 -/
Std.Async.Waiter.withPromise : {α β : Type} → Std.Async.Waiter α → IO.Promise (Except IO.Error β) → Std.Async.Waiter β
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.of_nsmul : ∀ {M : Type u_1} [inst : AddCommMonoid M] {a b p : M} {n : ℕ}, a ≡ b [PMOD n • p] → a ≡ b [PMOD p]
-- Mathlib.FieldTheory.Normal.Basic
/-- If `x : L` is a root of `minpoly K y`, then we can find `(σ : Gal(L/K))` with `σ y = x`.
That is, `x` and `y` are Galois conjugates.  -/
minpoly.exists_algEquiv_of_root' : ∀ {K : Type u_6} {L : Type u_7} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Normal K L] {x y : L},
  IsAlgebraic K y → (Polynomial.aeval x) (minpoly K y) = 0 → ∃ σ, σ y = x
-- Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
/-- A presieve is *extensive* if it is finite and its arrows induce an isomorphism from the
coproduct to the target.  -/
CategoryTheory.Presieve.Extensive : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {X : C} → CategoryTheory.Presieve X → Prop
-- Mathlib.RingTheory.FiniteType
Algebra.FiniteType.instFreeAlgebraOfFinite : ∀ {R : Type uR} {S : Type uS} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {ι : Type u_1}
  [Finite ι] [Algebra.FiniteType R S], Algebra.FiniteType R (FreeAlgebra S ι)
-- Mathlib.Util.AddRelatedDecl
/-- An `(attr := ...)` argument for applying the same attributes to multiple declarations.  -/
Mathlib.Tactic.optAttrArg : Lean.ParserDescr
-- Mathlib.Data.Int.Interval
Int.card_Icc : ∀ (a b : ℤ), (Finset.Icc a b).card = (b + 1 - a).toNat
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_neg_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {c : ℝ} {g : α → F}
  {f' : α → E'} {l : Filter α}, Asymptotics.IsBigOWith c l (fun x => -f' x) g ↔ Asymptotics.IsBigOWith c l f' g
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.subschemeMap.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (J : Y.IdealSheafData) (f f_1 : X ⟶ Y) (e_f : f = f_1)
  (H : J ≤ I.map f), I.subschemeMap J f H = I.subschemeMap J f_1 ⋯