mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Tactic.ElabTerm
/-- Given a tactic
```
apply f
```
we want the `apply` tactic to create all metavariables. The following
definition will return `@f` for `f`. That is, it will **not** create
metavariables for implicit arguments.
A similar method is also used in Lean 3.
This method is useful when applying lemmas such as:
```
theorem infLeRight {s t : Set α} : s ⊓ t ≤ t
```
where `s ≤ t` here is defined as
```
∀ {x : α}, x ∈ s → x ∈ t
```
 -/
Lean.Elab.Tactic.elabTermForApply : Lean.Syntax → optParam Bool true → Lean.Elab.Tactic.TacticM Lean.Expr
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- A non-unital subring of a non-unital ring inherits a non-unital ring structure  -/
NonUnitalSubringClass.toNonUnitalNonAssocRing : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocRing R] →
      [inst_1 : SetLike S R] → [hSR : NonUnitalSubringClass S R] → (s : S) → NonUnitalNonAssocRing ↥s
-- Init.Data.Nat.Basic
Nat.le_of_sub_le_sub_right : ∀ {n m k : ℕ}, k ≤ m → n - k ≤ m - k → n ≤ m
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.outerMeasure_interior_compacts : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (K : TopologicalSpace.Compacts G),
  μ.outerMeasure (interior ↑K) ≤ μ K
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_delete_contract : ∀ {α : Type u_1} (M : Matroid α) (C D C' : Set α),
  Disjoint C' D → ((M.contract C).delete D).contract C' = (M.contract (C ∪ C')).delete D
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.mulMap_comm : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (M N : Submodule R S), N.mulMap M = M.mulMap N ∘ₗ ↑(TensorProduct.comm R ↥N ↥M)
-- Init.System.ST
ST.Out.mk.sizeOf_spec : ∀ {σ α : Type} [inst : SizeOf σ] [inst_1 : SizeOf α] (val : α) (state : Void σ),
  sizeOf { val := val, state := state } = 1 + sizeOf val + sizeOf state
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey_insertMany!_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {l : List (α × β)} {k k' : α},
      compare k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
          k ∈ List.map Prod.fst l →
            ∀ {h' : Std.DTreeMap.Internal.Impl.contains k' ↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l) = true},
              (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)).getKey k' h' = k
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.swap_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial (Polynomial R)),
  Polynomial.Bivariate.swap p = (Polynomial.aevalAeval Polynomial.X (Polynomial.C Polynomial.X)) p
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
_private.Mathlib.AlgebraicTopology.SimplicialSet.HornColimits.0.SSet.horn.IsCompatible.multicofork.match_1.splitter : {n : ℕ} →
  {i : Fin (n + 2)} →
    (motive : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ↑{i}ᶜ).R → Sort u_1) →
      (x : (CategoryTheory.Limits.MultispanShape.ofLinearOrder ↑{i}ᶜ).R) →
        ((j : Fin (n + 1 + 1)) → (hj : j ∈ {i}ᶜ) → motive ⟨j, hj⟩) → motive x
