mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Time.Notation
_private.Std.Time.Notation.0.Std.Time.convertPlainDateTime : Std.Time.PlainDateTime → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.MvPolynomialC.numBound.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instSetLike : {G : Type u_1} → [inst : Group G] → [inst_1 : TopologicalSpace G] → SetLike (OpenSubgroup G) G
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.smulRightL_apply_apply : ∀ (𝕜 : Type u_1) (E : Type u_4) (Fₗ : Type u_7) [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup Fₗ]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 Fₗ] (x : StrongDual 𝕜 E)
  (f : Fₗ), ((ContinuousLinearMap.smulRightL 𝕜 E Fₗ) x) f = ContinuousLinearMap.smulRight x f
-- Init.Data.Vector.Lemmas
Vector.swap.congr_simp : ∀ {α : Type u_1} {n : ℕ} (xs xs_1 : Vector α n),
  xs = xs_1 →
    ∀ (i i_1 : ℕ) (e_i : i = i_1) (j j_1 : ℕ) (e_j : j = j_1) (hi : i < n) (hj : j < n),
      xs.swap i j hi hj = xs_1.swap i_1 j_1 ⋯ ⋯
-- Mathlib.Data.Prod.Basic
Prod.map_leftInverse : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [Nonempty β] [Nonempty δ] {f₁ : α → β} {g₁ : γ → δ}
  {f₂ : β → α} {g₂ : δ → γ},
  Function.LeftInverse (Prod.map f₁ g₁) (Prod.map f₂ g₂) ↔ Function.LeftInverse f₁ f₂ ∧ Function.LeftInverse g₁ g₂
-- Mathlib.Order.PiLex
/-- The lexicographic relation on `Π i : ι, β i`, where `ι` is ordered by `r`,
and each `β i` is ordered by `s`.

The `<` relation on `Lex (∀ i, β i)` is `Pi.Lex (· < ·) (· < ·)`, while the `<` relation on
`Colex (∀ i, β i)` is `Pi.Lex (· > ·) (· < ·)`.  -/
Pi.Lex : {ι : Type u_1} →
  {β : ι → Type u_2} → (ι → ι → Prop) → ({i : ι} → β i → β i → Prop) → ((i : ι) → β i) → ((i : ι) → β i) → Prop
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableWithinAt.mono : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {s t : Set M},
  s ⊆ t → MDiffAt[t] f x → MDiffAt[s] f x
-- Mathlib.Algebra.Lie.Loop
LieAlgebra.LoopAlgebra.residuePairing_apply_apply : ∀ (R : Type u_1) (A : Type u_2) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup A] [inst_4 : DistribSMul A R] [inst_5 : SMulCommClass A R R] (Φ : LinearMap.BilinForm R L)
  (f g : LieAlgebra.loopAlgebra R A L),
  ((LieAlgebra.LoopAlgebra.residuePairing R A L Φ) f) g =
    ((LieAlgebra.LoopAlgebra.toFinsupp R A L) g).sum fun a v =>
      a • (Φ (((LieAlgebra.LoopAlgebra.toFinsupp R A L) f) (-a))) v
-- Mathlib.Data.Finset.Card
Finset.exists_eq_insert_iff : ∀ {α : Type u_1} {s t : Finset α} [inst : DecidableEq α], (∃ a ∉ s, insert a s = t) ↔ s ⊆ t ∧ s.card + 1 = t.card
-- Std.Data.HashMap.Lemmas
Std.HashMap.erase_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {a : α}, ∅.erase a = ∅
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
/-- The composition `t.truncLE b ⋙ t.truncGE a`.  -/
CategoryTheory.Triangulated.TStructure.truncGELE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              CategoryTheory.Triangulated.TStructure C → ℤ → ℤ → CategoryTheory.Functor C C
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.instInhabited : {n : ℕ} → Inhabited (MvPFunctor.{u_1} n)
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.ext_iff : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] {b₁ b₂ : AffineBasis ι k P}, b₁ = b₂ ↔ ⇑b₁ = ⇑b₂
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  t.isEmpty = true → t.contains a = false
-- Init.Data.Array.Subarray
/-- Runs a monadic action on each element of a subarray, in reverse order.

