mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.Deriv.Mul
ContinuousLinearMap.hasDerivWithinAt_of_bilinear : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {G : Type u_1}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x : 𝕜} {s : Set 𝕜} {B : E →L[𝕜] F →L[𝕜] G} {u : 𝕜 → E}
  {v : 𝕜 → F} {u' : E} {v' : F},
  HasDerivWithinAt u u' s x →
    HasDerivWithinAt v v' s x → HasDerivWithinAt (fun x => (B (u x)) (v x)) ((B (u x)) v' + (B u') (v x)) s x
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃' : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ i₅ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (hi₄₅ : i₄ ≤ i₅) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃'._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃'._auto_3),
  CategoryTheory.CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂)
      (X'.mapFourδ₄Toδ₃' i₁ i₂ i₃ i₄ i₅ hi₁₂ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂) =
    CategoryTheory.CategoryStruct.comp (X'.mapFourδ₄Toδ₃' i₀ i₂ i₃ i₄ i₅ ⋯ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂)
      (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₅ hi₀₁ hi₁₂ hi₂₃ ⋯ n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Unlike `HasFDerivAt.finsetProd`, supports duplicate elements.
 -/
HasFDerivAt.multiset_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_5} {𝔸' : Type u_7} [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸']
  {g : ι → E → 𝔸'} {g' : ι → E →L[𝕜] 𝔸'} [inst_5 : DecidableEq ι] {u : Multiset ι} {x : E},
  (∀ i ∈ u, HasFDerivAt (fun x => g i x) (g' i) x) →
    HasFDerivAt (fun x => (Multiset.map (fun x_1 => g x_1 x) u).prod)
      (Multiset.map (fun i => (Multiset.map (fun x_1 => g x_1 x) (u.erase i)).prod • g' i) u).sum x
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Tries different modifiers, logs info messages with modifiers that worked, but stores just the first one that worked.

Remark: if `backward.grind.inferPattern` is `true`, then `.default false` is used.
The parameter `showInfo` is only taken into account when `backward.grind.inferPattern` is `true`.
 -/
Lean.Meta.Grind.Extension.addEMatchAttrAndSuggest : Lean.Meta.Grind.Extension →
  Lean.Syntax →
    Lean.Name →
      Lean.AttributeKind → Lean.Meta.Grind.SymbolPriorities → Bool → Bool → optParam Bool false → Lean.MetaM Unit
-- Mathlib.Algebra.GroupWithZero.Basic
IsReduced.mk : ∀ {R : Type u_5} [inst : Zero R] [inst_1 : Pow R ℕ], (∀ (x : R), IsNilpotent x → x = 0) → IsReduced R
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (m₁ \ m₂).size + (m₁ ∩ m₂).size = m₁.size
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.instLE : {M : Type u_1} → [AddGroup M] → [Lattice M] → LE (ArchimedeanOrder M)
-- Lean.Meta.Structure
Lean.Meta.StructProjDecl.projName : Lean.Meta.StructProjDecl → Lean.Name
-- Mathlib.Order.WithBot
WithBot.ofDual_lt_ofDual_iff : ∀ {α : Type u_1} [inst : LT α] {x y : WithBot αᵒᵈ}, WithBot.ofDual x < WithBot.ofDual y ↔ y < x
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- A variant of `Matrix.mulVecLin_submatrix` that keeps around `LinearEquiv`s.  -/
Matrix.mulVecLin_reindex : ∀ {R : Type u_1} [inst : CommSemiring R] {k : Type u_2} {l : Type u_3} {m : Type u_4} {n : Type u_5}
  [inst_1 : Fintype n] [inst_2 : Fintype l] (e₁ : k ≃ m) (e₂ : l ≃ n) (M : Matrix k l R),
  ((Matrix.reindex e₁ e₂) M).mulVecLin =
    ↑(LinearEquiv.funCongrLeft R R e₁.symm) ∘ₗ M.mulVecLin ∘ₗ ↑(LinearEquiv.funCongrLeft R R e₂)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_isEmpty : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] [IsEmpty n]
  {A : Matrix n n R}, A.det = 1
-- Lean.Data.JsonRpc
Lean.JsonRpc.RequestID.num.inj : ∀ {n n_1 : Lean.JsonNumber}, Lean.JsonRpc.RequestID.num n = Lean.JsonRpc.RequestID.num n_1 → n = n_1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_of_mem_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∪ t₂ → k ∉ t₂ → k ∈ t₁
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
/-- Every coefficient in the Cantor normal form `CNF b o` is less than `b`.  -/
Ordinal.CNF.snd_lt : ∀ {b o : Ordinal.{u}}, 1 < b → ∀ {x : Ordinal.{u} × Ordinal.{u}}, x ∈ Ordinal.CNF b o → x.2 < b
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.Iter.forIn_map : ∀ {α β β₂ γ : Type w} [inst : Std.Iterator α Id β] {ps : Std.Do.PostShape} {n : Type w → Type u_1} [inst_1 : Monad n]
  [LawfulMonad n] [inst_3 : Std.Do.WPMonad n ps] [Std.Iterators.Finite α Id] [inst_5 : Std.IteratorLoop α Id n]
  [Std.LawfulIteratorLoop α Id n] {it : Std.Iter β} {f : β → β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)}
  {P : Std.Do.Assertion ps} {Q : Std.Do.PostCond γ ps},
  ⦃P⦄ forIn it init fun out acc => g (f out) acc ⦃Q⦄ → ⦃P⦄ forIn (Std.Iter.map f it) init g ⦃Q⦄
-- Mathlib.Geometry.Manifold.Immersion
/-- A `C^n` immersion is `C^n`.  -/
Manifold.IsImmersionOfComplement.contMDiff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N},
  Manifold.IsImmersionOfComplement F I J n f → ContMDiff I J n f
-- Init.Data.Vector.Lemmas
Vector.mk_isPrefixOf_mk : ∀ {α : Type u_1} {n : ℕ} [inst : BEq α] {xs ys : Array α} (h : xs.size = n) (h' : ys.size = n),
  (Vector.mk xs h).isPrefixOf (Vector.mk ys h') = xs.isPrefixOf ys
-- Mathlib.LinearAlgebra.DirectSum.Finsupp
TensorProduct.finsuppLeft_symm_apply_single : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  [inst_7 : AddCommMonoid N] [inst_8 : Module R N] {ι : Type u_5} [inst_9 : DecidableEq ι] (i : ι) (m : M) (n : N),
  ((TensorProduct.finsuppLeft R S M N ι).symm fun₀ | i => m ⊗ₜ[R] n) = (fun₀ | i => m) ⊗ₜ[R] n
-- Mathlib.Topology.Algebra.MulAction
AddSubgroup.continuousVAdd : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : AddGroup M]
  [inst_3 : AddAction M X] [ContinuousVAdd M X] {S : AddSubgroup M}, ContinuousVAdd (↥S) X
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.RootOrdered.eq_1 : ∀ {α : Type u_1} (cmp : α → α → Ordering) (x : α), RBTree.RBNode.Path.RootOrdered cmp RBTree.RBNode.Path.root x = True
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.Hom.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C] {κ : Type u_2}
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} {E E' : CategoryTheory.SpectralSequence C c r₀}
  (hom : (r : ℤ) → (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.Hom._auto_1) → E.page r ⋯ ⟶ E'.page r ⋯)
  (comm :
    autoParam
      (∀ (r r' : ℤ) (pq : κ) (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence.Hom._auto_5)
        (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.Hom._auto_7),
        CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (hom r ⋯) pq) (E'.iso r r' pq ⋯ ⋯).hom =
          CategoryTheory.CategoryStruct.comp (E.iso r r' pq ⋯ ⋯).hom ((hom r' ⋯).f pq))
      CategoryTheory.SpectralSequence.Hom.comm._autoParam)
  (hom_1 : (r : ℤ) → (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.Hom._auto_1) → E.page r ⋯ ⟶ E'.page r ⋯)
  (comm_1 :
    autoParam
      (∀ (r r' : ℤ) (pq : κ) (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence.Hom._auto_5)
        (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.Hom._auto_7),
        CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (hom_1 r ⋯) pq) (E'.iso r r' pq ⋯ ⋯).hom =
          CategoryTheory.CategoryStruct.comp (E.iso r r' pq ⋯ ⋯).hom ((hom_1 r' ⋯).f pq))
      CategoryTheory.SpectralSequence.Hom.comm._autoParam),
  ({ hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 }) = (hom = hom_1)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.toReal_neg_iff_sign_neg : ∀ {θ : Real.Angle}, θ.toReal < 0 ↔ θ.sign = -1
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.hasCoeSubgroup.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G],
  OpenSubgroup.hasCoeSubgroup = { coe := OpenSubgroup.toSubgroup }
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueAdd.mt : ∀ {G : Type u_1} [inst : Add G] {A B : Finset G} {a0 b0 : G},
  UniqueAdd A B a0 b0 → ∀ ⦃a b : G⦄, a ∈ A → b ∈ B → a ≠ a0 ∨ b ≠ b0 → a + b ≠ a0 + b0
-- Init.Data.Array.Lemmas
Array.extract.loop.eq_1 : ∀ {α : Type u_1} (as : Array α) (i j : ℕ) (bs : Array α),
  Array.extract.loop as i j bs =
    if hlt : j < as.size then
      match i with
      | 0 => bs
      | i'.succ => Array.extract.loop as i' (j + 1) (bs.push (as.getInternal j hlt))
    else bs
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalRingHom.srange_eq_top_iff_surjective : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] {F : Type u_1} [inst_1 : FunLike F R S]
  [inst_2 : NonUnitalNonAssocSemiring S] [inst_3 : NonUnitalRingHomClass F R S] {f : F},
  NonUnitalRingHom.srange f = ⊤ ↔ Function.Surjective ⇑f
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_insert_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {v : β k}, (m.insert k v).get? k = some v
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.comm : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {A B : HomologicalComplex V c} (f : A.Hom B)
  (i j : ι), CategoryTheory.CategoryStruct.comp (f.f i) (B.d i j) = CategoryTheory.CategoryStruct.comp (A.d i j) (f.f j)
