mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Guard
/-- Tactic to check that the target agrees with a given expression.
* `guard_target = e` checks that the target is defeq at reducible transparency to `e`.
* `guard_target =~ e` checks that the target is defeq at default transparency to `e`.
* `guard_target =ₛ e` checks that the target is syntactically equal to `e`.
* `guard_target =ₐ e` checks that the target is alpha-equivalent to `e`.

The term `e` is elaborated with the type of the goal as the expected type, which is mostly
useful within `conv` mode.
 -/
Lean.Parser.Tactic.guardTarget : Lean.ParserDescr
-- Mathlib.RingTheory.WittVector.Identities
WittVector.coeff_p : ∀ (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p] (i : ℕ),
  (↑p).coeff i = if i = 1 then 1 else 0
-- Mathlib.Data.Set.Sigma
Set.image_sigmaMk_preimage_sigmaMap : ∀ {ι : Type u_1} {ι' : Type u_2} {α : ι → Type u_3} {β : ι' → Type u_4} {f : ι → ι'},
  Function.Injective f →
    ∀ (g : (i : ι) → α i → β (f i)) (i : ι) (s : Set (β (f i))),
      Sigma.mk i '' g i ⁻¹' s = Sigma.map f g ⁻¹' Sigma.mk (f i) '' s
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGED.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β) (fallback : α),
  Std.DTreeMap.Internal.Impl.getKeyGED k t fallback = (Std.DTreeMap.Internal.Impl.getKeyGE? k t).getD fallback
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.assoc_flip : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.MonObj A] (M : CategoryTheory.Mod D A),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A CategoryTheory.ModObj.smul)
      CategoryTheory.ModObj.smul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso A A M.X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.MonObj.mul M.X)
        CategoryTheory.ModObj.smul)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsCyclic.of_exponent_eq_card : ∀ {α : Type u_1} [inst : CommGroup α] [Finite α], Monoid.exponent α = Nat.card α → IsCyclic α
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse_map_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat)
  {X Y : CategoryTheory.Grothendieck F} (f : X ⟶ Y),
  ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceInverse F).map f).base = f.base
-- Mathlib.Analysis.Complex.Spectrum
QuasispectrumRestricts.real_iff : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] {a : A},
  QuasispectrumRestricts a ⇑Complex.reCLM ↔ ∀ x ∈ quasispectrum ℂ a, x = ↑x.re
-- Mathlib.Tactic.ClickSuggestions.Apply
/-- The name of the used lemma.  -/
Mathlib.Tactic.ClickSuggestions.ApplyKey.name : Mathlib.Tactic.ClickSuggestions.ApplyKey → String
-- Mathlib.Order.Lattice
sup_assoc : ∀ {α : Type u} [inst : SemilatticeSup α] (a b c : α), a ⊔ b ⊔ c = a ⊔ (b ⊔ c)
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
_private.Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas.0.Nat.nthRoot.match_3.eq_2 : ∀ (motive : ℕ → ℕ → Sort u_1) (a : ℕ) (h_1 : (x : ℕ) → motive 0 x) (h_2 : (a : ℕ) → motive 1 a)
  (h_3 : (n a : ℕ) → motive n.succ.succ a),
  (match 1, a with
    | 0, x => h_1 x
    | 1, a => h_2 a
    | n.succ.succ, a => h_3 n a) =
    h_2 a
-- Mathlib.Topology.UniformSpace.Basic
instIsCountablyGeneratedProdElemUniformity : ∀ {α : Type ua} [inst : UniformSpace α] [(uniformity α).IsCountablyGenerated] (s : Set α),
  (uniformity ↑s).IsCountablyGenerated
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Valuation.satisfies_fmla.mk : ∀ {v : Sat.Valuation} {f : Sat.Fmla}, (∀ c ∈ f, v.satisfies c) → v.satisfies_fmla f
-- Mathlib.Order.RelClasses
WellFoundedGT.eq_1 : ∀ (α : Type u_1) [inst : LT α], WellFoundedGT α = IsWellFounded α fun x1 x2 => x2 < x1
-- Lean.Meta.WHNF
Lean.Meta.isAuxDef : Lean.Name → Lean.MetaM Bool
-- Mathlib.Logic.Equiv.Bool
Bool.not_hasLeftInverse : Function.HasLeftInverse not
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.disjoint_inv_left_iff : ∀ {α : Type u_1} {f g : Equiv.Perm α}, f⁻¹.Disjoint g ↔ f.Disjoint g
-- Mathlib.Data.Finsupp.Basic
Finsupp.graph_injective : ∀ (α : Type u_12) (M : Type u_13) [inst : Zero M], Function.Injective Finsupp.graph
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.instOrderHomClassContinuousHom : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β],
  OrderHomClass (α →𝒄 β) α β
