mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ClusterPt
ClusterPt.of_inf_left : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {f g : Filter X}, ClusterPt x (f ⊓ g) → ClusterPt x f
-- Mathlib.Analysis.Distribution.TemperateGrowth
/-- Eta-expanded form of `Function.HasTemperateGrowth.sub` -/
Function.HasTemperateGrowth.fun_sub : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f g : E → F},
  Function.HasTemperateGrowth f → Function.HasTemperateGrowth g → Function.HasTemperateGrowth fun i => f i - g i
-- Std.Http.Data.Request
/-- Creates a new HTTP PATCH Request builder with the specified URI.
 -/
Std.Http.Request.patch : Std.Http.RequestTarget → Std.Http.Request.Builder
-- Mathlib.Data.Set.SMulAntidiagonal
Set.mem_vaddAntidiagonal : ∀ {G : Type u_1} {P : Type u_2} [inst : VAdd G P] {s : Set G} {t : Set P} {a : P} {x : G × P},
  x ∈ s.vaddAntidiagonal t a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 +ᵥ x.2 = a
-- Mathlib.FieldTheory.Galois.GaloisClosure
/-- Turns the collection of finite Galois IntermediateFields of `K/k` into a lattice.  -/
FiniteGaloisIntermediateField.instIsGaloisSubtypeMemIntermediateFieldMax : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  (L₁ L₂ : IntermediateField k K) [IsGalois k ↥L₁] [IsGalois k ↥L₂], IsGalois k ↥(L₁ ⊔ L₂)
-- Init.Data.String.Subslice
String.Slice.Subslice.toSlice.eq_1 : ∀ {s : String.Slice} (sl : s.Subslice), sl.toSlice = s.slice sl.startInclusive sl.endExclusive ⋯
-- Mathlib.Order.InitialSeg
PrincipalSeg.ofIsEmpty_top : ∀ {α : Type u_1} {β : Type u_2} {s : β → β → Prop} (r : α → α → Prop) [inst : IsEmpty α] {b : β}
  (H : ∀ (b' : β), ¬s b' b), (PrincipalSeg.ofIsEmpty r H).top = b
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.comm₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (self : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  φ₁.τ₂ = CategoryTheory.CategoryStruct.comp S₁.g self.h₂ + CategoryTheory.CategoryStruct.comp self.h₁ S₂.f + φ₂.τ₂
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' fallback : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).getKeyD k' fallback =
    if cmp k k' = Ordering.eq then if (f (t.get? k)).isSome = true then k else fallback else t.getKeyD k' fallback
-- Mathlib.Analysis.InnerProductSpace.ProdL2
Submodule.coe_orthogonalDecomposition_symm : ∀ {𝕜 : Type u_1} {E : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection],
  ↑↑K.orthogonalDecomposition.symm = K.subtypeL.coprod Kᗮ.subtypeL ∘SL ↑(WithLp.prodContinuousLinearEquiv 2 𝕜 ↥K ↥Kᗮ)
-- Mathlib.Analysis.Complex.Basic
Complex.lipschitz_equivRealProd : LipschitzWith 1 ⇑Complex.equivRealProd
-- Std.Data.HashMap.Lemmas
Std.HashMap.values_emptyWithCapacity : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {c : ℕ} {β : Type v}, (Std.HashMap.emptyWithCapacity c).values = []
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- The integral of a continuous function is differentiable on a real set `s`.  -/
intervalIntegral.differentiable_integral_of_continuous : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a : ℝ},
  Continuous f → Differentiable ℝ fun u => ∫ (x : ℝ) in a..u, f x
-- Mathlib.Algebra.Order.Ring.Ordering.Basic
RingPreordering.inv_mem : ∀ {F : Type u_2} [inst : Field F] {P : RingPreordering F} {a : F}, a ∈ P → a⁻¹ ∈ P
-- Mathlib.Topology.Algebra.LinearTopology
/-- Consider a (left-)module `M` over a ring `R`. A topology on `M` is *`R`-linear*
if the open sub-`R`-modules of `M` form a basis of neighborhoods of zero.

Typically one would also that the topology is invariant by translation (`ContinuousConstVAdd M M`),
or equivalently that `M` is a topological group, but we do not assume it for the definition.

In particular, we say that a topology on the ring `R` is *linear* if it is both
`R`-linear and `Rᵐᵒᵖ`-linear for the obvious module structures. To spell this in Lean,
simply use `[IsLinearTopology R R] [IsLinearTopology Rᵐᵒᵖ R]`.  -/
IsLinearTopology : (R : Type u_1) →
  (M : Type u_3) → [inst : Ring R] → [inst_1 : AddCommGroup M] → [Module R M] → [TopologicalSpace M] → Prop
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isEmpty_inter_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.isEmpty = true → (t₁ ∩ t₂).isEmpty = true
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_two_eq : ∀ (x : ℤ), x.fmod 2 = 0 ∨ x.fmod 2 = 1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Continuous.arcsin : ∀ {X : Type u_1} [inst : TopologicalSpace X] {f : X → ℝ}, Continuous f → Continuous fun x => Real.arcsin (f x)
-- Lean.Data.Lsp.Extra
/-- `$/lean/moduleHierarchy/imports` client->server request.

Response type: `Array LeanImport`
 -/
Lean.Lsp.LeanModuleHierarchyImportsParams : Type
-- Mathlib.Algebra.Notation.Pi.Defs
Function.const_neg : ∀ {ι : Type u_1} {G : Type u_7} [inst : Neg G] (a : G), -Function.const ι a = Function.const ι (-a)
-- Mathlib.Algebra.Group.Defs
ZPow.ofPow.eq_1 : ∀ {M : Type u_2} [inst : Pow M ℤ], ZPow.ofPow = { zpow := fun n x => Pow.pow x n }
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- When the inner matrices are square we can use the induced star operation  -/
Matrix.conjTranspose_comp' : ∀ {α : Type u_1} [inst : Star α] {I : Type u_5} {J : Type u_6} {K : Type u_7} (M : Matrix I J (Matrix K K α)),
  ((Matrix.comp I J K K α) M).conjTranspose = (Matrix.comp J I K K α) M.conjTranspose
-- Mathlib.Analysis.Normed.Operator.ContinuousLinearMap
LinearMap.toContinuousLinearMap₁_apply : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : IsBoundedSMul 𝕜 E] (f : 𝕜 →ₗ[𝕜] E) (x : 𝕜), f.toContinuousLinearMap₁ x = f x
-- Mathlib.Data.Rel
SetRel.preimage_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (R : SetRel α β) (S : SetRel β γ) (u : Set γ),
  (R.comp S).preimage u = R.preimage (S.preimage u)
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.toCore : {𝕜 : Type u_4} →
  {F : Type u_5} →
    [inst : RCLike 𝕜] →
      [inst_1 : AddCommGroup F] → [inst_2 : Module 𝕜 F] → InnerProductSpace.Core 𝕜 F → PreInnerProductSpace.Core 𝕜 F
