mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.Spaces.CharacterSpace
WeakDual.CharacterSpace.coe_toCLM : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : NonUnitalNonAssocSemiring A] [inst_5 : TopologicalSpace A]
  [inst_6 : Module 𝕜 A] (φ : ↑(WeakDual.characterSpace 𝕜 A)), ⇑(WeakDual.CharacterSpace.toCLM φ) = ⇑φ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get?_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∪ m₂).get? k = m₂.get? k
-- Mathlib.LinearAlgebra.Complex.FiniteDimensional
/-- `Fact` version of the dimension of `ℂ` over `ℝ`, locally useful in the definition of the
circle.  -/
Complex.finrank_real_complex_fact : Fact (Module.finrank ℝ ℂ = 2)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteS.eq_6 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (a : Lean.Grind.CommRing.Expr)
  (k : ℕ), Lean.Grind.CommRing.Expr.denoteS ctx (a.pow k) = Lean.Grind.CommRing.Expr.denoteS ctx a ^ k
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.ι_totalDesc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  {c₁₂ : ComplexShape I₁₂} [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  {A : C} {i₁₂ : I₁₂} (f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂ → ((K.X i₁).X i₂ ⟶ A)) (i₁ : I₁) (i₂ : I₂)
  (hi : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂),
  CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ hi) (K.totalDesc f) = f i₁ i₂ hi
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.unmopEquiv.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  CategoryTheory.MonoidalOpposite.unmopEquiv C = (CategoryTheory.MonoidalOpposite.mopEquiv C).symm
-- Mathlib.Data.Nat.Size
Nat.size_eq_zero : ∀ {n : ℕ}, n.size = 0 ↔ n = 0
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.instBEqReason.beq : Std.Time.Reason✝ → Std.Time.Reason✝ → Bool
-- Init.Data.Vector.Lemmas
Vector.getElem?_replace : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {n : ℕ} {a b : α} {xs : Vector α n} {i : ℕ},
  (xs.replace a b)[i]? = if (xs[i]? == some a) = true then if a ∈ xs.take i then some a else some b else xs[i]?
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.inhabited' : {R : Type u_1} →
  {M : Type u_3} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Inhabited (Submodule R M)
-- Lean.Util.ForEachExprWhere
Lean.ForEachExprWhere.State.mk : Array Lean.Expr → Std.HashSet Lean.Expr → Lean.ForEachExprWhere.State
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasMulAntidiagonal.mulAntidiagonal.snd_le : ∀ {A : Type u_1} [inst : CommMonoid A] [inst_1 : PartialOrder A] [CanonicallyOrderedMul A]
  [inst_3 : Finset.HasMulAntidiagonal A] {n : A} {kl : A × A},
  kl ∈ Finset.HasMulAntidiagonal.mulAntidiagonal n → kl.2 ≤ n
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntry?.match_1.congr_eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α fun x => β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size k v l
                          (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1)))
  (size : ℕ) (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β),
  x = Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf →
    (match x with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l
      | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =>
        h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h) ≍
      h_2 size k v l
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.brange_const : ∀ {α : Type u_1} {o : Ordinal.{u_3}}, o ≠ 0 → ∀ {c : α}, (o.brange fun x x_1 => c) = {c}
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.leftMulMatrix_basisOfBasisRight_algebraMap : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) {ι : Type u_1} [inst_3 : Fintype ι]
  [inst_4 : DecidableEq ι] (b : Module.Basis ι R ↥B) (x : ↥B),
  (Algebra.leftMulMatrix (H.basisOfBasisRight H' b)) ((algebraMap (↥B) S) x) =
    (algebraMap R ↥A).mapMatrix ((Algebra.leftMulMatrix b) x)
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.isPositive_one : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  LinearMap.IsPositive 1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.PackedBitVec.mk.injEq : ∀ {w : ℕ} (bv : BitVec w) (w_1 : ℕ) (bv_1 : BitVec w_1),
  ({ w := w, bv := bv } = { w := w_1, bv := bv_1 }) = (w = w_1 ∧ bv ≍ bv_1)
-- Init.Data.Ord.Basic
instDecidableEqOrdering : DecidableEq Ordering
-- Mathlib.Topology.Order.Real
ENNReal.instT4Space : T4Space ENNReal
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Map
CategoryTheory.Functor.mapExactFunctor_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.Additive] [inst_5 : CategoryTheory.Limits.PreservesFiniteLimits F]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] [inst_7 : CategoryTheory.HasExt C]
  [inst_8 : CategoryTheory.HasExt D] (X Y : C) (n : ℕ) (R : Type u_1) [inst_9 : Ring R]
  [inst_10 : CategoryTheory.Linear R C] [inst_11 : CategoryTheory.Linear R D] [CategoryTheory.Functor.Linear R F]
  (r : R) (f : CategoryTheory.Abelian.Ext X Y n),
  CategoryTheory.Abelian.Ext.mapExactFunctor F (r • f) = r • CategoryTheory.Abelian.Ext.mapExactFunctor F f
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_insertMany_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List α} {k fallback : α}, k ∉ t → l.contains k = false → (t.insertMany l).getD k fallback = fallback
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_inter_of_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited α] {k : α}, k ∈ m₂ → (m₁ ∩ m₂).getKey! k = m₁.getKey! k
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s'_comp_ε : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (self : X.ExtraDegeneracy),
  CategoryTheory.CategoryStruct.comp self.s' (X.hom.app (Opposite.op { len := 0 })) =
    CategoryTheory.CategoryStruct.id X.right
