mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- The product map of two `C^n` functions within a set at a point is `C^n`
within the product set at the product point.  -/
ContMDiffWithinAt.prodMap' : ∀ {𝕜 : 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 : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {F' : Type u_11} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F'] {G' : Type u_12}
  [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13} [inst_19 : TopologicalSpace N']
  [inst_20 : ChartedSpace G' N'] {f : M → M'} {s : Set M} {n : WithTop ℕ∞} {g : N → N'} {r : Set N} {p : M × N},
  ContMDiffWithinAt I I' n f s p.1 →
    ContMDiffWithinAt J J' n g r p.2 → ContMDiffWithinAt (I.prod J) (I'.prod J') n (Prod.map f g) (s ×ˢ r) p
-- Mathlib.Algebra.Homology.Embedding.TruncGE
/-- The natural transformation `K.πTruncGE e : K ⟶ K.truncGE e` for all `K`.  -/
ComplexShape.Embedding.πTruncGENatTrans : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        (e : c.Embedding c') →
          [inst : e.IsTruncGE] →
            (C : Type u_4) →
              [inst_1 : CategoryTheory.Category.{v_2, u_4} C] →
                [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
                  [inst_3 : CategoryTheory.Limits.HasZeroObject C] →
                    [inst_4 : CategoryTheory.CategoryWithHomology C] →
                      CategoryTheory.Functor.id (HomologicalComplex C c') ⟶ e.truncGEFunctor C
-- Mathlib.GroupTheory.Exponent
AddMonoid.addOrderOf_le_exponent : ∀ {G : Type u} [inst : AddMonoid G], AddMonoid.ExponentExists G → ∀ (g : G), addOrderOf g ≤ AddMonoid.exponent G
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min!_eq_iff_mem_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [inst_2 : Inhabited α], t ≠ ∅ → ∀ {km : α}, t.min! = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.evalSuggestSeq1Tac : Lean.Elab.Tactic.Try.TryTactic
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.one_lt_mul`.  -/
Left.one_lt_mul : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftStrictMono α] {a b : α}, 1 < a → 1 < b → 1 < a * b
-- Mathlib.LinearAlgebra.Contraction
TensorProduct.dualDistribEquivOfBasis_apply_apply : ∀ {R : Type u_7} {M : Type u_8} {N : Type u_9} {ι : Type u_10} {κ : Type u_11} [inst : DecidableEq ι]
  [inst_1 : DecidableEq κ] [inst_2 : Fintype ι] [inst_3 : Fintype κ] [inst_4 : CommSemiring R]
  [inst_5 : AddCommMonoid M] [inst_6 : AddCommMonoid N] [inst_7 : Module R M] [inst_8 : Module R N]
  (b : Module.Basis ι R M) (c : Module.Basis κ R N) (x : TensorProduct R (Module.Dual R M) (Module.Dual R N))
  (x_1 : TensorProduct R M N),
  ((TensorProduct.dualDistribEquivOfBasis b c) x) x_1 =
    (TensorProduct.lid R R) (((TensorProduct.homTensorHomMap (RingHom.id R) M N R R) x) x_1)
-- Init.Data.UInt.Lemmas
USize.ofNatLT_sub : ∀ {a b : ℕ} (ha : a < 2 ^ System.Platform.numBits) (hab : b ≤ a),
  USize.ofNatLT (a - b) ⋯ = USize.ofNatLT a ha - USize.ofNatLT b ⋯
-- Mathlib.Analysis.Real.Sqrt
NNReal.sqrt_le_sqrt : ∀ {x y : NNReal}, NNReal.sqrt x ≤ NNReal.sqrt y ↔ x ≤ y
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
/-- The `takeUntil` and `dropUntil` functions split a walk into two pieces.
The lemma `SimpleGraph.Walk.count_support_takeUntil_eq_one` specifies where this split occurs.  -/
SimpleGraph.Walk.take_spec : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support),
  (p.takeUntil u h).append (p.dropUntil u h) = p
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.SubseqResult.false.sizeOf_spec : sizeOf Lean.Grind.AC.SubseqResult.false = 1
-- Mathlib.Algebra.Homology.Homotopy
/-- homotopy is closed under composition (on the left)  -/
Homotopy.compLeft : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Preadditive V] →
        {c : ComplexShape ι} →
          {C D E : HomologicalComplex V c} →
            {f g : D ⟶ E} →
              Homotopy f g →
                (e : C ⟶ D) → Homotopy (CategoryTheory.CategoryStruct.comp e f) (CategoryTheory.CategoryStruct.comp e g)
-- Mathlib.Data.Sym.Sym2.Order
/-- The infimum of the two elements.  -/
Sym2.inf : {α : Type u_1} → [SemilatticeInf α] → Sym2 α → α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_insert_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k : α} {v : β k}, (m.insert k v).getKey? k = some k
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv'_below : ∀ {n : ℕ} {i : Fin (n + 1)} {m : Fin n}, m.castSucc < i → (finSuccEquiv' i) m.castSucc = some m
-- Lean.Elab.Attributes
Lean.Elab.Attribute.stx : Lean.Elab.Attribute → Lean.Syntax
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isSome_apply_of_contains_filterMap : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] {f : α → β → Option γ} {k : α} (h : t.WF)
  (h' : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl = true),
  (f (t.getKey k ⋯) (Std.DTreeMap.Internal.Impl.Const.get t k ⋯)).isSome = true
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- To construct an isomorphism of structured arrows,
we need an isomorphism of the objects underlying the target,
and to check that the triangle commutes.
 -/
CategoryTheory.StructuredArrow.isoMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : D} →
          {T : CategoryTheory.Functor C D} →
            {f f' : CategoryTheory.StructuredArrow S T} →
              (g : f.right ≅ f'.right) →
                autoParam (CategoryTheory.CategoryStruct.comp f.hom (T.map g.hom) = f'.hom)
                    CategoryTheory.StructuredArrow.isoMk._auto_1 →
                  (f ≅ f')
-- Mathlib.Computability.TuringMachine.Tape
_private.Mathlib.Computability.TuringMachine.Tape.0.Turing.ListBlank.append.match_1.eq_2 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (motive : List Γ → Turing.ListBlank Γ → Sort u_2) (a : Γ) (l : List Γ)
  (L : Turing.ListBlank Γ) (h_1 : (L : Turing.ListBlank Γ) → motive [] L)
  (h_2 : (a : Γ) → (l : List Γ) → (L : Turing.ListBlank Γ) → motive (a :: l) L),
  (match a :: l, L with
    | [], L => h_1 L
    | a :: l, L => h_2 a l L) =
    h_2 a l L
-- Mathlib.MeasureTheory.Function.LpSeminorm.Defs
MeasureTheory.MemLp.aemeasurable : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} [inst : ENorm ε] {μ : MeasureTheory.Measure α}
  [inst_1 : MeasurableSpace ε] [inst_2 : TopologicalSpace ε] [TopologicalSpace.PseudoMetrizableSpace ε] [BorelSpace ε]
  {f : α → ε} {p : ENNReal}, MeasureTheory.MemLp f p μ → AEMeasurable f μ
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.add_one_inj : ∀ {α β : Cardinal.{u_1}}, α + 1 = β + 1 ↔ α = β
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- If `q` and `r` are quotient and remainder in the Weierstrass division `f / g`, then they are
equal to `f /ʷ g` and `f %ʷ g`.  -/
PowerSeries.IsWeierstrassDivision.unique : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] {f g : PowerSeries A},
  (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0 →
    ∀ [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A] {q : PowerSeries A} {r : Polynomial A},
      f.IsWeierstrassDivision g q r → q = f /ʷ g ∧ r = f %ʷ g
-- Mathlib.RingTheory.Ideal.Operations
Ideal.add_eq_sup : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R}, I + J = I ⊔ J
-- Mathlib.Algebra.Regular.Basic
IsRightRegular.mul_right_eq_self_iff : ∀ {R : Type u_1} [inst : Monoid R] {a b : R}, IsRightRegular a → (b * a = a ↔ b = 1)
-- Mathlib.Order.Monotone.Defs
StrictAnti.strictAntiOn : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictAnti f → ∀ (s : Set α), StrictAntiOn f s
-- Mathlib.Algebra.Group.Hom.Defs
/-- `AddMonoidHom` down-cast to a `ZeroHom`, forgetting the additive property  -/
AddMonoidHom.coeToZeroHom : {M : Type u_4} → {N : Type u_5} → [inst : AddZero M] → [inst_1 : AddZero N] → Coe (M →+ N) (ZeroHom M N)
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.FixedParams.instToFormatInfo : Std.ToFormat Lean.Elab.FixedParams.Info
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.homologySequence_mono_shift_map_mor₂_iff : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [F.IsHomological] [inst_9 : F.ShiftSequence ℤ],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ : ℤ), CategoryTheory.Mono ((F.shift n₀).map T.mor₂) ↔ (F.shift n₀).map T.mor₁ = 0
-- Init.Data.BitVec.Lemmas
BitVec.ushiftRight_eq_extractLsb'_of_lt : ∀ {w : ℕ} {x : BitVec w} {n : ℕ} (hn : n < w), x >>> n = BitVec.cast ⋯ (0#n ++ BitVec.extractLsb' n (w - n) x)
-- Mathlib.Algebra.Homology.Monoidal
HomologicalComplex.leftUnitor'_inv_comm_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive]
  [inst_5 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] {I : Type u_2}
  [inst_6 : AddMonoid I] {c : ComplexShape I} [inst_7 : c.TensorSigns] (K : HomologicalComplex C c)
  [inst_8 : DecidableEq I]
  [inst_9 :
    ∀ (X₂ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)]
  (i j : I) {Z : C} (h : ((HomologicalComplex.tensorUnit C c).tensorObj K).X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.leftUnitor'.inv i)
      (CategoryTheory.CategoryStruct.comp (((HomologicalComplex.tensorUnit C c).tensorObj K).d i j) h) =
    CategoryTheory.CategoryStruct.comp (K.d i j) (CategoryTheory.CategoryStruct.comp (K.leftUnitor'.inv j) h)
-- Mathlib.ModelTheory.Algebra.Field.Basic
/-- The Proposition corresponding to each field axiom  -/
FirstOrder.Field.FieldAxiom.toProp : (K : Type u_2) → [Add K] → [Mul K] → [Neg K] → [Zero K] → [One K] → FirstOrder.Field.FieldAxiom → Prop
-- Mathlib.Probability.Kernel.Proper
ProbabilityTheory.Kernel.isProper_iff_inter_eq_indicator_mul : ∀ {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : ProbabilityTheory.Kernel X X},
  𝓑 ≤ 𝓧 →
    (π.IsProper ↔
      ∀ ⦃A : Set X⦄,
        MeasurableSet A → ∀ ⦃B : Set X⦄, MeasurableSet B → ∀ (x : X), (π x) (A ∩ B) = B.indicator 1 x * (π x) A)
-- Std.Net.Addr
Std.Net.instDecidableEqIPv6Addr.decEq : (x x_1 : Std.Net.IPv6Addr) → Decidable (x = x_1)
-- Mathlib.RingTheory.Etale.Weakly
/-- [Stacks Tag 092H](https://stacks.math.columbia.edu/tag/092H) ((2)) -/
Algebra.WeaklyEtale.instTensorProduct : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u_3}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [Algebra.WeaklyEtale R S], Algebra.WeaklyEtale T (TensorProduct R T S)
-- Mathlib.Algebra.Group.Action.Defs
IsCancelSMul.toIsLeftCancelSMul : ∀ {G : Type u_9} {P : Type u_10} {inst : SMul G P} [self : IsCancelSMul G P], IsLeftCancelSMul G P
-- Init.Data.Array.Sort.Lemmas
_private.Init.Data.Array.Sort.Lemmas.0.Array.MergeSort.merge_eq_listMerge : ∀ {α : Type u_1} {xs ys : Array α} {le : α → α → Bool},
  (Array.MergeSort.Internal.merge✝ xs ys le).toList = xs.toList.merge ys.toList le
-- Mathlib.MeasureTheory.Group.Integral
MeasureTheory.IntegrableOn.comp_neg_Iio : ∀ {G : Type u_4} {F : Type u_6} [inst : MeasurableSpace G] [inst_1 : NormedAddCommGroup F] {μ : MeasureTheory.Measure G}
  [inst_2 : PartialOrder G] [inst_3 : AddCommGroup G] [IsOrderedAddMonoid G] [MeasurableNeg G] [μ.IsNegInvariant]
  {c : G} {f : G → F},
  MeasureTheory.IntegrableOn f (Set.Ioi (-c)) μ → MeasureTheory.IntegrableOn (fun x => f (-x)) (Set.Iio c) μ
-- Init.Core
Ne.irrefl : ∀ {α : Sort u} {a : α}, a ≠ a → False
-- Mathlib.Data.List.Rotate
List.zipWith_rotate_distrib : ∀ {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β → γ) (l : List α) (l' : List β) (n : ℕ),
  l.length = l'.length → (List.zipWith f l l').rotate n = List.zipWith f (l.rotate n) (l'.rotate n)
-- Mathlib.RingTheory.DedekindDomain.Different
differentIdeal.eq_1 : ∀ (A : Type u_1) (B : Type u_3) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [inst_4 : IsDedekindDomain B] [inst_5 : Module.IsTorsionFree A B],
  differentIdeal A B =
    Submodule.comap (Algebra.linearMap B (FractionRing B)) (1 / Submodule.traceDual A (FractionRing A) 1)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.descTruncGT.congr_simp : ∀ {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) {X Y : C} (f f_1 : X ⟶ Y),
  f = f_1 →
    ∀ (n₀ n₁ n₁_1 : ℤ) (e_n₁ : n₁ = n₁_1) (h : n₀ + 1 = n₁) [inst_6 : t.IsGE Y n₁],
      t.descTruncGT f n₀ n₁ h = t.descTruncGT f_1 n₀ n₁_1 ⋯
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k k' : α} {f : β → β},
  (t.modify k f).getKey! k' = if cmp k k' = Ordering.eq then if k ∈ t then k else default else t.getKey! k'
-- Mathlib.Algebra.Module.Rat
map_rat_smul : ∀ {M : Type u_1} {M₂ : Type u_2} [inst : AddCommGroup M] [inst_1 : AddCommGroup M₂] [_instM : Module ℚ M]
  [_instM₂ : Module ℚ M₂] {F : Type u_3} [inst_2 : FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (c : ℚ) (x : M),
  f (c • x) = c • f x
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.comapDomain'.congr_simp : ∀ {ι : Type u} {β : ι → Type v} {κ : Type u_1} [inst : (i : ι) → Zero (β i)] (h : κ → ι) {h' h'_1 : ι → κ}
  (e_h' : h' = h'_1) (hh' : Function.LeftInverse h' h) (f f_1 : Π₀ (i : ι), β i),
  f = f_1 → DFinsupp.comapDomain' h hh' f = DFinsupp.comapDomain' h ⋯ f_1
-- Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf
/-- Gluing of sections in the closure.  -/
CategoryTheory.Precoverage.SubsheafClosure.amalgamate : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))} {Z : C}
  {R : CategoryTheory.Presieve Z},
  R ∈ K.coverings Z →
    ∀ {y : CategoryTheory.Presieve.FamilyOfElements F R},
      y.Compatible →
        (∀ ⦃W : C⦄ (r : W ⟶ Z) (hr : R r), K.SubsheafClosure 𝒮 W (y r hr)) →
          ∀ {t : F.obj (Opposite.op Z)}, y.IsAmalgamation t → K.SubsheafClosure 𝒮 Z t
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_mul' : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
  p.trailingCoeff * q.trailingCoeff ≠ 0 → (p * q).natTrailingDegree = p.natTrailingDegree + q.natTrailingDegree
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_congr_set : ∀ {𝕜 : 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] {s t : Set M} {x : M} {V W : (x : M) → TangentSpace I x},
  s =ᶠ[nhds x] t → VectorField.mlieBracketWithin I V W s x = VectorField.mlieBracketWithin I V W t x
-- Mathlib.RepresentationTheory.Basic
Representation.isTrivial_def : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) [ρ.IsTrivial] (g : G), ρ g = LinearMap.id
-- Lean.Environment
/-- Add declaration to kernel without type checking it.

**WARNING** This function is meant for temporarily working around kernel performance issues.
It compromises soundness because, for example, a buggy tactic may produce an invalid proof,
and the kernel will not catch it if the new option is set to true.
 -/
Lean.Kernel.Environment.addDeclWithoutChecking : Lean.Kernel.Environment → Lean.Declaration → Except Lean.Kernel.Exception Lean.Kernel.Environment
-- Mathlib.Data.Int.Cast.Lemmas
Commute.intCast_right : ∀ {α : Type u_3} [inst : NonAssocRing α] {a : α} {n : ℤ}, Commute a ↑n
-- Mathlib.CategoryTheory.Subobject.NoetherianObject
CategoryTheory.isNoetherianObject_iff_isEventuallyConstant : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.IsNoetherianObject X ↔
    ∀ (F : CategoryTheory.Functor ℕ (CategoryTheory.MonoOver X)), CategoryTheory.IsFiltered.IsEventuallyConstant F
-- Mathlib.NumberTheory.PrimeCounting
Nat.monotone_primeCounting : Monotone Nat.primeCounting
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- An action is preprimitive iff it is `1`-preprimitive.  -/
MulAction.is_one_preprimitive_iff : ∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α],
  MulAction.IsMultiplyPreprimitive M α 1 ↔ MulAction.IsPreprimitive M α
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesOnBall.pi : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_9} [inst_3 : Fintype ι] {e : E} {Fm : ι → Type u_10}
  [inst_4 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (Fm i)] {f : (i : ι) → E → Fm i}
  {r : ENNReal} {p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)},
  (∀ (i : ι), HasFPowerSeriesOnBall (f i) (p i) e r) →
    0 < r → HasFPowerSeriesOnBall (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) e r
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
_private.Mathlib.Algebra.SkewMonoidAlgebra.Basic.0.SkewMonoidAlgebra.smul.eq_1 : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {S : Type u_3} [inst_1 : SMulZeroClass S k] (x : S) (b : G →₀ k),
  SkewMonoidAlgebra.smul✝ x { coeff := b } = { coeff := x • b }
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIdsM.State.mk.inj : ∀ {equalMVarIds : Std.HashMap Lean.MVarId Lean.MVarId} {equalLMVarIds : Std.HashMap Lean.LMVarId Lean.LMVarId}
  {leftUnassignedMVarValues rightUnassignedMVarValues : Std.HashMap Lean.MVarId Lean.Expr}
  {equalMVarIds_1 : Std.HashMap Lean.MVarId Lean.MVarId} {equalLMVarIds_1 : Std.HashMap Lean.LMVarId Lean.LMVarId}
  {leftUnassignedMVarValues_1 rightUnassignedMVarValues_1 : Std.HashMap Lean.MVarId Lean.Expr},
  { equalMVarIds := equalMVarIds, equalLMVarIds := equalLMVarIds, leftUnassignedMVarValues := leftUnassignedMVarValues,
        rightUnassignedMVarValues := rightUnassignedMVarValues } =
      { equalMVarIds := equalMVarIds_1, equalLMVarIds := equalLMVarIds_1,
        leftUnassignedMVarValues := leftUnassignedMVarValues_1,
        rightUnassignedMVarValues := rightUnassignedMVarValues_1 } →
    equalMVarIds = equalMVarIds_1 ∧
      equalLMVarIds = equalLMVarIds_1 ∧
        leftUnassignedMVarValues = leftUnassignedMVarValues_1 ∧ rightUnassignedMVarValues = rightUnassignedMVarValues_1
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.weightedSMul_union : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (s t : Set α),
  MeasurableSet s →
    MeasurableSet t →
      μ s ≠ ⊤ →
        μ t ≠ ⊤ →
          Disjoint s t →
            MeasureTheory.weightedSMul μ (s ∪ t) = MeasureTheory.weightedSMul μ s + MeasureTheory.weightedSMul μ t
-- Mathlib.Algebra.Homology.Augment
CochainComplex.augmentTruncate_hom_f_succ : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : CochainComplex V ℕ) (i : ℕ), C.augmentTruncate.hom.f (i + 1) = CategoryTheory.CategoryStruct.id (C.X (i + 1))
-- Mathlib.Topology.UniformSpace.Ascoli
/-- A version of the **Arzela-Ascoli theorem**.

Let `X, ι` be topological spaces, `𝔖` a covering of `X` by compact subsets, `α` a uniform space,
and `F : ι → (X → α)`. Assume that:
* `F`, viewed as a function `ι → (X →ᵤ[𝔖] α)`, is a closed embedding (in other words, `ι`
  identifies to a closed subset of `X →ᵤ[𝔖] α` through `F`)
* `F` is equicontinuous on each `K ∈ 𝔖`
* For all `x`, the range of `i ↦ F i x` is contained in some fixed compact subset.

Then `ι` is compact.  -/
ArzelaAscoli.compactSpace_of_isClosedEmbedding : ∀ {ι : Type u_1} {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] {F : ι → X → α}
  [inst_2 : TopologicalSpace ι] {𝔖 : Set (Set X)},
  (∀ K ∈ 𝔖, IsCompact K) →
    Topology.IsClosedEmbedding (⇑(UniformOnFun.ofFun 𝔖) ∘ F) →
      (∀ K ∈ 𝔖, EquicontinuousOn F K) → (∀ K ∈ 𝔖, ∀ x ∈ K, ∃ Q, IsCompact Q ∧ ∀ (i : ι), F i x ∈ Q) → CompactSpace ι
-- Lean.Level
Lean.Level.quote : Lean.Level → optParam ℕ 0 → optParam Bool true → (Lean.LMVarId → Option ℕ) → Lean.Syntax.Level
-- Mathlib.RingTheory.Algebraic.Basic
IsAlgebraic.inv_iff : ∀ {R : Type u} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] {x : K},
  IsAlgebraic R x⁻¹ ↔ IsAlgebraic R x
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.instInsert : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → Insert α (Ordnode α)
-- Lean.Meta.Tactic.Grind.EqResolution
Lean.Meta.Grind.TopSort.State.mk.inj : ∀ {tempMark permMark : Std.HashSet Lean.Expr} {result : Array Lean.Expr} {tempMark_1 permMark_1 : Std.HashSet Lean.Expr}
  {result_1 : Array Lean.Expr},
  { tempMark := tempMark, permMark := permMark, result := result } =
      { tempMark := tempMark_1, permMark := permMark_1, result := result_1 } →
    tempMark = tempMark_1 ∧ permMark = permMark_1 ∧ result = result_1
-- Lean.Parser.Term.Basic
Lean.Parser.Term.structInstField : Lean.Parser.Parser
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- The restriction of scalars by the identity morphism identifies to the
identity functor.  -/
ModuleCat.restrictScalarsId : (R : Type u₁) → [inst : Ring R] → ModuleCat.restrictScalars (RingHom.id R) ≅ CategoryTheory.Functor.id (ModuleCat R)
-- Init.Data.List.Sublist
List.Sublist.reverse : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁.reverse.Sublist l₂.reverse
-- Mathlib.Topology.Inseparable
SeparationQuotient.inseparableSetoid_eq_top_iff : ∀ {α : Type u_4} [inst : TopologicalSpace α], inseparableSetoid α = ⊤ ↔ IndiscreteTopology α
-- Mathlib.MeasureTheory.Function.LpSeminorm.Prod
MeasureTheory.MemLp.comp_fst : ∀ {α : Type u_1} {β : Type u_2} {ε : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {μ : MeasureTheory.Measure α} {p : ENNReal} {f : α → ε},
  MeasureTheory.MemLp f p μ →
    ∀ (ν : MeasureTheory.Measure β) [MeasureTheory.IsFiniteMeasure ν], MeasureTheory.MemLp (fun x => f x.1) p (μ.prod ν)