mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- A multivariate polynomial is weighted homogeneous of weighted degree zero if and only if
its weighted total degree is equal to zero.  -/
MvPolynomial.isWeightedHomogeneous_zero_iff_weightedTotalDegree_eq_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : LinearOrder M] [inst_3 : OrderBot M] [CanonicallyOrderedAdd M] {w : σ → M} {p : MvPolynomial σ R},
  MvPolynomial.IsWeightedHomogeneous w p 0 ↔ MvPolynomial.weightedTotalDegree w p = 0
-- Aesop.Options.Public
/-- When Aesop fails to prove a goal, it reports the goals that remain after safe
rules have been applied exhaustively to the root goal, the safe
descendants of the root goal, and so on (i.e., after the "safe prefix" of the
search tree has been unfolded). However, it is possible for the search to fail
before the safe prefix has been completely generated. In this case, Aesop
expands the safe prefix after the fact. This option limits the number of
additional rule applications generated during this process. 0 means no limit.
 -/
Aesop.Options.maxSafePrefixRuleApplications : Aesop.Options → ℕ
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
/-- Consider a differentiable map `v : M → E₁` to a vector bundle, over a basemap `b₁ : M → B₁`, and
another basemap `b₂ : M → B₂`. Given linear maps `ϕ m : E₁ (b₁ m) → E₂ (b₂ m)` depending
differentiably on `m`, one can apply `ϕ m` to `g m`, and the resulting map is differentiable.

Note that the differentiability of `ϕ` cannot be always be stated as differentiability of a map
into a manifold, as the pullback bundles `b₁ *ᵖ E₁` and `b₂ *ᵖ E₂` only make sense when `b₁`
and `b₂` are globally smooth, but we want to apply this lemma with only local information.
Therefore, we formulate it using differentiability of `ϕ` read in coordinates.

Version for `MDifferentiableAt`. We also give a version for `MDifferentiableWithinAt`,
but no version for `MDifferentiableOn` or `MDifferentiable` as our assumption, written
in coordinates, only makes sense around a point.
 -/
MDifferentiableAt.clm_apply_of_inCoordinates : ∀ {𝕜 : Type u_1} {F₁ : Type u_2} {F₂ : Type u_3} {B₁ : Type u_4} {B₂ : Type u_5} {M : Type u_6} {E₁ : B₁ → Type u_7}
  {E₂ : B₂ → Type u_8} [inst : NontriviallyNormedField 𝕜] [inst_1 : (x : B₁) → AddCommGroup (E₁ x)]
  [inst_2 : (x : B₁) → Module 𝕜 (E₁ x)] [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_6 : (x : B₁) → TopologicalSpace (E₁ x)]
  [inst_7 : (x : B₂) → AddCommGroup (E₂ x)] [inst_8 : (x : B₂) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂]
  [inst_10 : NormedSpace 𝕜 F₂] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B₂) → TopologicalSpace (E₂ x)] {EB₁ : Type u_9} [inst_13 : NormedAddCommGroup EB₁]
  [inst_14 : NormedSpace 𝕜 EB₁] {HB₁ : Type u_10} [inst_15 : TopologicalSpace HB₁] {IB₁ : ModelWithCorners 𝕜 EB₁ HB₁}
  [inst_16 : TopologicalSpace B₁] [inst_17 : ChartedSpace HB₁ B₁] {EB₂ : Type u_11} [inst_18 : NormedAddCommGroup EB₂]
  [inst_19 : NormedSpace 𝕜 EB₂] {HB₂ : Type u_12} [inst_20 : TopologicalSpace HB₂] {IB₂ : ModelWithCorners 𝕜 EB₂ HB₂}
  [inst_21 : TopologicalSpace B₂] [inst_22 : ChartedSpace HB₂ B₂] {EM : Type u_13} [inst_23 : NormedAddCommGroup EM]
  [inst_24 : NormedSpace 𝕜 EM] {HM : Type u_14} [inst_25 : TopologicalSpace HM] {IM : ModelWithCorners 𝕜 EM HM}
  [inst_26 : TopologicalSpace M] [inst_27 : ChartedSpace HM M] [inst_28 : FiberBundle F₁ E₁]
  [inst_29 : VectorBundle 𝕜 F₁ E₁] [inst_30 : FiberBundle F₂ E₂] [inst_31 : VectorBundle 𝕜 F₂ E₂] {b₁ : M → B₁}
  {b₂ : M → B₂}, ⋯
-- Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
/-- If `s : Set α` is nonempty and its complement has at least two elements,
then `stabilizer (alternatingGroup α) s ≠ ⊤`.  -/
alternatingGroup.stabilizer_ne_top : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Set α},
  s.Nonempty → sᶜ.Nontrivial → MulAction.stabilizer (↥(alternatingGroup α)) s ≠ ⊤
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.coe_coe : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Star A] [inst_4 : Semiring B] [inst_5 : Algebra R B] [inst_6 : Star B] {F : Type u_7}
  [inst_7 : FunLike F A B] [inst_8 : AlgHomClass F R A B] [inst_9 : StarHomClass F A B] (f : F), ⇑↑f = ⇑f
-- Mathlib.Data.Set.Lattice.Image
Set.image_eq_iUnion : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), f '' s = ⋃ i ∈ s, {f i}
-- Mathlib.Order.WithBot
WithTop.total_le : ∀ {α : Type u_1} [inst : LE α] [Std.Total fun x1 x2 => x1 ≤ x2], Std.Total fun x1 x2 => x1 ≤ x2
-- Mathlib.GroupTheory.Index
AddSubgroup.relIndex_eq_zero_of_le_left : ∀ {G : Type u_1} [inst : AddGroup G] {H K L : AddSubgroup G}, H ≤ K → K.relIndex L = 0 → H.relIndex L = 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.min_one : ∀ {α : Type u_2} [inst : One α] [inst_1 : LinearOrder α], Finset.min 1 = 1
-- Mathlib.MeasureTheory.Measure.AddContent
_private.Mathlib.MeasureTheory.Measure.AddContent.0.MeasureTheory.AddContent.supClosureFun_apply_of_mem : ∀ {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [inst : AddCommMonoid G],
  MeasureTheory.IsSetSemiring C →
    ∀ (m : MeasureTheory.AddContent G C) {s : Set α}, s ∈ C → MeasureTheory.AddContent.supClosureFun✝ m s = m s
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.group_smul_def : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G)
  (w : HNNExtension.NormalWord d), g • w = { head := g * w.head, toList := w.toList, chain := ⋯, mem_set := ⋯ }
-- Init.Core
Exists.elim : ∀ {α : Sort u} {p : α → Prop} {b : Prop}, (∃ x, p x) → (∀ (a : α), p a → b) → b
-- Std.Data.ExtTreeSet.Lemmas
_private.Std.Data.ExtTreeSet.Lemmas.0.Std.ExtTreeSet.ext : ∀ {α : Type u} {cmp : α → α → Ordering} {t t' : Std.ExtTreeSet α cmp}, t.inner = t'.inner → t = t'
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.descResidueField_stalkClosedPointTo_fromSpecResidueField : ∀ (K : Type u) [inst : Field K] (X : AlgebraicGeometry.Scheme) (f : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Spec.map
        (AlgebraicGeometry.Scheme.descResidueField (AlgebraicGeometry.Scheme.stalkClosedPointTo f)))
      (X.fromSpecResidueField (f (IsLocalRing.closedPoint K))) =
    f
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functorInclusion_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) (x : Cᵒᵖ),
  S.functorInclusion.app x = TypeCat.ofHom fun f => ↑f
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.replaceFun_seq : ∀ {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)}
  (ms : Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl)) (f : ℝ → ℝ),
  (ms.replaceFun f).seq = ms.seq
-- Lean.Syntax
Lean.Syntax.isEscapedAntiquot : Lean.Syntax → Bool
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.introNext : Lean.Meta.Grind.Goal → ℕ → Lean.Meta.Grind.GrindM Lean.Meta.Grind.IntroResult✝
-- Mathlib.Algebra.MvPolynomial.Counit
MvPolynomial.counit_surjective : ∀ (R : Type u_3) [inst : CommRing R], Function.Surjective ⇑(MvPolynomial.counit R)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.coe_toContinuousAffineMap : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂), ⇑e.toContinuousAffineMap = ⇑e
-- Mathlib.MeasureTheory.Measure.DiracProba
CompletelyRegularSpace.exists_BCNN : ∀ {X : Type u_1} [inst : TopologicalSpace X] [CompletelyRegularSpace X] {K : Set X},
  IsClosed K → ∀ {x : X}, x ∉ K → ∃ f, f x = 1 ∧ ∀ y ∈ K, f y = 0