-- Mathlib.Algebra.Group.Even
IsSquare.mul : ∀ {α : Type u_2} [inst : CommSemigroup α] {a b : α}, IsSquare a → IsSquare b → IsSquare (a * b)
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_map_tsub : ∀ {ι : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [ExistsAddOfLE M] [AddLeftMono M]
  [AddLeftReflectLE M] [inst_5 : Sub M] [OrderedSub M] (l : Multiset ι) {f g : ι → M},
  (∀ x ∈ l, g x ≤ f x) → (Multiset.map (fun x => f x - g x) l).sum = (Multiset.map f l).sum - (Multiset.map g l).sum
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleRing.eq_1 : ∀ (R : Type u_2) [inst : Ring R], IsSemisimpleRing R = IsSemisimpleModule R R
-- Lean.Elab.PreDefinition.FixedParams
/-- For a given function, a mapping from its parameters to the (indices of the) fixed parameters of the
recursive group.
The length of the array is the arity of the function, as determined from its body, consistent
with the arity used by well-founded recursion.
For the first function, they appear in order; for other functions they may be reordered.
 -/
Lean.Elab.FixedParamPerm : Type
-- Mathlib.RingTheory.Valuation.RankOne
Valuation.nonempty_rankOne_iff_mulArchimedean : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀}
  [v.IsNontrivial], Nonempty v.RankOne ↔ MulArchimedean (MonoidWithZeroHom.ofClass v).ValueGroup₀
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.apply : ∀ {α : Type u_1} {n : Type u_4} [inst : Star α] {A : Matrix n n α}, A.IsHermitian → ∀ (i j : n), star (A j i) = A i j
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.mk.inj : ∀ {C : Type u'} {inst : CategoryTheory.Category.{v', u'} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat}
  {inst_2 : J.WEqualsLocallyBijective AddCommGrpCat} {M : SheafOfModules R} {I : Type u} {s : I → M.sections}
  {epi : autoParam (CategoryTheory.Epi (M.freeHomEquiv.symm s)) SheafOfModules.GeneratingSections.epi._autoParam}
  {I_1 : Type u} {s_1 : I_1 → M.sections}
  {epi_1 : autoParam (CategoryTheory.Epi (M.freeHomEquiv.symm s_1)) SheafOfModules.GeneratingSections.epi._autoParam},
  { I := I, s := s, epi := epi } = { I := I_1, s := s_1, epi := epi_1 } → I = I_1 ∧ s ≍ s_1
-- Batteries.Data.AssocList
Batteries.AssocList.all.eq_def : ∀ {α : Type u_1} {β : Type u_2} (p : α → β → Bool) (x : Batteries.AssocList α β),
  Batteries.AssocList.all p x =
    match x with
    | Batteries.AssocList.nil => true
    | Batteries.AssocList.cons k v es => p k v && Batteries.AssocList.all p es
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
Valued.instIsTopologicalRing : ∀ {R : Type u} [inst : Ring R] {Γ₀ : Type v} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [_i : Valued R Γ₀],
  IsTopologicalRing R
-- Mathlib.Algebra.Polynomial.UnitTrinomial
Polynomial.IsUnitTrinomial.leadingCoeff_isUnit : ∀ {p : Polynomial ℤ}, p.IsUnitTrinomial → IsUnit p.leadingCoeff
-- Std.Do.Triple.SpecLemmas
List.Cursor.mk.congr_simp : ∀ {α : Type u} {l : List α} («prefix» prefix_1 : List α) (e_prefix : «prefix» = prefix_1) (suffix suffix_1 : List α)
  (e_suffix : suffix = suffix_1) (property : «prefix» ++ suffix = l),
  { «prefix» := «prefix», suffix := suffix, property := property } =
    { «prefix» := prefix_1, suffix := suffix_1, property := ⋯ }
-- Aesop.Tree.Data
Aesop.GoalId.succ : Aesop.GoalId → Aesop.GoalId
-- Mathlib.Logic.Equiv.Set
/-- `univ α` is equivalent to `α`.  -/
Equiv.Set.univ : (α : Type u_3) → ↑Set.univ ≃ α
-- Mathlib.FieldTheory.PerfectClosure
PerfectClosure.mk_eq_iff : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (x y : ℕ × K),
  PerfectClosure.mk K p x = PerfectClosure.mk K p y ↔
    ∃ z, (⇑(frobenius K p))^[y.1 + z] x.2 = (⇑(frobenius K p))^[x.1 + z] y.2
-- Init.Data.Array.Basic
/-- `a ∈ as` is a predicate which asserts that `a` is in the array `as`.  -/
Array.Mem : {α : Type u} → Array α → α → Prop
-- Mathlib.Data.Fintype.BigOperators
/-- An uncurried version of `Finset.sum_prod_type_right`  -/
Fintype.sum_prod_type_right' : ∀ {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [inst : Fintype α₁] [inst_1 : Fintype α₂] [inst_2 : AddCommMonoid γ]
  (f : α₁ → α₂ → γ), ∑ x, f x.1 x.2 = ∑ y, ∑ x, f x y
-- Init.Data.BitVec.Basic
BitVec.instIntCast : {w : ℕ} → IntCast (BitVec w)
-- Mathlib.Order.CompleteLattice.Basic
biSup_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CompleteLattice α] {f : β × γ → α} {s : Set β} {t : Set γ},
  ⨆ x ∈ s ×ˢ t, f x = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b)
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.CharType.noConfusionType : Sort v✝ → Lean.FuzzyMatching.CharType → Lean.FuzzyMatching.CharType → Sort v✝
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes
/-- The adjunction `tensorLeft F ⊣ rightAdj F`.  -/
CategoryTheory.FunctorToTypes.adj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C (Type (max w v u))) →
      CategoryTheory.MonoidalCategory.tensorLeft F ⊣ CategoryTheory.FunctorToTypes.rightAdj F