-- Mathlib.RingTheory.PiTensorProduct
PiTensorProduct.constantBaseRingEquiv_symm : ∀ {ι : Type u_1} {R : Type u_3} [inst : CommSemiring R] [inst_1 : Fintype ι] (r : R),
  (PiTensorProduct.constantBaseRingEquiv ι R).symm r = (algebraMap R (PiTensorProduct R fun x => R)) r
-- Plausible.Shrinkable
Plausible.Shrinkable.shrink : {α : Type u} → [self : Plausible.Shrinkable α] → α → List α
-- Std.Time.Time.PlainTime
/-- Converts a `PlainTime` value to the total number of hours.
 -/
Std.Time.PlainTime.toHours : Std.Time.PlainTime → Std.Time.Hour.Offset
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.comap_map_eq : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G →+ N) (H : AddSubgroup G),
  AddSubgroup.comap f (AddSubgroup.map f H) = H ⊔ f.ker
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.bot_mul_bot : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α], ⊥ * ⊥ = ⊥
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.map_eq_of_lt_sub : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedAddCommMonoidWithTop Γ₀] (v : AddValuation R Γ₀)
  {x y : R}, v x < v (y - x) → v y = v x
-- Init.Data.UInt.Basic
instShiftLeftUSize : ShiftLeft USize
-- Mathlib.Algebra.Lie.Nilpotent
LieAlgebra.maxNilpotentIdeal_le_radical : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieAlgebra.maxNilpotentIdeal R L ≤ LieAlgebra.radical R L
-- Lean.Elab.DocString
/-- Built-in docstring directives, for bootstrapping.
 -/