-- Mathlib.Algebra.Category.Ring.Limits
/-- If `J` is `u`-small, `SemiRingCat.{u}` has limits of shape `J`.  -/
SemiRingCat.hasLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.HasLimitsOfShape J SemiRingCat
-- Init.Meta.Defs
/-- Syntax that represents a character literal.
 -/
Lean.Syntax.CharLit : Type
-- Mathlib.RepresentationTheory.Equiv
/-- The linear equiv between the hom module `k[G] ⟶ᵍ V` and `V` itself.  -/
Representation.leftRegularMapEquiv : {G : Type v} →
  [inst : Monoid G] →
    {V : Type v'} →
      [inst_1 : AddCommMonoid V] →
        {k : Type u} →
          [inst_2 : CommSemiring k] →
            [inst_3 : Module k V] →
              (σ : Representation k G V) → (Representation.leftRegular k G).IntertwiningMap σ ≃ₗ[k] V
-- Mathlib.Data.Prod.Lex
/-- Dictionary / lexicographic preorder for pairs.  -/
Prod.Lex.instPreorder : (α : Type u_3) → (β : Type u_4) → [Preorder α] → [Preorder β] → Preorder (Lex (α × β))
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso_inv_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (X : CategoryTheory.Arrow C) {I : C} (i : CategoryTheory.Limits.IsInitial I) {T : C}
  (t : CategoryTheory.Limits.IsTerminal T),
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.isInitialIsTerminalIso X i t).inv.left =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X.left).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X.left
          (t.from (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
        ⋯.isoPushout.hom)
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.TensorProduct.map_comp_assoc : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} {M' : Type u_6} {N' : Type u_7} {P' : Type u_8}
  {M₁ : Type u_11} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N]
  [inst_4 : Module R N] [inst_5 : AddCommMonoid P] [inst_6 : Module R P] [inst_7 : AddCommMonoid M']
  [inst_8 : Module R M'] [inst_9 : AddCommMonoid N'] [inst_10 : Module R N'] [inst_11 : AddCommMonoid P']
  [inst_12 : Module R P'] [inst_13 : AddCommMonoid M₁] [inst_14 : Module R M₁] (f : M →ₗ[R] N) (g : N →ₗ[R] P)
  (f' : M' →ₗ[R] N') (g' : N' →ₗ[R] P') (φ : M₁ →ₗ[R] TensorProduct R M M'),
  TensorProduct.map g g' ∘ₗ TensorProduct.map f f' ∘ₗ φ = TensorProduct.map (g ∘ₗ f) (g' ∘ₗ f') ∘ₗ φ
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.hom.congr_right : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} {φ₁ φ₂ : g ⟶ f},
  φ₁ = φ₂ → CategoryTheory.Arrow.Hom.right φ₁ = CategoryTheory.Arrow.Hom.right φ₂
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.Cell.Const.get?_empty : ∀ {α : Type u} {β : Type v} [inst : Ord α] {k : α},
  Std.DTreeMap.Internal.Cell.Const.get? Std.DTreeMap.Internal.Cell.empty = none
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.lift_neg_comp_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddGrpObj A] [inst_3 : CategoryTheory.AddGrpObj B] (f : A ⟶ B)
  [CategoryTheory.IsAddMonHom f],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg f)
        f)
      CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A)
      CategoryTheory.AddMonObj.zero
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.whiskerRight_toUnit_comp_leftUnitor_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) Y)
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).hom =
    CategoryTheory.SemiCartesianMonoidalCategory.snd X Y