-- Lean.Meta.Sym.LitValues
Lean.Meta.Sym.getFinValue? : Lean.Expr → OptionT Id Lean.Meta.Sym.FinValue
-- Mathlib.CategoryTheory.Adhesive.Basic
CategoryTheory.IsPushout.IsVanKampen.mono_of_mono_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
  [CategoryTheory.Mono g] {H : CategoryTheory.IsPushout f g h i}, H.IsVanKampen → CategoryTheory.Mono h
-- Init.Data.Fin.Lemmas
Fin.castAdd_natAdd : ∀ (p m : ℕ) {n : ℕ} (i : Fin n), Fin.castAdd p (Fin.natAdd m i) = Fin.cast ⋯ (Fin.natAdd m (Fin.castAdd p i))
-- Batteries.Data.List.Basic
List.product.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β),
  l₁.product l₂ = List.flatMap (fun a => List.map (Prod.mk a) l₂) l₁
-- Init.Data.SInt.Lemmas
Int32.toInt64_div_of_ne_left : ∀ (a b : Int32), a ≠ Int32.minValue → (a / b).toInt64 = a.toInt64 / b.toInt64
-- Mathlib.Algebra.Group.Submonoid.Basic
MonoidHom.ofClosureMEqTopLeft.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] {s : Set M} (f : M → N)
  (hs : Submonoid.closure s = ⊤) (h1 : f 1 = 1) (hmul : ∀ x ∈ s, ∀ (y : M), f (x * y) = f x * f y),
  MonoidHom.ofClosureMEqTopLeft f hs h1 hmul = { toFun := f, map_one' := h1, map_mul' := ⋯ }
-- Mathlib.Algebra.Regular.Basic
IsDedekindFiniteMonoid.iff_isRightRegular_of_mul_eq_one : ∀ {R : Type u_1} [inst : Monoid R], IsDedekindFiniteMonoid R ↔ ∀ (x y : R), x * y = 1 → IsRightRegular y
-- Mathlib.RingTheory.Localization.Module
LinearIndependent.localization : ∀ {R : Type u_1} (Rₛ : Type u_2) [inst : CommSemiring R] (S : Submonoid R) [inst_1 : CommSemiring Rₛ]
  [inst_2 : Algebra R Rₛ] [IsLocalization S Rₛ] {M : Type u_3} [inst_4 : AddCommMonoid M] [inst_5 : Module R M]
  [inst_6 : Module Rₛ M] [IsScalarTower R Rₛ M] {ι : Type u_5} {b : ι → M},
  LinearIndependent R b → LinearIndependent Rₛ b
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.map_smul : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] (f : E →ₗ.[R] F) (c : R) (x : ↥f.domain), ↑f (c • x) = c • ↑f x
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- "iff" version of `Summable.of_nat_of_neg_add_one`.  -/
summable_int_iff_summable_nat_and_neg_add_zero : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G] [CompleteSpace G] {f : ℤ → G},
  Summable f ↔ (Summable fun n => f ↑n) ∧ Summable fun n => f (-(↑n + 1))
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instLeftCancelMonoid : {α : Type u_1} → [LeftCancelMonoid α] → LeftCancelMonoid αᵒᵈ
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.ι_mapMap : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  {X Y : CategoryTheory.GradedObject I C} (φ : X ⟶ Y) (p : I → J) [inst_1 : X.HasMap p] [inst_2 : Y.HasMap p] (i : I)
  (j : J) (hij : p i = j),
  CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) (CategoryTheory.GradedObject.mapMap φ p j) =
    CategoryTheory.CategoryStruct.comp (φ i) (Y.ιMapObj p i j hij)
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderiv_smul : ∀ {𝕜 : 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] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {x : M} {a : M → 𝕜},
  MDiffAt a x → ∀ {g : M → F}, MDiffAt g x → d% (a • g) x = a x • d% g x + (d% a x).smulRight (g x)