Lean.Doc.builtinDocDirectives : IO.Ref (Lean.NameMap (Array (Lean.Name × Lean.Doc.DocDirectiveExpander)))
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atom_abs_left : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R},
  Function.Odd W → ∀ (a b : ℤ), IsEllipticNet.atom W |a| b = IsEllipticNet.atom W a b
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
Finsupp.DegLex.single_antitone : ∀ {α : Type u_1} [inst : LinearOrder α], Antitone fun a => toDegLex fun₀ | a => 1
-- Mathlib.Algebra.Group.TypeTags.Basic
toAdd_div : ∀ {α : Type u} [inst : Sub α] (x y : Multiplicative α),
  Multiplicative.toAdd (x / y) = Multiplicative.toAdd x - Multiplicative.toAdd y
-- Mathlib.Algebra.GroupWithZero.Hom
powMonoidWithZeroHom_apply : ∀ {M₀ : Type u_6} [inst : CommMonoidWithZero M₀] {n : ℕ} (hn : n ≠ 0) (a : M₀), (powMonoidWithZeroHom hn) a = a ^ n
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.subsingleton_tensorProduct_iff_right : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_1}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.FaithfullyFlat R M],
  Subsingleton (TensorProduct R M N) ↔ Subsingleton N
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.coeff_degree_ne_zero_iff : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R},
  MvPolynomial.coeff (m.degree f) f ≠ 0 ↔ f ≠ 0