-- Mathlib.Data.Sym.Sym2
Sym2.diagSet_eq_setOfPred_isDiag : ∀ {α : Type u_1}, Sym2.diagSet = {z | z.IsDiag}
-- Mathlib.Tactic.Linter.PPRoundtrip
/-- `zoomString str centre offset` returns the substring of `str` consisting of the `offset`
characters around the `centre`th character.  -/
_private.Mathlib.Tactic.Linter.PPRoundtrip.0.Mathlib.Linter.zoomString : String → ℕ → ℕ → Substring.Raw
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.expandTypeAscription : Lean.Macro
-- Mathlib.Computability.TuringMachine.Computable
/-- The type of configurations (functions) corresponding to this TM.  -/
Turing.FinTM2.Cfg : Turing.FinTM2 → Type
-- Lean.Data.Lsp.Basic
Lean.Lsp.CreateFile.Options.overwrite : Lean.Lsp.CreateFile.Options → Bool
-- Batteries.Data.Float.Rat
/-- Convert this floating point number to a rational value.  -/
Float.toRat? : Float → Option ℚ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ} {k fallback : α},
  (Std.ExtTreeMap.filterMap f t).getKeyD k fallback =
    ((t.getKey? k).pfilter fun x h' => (f x t[x]).isSome).getD fallback
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- If two ring homomorphisms from `R[M]` are equal on all `single m 1` and
`single 1 r`, then they are equal.  -/
MonoidAlgebra.ringHom_ext : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : MulOneClass M] [inst_2 : Semiring S]
  {f g : MonoidAlgebra R M →+* S},
  (∀ (r : R), f (MonoidAlgebra.single 1 r) = g (MonoidAlgebra.single 1 r)) →
    (∀ (m : M), f (MonoidAlgebra.single m 1) = g (MonoidAlgebra.single m 1)) → f = g
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, returning `none` if no such pair exists.
 -/
Std.ExtDTreeMap.getEntryGE? : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → Option ((a : α) × β a)
-- Mathlib.Data.Num.Prime
PosNum.minFacAux.eq_def : ∀ (n : PosNum) (x : ℕ) (x_1 : PosNum),
  n.minFacAux x x_1 =
    match x, x_1 with
    | 0, x => n
    | fuel.succ, k => if n < k.bit1 * k.bit1 then n else if k.bit1 ∣ n then k.bit1 else n.minFacAux fuel k.succ