-- Mathlib.Util.Export
_private.Mathlib.Util.Export.0.Lean.Export.exportDef.defn : String → Lean.Name → Lean.Expr → Lean.Expr → List Lean.Name → Lean.ExportM Unit
-- Mathlib.GroupTheory.OreLocalization.OreSet
/-- The trivial submonoid is an Ore set.  -/
OreLocalization.oreSetBot : {R : Type u_1} → [inst : Monoid R] → OreLocalization.OreSet ⊥
-- Mathlib.Analysis.Meromorphic.Order
/-- Eta-expanded form of `meromorphicOrderAt_zpow`

---

The order multiplies by `n` when taking a meromorphic function to its `n`th power.  -/
fun_meromorphicOrderAt_zpow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} {x : 𝕜},
  MeromorphicAt f x → ∀ {n : ℤ}, meromorphicOrderAt (fun i => f i ^ n) x = ↑n * meromorphicOrderAt f x
-- Mathlib.CategoryTheory.Limits.EssentiallySmall
CategoryTheory.Limits.hasLimitsOfShape_of_essentiallySmall : ∀ (J : Type u₂) [inst : CategoryTheory.Category.{v₂, u₂} J] (C : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} C]
  [CategoryTheory.EssentiallySmall.{w₁, v₂, u₂} J] [CategoryTheory.Limits.HasLimitsOfSize.{w₁, w₁, v₁, u₁} C],
  CategoryTheory.Limits.HasLimitsOfShape J C
-- Init.Data.String.Lemmas.FindPos
String.Slice.lt_posGE_iff : ∀ {s : String.Slice} {p : String.Pos.Raw} {h : p ≤ s.rawEndPos} {q : s.Pos}, q < s.posGE p h ↔ q.offset < p
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedPurity : Inhabited Lean.Compiler.LCNF.Purity
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.length_toList : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → (↑m).toList.length = (↑m).size
-- Mathlib.CategoryTheory.Sites.CoverLifting
/-- Given a functor between sites that is continuous and cocontinuous,
the pushforward for the continuous functor `G` is left adjoint to
the pushforward for the cocontinuous functor `G`.  -/
CategoryTheory.Functor.sheafAdjunctionCocontinuous : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (G : CategoryTheory.Functor C D) →
          (A : Type w) →
            [inst_2 : CategoryTheory.Category.{w', w} A] →
              (J : CategoryTheory.GrothendieckTopology C) →
                (K : CategoryTheory.GrothendieckTopology D) →
                  [inst_3 : G.IsCocontinuous J K] →
                    [inst_4 : ∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasPointwiseRightKanExtension F] →
                      [inst_5 : G.IsContinuous J K] →
                        G.sheafPushforwardContinuous A J K ⊣ G.sheafPushforwardCocontinuous A J K
-- Init.Tactics
/-- The `split` tactic is useful for breaking nested if-then-else and `match` expressions into separate cases.
For a `match` expression with `n` cases, the `split` tactic generates at most `n` subgoals.

For example, given `n : Nat`, and a target `if n = 0 then Q else R`, `split` will generate
one goal with hypothesis `n = 0` and target `Q`, and a second goal with hypothesis
`¬n = 0` and target `R`.  Note that the introduced hypothesis is unnamed, and is commonly
renamed using the `case` or `next` tactics.

- `split` will split the goal (target).
- `split at h` will split the hypothesis `h`.
 -/
Lean.Parser.Tactic.split : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientGroup.norm_eq_groupSeminorm : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] {S : Subgroup M} (x : M ⧸ S), ‖x‖ = QuotientGroup.groupSeminorm x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.insert k).size = if t.contains k = true then t.size else t.size + 1
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `1` and `*` is a cancel commutative monoid if it admits an injective map
that preserves `1` and `*` to a cancel commutative monoid. See note [reducible non-instances].  -/
Function.Injective.cancelCommMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₁] →
      [inst_1 : One M₁] →
        [inst_2 : Pow M₁ ℕ] →
          [inst_3 : CancelCommMonoid M₂] →
            (f : M₁ → M₂) →
              Function.Injective f →
                f 1 = 1 →
                  (∀ (x y : M₁), f (x * y) = f x * f y) →
                    (∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n) → CancelCommMonoid M₁