-- Lean.Elab.DocString
/-- The set of open declarations presently in force.

The `MonadLift TermElabM DocM` instance runs the lifted action in a context where these open
declarations are used, so elaboration commands that mutate this state cause it to take effect in
subsequent commands.
 -/
Lean.Doc.State.openDecls : Lean.Doc.State → List Lean.OpenDecl
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
aeSeq.measurable : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : ι → α → β}
  {μ : MeasureTheory.Measure α} (hf : ∀ (i : ι), AEMeasurable (f i) μ) (p : α → (ι → β) → Prop) (i : ι),
  Measurable (aeSeq hf p i)
-- Mathlib.Combinatorics.Additive.Energy
Finset.le_card_mul_mul_mulEnergy : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Mul α] (s t : Finset α),
  s.card ^ 2 * t.card ^ 2 ≤ (s * t).card * s.mulEnergy t
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.Quotient.restrictScalarsEquiv_symm_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (S : Type u_3)
  [inst_3 : Ring S] [inst_4 : SMul S R] [inst_5 : Module S M] [inst_6 : IsScalarTower S R M] (P : Submodule R M)
  (x : M), (Submodule.Quotient.restrictScalarsEquiv S P).symm (Submodule.Quotient.mk x) = Submodule.Quotient.mk x
-- Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
/-- The Characteristic Function of Value Distribution Theory

If `f : ℂ → E` is meromorphic and `a : WithTop E` is any value, the characteristic function of `f`
is defined as the sum of two terms: the proximity function, which quantifies how close `f` gets to
`a` on the circle `∣z∣ = r`, and the logarithmic counting function, which counts the number times
that `f` attains the value `a` inside the disk `∣z∣ ≤ r`, weighted by multiplicity.
 -/
ValueDistribution.characteristic : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → (ℂ → E) → WithTop E → ℝ → ℝ
-- Mathlib.Geometry.Manifold.ChartedSpace
/-- The preferred chart at a point `x` in a charted space `M`.  -/
chartAt : (H : Type u_5) →
  [inst : TopologicalSpace H] →
    {M : Type u_6} → [inst_1 : TopologicalSpace M] → [ChartedSpace H M] → M → OpenPartialHomeomorph M H