The elements are processed starting at the highest index and moving down.
 -/
Subarray.forRevM : {α : Type u} → {m : Type v → Type w} → [Monad m] → (α → m PUnit.{v + 1}) → Subarray α → m PUnit.{v + 1}
-- Mathlib.Algebra.Category.ModuleCat.InjectiveDimension
ModuleCat.injectiveDimension_eq_of_semiLinearEquiv : ∀ {R : Type u} [inst : Ring R] [Small.{v, u} R] {R' : Type u'} [inst_2 : Ring R'] (eR : R ≃+* R') [Small.{v', u'} R']
  {M : ModuleCat R} {N : ModuleCat R'} (e : ↑M ≃ₛₗ[↑eR] ↑N),
  CategoryTheory.injectiveDimension M = CategoryTheory.injectiveDimension N
-- Mathlib.Data.ENat.Basic
ENat.WithBot.add_le_add_natCast_left_iff : ∀ {a b : WithBot ℕ∞} {c : ℕ}, ↑c + a ≤ ↑c + b ↔ a ≤ b
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_9.eq_4 : ∀ (motive : Std.Tactic.BVDecide.BVBinOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVBinOp.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.BVBinOp.or) (h_3 : Unit → motive Std.Tactic.BVDecide.BVBinOp.xor)
  (h_4 : Unit → motive Std.Tactic.BVDecide.BVBinOp.add) (h_5 : Unit → motive Std.Tactic.BVDecide.BVBinOp.mul)
  (h_6 : Unit → motive Std.Tactic.BVDecide.BVBinOp.udiv) (h_7 : Unit → motive Std.Tactic.BVDecide.BVBinOp.umod),
  (match Std.Tactic.BVDecide.BVBinOp.add with
    | Std.Tactic.BVDecide.BVBinOp.and => h_1 ()
    | Std.Tactic.BVDecide.BVBinOp.or => h_2 ()
    | Std.Tactic.BVDecide.BVBinOp.xor => h_3 ()
    | Std.Tactic.BVDecide.BVBinOp.add => h_4 ()
    | Std.Tactic.BVDecide.BVBinOp.mul => h_5 ()
    | Std.Tactic.BVDecide.BVBinOp.udiv => h_6 ()
    | Std.Tactic.BVDecide.BVBinOp.umod => h_7 ()) =
    h_4 ()
-- Mathlib.Algebra.Star.Unitary
Unitary.instSMulCommClassSubtypeMemSubmonoidUnitary : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : Monoid A]
  [inst_3 : StarMul R] [inst_4 : StarMul S] [inst_5 : StarMul A] [inst_6 : MulAction R A] [inst_7 : MulAction S A]
  [inst_8 : StarModule R A] [inst_9 : StarModule S A] [inst_10 : IsScalarTower R A A] [inst_11 : IsScalarTower S A A]
  [inst_12 : SMulCommClass R A A] [inst_13 : SMulCommClass S A A] [SMulCommClass R S A],
  SMulCommClass ↥(unitary R) ↥(unitary S) ↥(unitary A)
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.coe_of : ∀ (R : Type u) [inst : CommGroup R], ↑(CommGrpCat.of R) = R
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
/-- proof that the `parts` are positive  -/
Nat.Partition.parts_pos : ∀ {n : ℕ} (self : n.Partition) {i : ℕ}, i ∈ self.parts → 0 < i
-- Mathlib.Algebra.Algebra.Subalgebra.Pi
Subalgebra.pi_mono : ∀ {ι : Type u_1} {R : Type u_2} {S : ι → Type u_3} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (S i)]
  [inst_2 : (i : ι) → Algebra R (S i)] {s : Set ι} {t₁ t₂ : (i : ι) → Subalgebra R (S i)},
  (∀ i ∈ s, t₁ i ≤ t₂ i) → Subalgebra.pi s t₁ ≤ Subalgebra.pi s t₂
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.neg_insert : ∀ {α : Type u_2} [inst : InvolutiveNeg α] (a : α) (s : Set α), -insert a s = insert (-a) (-s)
-- Mathlib.Logic.Relation
Relation.onFun_map_eq_of_injective : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f : α → β},
  Function.Injective f → Function.onFun (Relation.Map r f f) f = r
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.hasSmallLocalizedShiftedHom_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (W : CategoryTheory.MorphismProperty C) (M : Type w') [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C M]
  [inst_4 : CategoryTheory.HasShift D M] (L : CategoryTheory.Functor C D) [L.IsLocalization W] [L.CommShift M]
  (X Y : C),
  CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y ↔
    ∀ (a b : M),
      Small.{w, v₂} ((CategoryTheory.shiftFunctor D a).obj (L.obj X) ⟶ (CategoryTheory.shiftFunctor D b).obj (L.obj Y))
-- Mathlib.Algebra.Homology.AlternatingConst
/-- The `i, j, k`th short complex associated to the alternating constant complex on `φ, ψ : A ⟶ A`
is `A --ψ--> A --φ--> A` when `i ~ j, j ~ k` and `j` is even.  -/
HomologicalComplex.alternatingConstScIsoEven : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (A : C) →
        {φ ψ : A ⟶ A} →
          (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0) →
            (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) →
              {c : ComplexShape ℕ} →
                [inst_2 : DecidableRel c.Rel] →
                  (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) →
                    {i j k : ℕ} →
                      c.Rel i j →
                        c.Rel j k →
                          Even j →
                            ((HomologicalComplex.alternatingConst A hOdd hEven hc).sc' i j k ≅
                              { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven })
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.exists_ne_zero_mem_ringOfIntegers_of_norm_le : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {B : ℝ},
  NumberField.mixedEmbedding.minkowskiBound K 1 ≤ MeasureTheory.volume (NumberField.mixedEmbedding.convexBodySum K B) →
    ∃ a, a ≠ 0 ∧ ↑|(Algebra.norm ℚ) ↑a| ≤ (B / ↑(Module.finrank ℚ K)) ^ Module.finrank ℚ K
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetProd_of_notMem : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β}
  [inst : CommMonoid β] [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.Kernel.IndepFun (∏ j ∈ s, f j) (f i) κ μ
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.sSup.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  [inst_2 : CategoryTheory.WellPowered.{w, v₁, u₁} C] [inst_3 : CategoryTheory.Limits.HasCoproducts C]
  [inst_4 : CategoryTheory.Limits.HasImages C] {A : C} (s : Set (CategoryTheory.Subobject A)),
  CategoryTheory.Subobject.sSup s =
    CategoryTheory.Subobject.mk (CategoryTheory.Limits.image.ι (CategoryTheory.Subobject.smallCoproductDesc s))
-- Mathlib.Topology.Constructions.SumProd
ContinuousAt.prodMk : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y} {g : X → Z} {x : X},
  ContinuousAt f x → ContinuousAt g x → ContinuousAt (fun x => (f x, g x)) x