-- Lean.Meta.Match.Match
/-- Execute `k hs` where `hs` contains new equalities `h : lhs[i] = rhs[i]` for each `discrInfos[i] = some h`.
Assume `lhs.size == rhs.size == discrInfos.size`
 -/
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.withEqs : {α : Type} →
  Array Lean.Expr → Array Lean.Expr → Array Lean.Meta.Match.DiscrInfo → (Array Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.IsPath.snd_of_toSubgraph_adj : ∀ {V : Type u} {G : SimpleGraph V} {u v v' : V} {p : G.Walk u v}, p.IsPath → p.toSubgraph.Adj u v' → p.snd = v'
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofUserWidgetInfo.inj : ∀ {i i_1 : Lean.Elab.UserWidgetInfo}, Lean.Elab.Info.ofUserWidgetInfo i = Lean.Elab.Info.ofUserWidgetInfo i_1 → i = i_1
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitInfo.imp.sizeOf_spec : ∀ (e : Lean.Expr) (h : e.isForall = true) (source : Lean.Meta.Grind.SplitSource),
  sizeOf (Lean.Meta.Grind.SplitInfo.imp e h source) = 1 + sizeOf e + sizeOf h + sizeOf source
-- Mathlib.Analysis.Calculus.Deriv.Mul
deriv_smul_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {𝕜' : Type u_2} [inst_3 : NormedRing 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  [inst_5 : Module 𝕜' F] [IsBoundedSMul 𝕜' F] [IsScalarTower 𝕜 𝕜' F] {c : 𝕜 → 𝕜'},
  DifferentiableAt 𝕜 c x → ∀ (f : F), deriv (fun y => c y • f) x = deriv c x • f
-- Mathlib.LinearAlgebra.CliffordAlgebra.Grading
CliffordAlgebra.evenOdd_isCompl : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M), IsCompl (CliffordAlgebra.evenOdd Q 0) (CliffordAlgebra.evenOdd Q 1)
-- Mathlib.Order.RelIso.Basic
RelIso.symm_apply_apply : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s) (x : α), e.symm (e x) = x
-- Mathlib.Algebra.GroupWithZero.Hom
/-- `MonoidWithZeroHomClass F α β` states that `F` is a type of
`MonoidWithZero`-preserving homomorphisms.

You should also extend this typeclass when you extend `MonoidWithZeroHom`.  -/
MonoidWithZeroHomClass : (F : Type u_7) →
  (α : outParam (Type u_8)) →
    (β : outParam (Type u_9)) → [MulZeroOneClass α] → [MulZeroOneClass β] → [FunLike F α β] → Prop
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex_unique : ∀ (𝕜 : Type u_2) (ι : Type u_1) [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : Fintype ι] [ZeroLEOneClass 𝕜]
  [Nonempty ι] [Subsingleton ι], stdSimplex 𝕜 ι = {fun x => 1}
-- Init.NotationExtra
unexpandPSigma : Lean.PrettyPrinter.Unexpander
-- Init.Data.String.Lemmas.IsEmpty
String.isEmpty_slice : ∀ {s : String} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂}, (s.slice p₁ p₂ h).isEmpty = true ↔ p₁ = p₂
-- Batteries.Data.List.Lemmas
List.mem_inter_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {x : α} {l₁ l₂ : List α}, x ∈ l₁ ∩ l₂ ↔ x ∈ l₁ ∧ x ∈ l₂
-- Mathlib.Data.Multiset.Powerset
Multiset.powersetCard_coe : ∀ {α : Type u_1} (n : ℕ) (l : List α), Multiset.powersetCard n ↑l = ↑(List.map Multiset.ofList (List.sublistsLen n l))
-- Mathlib.Analysis.SpecialFunctions.ImproperIntegrals
integral_Iic_inv_one_add_sq : ∀ {i : ℝ}, ∫ (x : ℝ) in Set.Iic i, (1 + x ^ 2)⁻¹ = Real.arctan i + Real.pi / 2
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHint.position : Lean.Lsp.InlayHint → Lean.Lsp.Position
-- Mathlib.RingTheory.GradedAlgebra.Noetherian
/-- If the internally graded ring `A` is Noetherian, then `𝒜 0` is a Noetherian ring.  -/
GradedRing.GradeZero.isNoetherianRing : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : Ring A] [IsNoetherianRing A] [inst_2 : DecidableEq ι]
  [inst_3 : AddCommMonoid ι] [inst_4 : PartialOrder ι] [CanonicallyOrderedAdd ι] [inst_6 : SetLike σ A]
  [inst_7 : AddSubgroupClass σ A] (𝒜 : ι → σ) [inst_8 : GradedRing 𝒜], IsNoetherianRing ↥(𝒜 0)
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
ULift.dist_up_up : ∀ {β : Type u_2} [inst : PseudoMetricSpace β] (x y : β), dist { down := x } { down := y } = dist x y
-- Mathlib.Control.Monad.Cont
ReaderT.goto_mkLabel : ∀ {m : Type u → Type v} {α : Type u_1} {ρ β : Type u} (x : MonadCont.Label α m β) (i : α),
  MonadCont.goto (ReaderT.mkLabel ρ x) i = monadLift (MonadCont.goto x i)
-- Mathlib.Algebra.Group.Action.Basic
/-- Given an action of an additive group `α` on `β`, each `g : α` defines a permutation of `β`.  -/
AddAction.toPerm : {α : Type u_5} → {β : Type u_6} → [inst : AddGroup α] → [AddAction α β] → α → Equiv.Perm β
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.RefreshRef.mk.inj : ∀ {ref ref_1 : IO.Ref ProofWidgets.RefreshComponent.RefreshState}, { ref := ref } = { ref := ref_1 } → ref = ref_1
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
  (h : Std.Internal.List.containsKey a l = true), ⟨a, Std.Internal.List.getValueCast a l h⟩ ∈ l