-- Mathlib.Algebra.Group.Torsion
IsMulTorsionFree.zpow_eq_one_iff : ∀ {G : Type u_2} [inst : Group G] [IsMulTorsionFree G] {n : ℤ} {a : G}, a ^ n = 1 ↔ a = 1 ∨ n = 0
-- Mathlib.Topology.Algebra.MulAction
AddUnits.continuousVAdd : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : AddMonoid M]
  [inst_3 : AddAction M X] [ContinuousVAdd M X], ContinuousVAdd (AddUnits M) X
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.toAddSubgroup_strictMono : ∀ {R : Type u} [inst : NonAssocRing R], StrictMono Subring.toAddSubgroup
-- Mathlib.Analysis.Convex.Basic
convex_iff_pairwise_pos : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E},
  Convex 𝕜 s ↔ s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
-- Mathlib.CategoryTheory.Idempotents.Basic
CategoryTheory.Idempotents.split_imp_of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X X' : C} (φ : X ≅ X') (p : X ⟶ X) (p' : X' ⟶ X'),
  CategoryTheory.CategoryStruct.comp p φ.hom = CategoryTheory.CategoryStruct.comp φ.hom p' →
    (∃ Y i e,
        CategoryTheory.CategoryStruct.comp i e = CategoryTheory.CategoryStruct.id Y ∧
          CategoryTheory.CategoryStruct.comp e i = p) →
      ∃ Y' i' e',
        CategoryTheory.CategoryStruct.comp i' e' = CategoryTheory.CategoryStruct.id Y' ∧
          CategoryTheory.CategoryStruct.comp e' i' = p'
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.step_filterM.match_1.eq_1 : ∀ {β : Type u_1} {n : Type u_1 → Type u_2} {f : β → n (ULift.{u_1, 0} Bool)} [inst : MonadAttach n] (out : β)
  (motive : Subtype (MonadAttach.CanReturn (f out)) → Sort u_3) (hf : MonadAttach.CanReturn (f out) { down := false })
  (h_1 : (hf : MonadAttach.CanReturn (f out) { down := false }) → motive ⟨{ down := false }, hf⟩)
  (h_2 : (hf : MonadAttach.CanReturn (f out) { down := true }) → motive ⟨{ down := true }, hf⟩),
  (match ⟨{ down := false }, hf⟩ with
    | ⟨{ down := false }, hf⟩ => h_1 hf
    | ⟨{ down := true }, hf⟩ => h_2 hf) =
    h_1 hf
-- Mathlib.FieldTheory.KummerExtension
/-- Suppose `L/K` is a finite extension of dimension `n`,
and `K` contains a primitive`n`-th root of unity.
Then `L/K` is cyclic iff
`L` is a splitting field of some irreducible polynomial of the form `Xⁿ - a : K[X]` iff
`L = K[α]` for some `αⁿ ∈ K`.
 -/
isCyclic_tfae : ∀ (K : Type u_1) (L : Type u_2) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [FiniteDimensional K L],
  (primitiveRoots (Module.finrank K L) K).Nonempty →
    [IsGalois K L ∧ IsCyclic Gal(L/K),
        ∃ a,
          Irreducible (Polynomial.X ^ Module.finrank K L - Polynomial.C a) ∧
            Polynomial.IsSplittingField K L (Polynomial.X ^ Module.finrank K L - Polynomial.C a),
        ∃ α, α ^ Module.finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤].TFAE
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.pow_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Monoid β] (n : ℕ)
  (f : MeasureTheory.SimpleFunc α β) (a : α), (f ^ n) a = f a ^ n