-- Mathlib.Data.Sign.Basic
SignType.coe_pow : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : HasDistribNeg α] (a : SignType) (k : ℕ), ↑(a ^ k) = ↑a ^ k
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- An equivalence of categories induces an equivalence on over categories.  -/
CategoryTheory.Over.postEquiv : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (X : T) → (F : T ≌ D) → CategoryTheory.Over X ≌ CategoryTheory.Over (F.functor.obj X)
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.instAdditiveSimplicialObjectChainComplexNatAlternatingFaceMapComplex : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C],
  (AlgebraicTopology.alternatingFaceMapComplex C).Additive
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.zero_veq_iff : ∀ {K : Type u_2} [inst : DivisionRing K] [inst_1 : ValuativeRel K] {a : K}, a =ᵥ 0 ↔ a = 0
-- Init.Tactics
/-- `ac_nf` normalizes equalities up to application of an associative and commutative operator.
- `ac_nf` normalizes all hypotheses and the goal target of the goal.
- `ac_nf at l` normalizes at location(s) `l`, where `l` is either `*` or a
  list of hypotheses in the local context. In the latter case, a turnstile `⊢` or `|-`
  can also be used, to signify the target of the goal.
```
instance : Std.Associative (α := Nat) (.+.) := ⟨Nat.add_assoc⟩
instance : Std.Commutative (α := Nat) (.+.) := ⟨Nat.add_comm⟩

example (a b c d : Nat) : a + b + c + d = d + (b + c) + a := by
 ac_nf
 -- goal: a + (b + (c + d)) = a + (b + (c + d))
```
 -/