-- Mathlib.Order.InitialSeg
/-- Given a well order `s`, there is at most one initial segment embedding of `r` into `s`.  -/
InitialSeg.instSubsingletonOfIsWellOrder : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder β s], Subsingleton (InitialSeg r s)
-- Mathlib.NumberTheory.LegendreSymbol.Complex
_private.Mathlib.NumberTheory.LegendreSymbol.Complex.0.AddChar.ringChar_ne : ∀ (F : Type u_1) [inst : Field F] [Finite F], ringChar ℂ ≠ ringChar F
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isLittleO_norm_right`. -/
Asymptotics.IsLittleO.of_norm_right : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α}, (f =o[l] fun x => ‖g' x‖) → f =o[l] g'
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
AEMeasurable.ccosh : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ},
  AEMeasurable f μ → AEMeasurable (fun x => Complex.cosh (f x)) μ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_le_size_insertMany : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} {ρ : Type w}
  [inst : ForIn Id ρ (α × β)] [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {l : ρ}, m.size ≤ (m.insertMany l).size
-- Lean.Meta.Tactic.Backtrack
_private.Lean.Meta.Tactic.Backtrack.0.Lean.Meta.Tactic.Backtrack.Backtrack.run.match_1.eq_2 : ∀ (motive : Option (List Lean.MVarId) → Sort u_1) (l : List Lean.MVarId) (h_1 : Unit → motive none)
  (h_2 : (l : List Lean.MVarId) → motive (some l)),
  (match some l with
    | none => h_1 ()
    | some l => h_2 l) =
    h_2 l
-- Lean.Meta.Tactic.Grind.Arith.FieldNormNum
_private.Lean.Meta.Tactic.Grind.Arith.FieldNormNum.0.Lean.Meta.Grind.Arith.FieldNormNum.mkIntCastInst : Lean.Meta.Grind.Arith.FieldNormNum.M✝ Lean.Expr
-- Mathlib.Analysis.Normed.Module.Convex
Convex.thickening : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {s : Set E},
  Convex ℝ s → ∀ (δ : ℝ), Convex ℝ (Metric.thickening δ s)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_add_left : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] (a : α),
  UniformContinuous fun b => a + b
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : Inhabited α] {k k' : α}, (k == k') = true → m.get! k = m.get! k'
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- The isomorphism `E ⧸ S.rightHom.ker ≃* G` induced by `S.rightHom`  -/
GroupExtension.quotientKerRightHomEquivRight : {N : Type u_1} →
  {G : Type u_2} →
    [inst : Group N] →
      [inst_1 : Group G] → {E : Type u_3} → [inst_2 : Group E] → (S : GroupExtension N E G) → E ⧸ S.rightHom.ker ≃* G
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.coe_pow : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℕ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- A characterization lemma for the addition on the Ore localization,
allowing for a choice of Ore minuend and Ore subtrahend.  -/
AddOreLocalization.oreSub_add_char : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] (r₁ r₂ : R)
  (s₁ s₂ : ↥S) (r' : R) (s' : ↥S), ↑s' + r₁ = r' + ↑s₂ → r₁ -ₒ s₁ + (r₂ -ₒ s₂) = r' + r₂ -ₒ (s' + s₁)
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.center_toSubsemigroup : ∀ (R : Type u) [inst : NonUnitalNonAssocSemiring R],
  (NonUnitalSubsemiring.center R).toSubsemigroup = Subsemigroup.center R
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.functorMk_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : CategoryTheory.Functor J C} (mor₁ : obj₁ ⟶ obj₂)
  (mor₂ : obj₂ ⟶ obj₃) (mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)) (j : J),
  (CategoryTheory.Pretriangulated.Triangle.functorMk mor₁ mor₂ mor₃).obj j =
    CategoryTheory.Pretriangulated.Triangle.mk (mor₁.app j) (mor₂.app j) (mor₃.app j)
-- Mathlib.RingTheory.Perfection
PreTilt.map_eq_zero : ∀ {K : Type u₁} [inst : Field K] {v : Valuation K NNReal} {O : Type u₂} [inst_1 : CommRing O] [inst_2 : Algebra O K]
  (hv : v.Integers O) {p : ℕ} [inst_3 : Fact (Nat.Prime p)] [inst_4 : Fact ¬IsUnit ↑p] {f : PreTilt O p},
  (PreTilt.val K v O hv p) f = 0 ↔ f = 0
-- Init.Data.List.Basic
List.drop_succ_cons : ∀ {α : Type u} {a : α} {l : List α} {i : ℕ}, List.drop (i + 1) (a :: l) = List.drop i l
-- Mathlib.Algebra.Group.Subgroup.Order
AddEquiv.strictMono_symm : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddCommMonoid G] [inst_1 : LinearOrder G] [inst_2 : AddCommMonoid G']
  [inst_3 : Preorder G'] {e : G ≃+ G'}, StrictMono ⇑e → StrictMono ⇑e.symm
-- Mathlib.GroupTheory.IndexNormal
/-- A subgroup of a finite group whose index is the smallest prime factor is normal.

Note : if `G` is infinite, then `Nat.card G = 0` and `(Nat.card G).minFac = 2`  -/
Subgroup.normal_of_index_eq_minFac_card : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index = (Nat.card G).minFac → H.Normal
-- Mathlib.Order.DirectedInverseSystem
InverseSystem.piEquivSucc_self : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [inst : LinearOrder ι] [inst_1 : SuccOrder ι]
  (equiv : (j : ↑(Set.Iic i)) → F ↑j ≃ InverseSystem.piLT X ↑j) (e : F (Order.succ i) ≃ F i × X i) (hi : ¬IsMax i)
  {x : F ↑⟨Order.succ i, ⋯⟩}, (InverseSystem.piEquivSucc equiv e hi ⟨Order.succ i, ⋯⟩) x ⟨i, ⋯⟩ = (e x).2
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_erase_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k fallback : α}, (m.erase k).getKeyD k fallback = fallback
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.codiscreteEquiv_symm_apply_as : ∀ {α : Type u} (as : α), (CategoryTheory.codiscreteEquiv.symm as).as = as
-- Mathlib.Order.Partition.Equipartition
Finpartition.IsEquipartition.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s),
  P.IsEquipartition = (↑P.parts).EquitableOn Finset.card
-- Init.ShareCommon
/-- A more restrictive but efficient max sharing primitive.

Remark: it optimizes the number of RC operations, and the strategy for caching results.
 -/
ShareCommon.shareCommon' : {α : Sort u_1} → α → α
-- Init.Data.Vector.Lemmas
Vector.mem_of_getElem : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {h : i < n} {a : α}, xs[i] = a → a ∈ xs
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
ProbabilityTheory.BrownianReal.isGaussian_projectiveFamily : ∀ (I : Finset NNReal), ProbabilityTheory.IsGaussian (ProbabilityTheory.BrownianReal.projectiveFamily I)
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.Weight.toLinear.congr_simp : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : LieModule.LinearWeights R L M] (χ χ_1 : LieModule.Weight R L M),
  χ = χ_1 → LieModule.Weight.toLinear R L M χ = LieModule.Weight.toLinear R L M χ_1
-- Mathlib.Algebra.Group.ModEq
/-- **Alias** of the forward direction of `AddCommGroup.ModEq.add_iff_right`. -/
AddCommGroup.ModEq.add_right_cancel : ∀ {M : Type u_1} [inst : AddCancelCommMonoid M] {a b c d p : M},
  c ≡ d [PMOD p] → a + c ≡ b + d [PMOD p] → a ≡ b [PMOD p]
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.contains_iff : ∀ {α : outParam (Type u)} {β : Type v} [self : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] (c : β)
  (l : Std.Sat.Literal α),
  Std.Tactic.BVDecide.LRAT.Internal.Clause.contains c l = true ↔ l ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.maxD_eq_getLastD_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {fallback : α},
  t.maxD fallback = t.toList.getLastD fallback
-- Mathlib.Order.Basic
forall_lt_iff_le : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, (∀ ⦃c : α⦄, c < a → c < b) ↔ a ≤ b
-- Mathlib.Data.Set.Function
Set.EqOn.union : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {f₁ f₂ : α → β},
  Set.EqOn f₁ f₂ s₁ → Set.EqOn f₁ f₂ s₂ → Set.EqOn f₁ f₂ (s₁ ∪ s₂)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.instInhabitedHom : {J : CategoryTheory.Limits.MultispanShape} → {a : CategoryTheory.Limits.WalkingMultispan J} → Inhabited (a.Hom a)
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.eq_zero_iff : ∀ {σ : Type u_1} (m : MonomialOrder σ) {a : m.syn}, a = 0 ↔ a ≤ 0
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.skipPrefix?_eq_skipPrefix?_decide : ∀ {p : Char → Prop} [inst : DecidablePred p],
  String.Slice.Pattern.ForwardPattern.skipPrefix? p =
    String.Slice.Pattern.ForwardPattern.skipPrefix? fun x => decide (p x)
-- Std.Time.DateTime.PlainDateTime
/-- Getter for the `Weekday` inside of a `PlainDateTime`.
 -/
Std.Time.PlainDateTime.weekday : Std.Time.PlainDateTime → Std.Time.Weekday
-- Mathlib.Analysis.Normed.Ring.Basic
normHom_apply : ∀ {α : Type u_2} [inst : SeminormedRing α] [inst_1 : NormOneClass α] [inst_2 : NormMulClass α] (x : α), normHom x = ‖x‖
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.toPolyS.match_1.splitter : (motive : Lean.Grind.CommRing.Expr → Sort u_1) →
  (a : Lean.Grind.CommRing.Expr) →
    ((n : ℤ) → motive (Lean.Grind.CommRing.Expr.num n)) →
      ((x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x)) →
        ((x : Lean.Grind.CommRing.Expr) →
            (∀ (n : ℤ), x = Lean.Grind.CommRing.Expr.num n → False) →
              (∀ (x_2 : Lean.Grind.CommRing.Var), x = Lean.Grind.CommRing.Expr.var x_2 → False) → motive x) →
          motive a
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.mem_ae_of_mem_ae_map : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β},
  AEMeasurable f μ → ∀ {s : Set β}, s ∈ MeasureTheory.ae (MeasureTheory.Measure.map f μ) → f ⁻¹' s ∈ MeasureTheory.ae μ
-- Mathlib.Data.List.Permutation
Nat.factorial.eq_2 : ∀ (n : ℕ), n.succ.factorial = n.succ * n.factorial
-- Mathlib.Data.Set.SymmDiff
Set.bihimp_def : ∀ {α : Type u} {s t : Set α}, bihimp s t = (s ∪ tᶜ) ∩ (t ∪ sᶜ)
-- Mathlib.Topology.EMetricSpace.Defs
/-- Characterization of the elements of the uniformity in terms of the extended distance  -/
mem_uniformity_edist : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s : Set (α × α)},
  s ∈ uniformity α ↔ ∃ ε > 0, ∀ {a b : α}, edist a b < ε → (a, b) ∈ s
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp_I₀ : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (S : AlgebraicGeometry.Scheme)
  [inst : P.IsStableUnderBaseChange] [inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P]
  {X W : AlgebraicGeometry.Scheme} (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  (f : W ⟶ X) [inst_2 : W.Over S] [inst_3 : X.Over S] [inst_4 : AlgebraicGeometry.Scheme.Cover.Over S 𝒰]
  [inst_5 : AlgebraicGeometry.Scheme.Hom.IsOver f S] {Q : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  [inst_6 : Q.HasOfPostcompProperty Q] [inst_7 : Q.IsStableUnderBaseChange] [inst_8 : Q.IsStableUnderComposition]
  (hX : Q (X ↘ S)) (hW : Q (W ↘ S)) (hQ : ∀ (j : 𝒰.I₀), Q (𝒰.X j ↘ S)),
  (AlgebraicGeometry.Scheme.Cover.pullbackCoverOverProp S 𝒰 f hX hW hQ).I₀ = 𝒰.I₀
-- Lean.Util.NumObjs
_private.Lean.Util.NumObjs.0.Lean.Expr.numObjs.unsafe_impl_2 : Lean.Expr → ℕ
-- Mathlib.Order.Defs.Unbundled
IsStrictWeakOrder.mk : ∀ {α : Sort u_1} {lt : α → α → Prop} [toIsStrictOrder : IsStrictOrder α lt],
  (∀ (a b c : α), ¬lt a b ∧ ¬lt b a → ¬lt b c ∧ ¬lt c b → ¬lt a c ∧ ¬lt c a) → IsStrictWeakOrder α lt
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.TransvectionStruct.mk.congr_simp : ∀ {n : Type u_1} {R : Type u₂} (i i_1 : n) (e_i : i = i_1) (j j_1 : n) (e_j : j = j_1) (hij : i ≠ j) (c c_1 : R),
  c = c_1 → { i := i, j := j, hij := hij, c := c } = { i := i_1, j := j_1, hij := ⋯, c := c_1 }
-- Lean.Meta.Tactic.Grind.Util
/-- Converts nested `Expr.proj`s into projection applications if possible.
 -/
Lean.Meta.Grind.foldProjs : Lean.Expr → Lean.MetaM Lean.Expr
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.allDiffAuxAux.congr_simp : ∀ {α : Type u} [inst : BEq α] (as as_1 : Array α) (e_as : as = as_1) (a a_1 : α),
  a = a_1 →
    ∀ (i i_1 : ℕ) (e_i : i = i_1) (a_2 : i < as.size),
      Array.allDiffAuxAux✝ as a i a_2 = Array.allDiffAuxAux✝ as_1 a_1 i_1 ⋯
-- Mathlib.Order.Max
/-- `a` is a maximal element of `α` if no element is strictly greater than it. We spell it without
`<` to avoid having to convert between `≤` and `<`. Instead, `isMax_iff_forall_not_lt` does the
conversion.  -/
IsMax : {α : Type u_1} → [LE α] → α → Prop
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_lt_degree : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.natDegree < q.natDegree → p.degree < q.degree
-- Mathlib.CategoryTheory.Preadditive.Basic
CategoryTheory.Preadditive.instSMulUnitsIntIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → [CategoryTheory.Preadditive C] → {X Y : C} → SMul ℤˣ (X ≅ Y)
-- Mathlib.Data.Fintype.Sets
Set.toFinset.eq_1 : ∀ {α : Type u_1} (s : Set α) [inst : Fintype ↑s],
  s.toFinset = Finset.map (Function.Embedding.subtype fun x => x ∈ s) Finset.univ
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int32.reduceToInt : Lean.Meta.Simp.DSimproc
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.isAdjointPair_equiv : ∀ {R : Type u_1} {n : Type u_11} [inst : CommRing R] [inst_1 : Fintype n] (J A₁ A₂ : Matrix n n R)
  [inst_2 : DecidableEq n] (P : Matrix n n R),
  IsUnit P →
    ((P.transpose * J * P).IsAdjointPair (P.transpose * J * P) A₁ A₂ ↔ J.IsAdjointPair J (P * A₁ * P⁻¹) (P * A₂ * P⁻¹))
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddEquiv.apply_eq_iff_symm_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Add M]
  [inst_3 : Add N] (e : M ≃ₜ+ N) {x : M} {y : N}, e x = y ↔ x = e.symm y
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
ftaylorSeriesWithin_univ : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
  ftaylorSeriesWithin 𝕜 f Set.univ = ftaylorSeries 𝕜 f
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.ringEquiv_apply : ∀ {𝕜₁ : Type u_1} [inst : NormedField 𝕜₁] {E : Type u_3} [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜₁ E] [inst_4 : IsTopologicalAddGroup E] (self : E →WOT[𝕜₁] E),
  ContinuousLinearMapWOT.ringEquiv self = self.toCLM
-- Mathlib.Data.Finsupp.Defs
/-- The support of a finitely supported function (aka `Finsupp`).  -/
Finsupp.support : {α : Type u_9} → {M : Type u_10} → [inst : Zero M] → (α →₀ M) → Finset α
-- Lean.Elab.PreDefinition.WF.Preprocess
_private.Lean.Elab.PreDefinition.WF.Preprocess.0.Lean.Elab.WF.numLetsWithValueNotIsWfParam : Lean.Expr → optParam ℕ 0 → ℕ
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
HasStrictDerivAt.arctan : ∀ {f : ℝ → ℝ} {f' x : ℝ},
  HasStrictDerivAt f f' x → HasStrictDerivAt (fun x => Real.arctan (f x)) (1 / (1 + f x ^ 2) * f') x
-- Mathlib.RingTheory.Coalgebra.Basic
/-- the finite indexing set of a representation of `comul a`  -/
Coalgebra.Repr.index : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] →
        [inst_2 : Module R A] →
          [inst_3 : CoalgebraStruct R A] → {a : A} → {ι : Type u_1} → Coalgebra.Repr R a ι → Finset ι