-- Lean.SubExpr
Lean.SubExpr.Pos.maxChildren : ℕ
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.IsBilimit.binary_total : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {b : CategoryTheory.Limits.BinaryBicone X Y} (i : b.IsBilimit),
  CategoryTheory.CategoryStruct.comp b.fst b.inl + CategoryTheory.CategoryStruct.comp b.snd b.inr =
    CategoryTheory.CategoryStruct.id b.pt
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.natTransTruncLEOfLE_ι_app : ∀ {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) (n₀ n₁ : ℤ) (h : n₀ ≤ n₁) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.natTransTruncLEOfLE n₀ n₁ h).app X) ((t.truncLEι n₁).app X) =
    (t.truncLEι n₀).app X
-- Mathlib.Algebra.Module.End
/-- `(•)` as an `AddMonoidHom`.

This is a stronger version of `DistribMulAction.toAddMonoidEnd`  -/
Module.toAddMonoidEnd : (R : Type u_1) →
  (M : Type u_3) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → R →+* AddMonoid.End M
-- Mathlib.SetTheory.Ordinal.Notation
NONote.instWellFoundedLT : WellFoundedLT NONote
-- Lean.Parser.Types
Lean.Parser.TokenCacheEntry.mk : String.Pos.Raw → String.Pos.Raw → Lean.Syntax → Lean.Parser.TokenCacheEntry
-- Mathlib.Probability.Moments.CovarianceBilin
ProbabilityTheory.covarianceOperator_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] [inst_4 : CompleteSpace E], ProbabilityTheory.covarianceOperator 0 = 0
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.πTruncGE_naturality_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [inst_2 : e.IsTruncGE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i']
  [inst_5 : CategoryTheory.Limits.HasZeroObject C] {Z : HomologicalComplex C c'} (h : L.truncGE e ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.πTruncGE e)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncGEMap φ e) h) =
    CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp (L.πTruncGE e) h)
-- Mathlib.Algebra.Group.Equiv.Defs
/-- The `simp`-normal form to turn something into a `MulHom` is via `MulHomClass.toMulHom`.  -/
MulEquiv.toMulHom_eq_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M ≃* N), f.toMulHom = ↑f
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.equiv_of_forall_get?_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β)
  [inst_2 : LawfulBEq α], (↑m₁).WF → (↑m₂).WF → (∀ (k : α), m₁.get? k = m₂.get? k) → (↑m₁).Equiv ↑m₂