Lean.Parser.Tactic.tacticAc_nf_ : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
/-- The subscheme associated to an ideal sheaf.  -/
AlgebraicGeometry.Scheme.IdealSheafData.subscheme : {X : AlgebraicGeometry.Scheme} → X.IdealSheafData → AlgebraicGeometry.Scheme
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_finset_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace β] {g : β → Finset α},
  Measurable g ↔ ∀ (a : α), Measurable fun x => a ∈ g x
-- Lean.Data.Lsp.Internal
Lean.Lsp.DeclInfo.mk.inj : ∀
  {rangeStartPosLine rangeStartPosCharacter rangeEndPosLine rangeEndPosCharacter selectionRangeStartPosLine
    selectionRangeStartPosCharacter selectionRangeEndPosLine selectionRangeEndPosCharacter rangeStartPosLine_1
    rangeStartPosCharacter_1 rangeEndPosLine_1 rangeEndPosCharacter_1 selectionRangeStartPosLine_1
    selectionRangeStartPosCharacter_1 selectionRangeEndPosLine_1 selectionRangeEndPosCharacter_1 : ℕ},
  { rangeStartPosLine := rangeStartPosLine, rangeStartPosCharacter := rangeStartPosCharacter,
        rangeEndPosLine := rangeEndPosLine, rangeEndPosCharacter := rangeEndPosCharacter,
        selectionRangeStartPosLine := selectionRangeStartPosLine,
        selectionRangeStartPosCharacter := selectionRangeStartPosCharacter,
        selectionRangeEndPosLine := selectionRangeEndPosLine,
        selectionRangeEndPosCharacter := selectionRangeEndPosCharacter } =
      { rangeStartPosLine := rangeStartPosLine_1, rangeStartPosCharacter := rangeStartPosCharacter_1,
        rangeEndPosLine := rangeEndPosLine_1, rangeEndPosCharacter := rangeEndPosCharacter_1,
        selectionRangeStartPosLine := selectionRangeStartPosLine_1,
        selectionRangeStartPosCharacter := selectionRangeStartPosCharacter_1,
        selectionRangeEndPosLine := selectionRangeEndPosLine_1,
        selectionRangeEndPosCharacter := selectionRangeEndPosCharacter_1 } →
    rangeStartPosLine = rangeStartPosLine_1 ∧
      rangeStartPosCharacter = rangeStartPosCharacter_1 ∧
        rangeEndPosLine = rangeEndPosLine_1 ∧
          rangeEndPosCharacter = rangeEndPosCharacter_1 ∧
            selectionRangeStartPosLine = selectionRangeStartPosLine_1 ∧
              selectionRangeStartPosCharacter = selectionRangeStartPosCharacter_1 ∧
                selectionRangeEndPosLine = selectionRangeEndPosLine_1 ∧
                  selectionRangeEndPosCharacter = selectionRangeEndPosCharacter_1
-- Mathlib.Topology.Sheaves.Sheaf
TopCat.Presheaf.isSheaf_iso_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat} {F G : TopCat.Presheaf C X} (α : F ≅ G),
  F.IsSheaf ↔ G.IsSheaf
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.filterMap_equiv_filter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {f : (a : α) → β a → Bool},
  (↑(Std.DHashMap.Internal.Raw₀.filterMap (fun k => Option.guard fun v => f k v) m)).Equiv
    ↑(Std.DHashMap.Internal.Raw₀.filter f m)
-- Mathlib.Algebra.Star.UnitaryStarAlgAut
/-- Each unitary element `u` defines a ⋆-algebra automorphism such that
`x ↦ u * x * star u`.

This is the ⋆-algebra automorphism version of a specialized version of
`MulSemiringAction.toAlgAut`.  -/
Unitary.conjStarAlgAut : (S : Type u_1) →
  (R : Type u_2) →
    [inst : Semiring R] →
      [inst_1 : StarMul R] →
        [inst_2 : SMul S R] → [IsScalarTower S R R] → [SMulCommClass S R R] → ↥(unitary R) →* R ≃⋆ₐ[S] R