-- Mathlib.Data.ENNReal.Inv
ENNReal.le_mul_of_forall_lt : ∀ {a b c : ENNReal}, a ≠ 0 ∨ b ≠ ⊤ → a ≠ ⊤ ∨ b ≠ 0 → (∀ a' > a, ∀ b' > b, c ≤ a' * b') → c ≤ a * b
-- Mathlib.Data.Matrix.Mul
/-- `dotProduct v w` is the sum of the entrywise products `v i * w i`.

See also `dotProductEquiv`.  -/
«term_⬝ᵥ_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Calculus.Deriv.Slope
HasDerivWithinAt.liminf_right_slope_le : ∀ {f : ℝ → ℝ} {f' x r : ℝ},
  HasDerivWithinAt f f' (Set.Ici x) x → f' < r → ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), slope f x z < r
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.mem_toNonUnitalStarSubalgebra : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] {S : StarSubalgebra R A} {x : A},
  x ∈ S.toNonUnitalStarSubalgebra ↔ x ∈ S
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.emptyBefore.sizeOf_spec : ∀ {s : String.Slice} (pos : s.Pos), sizeOf (String.Slice.Pattern.ForwardSliceSearcher.emptyBefore pos) = 1 + sizeOf pos
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.instAdditivePullbackShiftShiftFunctorOfCoeAddMonoidHom : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) [inst_4 : CategoryTheory.Preadditive C]
  (a : A) [(CategoryTheory.shiftFunctor C (φ a)).Additive],
  (CategoryTheory.shiftFunctor (CategoryTheory.PullbackShift C φ) a).Additive