-- Mathlib.RingTheory.Invariant.Basic
/-- If `G` acts on `B/A` with `A` as the fixed subring, then `G` also acts on `L/K` with `K` as
the fixed subfield, where `K` and `L` are the fraction fields of `A` and `B` respectively.  -/
IsFractionRing.isInvariant_of_isIntegral : ∀ (G : Type u_1) (A : Type u_2) (B : Type u_3) (K : Type u_4) (L : Type u_5) [inst : Group G] [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : Algebra A B] [inst_4 : Field K] [inst_5 : Field L] [inst_6 : Algebra K L]
  [inst_7 : Algebra A K] [inst_8 : Algebra B L] [inst_9 : Algebra A L] [IsFractionRing A K] [IsFractionRing B L]
  [IsScalarTower A K L] [IsScalarTower A B L] [inst_14 : MulSemiringAction G B] [inst_15 : MulSemiringAction G L]
  [SMulDistribClass G B L] [hAB : Algebra.IsInvariant A B G] [SMulCommClass G A B] [Algebra.IsIntegral A B],
  Algebra.IsInvariant K L G
-- Lean.Meta.Tactic.SolveByElim
/-- Add a discharging tactic, falling back to the original discharging tactic if it fails.
Return `none` to return the goal as a new subgoal, or `some goals` to replace it.  -/
Lean.Meta.SolveByElim.SolveByElimConfig.withDischarge : optParam Lean.Meta.SolveByElim.SolveByElimConfig { } →
  (Lean.MVarId → Lean.MetaM (Option (List Lean.MVarId))) → Lean.Meta.SolveByElim.SolveByElimConfig
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.IsHashSelf.updateAllBuckets : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] [LawfulHashable α]
  {m : Array (Std.DHashMap.Internal.AssocList α β)}
  {f : Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α δ},
  (∀ (l : Std.DHashMap.Internal.AssocList α β),
      ∀ p ∈ (f l).toList, Std.Internal.List.containsKey p.fst l.toList = true) →
    Std.DHashMap.Internal.IsHashSelf m → Std.DHashMap.Internal.IsHashSelf (Std.DHashMap.Internal.updateAllBuckets m f)
-- Mathlib.Data.Set.Lattice.Image
Set.biUnion_preimage_singleton : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set β), ⋃ y ∈ s, f ⁻¹' {y} = f ⁻¹' s
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k fallback : α},
  (Std.HashMap.filter f m).getKeyD k fallback = ((m.getKey? k).pfilter fun x_2 h' => f x_2 m[x_2]).getD fallback
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.BasicMeasure.mk : Lean.Elab.TerminationMeasure → Lean.Expr → Lean.Elab.WF.GuessLex.BasicMeasure
-- Mathlib.AlgebraicTopology.CechNerve
/-- The augmented Čech conerve associated to an arrow.  -/
CategoryTheory.Arrow.augmentedCechConerve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (f : CategoryTheory.Arrow C) →
      [∀ (n : ℕ), CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] →
        CategoryTheory.CosimplicialObject.Augmented C
-- Mathlib.RingTheory.Polynomial.Nilpotent
Polynomial.not_isUnit_of_degree_pos_of_isReduced : ∀ {R : Type u_1} [inst : CommRing R] [IsReduced R] (p : Polynomial R), 0 < p.degree → ¬IsUnit p
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Maps
HomogeneousIdeal.map_comp : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {σ : Type u_4} {τ : Type u_5} {ω : Type u_6} {ι : Type u_7}
  [inst : Semiring A] [inst_1 : Semiring B] [inst_2 : Semiring C] [inst_3 : SetLike σ A] [inst_4 : SetLike τ B]
  [inst_5 : SetLike ω C] [inst_6 : AddSubmonoidClass σ A] [inst_7 : AddSubmonoidClass τ B]
  [inst_8 : AddSubmonoidClass ω C] [inst_9 : DecidableEq ι] [inst_10 : AddMonoid ι] {𝒜 : ι → σ} {ℬ : ι → τ} {𝒞 : ι → ω}
  [inst_11 : GradedRing 𝒜] [inst_12 : GradedRing ℬ] [inst_13 : GradedRing 𝒞] (f : 𝒜 →+*ᵍ ℬ) (g : ℬ →+*ᵍ 𝒞)
  {I : HomogeneousIdeal 𝒜}, HomogeneousIdeal.map (g.comp f) I = HomogeneousIdeal.map g (HomogeneousIdeal.map f I)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castAdd_Ici_castAdd : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Fin.castAdd m ⁻¹' Set.Ici (Fin.castAdd m i) = Set.Ici i
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ofCoeff_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (r : R),
  (MonoidAlgebra.ofCoeff fun₀ | m => r) = MonoidAlgebra.single m r
-- Mathlib.Algebra.Order.Field.Power
zpow_eq_neg_zpow_iff₀ : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α} {n : ℤ},
  b ≠ 0 → (a ^ n = -b ^ n ↔ a = -b ∧ Odd n)