-- Init.Data.List.ControlImpl
List.flatMapMTR.loop.eq_def : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (x : List α)
  (x_1 : List (List β)),
  List.flatMapMTR.loop f x x_1 =
    match x, x_1 with
    | [], bs => pure bs.reverse.flatten
    | a :: as, bs => do
      let bs' ← f a
      List.flatMapMTR.loop f as (bs' :: bs)
-- Mathlib.RingTheory.QuasiFinite.Weakly
Algebra.WeaklyQuasiFiniteAt.instOfQuasiFiniteAt : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (q : Ideal S)
  [inst_3 : q.IsPrime] [Algebra.QuasiFiniteAt R q], Algebra.WeaklyQuasiFiniteAt R q
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.eq_prod_iff : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} {M₃ : Type w₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃]
  [inst_7 : (i : ι) → TopologicalSpace (M₁ i)] [inst_8 : TopologicalSpace M₂] [inst_9 : TopologicalSpace M₃]
  {f : ContinuousMultilinearMap R M₁ (M₂ × M₃)} {g : ContinuousMultilinearMap R M₁ M₂}
  {h : ContinuousMultilinearMap R M₁ M₃},
  f = g.prod h ↔
    (ContinuousLinearMap.fst R M₂ M₃).compContinuousMultilinearMap f = g ∧
      (ContinuousLinearMap.snd R M₂ M₃).compContinuousMultilinearMap f = h
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.evalOneₐ_of : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (x : R),
  (AdicCompletion.evalOneₐ I) ((AdicCompletion.of I R) x) = (Ideal.Quotient.mk I) x
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toLinearEquiv_trans : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} {A₃ : Type uA₃} [inst : CommSemiring R] [inst_1 : Semiring A₁]
  [inst_2 : Semiring A₂] [inst_3 : Semiring A₃] [inst_4 : Algebra R A₁] [inst_5 : Algebra R A₂] [inst_6 : Algebra R A₃]
  (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃), ↑(e₁.trans e₂) = ↑e₁ ≪≫ₗ ↑e₂
-- Mathlib.RingTheory.Int.Basic
Int.isCoprime_iff_nat_coprime : ∀ {a b : ℤ}, IsCoprime a b ↔ a.natAbs.Coprime b.natAbs
-- Mathlib.Order.Bounds.Image
mem_lowerBounds_image2_of_mem_upperBounds : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β} {a : α} {b : β},
  (∀ (b : β), Antitone (Function.swap f b)) →
    (∀ (a : α), Antitone (f a)) → a ∈ upperBounds s → b ∈ upperBounds t → f a b ∈ lowerBounds (Set.image2 f s t)
-- Init.Data.Sum.Lemmas
_private.Init.Data.Sum.Lemmas.0.Sum.getRight?.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : α ⊕ β → Sort u_3) →
      (x : α ⊕ β) → ((b : β) → motive (Sum.inr b)) → ((val : α) → motive (Sum.inl val)) → motive x
-- Mathlib.Algebra.Order.CompleteField
LinearOrderedField.cutMap_coe : ∀ {α : Type u_2} (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : LinearOrder β] [IsStrictOrderedRing β] (q : ℚ), LinearOrderedField.cutMap β ↑q = Rat.cast '' {r | ↑r < ↑q}
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.coinduced_continuous : ∀ {α : Type u_1} {β : Type u_2} [t : TopologicalSpace α] [inst : AddGroup β] (f : α → β), Continuous f
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.default_eq : ∀ {α : Type u_1} {cmp : α → α → Ordering}, default = ∅
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_mono_left : ∀ {R : Type u} [inst : Semiring R] {I J K : Ideal R}, I ≤ J → I * K ≤ J * K
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.ae_null_of_compProd_null : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {s : Set (β × γ)} {κ : ProbabilityTheory.Kernel α β} [ProbabilityTheory.IsSFiniteKernel κ]
  {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η] {a : α},
  ((κ.compProd η) a) s = 0 → (fun b => (η (a, b)) (Prod.mk b ⁻¹' s)) =ᵐ[κ a] 0
-- Mathlib.Data.Sym.Sym2
Sym2.fromRel_relationMap : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} (hr : Std.Symm r) (f : α → β),
  Sym2.fromRel ⋯ = Sym2.map f '' Sym2.fromRel hr
-- Mathlib.Data.Seq.Basic
Stream'.Seq.of_mem_append : ∀ {α : Type u} {s₁ s₂ : Stream'.Seq α} {a : α}, a ∈ s₁.append s₂ → a ∈ s₁ ∨ a ∈ s₂
-- Mathlib.Topology.Instances.AddCircle.Real
/-- The unit circle `ℝ ⧸ ℤ`.  -/
UnitAddCircle : Type
-- Std.Sat.CNF.Basic
Std.Sat.CNF.mk.injEq : ∀ {α : Type u} (clauses clauses_1 : Array (Std.Sat.CNF.Clause α)),
  ({ clauses := clauses } = { clauses := clauses_1 }) = (clauses = clauses_1)