-- Mathlib.Analysis.CStarAlgebra.Basic
NormedStarGroup.norm_star_le : ∀ {E : Type u_1} {inst : SeminormedAddCommGroup E} {inst_1 : StarAddMonoid E} [self : NormedStarGroup E] (x : E),
  ‖star x‖ ≤ ‖x‖
-- Mathlib.Tactic.SetNotationForOrder
/-- Declare `∀ x ⊃ y, ...` as syntax for `∀ x, x ⊃ y → ...` and `∃ x ⊃ y, ...` as syntax for
`∃ x, x ⊃ y ∧ ...`  -/
Mathlib.Meta.SetNotationForOrder.«binderPred⊃_» : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_insert!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insert! k v t).getKey k ⋯ = k
-- Std.Http.Data.URI.Basic
/-- The URI scheme (e.g., "http", "https").
 -/
Std.Http.URI.Builder.scheme : Std.Http.URI.Builder → Option Std.Http.URI.Scheme
-- Mathlib.RingTheory.RingHom.Etale
RingHom.etale_iff_formallyUnramified_and_smooth : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  f.Etale ↔ f.FormallyUnramified ∧ f.Smooth
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_out : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] (A : MulArchimedeanClass M),
  MulArchimedeanClass.mk A.out = A
-- Batteries.Data.List.Perm
List.Perm.subperm_idxBij : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : ReflBEq α] {xs ys : List α} (h : xs.Perm ys), ⋯.idxInj = h.idxBij
-- Mathlib.Data.Set.Image
Disjoint.of_image : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set α}, Disjoint (f '' s) (f '' t) → Disjoint s t
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Multipliable.tprod_pow : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {L : SummationFilter β}
  [T2Space α] [ContinuousMul α] [L.NeBot],
  Multipliable f L → ∀ (n : ℕ), ∏'[L] (b : β), f b ^ n = (∏'[L] (b : β), f b) ^ n
-- Mathlib.Tactic.IrreducibleDef
/-- `eta_helper f = (· + 3)` elabs to `∀ x, f x = x + 3`  -/
_private.Mathlib.Tactic.IrreducibleDef.0.Lean.Elab.Command.termEta_helper_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_obj_iso_inv_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  (X : Type u₇) [inst_6 : CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X_1 : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).obj S).iso.inv.app X_1 =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso G ψ.right ψ.base G₁).inv.app (S.snd.obj X_1))
      (CategoryTheory.CategoryStruct.comp (ψ.base.map (S.iso.inv.app X_1))
        ((CategoryTheory.CatCommSq.iso F ψ.left ψ.base F₁).hom.app (S.fst.obj X_1)))
-- Init.Grind.Lemmas
Lean.Grind.heq_congr : ∀ {α β : Sort u} {a₁ b₁ : α} {a₂ b₂ : β}, a₁ ≍ a₂ → b₁ ≍ b₂ → (a₁ = b₁) = (a₂ = b₂)
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.checkMacro : Lean.Linter.MissingDocs.SimpleHandler
-- Batteries.CodeAction.Misc
/-- Finds the `TermInfo` for an elaborated term `stx`.  -/
Batteries.CodeAction.findTermInfo? : Lean.Elab.InfoTree → Lean.Term → Option Lean.Elab.TermInfo
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.forIn_eq_forInUncurried : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w'} {β : Type v}
  {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m]
  {f : α → β → δ → m (ForInStep δ)} {init : δ},
  Std.ExtDTreeMap.forIn f init t = Std.ExtDTreeMap.Const.forInUncurried (fun a b => f a.1 a.2 b) init t