-- Init.System.IOError
IO.Error.interrupted.injEq : ∀ (filename : String) (osCode : UInt32) (details filename_1 : String) (osCode_1 : UInt32) (details_1 : String),
  (IO.Error.interrupted filename osCode details = IO.Error.interrupted filename_1 osCode_1 details_1) =
    (filename = filename_1 ∧ osCode = osCode_1 ∧ details = details_1)
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a differentiable vector field by a `C^n` function with `2 ≤ n` is
differentiable. Version on a set, but with full pullback  -/
MDifferentiableOn.mpullback_vectorField_preimage : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'}
  {V : (x : M') → TangentSpace I' x} {n : WithTop ℕ∞} {t : Set M'} [inst_11 : IsManifold I 2 M]
  [inst_12 : IsManifold I' 2 M'] [CompleteSpace E],
  MDiff[t] (T% V) →
    ContMDiff I I' n f →
      (∀ x ∈ f ⁻¹' t, (mfderiv% f x).IsInvertible) →
        2 ≤ n → MDiff[f ⁻¹' t] fun x => ⟨x, VectorField.mpullback I I' f V x⟩
-- Mathlib.GroupTheory.GroupAction.Iwasawa
/-- The Iwasawa criterion : If a quasiprimitive action of a group G on X
has an Iwasawa structure, then any normal subgroup that acts nontrivially
contains the group of commutators.  -/
MulAction.IwasawaStructure.commutator_le : ∀ {M : Type u_1} [inst : Group M] {α : Type u_2} [inst_1 : MulAction M α] (IwaS : MulAction.IwasawaStructure M α)
  [MulAction.IsQuasiPreprimitive M α] (N : Subgroup M) [nN : N.Normal],
  MulAction.fixedPoints (↥N) α ≠ Set.univ → commutator M ≤ N
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_renameEquiv : ∀ {R : Type u} {σ : Type u_1} {τ : Type u_2} [inst : CommSemiring R] (f : σ ≃ τ) (p : MvPolynomial σ R),
  ((MvPolynomial.renameEquiv R f) p).totalDegree = p.totalDegree
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.mk_ρ_inv : ∀ {C : Type u} {X : CategoryTheory.FreeMonoidalCategory C},
  ⟦CategoryTheory.FreeMonoidalCategory.Hom.ρ_inv X⟧ = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.AffineScheme.hasLimits : CategoryTheory.Limits.HasLimits AlgebraicGeometry.AffineScheme
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a : α} {v : β k}, (t.insertIfNew k v).getKey? a = if cmp k a = Ordering.eq ∧ k ∉ t then some k else t.getKey? a
-- Lean.Parser.Extension
Lean.Parser.AliasValue.binary.inj : ∀ {α : Type} {p p_1 : α → α → α}, Lean.Parser.AliasValue.binary p = Lean.Parser.AliasValue.binary p_1 → p = p_1
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.measure_inter_eq_zero_of_restrict : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  (μ.restrict s) t = 0 → μ (t ∩ s) = 0
-- Mathlib.Tactic.FunProp.Core
/-- Main `funProp` function. Returns proof of `e`.  -/
_private.Mathlib.Tactic.FunProp.Core.0.Mathlib.Meta.FunProp.main : Lean.Expr → Mathlib.Meta.FunProp.FunPropM (Option Mathlib.Meta.FunProp.Result)
-- Mathlib.Analysis.InnerProductSpace.Spectrum
/-- The mutual orthogonal complement of the eigenspaces of a self-adjoint operator on an inner
product space is an invariant subspace of the operator.  -/
LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_invariant : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E},
  T.IsSymmetric → ∀ ⦃v : E⦄, v ∈ (⨆ μ, Module.End.eigenspace T μ)ᗮ → T v ∈ (⨆ μ, Module.End.eigenspace T μ)ᗮ
-- Std.Sat.CNF.Basic
/-- Evaluating a `CNF` formula with respect to an assignment `a`.
 -/
Std.Sat.CNF.eval : {α : Type u_1} → (α → Bool) → Std.Sat.CNF α → Bool
-- Mathlib.CategoryTheory.Limits.Cones
/-- Forget the cone structure and obtain just the cone point.  -/
CategoryTheory.Limits.Cone.forget : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        (F : CategoryTheory.Functor J C) → CategoryTheory.Functor (CategoryTheory.Limits.Cone F) C
-- Mathlib.Topology.Category.Sequential
/-- The functor to `TopCat` is indeed fully faithful.  -/
Sequential.fullyFaithfulSequentialToTop : Sequential.sequentialToTop.FullyFaithful
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.pushforwardIso_I₀ : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.RespectsIso] [inst_1 : P.ContainsIdentities]
  [inst_2 : P.IsStableUnderComposition] {X Y : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) (f : X ⟶ Y)
  [inst_3 : CategoryTheory.IsIso f], (𝒰.pushforwardIso f).I₀ = 𝒰.I₀
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
OrdinalApprox.gfpApprox_anti_right : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α}, Antitone (OrdinalApprox.gfpApprox f x)
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.norm_eq_of_add_norm_lt_max : ∀ {S : Type u_1} [inst : SeminormedAddGroup S] [IsUltrametricDist S] {x y : S}, ‖x + y‖ < max ‖x‖ ‖y‖ → ‖x‖ = ‖y‖
-- Mathlib.Data.Matrix.Mul
Matrix.nonUnitalSemiring : {n : Type u_3} → {α : Type v} → [NonUnitalSemiring α] → [Fintype n] → NonUnitalSemiring (Matrix n n α)
-- Mathlib.Logic.Function.Basic
Function.surjective_comp_left_iff : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} [Nonempty α] {g : β → γ},
  (Function.Surjective fun x => g ∘ x) ↔ Function.Surjective g
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_eq_default : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {a : α}, a ∉ t → t.get! a = default
-- Mathlib.Topology.Algebra.Monoid
/-- If addition is separately continuous in `α`, then it also is in `αᵃᵒᵖ`.  -/
AddOpposite.instSeparatelyContinuousAdd : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : Add α] [SeparatelyContinuousAdd α], SeparatelyContinuousAdd αᵃᵒᵖ
-- Mathlib.Topology.Connected.LocallyPathConnected
pathConnectedSpace_iff_connectedSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyPathConnectedSpace X], PathConnectedSpace X ↔ ConnectedSpace X
-- Mathlib.GroupTheory.Index
AddSubgroup.instFiniteIndexMin : ∀ {G : Type u_1} [inst : AddGroup G] {H K : AddSubgroup G} [H.FiniteIndex] [K.FiniteIndex], (H ⊓ K).FiniteIndex
-- Mathlib.Algebra.Lie.Extension
/-- `L` is a Lie ring.  -/
LieAlgebra.Extension.instLieRing : {R : Type u_1} →
  {N : Type u_2} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing N] →
          [inst_2 : LieAlgebra R N] →
            [inst_3 : LieRing M] → [inst_4 : LieAlgebra R M] → (self : LieAlgebra.Extension R N M) → LieRing self.L