-- Mathlib.Algebra.Polynomial.Sequence
/-- Every polynomial sequence is a basis of `R[X]`.  -/
Polynomial.Sequence.basis : {R : Type u_1} →
  [inst : Ring R] →
    (S : Polynomial.Sequence R) →
      [IsDomain R] → (∀ (i : ℕ), IsUnit (↑S i).leadingCoeff) → Module.Basis ℕ R (Polynomial R)
-- Init.Prelude
Seq.mk : {f : Type u → Type v} → ({α β : Type u} → f (α → β) → (Unit → f α) → f β) → Seq f
-- Lean.ErrorExplanation
Lean.ErrorExplanation.metadata : Lean.ErrorExplanation → Lean.ErrorExplanation.Metadata
-- Mathlib.Data.Erased
Erased.Monad : Monad Erased
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Over.instHasTerminal : ∀ {T : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} T] {X : T},
  CategoryTheory.Limits.HasTerminal (CategoryTheory.Over X)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instMonadTermElabM : Monad Lean.Elab.TermElabM
-- Mathlib.Algebra.Star.Pointwise
Set.instTrivialStar : ∀ {α : Type u_1} [inst : Star α] [TrivialStar α], TrivialStar (Set α)
-- Mathlib.Geometry.Manifold.Algebra.SMul
ContMDiffSMul.contMDiff_smul : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {H : Type u_2} {inst_1 : TopologicalSpace H} {E : Type u_3}
  {inst_2 : NormedAddCommGroup E} {inst_3 : NormedSpace 𝕜 E} {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  {inst_4 : TopologicalSpace H'} {E' : Type u_5} {inst_5 : NormedAddCommGroup E'} {inst_6 : NormedSpace 𝕜 E'}
  {I' : ModelWithCorners 𝕜 E' H'} {n : WithTop ℕ∞} {G : Type u_6} {inst_7 : TopologicalSpace G}
  {inst_8 : ChartedSpace H G} {M : Type u_7} {inst_9 : TopologicalSpace M} {inst_10 : ChartedSpace H' M}
  {inst_11 : SMul G M} [self : ContMDiffSMul I I' n G M], ContMDiff (I.prod I') I' n fun p => p.1 • p.2
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_append_eq_shiftLeft_setWidth_or : ∀ {w w' w'' : ℕ} {b : BitVec w} {b' : BitVec w'},
  BitVec.setWidth w'' (b ++ b') = BitVec.setWidth w'' b <<< w' ||| BitVec.setWidth w'' b'
-- Mathlib.LinearAlgebra.Complex.Module
realPart_I_smul : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  (a : A), realPart (Complex.I • a) = -imaginaryPart a
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.one_mem_div : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Group α] {s : Finset α}, s.Nonempty → 1 ∈ s / s
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.deriv_zero_right : ∀ (f : Ordinal.{u_1} → Ordinal.{u_1}), Ordinal.deriv f 0 = Ordinal.nfp f 0
-- Mathlib.CategoryTheory.Triangulated.TStructure.Basic
CategoryTheory.Triangulated.TStructure.shift_le : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a n n' : ℤ), a + n = n' → (t.le n).shift a = t.le n'
-- Mathlib.Algebra.Ring.Defs
NonUnitalCommSemiring.toNonUnitalNonAssocCommSemiring : {α : Type u} → [NonUnitalCommSemiring α] → NonUnitalNonAssocCommSemiring α