-- Lean.Elab.Level
Lean.Elab.Level.elabLevel : Lean.Syntax → Lean.Elab.Level.LevelElabM Lean.Level
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imK_mul : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Ring R] (a b : QuaternionAlgebra R c₁ c₂ c₃),
  (a * b).imK = a.re * b.imK + a.imI * b.imJ + c₂ * a.imI * b.imK - a.imJ * b.imI + a.imK * b.re
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- Consider a function `f : α × β → γ`. Suppose that it is continuous on each “vertical section”
`{a} × univ` for `a : α` from a dense set. Suppose that it is Lipschitz continuous on each
“horizontal section” `univ × {b}`, `b : β` with the same Lipschitz constant `K`. Then it is
continuous.

The actual statement uses (Lipschitz) continuity of `fun y ↦ f (a, y)` and `fun x ↦ f (x, b)`
instead of continuity of `f` on subsets of the product space.  -/
continuous_prod_of_dense_continuous_lipschitzWith : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : PseudoEMetricSpace γ] (f : α × β → γ) (K : NNReal) {s : Set α},
  Dense s → (∀ a ∈ s, Continuous fun y => f (a, y)) → (∀ (b : β), LipschitzWith K fun x => f (x, b)) → Continuous f
-- Mathlib.Algebra.Lie.Basic
LieHom.one_apply : ∀ {R : Type u} {L₁ : Type v} [inst : CommRing R] [inst_1 : LieRing L₁] [inst_2 : LieAlgebra R L₁] (x : L₁), 1 x = x
-- Mathlib.Algebra.Ring.Subring.Basic
/-- Makes the identity isomorphism from a proof two subrings of a multiplicative
monoid are equal.  -/
RingEquiv.subringCongr : {R : Type u} → [inst : NonAssocRing R] → {s t : Subring R} → s = t → ↥s ≃+* ↥t
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.CokernelData.mk.sizeOf_spec : ∀ {A : Type u} [inst : Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : Module A M₁]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₂] {pres₂ : Module.Presentation A M₂} {f : M₁ →ₗ[A] M₂} {ι : Type w₁}
  {g₁ : ι → M₁} [inst_5 : SizeOf A] [inst_6 : SizeOf M₁] [inst_7 : SizeOf M₂] [inst_8 : SizeOf ι]
  (lift : ι → pres₂.G →₀ A) (π_lift : ∀ (i : ι), pres₂.π (lift i) = f (g₁ i)),
  sizeOf { lift := lift, π_lift := π_lift } = 1