-- Mathlib.Condensed.AB
Condensed.hasExactColimitsOfShape : ∀ (A : Type u_1) (J : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J] [CategoryTheory.Preadditive A]
  [∀ (X : CompHausᵒᵖ),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X Stonean.toCompHaus.op) A]
  [inst_4 : CategoryTheory.HasWeakSheafify (CategoryTheory.coherentTopology CompHaus) A]
  [CategoryTheory.HasWeakSheafify (CategoryTheory.extensiveTopology Stonean) A]
  [inst_6 : CategoryTheory.Limits.HasColimitsOfShape J A] [CategoryTheory.HasExactColimitsOfShape J A]
  [CategoryTheory.Limits.HasFiniteLimits A], CategoryTheory.HasExactColimitsOfShape J (Condensed A)
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.minimalPeriod.eq_1 : ∀ {α : Type u_1} (f : α → α) (x : α),
  Function.minimalPeriod f x = if h : x ∈ Function.periodicPts f then Nat.find h else 0
-- Mathlib.Order.Partition.Basic
Partition.IsRepFun.apply_mem_iff : ∀ {α : Type u_1} {s u : Set α} {P : Partition u} {f : α → α} {a : α}, P.IsRepFun f → u ⊆ s → (f a ∈ s ↔ a ∈ s)
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
PointwiseConvergenceCLM.equivWeakDual_symm_apply : ∀ (𝕜 : Type u_3) [inst : NormedField 𝕜] (E : Type u_7) [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] (a : E →L[𝕜] 𝕜), (PointwiseConvergenceCLM.equivWeakDual 𝕜 E).symm a = a
-- Mathlib.Data.DFinsupp.Defs
/-- `subtypeDomain p f` is the restriction of the finitely supported function
`f` to the subtype `p`.  -/
DFinsupp.subtypeDomain : {ι : Type u} →
  {β : ι → Type v} →
    [inst : (i : ι) → Zero (β i)] → (p : ι → Prop) → [DecidablePred p] → (Π₀ (i : ι), β i) → Π₀ (i : Subtype p), β ↑i
-- Mathlib.GroupTheory.Nilpotent
/-- `upperCentralSeries G n` is the `n`th term in the upper central series of `G`.

This is the increasing chain of subgroups of `G` that starts with the trivial subgroup `⊥` of `G`
and then continues defining `upperCentralSeries G (n + 1)` to be all the elements of `G`
that, modulo `upperCentralSeries G n`, belong to the center of the quotient
`G ⧸ upperCentralSeries G n`.

In particular, the identities
* `upperCentralSeries G 0 = ⊥` (`upperCentralSeries_zero`);
* `upperCentralSeries G 1 = center G` (`upperCentralSeries_one`);

hold.
 -/
Subgroup.upperCentralSeries : (G : Type u_1) → [inst : Group G] → ℕ → Subgroup G
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- The map `(eVariationOn · s)` is lower semicontinuous for pointwise convergence *on `s`*.
Pointwise convergence on `s` is encoded here as uniform convergence on the family consisting of the
singletons of elements of `s`.
 -/
eVariationOn.lowerSemicontinuous : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (s : Set α),
  LowerSemicontinuous fun f => eVariationOn f s
-- Mathlib.Topology.Algebra.ProperConstSMul
/-- The preimage of a compact set under `(c +ᵥ ·)` is a compact set.  -/
IsCompact.preimage_vadd : ∀ {M : Type u_1} {X : Type u_2} [inst : VAdd M X] [inst_1 : TopologicalSpace X] [ProperConstVAdd M X] {s : Set X},
  IsCompact s → ∀ (c : M), IsCompact ((fun x => c +ᵥ x) ⁻¹' s)