-- Mathlib.Data.Set.PowersetCard
Set.powersetCard.ofCard_coe : ∀ {α : Type u_1} {n : ℕ} {s : ↑(Set.powersetCard α n)} (h : (↑s).card = n), Set.powersetCard.ofCard h = s
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.appr.eq_def : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]) (x_1 : ℕ),
  x.appr x_1 =
    match x, x_1 with
    | _x, 0 => 0
    | x, n.succ =>
      have y := x - ↑(x.appr n);
      if hy : y = 0 then x.appr n
      else
        have u := ↑(PadicInt.unitCoeff hy);
        x.appr n + p ^ n * (PadicInt.toZMod (u * ↑p ^ (↑y.valuation - ↑n).natAbs)).val
-- Mathlib.Analysis.SpecialFunctions.CompareExp
Complex.IsExpCmpFilter.eventually_ne : ∀ {l : Filter ℂ}, Complex.IsExpCmpFilter l → ∀ᶠ (w : ℂ) in l, w ≠ 0
-- Lean.Elab.PreDefinition.FixedParams
Lean.Elab.FixedParamPerm.forallTelescope : {n : Type → Type u_1} →
  {α : Type} →
    [MonadControlT Lean.MetaM n] → [Monad n] → Lean.Elab.FixedParamPerm → Lean.Expr → (Array Lean.Expr → n α) → n α
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {l : List (α × β)}
  {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β} [inst : Inhabited β],
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → (k, v) ∈ l → (t.insertMany l)[k']! = v
-- Mathlib.NumberTheory.MulChar.Basic
/-- **Alias** of `MulChar.domRestrict_eq_one_iff`. -/
MulChar.restrict_eq_one_iff : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] {S : Type u_3}
  [inst_2 : SetLike S R] [inst_3 : SubmonoidClass S R] {T : S} {χ : MulChar R R'},
  MulChar.domRestrict T χ = 1 ↔ ∀ (x : (↥T)ˣ), χ ↑↑x = 1
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- Uses `left` co(ntra)variant.  -/
Left.nonneg_neg_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] {a : α}, 0 ≤ -a ↔ a ≤ 0
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic
/-- Given a covariant derivative `cov` on a neighborhood `s` of a point `x`, if sections `σ` and
`σ'` agree near `x` and are differentiable at `x`, then `cov σ x = cov σ x'`.  -/
IsCovariantDerivativeOn.congr_of_eventuallyEq : ∀ {𝕜 : 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_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : ∀ (x : M), IsTopologicalAddGroup (V x)]
  [inst_13 : ∀ (x : M), ContinuousSMul 𝕜 (V x)] [inst_14 : FiberBundle F V]
  {cov : ((x : M) → V x) → (x : M) → TangentSpace I x →L[𝕜] V x} {s : Set M},
  IsCovariantDerivativeOn F cov s →
    ∀ {σ σ' : (x : M) → V x} {x : M},
      MDiffAt (T% σ) x → MDiffAt (T% σ') x → s ∈ nhds x → (∀ᶠ (x : M) in nhds x, σ x = σ' x) → cov σ x = cov σ' x
-- Mathlib.Algebra.Homology.HomologicalComplex
CochainComplex.mkHom_f_1 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (P Q : CochainComplex V ℕ) (zero : P.X 0 ⟶ Q.X 0) (one : P.X 1 ⟶ Q.X 1)
  (one_zero_comm : CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) = CategoryTheory.CategoryStruct.comp (P.d 0 1) one)
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X n ⟶ Q.X n) ×'
            (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×'
              CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) =
                CategoryTheory.CategoryStruct.comp (P.d n (n + 1)) f') →
        (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
          CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) =
            CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f''),
  (P.mkHom Q zero one one_zero_comm succ).f 1 = one
-- Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.instInhabitedGrwKey : Inhabited Mathlib.Tactic.ClickSuggestions.GrwKey
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.iSup_apply : ∀ {α : Type u_1} {ι : Sort u_3} (f : ι → MeasureTheory.OuterMeasure α) (s : Set α), (⨆ i, f i) s = ⨆ i, (f i) s
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.ClosedComplemented.isClosed : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [ContinuousSub M] [T1Space M] {p : Submodule R M}, p.ClosedComplemented → IsClosed ↑p
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
UniformSpace.ofDist_aux : ∀ (ε : ℝ), 0 < ε → ∃ δ > 0, ∀ x < δ, ∀ y < δ, x + y < ε
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.le_order_smul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R} {a : R}, f.order ≤ (a • f).order
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_inter_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α},
  k ∈ m₂ → (m₁ ∩ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.Order.RelIso.Basic
RelEmbedding.mk.congr_simp : ∀ {α : Type u_5} {β : Type u_6} {r : α → α → Prop} {s : β → β → Prop} (toEmbedding toEmbedding_1 : α ↪ β)
  (e_toEmbedding : toEmbedding = toEmbedding_1) (map_rel_iff' : ∀ {a b : α}, s (toEmbedding a) (toEmbedding b) ↔ r a b),
  { toEmbedding := toEmbedding, map_rel_iff' := map_rel_iff' } = { toEmbedding := toEmbedding_1, map_rel_iff' := ⋯ }
-- Mathlib.Algebra.Module.Torsion.Basic
Module.isTorsionBy_quotient_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  (r : R), Module.IsTorsionBy R (M ⧸ N) r ↔ ∀ (x : M), r • x ∈ N
-- Mathlib.Logic.Equiv.Fin.Basic
Int.divModEquiv_symm_apply : ∀ (n : ℕ) [inst : NeZero n] (p : ℤ × Fin n), (Int.divModEquiv n).symm p = p.1 * ↑n + ↑↑p.2
-- Mathlib.Data.ENNReal.Operations
/-- This lemma has an abbreviated name because it is used frequently.  -/
ENNReal.cancel_of_lt' : ∀ {a b : ENNReal}, a < b → AddLECancellable a
-- Mathlib.Order.Partition.Finpartition
Finpartition.ext_iff : ∀ {α : Type u_1} {inst : Lattice α} {inst_1 : OrderBot α} {a : α} {x y : Finpartition a}, x = y ↔ x.parts = y.parts
-- Mathlib.Tactic.ProdAssoc
Lean.Expr.ProdTree.type : Lean.Expr → Lean.Level → Lean.Expr.ProdTree
-- Mathlib.Data.Set.Basic
Set.inter_univ : ∀ {α : Type u} (a : Set α), a ∩ Set.univ = a
-- Init.Data.SInt.Lemmas
UInt64.toInt64_ofBitVec : ∀ (b : BitVec 64), { toBitVec := b }.toInt64 = Int64.ofBitVec b
-- Mathlib.NumberTheory.Fermat
Nat.fermatNumber_succ : ∀ (n : ℕ), (n + 1).fermatNumber = (n.fermatNumber - 1) ^ 2 + 1
-- Mathlib.Algebra.Group.Action.Units
Units.instMulAction : {M : Type u_3} → {α : Type u_5} → [inst : Monoid M] → [MulAction M α] → MulAction Mˣ α
-- Init.Prelude
/-- The notation typeclass for heterogeneous modulo / remainder.
This enables the notation `a % b : γ` where `a : α`, `b : β`.
 -/
HMod : Type u → Type v → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.Analysis.Calculus.FDeriv.Basic
DifferentiableWithinAt.empty : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E}, DifferentiableWithinAt 𝕜 f ∅ x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_eq_false_of_isEmpty_erase_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).isEmpty = false → t.isEmpty = false
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
CategoryTheory.Bicategory.LeftExtension.IsKan.fac_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  {t : CategoryTheory.Bicategory.LeftExtension f g} (H : t.IsKan) (s : CategoryTheory.Bicategory.LeftExtension f g)
  {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp f s.extension ⟶ Z),
  CategoryTheory.CategoryStruct.comp t.unit
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (H.desc s)) h) =
    CategoryTheory.CategoryStruct.comp s.unit h
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- Version of `PowerSeries.IsWeierstrassFactorizationAt` for local rings with respect to
its maximal ideal.  -/
PowerSeries.IsWeierstrassFactorization : {A : Type u_1} → [inst : CommRing A] → PowerSeries A → Polynomial A → PowerSeries A → [IsLocalRing A] → Prop
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.image_log_uIcc : ∀ {a b : ℝ}, 0 < a → 0 < b → Real.log '' Set.uIcc a b = Set.uIcc (Real.log a) (Real.log b)
-- Mathlib.Util.Notation3
Mathlib.Notation3.DelabKey.other.injEq : ∀ (key key_1 : Lean.Name),
  (Mathlib.Notation3.DelabKey.other key = Mathlib.Notation3.DelabKey.other key_1) = (key = key_1)