-- Mathlib.Combinatorics.SetFamily.Shatter
Finset.shatterer_compress_subset_shatterer : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (𝒜 : Finset (Finset α)), (Down.compression a 𝒜).shatterer ⊆ 𝒜.shatterer
-- Lean.Meta.Eqns
Lean.Meta.instInhabitedEqnsExtState.default : Lean.Meta.EqnsExtState
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Limits.PreservesBinaryBiproducts.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.PreservesZeroMorphisms],
  autoParam (∀ {X Y : C}, CategoryTheory.Limits.PreservesBinaryBiproduct X Y F)
      CategoryTheory.Limits.PreservesBinaryBiproducts.preserves._autoParam →
    CategoryTheory.Limits.PreservesBinaryBiproducts F
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.UseImplicitLambdaResult.no : Lean.Elab.Term.UseImplicitLambdaResult
-- Mathlib.LinearAlgebra.Matrix.Bilinear
/-- A version of `LinearMap.pow_mulRight` for matrix multiplication.  -/
pow_mulRightLinearMap : ∀ {l : Type u_1} {m : Type u_2} {R : Type u_5} {A : Type u_6} [inst : Fintype m] [inst_1 : DecidableEq m]
  [inst_2 : Semiring R] [inst_3 : Semiring A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] (a : Matrix m m A)
  (k : ℕ), mulRightLinearMap l R a ^ k = mulRightLinearMap l R (a ^ k)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.IsFiniteMeasureOnCompacts.comap' : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} [inst : TopologicalSpace α]
  [inst_1 : TopologicalSpace β] (μ : MeasureTheory.Measure β) [MeasureTheory.IsFiniteMeasureOnCompacts μ] {f : α → β},
  Continuous f → MeasurableEmbedding f → MeasureTheory.IsFiniteMeasureOnCompacts (MeasureTheory.Measure.comap f μ)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.id_base : ∀ {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),
  (CategoryTheory.Limits.CatCospanTransform.id F G).base = CategoryTheory.Functor.id B
-- Init.Prelude
instInhabitedULift : {α : Type u_1} → [Inhabited α] → Inhabited (ULift.{u_2, u_1} α)
-- Mathlib.Data.Fintype.Card
Fintype.card_setUniv : ∀ {α : Type u_1} [inst : Fintype α] {h : Fintype ↑Set.univ}, Fintype.card ↑Set.univ = Fintype.card α
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.functor_obj_obj : ∀ (n : Type uᵒᵖ) (S : AlgebraicGeometry.Scheme),
  (AlgebraicGeometry.AffineSpace.functor.obj n).obj S = AlgebraicGeometry.AffineSpace (Opposite.unop n) S
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.get_bind_get : ∀ {σ : Type u_2} {m : Type u_2 → Type u_1} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m],
  (do
      let _ ← get
      get) =
    get
-- Mathlib.Algebra.Order.Archimedean.Defs
/-- An ordered commutative monoid is called `MulArchimedean` if for any two elements `x`, `y`
such that `1 < y`, there exists a natural number `n` such that `x ≤ y ^ n`.  -/
MulArchimedean : (R : Type u_2) → [CommMonoid R] → [PartialOrder R] → Prop
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.ι_δ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal] (X Y : P.FullSubcategory),
  CategoryTheory.Functor.OplaxMonoidal.δ P.ι X Y =
    CategoryTheory.CategoryStruct.id (P.ι.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
-- Mathlib.Data.Finset.SDiff
/-- `s \ t` is the set consisting of the elements of `s` that are not in `t`.  -/
Finset.instSDiff : {α : Type u_1} → [DecidableEq α] → SDiff (Finset α)
-- Mathlib.Algebra.Ring.Pi
NonUnitalRingHom.pi_apply : ∀ {I : Type u} {f : I → Type u_1} {γ : Type u_2} [inst : (i : I) → NonUnitalNonAssocSemiring (f i)]
  [inst_1 : NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i) (x : γ) (b : I),
  (NonUnitalRingHom.pi g) x b = (g b) x
-- Init.Data.UInt.Lemmas
UInt8.div_zero : ∀ {a : UInt8}, a / 0 = 0
-- Mathlib.Geometry.Manifold.Instances.Icc
EuclideanHalfSpace.congr_simp : ∀ (n n_1 : ℕ) (e_n : n = n_1) [inst : NeZero n], EuclideanHalfSpace n = EuclideanHalfSpace n_1
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.mono_set_ae : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b c d : ℝ}
  {μ : MeasureTheory.Measure ℝ} [TopologicalSpace.PseudoMetrizableSpace ε],
  IntervalIntegrable f μ a b → Set.uIoc c d ≤ᵐ[μ] Set.uIoc a b → IntervalIntegrable f μ c d
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.Hom.hom.eq_1 : ∀ {X Y : GrpCat} (f : X.Hom Y), f.hom = CategoryTheory.ConcreteCategory.hom f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_insert_le_minKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {he : t ≠ ∅}, (cmp ((t.insert k v).minKey ⋯) (t.minKey he)).isLE = true
-- Init.Data.List.ToArray
List.foldr_toArray : ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (l : List α),
  Array.foldr f init l.toArray = List.foldr f init l
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
/-- Given a right adjoint functor between categories of cones,
the image of a weak limit cone is a weak limit cone.
 -/