-- Mathlib.Analysis.Normed.Module.Ball.Action
continuousSMul_closedBall_ball : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {r : ℝ}, ContinuousSMul ↑(Metric.closedBall 0 1) ↑(Metric.ball 0 r)
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sUnion_sub : ∀ {α : Type u_2} [inst : Sub α] (S : Set (Set α)) (t : Set α), ⋃₀ S - t = ⋃ s ∈ S, s - t
-- Lean.HeadIndex
Lean.HeadIndex.sort.sizeOf_spec : sizeOf Lean.HeadIndex.sort = 1
-- Init.Data.Array.Lemmas
Array.map_set : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {xs : Array α} {i : ℕ} {h : i < xs.size} {a : α},
  Array.map f (xs.set i a h) = (Array.map f xs).set i (f a) ⋯
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_rotateLeft : ∀ {r n w : ℕ} {x : BitVec w}, (x.rotateLeft r).getMsbD n = (decide (n < w) && x.getMsbD ((r + n) % w))
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquivClass.mk : ∀ {F : Type u_1} {X : outParam (Type u_2)} {Y : outParam (Type u_3)} [inst : PseudoEMetricSpace X]
  [inst_1 : PseudoEMetricSpace Y] [inst_2 : EquivLike F X Y],
  (∀ (f : F), ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (f x) (f y) = ↑r * edist x y) → DilationEquivClass F X Y
-- Mathlib.Algebra.Category.Ring.Basic
/-- Turn a morphism in `CommSemiRingCat` back into a `RingHom`.  -/
CommSemiRingCat.Hom.hom : {R S : CommSemiRingCat} → R.Hom S → ↑R →+* ↑S
-- Lean.Meta.Tactic.Grind.Arith.EvalNum
_private.Lean.Meta.Tactic.Grind.Arith.EvalNum.0.Lean.Meta.Grind.Arith.evalNatCore : Lean.Expr → OptionT Lean.Meta.Grind.GrindM ℕ
-- Mathlib.RingTheory.DedekindDomain.Dvr
/-- Localizing a domain of Krull dimension `≤ 1` gives another ring of Krull dimension `≤ 1`.

Note that the same proof can/should be generalized to preserving any Krull dimension,
once we have a suitable definition.
 -/
Ring.DimensionLEOne.localization : ∀ {R : Type u_2} (Rₘ : Type u_3) [inst : CommRing R] [IsDomain R] [inst_2 : CommRing Rₘ] [inst_3 : Algebra R Rₘ]
  {M : Submonoid R} [IsLocalization M Rₘ], M ≤ nonZeroDivisors R → ∀ [h : Ring.DimensionLEOne R], Ring.DimensionLEOne Rₘ
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
/-- If `F` creates finite limits in any universe, then it creates finite limits.  -/
CategoryTheory.Limits.createsFiniteLimitsOfCreatesFiniteLimitsOfSize : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          ((J : Type w) →
              {x : CategoryTheory.SmallCategory J} →
                CategoryTheory.FinCategory J → CategoryTheory.CreatesLimitsOfShape J F) →
            CategoryTheory.Limits.CreatesFiniteLimits F
-- Init.Data.Float.Model.Unpacked.Basic
Float.Model.instBEqUnpackedFloat.beq : Float.Model.UnpackedFloat → Float.Model.UnpackedFloat → Bool
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Equivalence.enoughProjectives_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : C ≌ D), CategoryTheory.EnoughProjectives C ↔ CategoryTheory.EnoughProjectives D
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem_toArray_roc : ∀ {m n i : ℕ} (_h : i < (m<...=n).toArray.size), (m<...=n).toArray[i] = m + 1 + i
-- Mathlib.GroupTheory.DivisibleHull
_private.Mathlib.GroupTheory.DivisibleHull.0.«term↑ⁿ» : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject
CategoryTheory.SimplicialObject.Splitting.homotopyEquivNondegComplex_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C} (s : X.Splitting)
  [inst_1 : CategoryTheory.Preadditive C], s.homotopyEquivNondegComplex.inv = s.fromNondegComplex