-- Mathlib.Analysis.Analytic.IsolatedZeros
/-- For a function `f` on `𝕜`, and `z₀ ∈ 𝕜`, there exists at most one `n` such that on a punctured
neighbourhood of `z₀` we have `f z = (z - z₀) ^ n • g z`, with `g` analytic and nonvanishing at
`z₀`. We formulate this with `n : ℤ`, and deduce the case `n : ℕ` later, for applications to
meromorphic functions.  -/
AnalyticAt.unique_eventuallyEq_zpow_smul_nonzero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜} {m n : ℤ},
  (∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z = (z - z₀) ^ m • g z) →
    (∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in nhdsWithin z₀ {z₀}ᶜ, f z = (z - z₀) ^ n • g z) → m = n
-- Mathlib.LinearAlgebra.Lagrange
Lagrange.eval_nodal_at_node : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_2} {s : Finset ι} {v : ι → R} {i : ι},
  i ∈ s → Polynomial.eval (v i) (Lagrange.nodal s v) = 0
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.refl_symm : ∀ {A : Type u_2} [inst : Mul A] [inst_1 : Star A], (StarMulEquiv.refl A).symm = StarMulEquiv.refl A
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.natSepDegree_le_of_dvd : ∀ {F : Type u} [inst : Field F] (f g : Polynomial F), f ∣ g → g ≠ 0 → f.natSepDegree ≤ g.natSepDegree
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.map_smul : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G] {r : 𝕜}
  (X : LeftInvariantDerivation I G) (f : ContMDiffMap I (modelWithCornersSelf 𝕜 𝕜) G 𝕜 ↑⊤), X (r • f) = r • X f
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.isDynCoverOf_zero : ∀ {X : Type u_1} {s : Set X} (T : X → X) (F : Set X) (U : SetRel X X), s.Nonempty → Dynamics.IsDynCoverOf T F U 0 s