CategoryTheory.Limits.IsWeakLimit.ofRightAdjoint : {J : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} J] →
    {K : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            {F : CategoryTheory.Functor J C} →
              {D : Type u_4} →
                [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                  {G : CategoryTheory.Functor K D} →
                    {left : CategoryTheory.Functor (CategoryTheory.Limits.Cone F) (CategoryTheory.Limits.Cone G)} →
                      {right : CategoryTheory.Functor (CategoryTheory.Limits.Cone G) (CategoryTheory.Limits.Cone F)} →
                        (left ⊣ right) →
                          {c : CategoryTheory.Limits.Cone G} →
                            CategoryTheory.Limits.IsWeakLimit c → CategoryTheory.Limits.IsWeakLimit (right.obj c)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdx?.match_1.congr_eq_3 : ∀ (motive : Ordering → Sort u_1) (x : Ordering) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  x = Ordering.gt →
    (match x with
      | Ordering.lt => h_1 ()
      | Ordering.eq => h_2 ()
      | Ordering.gt => h_3 ()) ≍
      h_3 ()
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_f_3_comp_chainsIso₃_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) (x : (Fin 3 → G) →₀ ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₃ B).hom)
      ((CategoryTheory.ConcreteCategory.hom ((groupHomology.chainsMap f φ).f 3)) x) =
    Finsupp.mapRange ⇑(Rep.Hom.hom φ) ⋯
      (Finsupp.mapDomain (Prod.map (⇑f) (Prod.map ⇑f ⇑f))
        ((CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₃ A).hom) x))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] (m m_1 : Std.ExtDHashMap α β),
  m = m_1 → ∀ (a : α) (fallback fallback_1 : β a), fallback = fallback_1 → m.getD a fallback = m_1.getD a fallback_1
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.sylvester_comm : ∀ {R : Type u_1} [inst : Semiring R] (f g : Polynomial R) (m n : ℕ),
  f.sylvester g m n =
    (Matrix.reindex (finCongr ⋯) (finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin n) (Fin m)).trans finSumFinEquiv)))
      (g.sylvester f n m)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.add_subset_add_right : ∀ {α : Type u_2} [inst : Add α] {s₁ s₂ t : Set α}, s₁ ⊆ s₂ → s₁ + t ⊆ s₂ + t
-- Mathlib.Order.Disjoint
eq_bot_of_isCompl_top : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : BoundedOrder α] {x : α}, IsCompl x ⊤ → x = ⊥
-- Mathlib.LinearAlgebra.Alternating.Basic
LinearMap.add_compAlternatingMap : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {N₂ : Type u_11} [inst_5 : AddCommMonoid N₂]
  [inst_6 : Module R N₂] (g₁ g₂ : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N),
  (g₁ + g₂).compAlternatingMap f = g₁.compAlternatingMap f + g₂.compAlternatingMap f
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.unitGroup_le_unitGroup : ∀ {K : Type u} [inst : Field K] {A B : ValuationSubring K}, A.unitGroup ≤ B.unitGroup ↔ A ≤ B