-- Mathlib.Order.Preorder.Finite
Set.infinite_of_forall_exists_gt : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α} [Nonempty α], (∀ (a : α), ∃ b ∈ s, a < b) → s.Infinite
-- Mathlib.Topology.Algebra.Equicontinuity
uniformEquicontinuous_of_equicontinuousAt_one : ∀ {ι : Type u_1} {G : Type u_2} {M : Type u_3} {hom : Type u_4} [inst : UniformSpace G] [inst_1 : UniformSpace M]
  [inst_2 : Group G] [inst_3 : Group M] [IsUniformGroup G] [IsUniformGroup M] [inst_6 : FunLike hom G M]
  [MonoidHomClass hom G M] (F : ι → hom),
  EquicontinuousAt (DFunLike.coe ∘ F) 1 → UniformEquicontinuous (DFunLike.coe ∘ F)
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- Version of `algHom_ext` where both assumptions are written as equalities of bundled homs.  -/
AddMonoidAlgebra.algHom_ext' : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {M : Type u_7} [inst : CommSemiring R] [inst_1 : AddMonoid M]
  [inst_2 : Semiring A] [inst_3 : Algebra R A] [inst_4 : Semiring B] [inst_5 : Algebra R B]
  ⦃φ₁ φ₂ : AddMonoidAlgebra A M →ₐ[R] B⦄,
  (↑φ₁).comp (AddMonoidAlgebra.of A M) = (↑φ₂).comp (AddMonoidAlgebra.of A M) →
    φ₁.comp AddMonoidAlgebra.singleZeroAlgHom = φ₂.comp AddMonoidAlgebra.singleZeroAlgHom → φ₁ = φ₂
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.sumAux.eq_2 : ∀ {M : Type u_6} [inst : AddMonoid M] (x_1 : M) (xs : List M),
  FreeAddMonoid.sumAux (x_1 :: xs) = List.foldl (fun x1 x2 => x1 + x2) x_1 xs
-- Mathlib.RingTheory.Bialgebra.Quotient
/-- The counit on `A ⧸ I`, as an `R`-algebra homomorphism.  -/
Bialgebra.Quotient.counitAlgHom : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : Ring A] →
        [inst_2 : Bialgebra R A] →
          (I : Ideal A) → [inst_3 : I.IsTwoSided] → [(Submodule.restrictScalars R I).IsCoideal] → A ⧸ I →ₐ[R] R
-- Mathlib.CategoryTheory.Bicategory.Coherence
/-- The coherence theorem for bicategories.  -/
CategoryTheory.FreeBicategory.locally_thin : ∀ {B : Type u} [inst : Quiver B] {a b : CategoryTheory.FreeBicategory B}, Quiver.IsThin (a ⟶ b)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_pos : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R},
  r = 0 → v.intValuationDef r = 0
-- Mathlib.Algebra.Category.Ring.Adjunctions
CommRingCat.monoidAlgebra_obj : ∀ (R : CommRingCat) (G : CommMonCat),
  R.monoidAlgebra.obj G = CategoryTheory.Under.mk (CommRingCat.ofHom MonoidAlgebra.singleOneRingHom)