mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finset.Insert
List.toFinset_replicate_of_ne_zero : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {n : ℕ}, n ≠ 0 → (List.replicate n a).toFinset = {a}
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.toListModel_eq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.OrientedOrd α] {t t' : Std.DTreeMap.Internal.Impl α β},
  t.Equiv t' → t.Ordered → t'.Ordered → t.toListModel = t'.toListModel
-- Std.Do.Triple.SpecLemmas
_private.Std.Do.Triple.SpecLemmas.0.Lean.Loop.forIn.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (__do_lift : ForInStep β) →
      ((b' : β) → motive (ForInStep.done b')) → ((b' : β) → motive (ForInStep.yield b')) → motive __do_lift
-- Mathlib.Condensed.Discrete.Module
LightCondMod.LocallyConstant.functorIsoDiscreteAux₂.eq_1 : ∀ (R : Type u) [inst : Ring R] (M : ModuleCat R),
  LightCondMod.LocallyConstant.functorIsoDiscreteAux₂ R M =
    (LightCondensed.discrete (ModuleCat R)).mapIso (LightCondMod.LocallyConstant.functorIsoDiscreteAux₁ R M)
-- Mathlib.RingTheory.Frobenius
IsArithFrobAt.arithFrobAt_mem_stabilizer : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (G : Type u_3)
  [inst_3 : Group G] [inst_4 : MulSemiringAction G S] [inst_5 : SMulCommClass G R S] (Q : Ideal S) [inst_6 : Finite G]
  [inst_7 : Algebra.IsInvariant R S G] [inst_8 : Q.IsPrime] [inst_9 : Finite (S ⧸ Q)],
  arithFrobAt R G Q ∈ MulAction.stabilizer G Q
-- Mathlib.Algebra.Ring.Action.Pointwise.Finset
Finset.zero_mem_smul_finset_iff : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [IsDomain R] [inst_2 : AddCommMonoid M] [inst_3 : DecidableEq M]
  [inst_4 : Module R M] [Module.IsTorsionFree R M] {t : Finset M} {r : R}, r ≠ 0 → (0 ∈ r • t ↔ 0 ∈ t)
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- An `n`-dimensional `InnerProductSpace` equipped with a decomposition as an internal direct
sum has an orthonormal basis indexed by `Fin n` and subordinate to that direct sum.  -/
DirectSum.IsInternal.subordinateOrthonormalBasis : {ι : Type u_7} →
  {𝕜 : Type u_8} →
    [inst : RCLike 𝕜] →
      {E : Type u_9} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [Fintype ι] →
              [FiniteDimensional 𝕜 E] →
                {n : ℕ} →
                  Module.finrank 𝕜 E = n →
                    [inst_5 : DecidableEq ι] →
                      {V : ι → Submodule 𝕜 E} →
                        DirectSum.IsInternal V →
                          (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) → OrthonormalBasis (Fin n) 𝕜 E
-- Init.GrindInstances.Ring.Fin
Lean.Grind.Fin.instPowIdentityFinOfNatNat : Lean.Grind.PowIdentity (Fin 2) 2
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.Hom.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {V₀ V₁ : CategoryTheory.Endofunctor.Coalgebra F} [inst_1 : SizeOf C] (f : V₀.V ⟶ V₁.V)
  (h :
    autoParam (CategoryTheory.CategoryStruct.comp V₀.str (F.map f) = CategoryTheory.CategoryStruct.comp f V₁.str)
      CategoryTheory.Endofunctor.Coalgebra.Hom.h._autoParam),
  sizeOf { f := f, h := h } = 1 + sizeOf f + sizeOf h
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.isWeaklyEisensteinAt_iff : ∀ {R : Type u} [inst : CommSemiring R] (f : Polynomial R) (𝓟 : Ideal R),
  f.IsWeaklyEisensteinAt 𝓟 ↔ ∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟
-- Mathlib.GroupTheory.RegularWreathProduct
iteratedWreathToPermHomInj : ∀ (G : Type u_3) [inst : Group G] (n : ℕ), Function.Injective ⇑(iteratedWreathToPermHom G n)
-- Mathlib.Topology.Order.HullKernel
/-- For `a` of type `α` the set of element of `T` which dominate `a` is the `hull` of `a` in `T`.  -/
PrimitiveSpectrum.hull : {α : Type u_1} → [SemilatticeInf α] → (T : Set α) → α → Set ↑T
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_filter_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.getEntry? k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) =
      if Std.Internal.List.containsKey k l₂ = true then Std.Internal.List.getEntry? k l₁ else none
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_eq_choose_pred_add : ∀ {n k : ℕ}, 0 < n → 0 < k → n.choose k = (n - 1).choose (k - 1) + (n - 1).choose k
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_coe_angle_toReal_eq_arg : ∀ (z : ℂ), (↑z.arg).toReal = z.arg
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Real.closedBall_eq_Icc : ∀ {x r : ℝ}, Metric.closedBall x r = Set.Icc (x - r) (x + r)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMonNatIso.eq_1 : ∀ {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 D]
  {F F' : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] [inst_5 : F'.LaxMonoidal] (e : F ≅ F')
  [inst_6 : CategoryTheory.NatTrans.IsMonoidal e.hom],
  CategoryTheory.Functor.mapMonNatIso e =
    CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Mon.mkIso (e.app X.X) ⋯ ⋯) ⋯
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
/-- For a slightly stronger version, see `eval_single_add`.  -/
Ordinal.CNF.eval_single_add' : ∀ (b : Ordinal.{u_1}) {e x : Ordinal.{u_1}} {f : Ordinal.{u_1} →₀ Ordinal.{u_1}},
  (∀ e' ∈ f.support, e' < e) → Ordinal.CNF.eval b ((fun₀ | e => x) + f) = b ^ e * x + Ordinal.CNF.eval b f
-- Lean.Elab.Do.InferControlInfo
Lean.Elab.Do.instInhabitedControlInfo : Inhabited Lean.Elab.Do.ControlInfo
-- Mathlib.CategoryTheory.Limits.MonoCoprod
/-- This condition expresses that inclusion morphisms into coproducts are monomorphisms.  -/
CategoryTheory.Limits.MonoCoprod : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Prop
-- Init.Data.List.Basic
List.find?_cons : ∀ {α : Type u_1} {a : α} {as : List α} {p : α → Bool},
  List.find? p (a :: as) =
    match p a with
    | true => some a
    | false => List.find? p as
-- Mathlib.Analysis.Convex.Between
wbtw_mul_sub_add_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [IsDomain R] {x y r : R},
  Wbtw R x (r * (y - x) + x) y ↔ x = y ∨ r ∈ Set.Icc 0 1
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.coe_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {N : Type u_6}
  [inst_4 : TopologicalSpace N] [inst_5 : ChartedSpace H N] {n : WithTop ℕ∞} {V : Type u_10}
  [inst_6 : NormedAddCommGroup V] [inst_7 : NormedSpace 𝕜 V] (r : 𝕜)
  (f : ContMDiffMap I (modelWithCornersSelf 𝕜 V) N V n), ⇑(r • f) = r • ⇑f
-- Mathlib.Analysis.Normed.Operator.NNNorm
/-- continuous linear maps are Lipschitz continuous.  -/
ContinuousLinearMap.lipschitz : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  (f : E →SL[σ₁₂] F), LipschitzWith ‖f‖₊ ⇑f
-- Lean.Meta.Tactic.LibrarySearch
Lean.Meta.LibrarySearch.DeclMod.noConfusionType : Sort v✝ → Lean.Meta.LibrarySearch.DeclMod → Lean.Meta.LibrarySearch.DeclMod → Sort v✝
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_ric_eq_some : ∀ {n i : ℕ}, i ≤ n → (*...=n).toArray[i]? = some i
-- Lean.Parser.Command
Lean.Parser.Command.sectionHeader.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.CountableDenseLinearOrder
/-- The set of partial isomorphisms defined at `a : α`, together with a proof that any
partial isomorphism can be extended to one defined at `a`.  -/
Order.PartialIso.definedAtLeft : {α : Type u_1} →
  (β : Type u_2) →
    [inst : LinearOrder α] →
      [inst_1 : LinearOrder β] →
        [DenselyOrdered β] → [NoMinOrder β] → [NoMaxOrder β] → [Nonempty β] → α → Order.Cofinal (Order.PartialIso α β)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → γ} {k : α} {h' : k ∈ Std.ExtHashMap.map f m},
  (Std.ExtHashMap.map f m).getKey k h' = m.getKey k ⋯
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
ordinaryHypergeometricSeries_apply_zero : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (a b c : 𝕂) (n : ℕ),
  ((ordinaryHypergeometricSeries 𝔸 a b c n) fun x => 0) = Pi.single 0 1 n
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Projection
isIdempotentElem_star_mul_self_iff_isIdempotentElem_self_mul_star : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℝ A]
  [inst_4 : IsScalarTower ℝ A A] [inst_5 : SMulCommClass ℝ A A]
  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] {x : A},
  IsIdempotentElem (star x * x) ↔ IsIdempotentElem (x * star x)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms
SimplexCategoryGenRel.IsAdmissible.isChain : ∀ {m : ℕ} {L : List ℕ}, SimplexCategoryGenRel.IsAdmissible m L → List.IsChain (fun x1 x2 => x1 < x2) L
-- Mathlib.Algebra.Module.Torsion.Basic
/-- A torsion module is a module where every element is `a`-torsion for some non-zero-divisor `a`.
 -/
Module.IsTorsion : (R : Type u_1) → (M : Type u_2) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Prop
-- Mathlib.LinearAlgebra.Dimension.OrzechProperty
finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : OrzechProperty R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {s : Finset M} (le_span : ⊤ ≤ Submodule.span R ↑s) (card_eq : s.card = Module.finrank R M)
  (x : M),
  (finsetBasisOfTopLeSpanOfCardEqFinrank le_span card_eq).repr x =
    ⋯.repr ((LinearMap.codRestrict (Submodule.span R (Set.range Subtype.val)) LinearMap.id ⋯) x)
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.le_order_prod : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {ι : Type u_4} (f : ι → MvPowerSeries σ R) (s : Finset ι),
  ∑ i ∈ s, (f i).order ≤ (∏ i ∈ s, f i).order
-- Mathlib.Condensed.Discrete.Basic
CompHaus.of.congr_simp : ∀ (X : Type u_1) [inst : TopologicalSpace X] [inst_1 : CompactSpace X] [inst_2 : T2Space X],
  CompHaus.of X = CompHaus.of X
-- Mathlib.Data.DFinsupp.WellFounded
Pi.wellFoundedLT : ∀ {ι : Type u_1} {α : ι → Type u_2} [Finite ι] [inst : (i : ι) → Preorder (α i)] [hw : ∀ (i : ι), WellFoundedLT (α i)],
  WellFoundedLT ((i : ι) → α i)
-- Mathlib.Algebra.Module.Bimodule
Subbimodule.coe_toSubmodule : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring A] [inst_4 : Semiring B] [inst_5 : Module A M] [inst_6 : Module B M]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M]
  [inst_11 : SMulCommClass A B M] (p : Submodule (TensorProduct R A B) M), ↑(Subbimodule.toSubmodule p) = ↑p
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.instRepr : {α : Type u_2} → [Repr α] → Repr (Ordnode α)
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
CategoryTheory.PreZeroHypercover.Relation.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S : C} {E : CategoryTheory.PreZeroHypercover S}
  {i j : E.I₀} (obj : C) (fst : obj ⟶ E.X i) (snd : obj ⟶ E.X j)
  (w : CategoryTheory.CategoryStruct.comp fst (E.f i) = CategoryTheory.CategoryStruct.comp snd (E.f j)) (obj_1 : C)
  (fst_1 : obj_1 ⟶ E.X i) (snd_1 : obj_1 ⟶ E.X j)
  (w_1 : CategoryTheory.CategoryStruct.comp fst_1 (E.f i) = CategoryTheory.CategoryStruct.comp snd_1 (E.f j)),
  ({ obj := obj, fst := fst, snd := snd, w := w } = { obj := obj_1, fst := fst_1, snd := snd_1, w := w_1 }) =
    (obj = obj_1 ∧ fst ≍ fst_1 ∧ snd ≍ snd_1)
-- Mathlib.Data.Set.Prod
Set.compl_prod_eq_union : ∀ {α : Type u_5} {β : Type u_6} (s : Set α) (t : Set β), (s ×ˢ t)ᶜ = sᶜ ×ˢ Set.univ ∪ Set.univ ×ˢ tᶜ
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.single_kronecker_single : ∀ {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [inst : MulZeroClass α]
  [inst_1 : DecidableEq l] [inst_2 : DecidableEq m] [inst_3 : DecidableEq n] [inst_4 : DecidableEq p] (ia : l) (ja : m)
  (ib : n) (jb : p) (a b : α),
  Matrix.kroneckerMap (fun x1 x2 => x1 * x2) (Matrix.single ia ja a) (Matrix.single ib jb b) =
    Matrix.single (ia, ib) (ja, jb) (a * b)
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.coeffs_h_subset : ∀ (R : Type u_1) [inst : CommRing R] {A : Type u} {B : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra A B] (D : Algebra.Smooth.DescentAux✝ A B)
  (i : Algebra.Smooth.DescentAux.vars✝ D),
  ↑(Algebra.Smooth.DescentAux.h✝ D i).coeffs ⊆ Set.range ⇑(algebraMap (↥(Algebra.Smooth.DescentAux.subalgebra✝ R D)) A)
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- **Alias** of the reverse direction of `hasFDerivAt_iff_isLittleO`. -/
HasFDerivAt.of_isLittleO : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E}, ((fun x' => f x' - f x - f' (x' - x)) =o[nhds x] fun x' => x' - x) → HasFDerivAt f f' x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equifibered
CategoryTheory.NatTrans.Equifibered.unop : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} C] {F G : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} {α : F ⟶ G},
  CategoryTheory.NatTrans.Equifibered α → CategoryTheory.NatTrans.Coequifibered (CategoryTheory.NatTrans.unop α)
-- Mathlib.Probability.Process.Predictable
MeasureTheory.measurableSet_predictable_singleton_prod : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {𝓕 : MeasureTheory.Filtration ℕ m} {n : ℕ} {s : Set Ω},
  MeasurableSet s → MeasurableSet ({n + 1} ×ˢ s)
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.setCurr.eq_1 : ∀ (x : Char) (s : String) (i : String.Pos.Raw), { s := s, i := i }.setCurr x = { s := String.Pos.Raw.set s i x, i := i }
-- Mathlib.Data.PFun
PFun.Dom.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β), f.Dom = {a | (f a).Dom}
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instAddMonoidWithOne : {n : Type u_2} → {A : Type u_5} → [DecidableEq n] → [AddMonoidWithOne A] → AddMonoidWithOne (CStarMatrix n n A)
-- Mathlib.Analysis.Convex.Gauge
comap_gauge_nhds_zero_le : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : TopologicalSpace E],
  Absorbent ℝ s → Bornology.IsVonNBounded ℝ s → Filter.comap (gauge s) (nhds 0) ≤ nhds 0
-- Lean.Elab.App
/-- Process a `fType` of the form `[x : A] → B x`.
This method assume `fType` is a function type.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.processInstImplicitArg : Lean.Name → Lean.Elab.Term.ElabAppArgs.M Lean.Expr
-- Mathlib.Topology.MetricSpace.Algebra
/-- Eta-expanded form of `TendstoLocallyUniformly.mul₀_of_isBoundedUnder` -/
TendstoLocallyUniformly.fun_mul₀_of_isBoundedUnder : ∀ {X : Type u_3} {M : Type u_4} {ι : Type u_5} [inst : TopologicalSpace X] [inst_1 : PseudoMetricSpace M]
  [inst_2 : Zero M] [inst_3 : Mul M] [IsBoundedSMul M M] {F G : ι → X → M} {f g : X → M} {l : Filter ι},
  TendstoLocallyUniformly F f l →
    TendstoLocallyUniformly G g l →
      (∀ (x : X), Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhds x) fun y => dist (f y) 0) →
        (∀ (x : X), Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhds x) fun y => dist (g y) 0) →
          TendstoLocallyUniformly (fun i i_1 => F i i_1 * G i i_1) (fun i => f i * g i) l
-- Mathlib.Logic.Relation
Relation.ReflTransGen.cases_head_iff : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α},
  Relation.ReflTransGen r a b ↔ a = b ∨ ∃ c, r a c ∧ Relation.ReflTransGen r c b
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.dec.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId} {n : ℕ} {check persistent : Bool} {objs? : Option ℕ}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_13} {fvarId_1 : Lean.FVarId}
  {n_1 : ℕ} {check_1 persistent_1 : Bool} {objs?_1 : Option ℕ}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_13},
  Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h =
      Lean.Compiler.LCNF.CodeDecl.dec fvarId_1 n_1 check_1 persistent_1 objs?_1 h_1 →
    fvarId = fvarId_1 ∧ n = n_1 ∧ check = check_1 ∧ persistent = persistent_1 ∧ objs? = objs?_1
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
hasProd_subtype_iff_mulIndicator : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α} {s : Set β},
  HasProd (f ∘ Subtype.val) a ↔ HasProd (s.mulIndicator f) a
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsAddTorsion.torsionAddEquiv_apply`. -/
AddMonoid.IsTorsion.torsionAddEquiv_apply : ∀ {G : Type u_1} [inst : AddCommMonoid G] (tG : IsAddTorsion G) (a : ↥(AddCommMonoid.addTorsion G)),
  tG.torsionAddEquiv a = ↑((AddEquiv.addSubmonoidCongr ⋯) a)
-- Mathlib.RingTheory.Kaehler.Basic
/-- The `S`-submodule of `S →₀ S` (the direct sum of copies of `S` indexed by `S`) generated by
the relations:
1. `dx + dy = d(x + y)`
2. `x dy + y dx = d(x * y)`
3. `dr = 0` for `r ∈ R`

where `db` is the unit in the copy of `S` with index `b`.

This is the kernel of the surjection
`Finsupp.linearCombination S Ω[S⁄R] S (KaehlerDifferential.D R S)`.
See `KaehlerDifferential.kerTotal_eq` and `KaehlerDifferential.linearCombination_surjective`.
 -/
KaehlerDifferential.kerTotal : (R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Submodule S (S →₀ S)
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.BoundedFormula.listEncode.match_1.eq_4 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) (x : ℕ)
  (φ₁ φ₂ : L.BoundedFormula α x) (h_1 : (n : ℕ) → motive n FirstOrder.Language.BoundedFormula.falsum)
  (h_2 : (x : ℕ) → (t₁ t₂ : L.Term (α ⊕ Fin x)) → motive x (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (n l : ℕ) →
      (R : L.Relations l) → (ts : Fin l → L.Term (α ⊕ Fin n)) → motive n (FirstOrder.Language.BoundedFormula.rel R ts))
  (h_4 : (x : ℕ) → (φ₁ φ₂ : L.BoundedFormula α x) → motive x (φ₁.imp φ₂))
  (h_5 : (x : ℕ) → (φ : L.BoundedFormula α (x + 1)) → motive x φ.all),
  (match x, φ₁.imp φ₂ with
    | n, FirstOrder.Language.BoundedFormula.falsum => h_1 n
    | x, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 x t₁ t₂
    | n, FirstOrder.Language.BoundedFormula.rel R ts => h_3 n l R ts
    | x, φ₁.imp φ₂ => h_4 x φ₁ φ₂
    | x, φ.all => h_5 x φ) =
    h_4 x φ₁ φ₂
-- Mathlib.Algebra.Group.End
Equiv.Perm.sumCongr_one : ∀ {α : Type u_7} {β : Type u_8}, Equiv.Perm.sumCongr 1 1 = 1
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- An additive character on `ZMod n` is nontrivial iff it takes a value `≠ 1` on `1`.  -/
AddChar.zmod_char_ne_one_iff : ∀ {C : Type v} [inst : CommMonoid C] (n : ℕ) [NeZero n] (ψ : AddChar (ZMod n) C), ψ ≠ 1 ↔ ψ 1 ≠ 1
-- Mathlib.Data.ENNReal.Inv
ENNReal.smul_iSup : ∀ {ι : Sort u_1} {R : Type u_3} [inst : SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (f : ι → ENNReal) (c : R),
  c • ⨆ i, f i = ⨆ i, c • f i
-- Mathlib.Topology.ContinuousMap.Ideals
ContinuousMap.setOfTop_eq_univ : ∀ {X : Type u_1} {R : Type u_2} [inst : TopologicalSpace X] [inst_1 : Semiring R] [inst_2 : TopologicalSpace R]
  [inst_3 : IsTopologicalSemiring R] [Nontrivial R], ContinuousMap.setOfIdeal ⊤ = Set.univ
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.text : {α : Type u} → String → Lean.Widget.TaggedText α
-- Mathlib.Order.Filter.Map
Filter.comap_const_of_notMem : ∀ {α : Type u_1} {β : Type u_2} {g : Filter β} {t : Set β} {x : β}, t ∈ g → x ∉ t → Filter.comap (fun x_1 => x) g = ⊥
-- Lean.Elab.Term.TermElabM
/-- Map from internal name to fvar  -/
Lean.Elab.Term.Context.sectionFVars : Lean.Elab.Term.Context → Lean.NameMap Lean.Expr
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.Quotient.cast.congr_simp : ∀ {X : Type u} [inst : TopologicalSpace X] {x y : X} (γ γ_1 : Path.Homotopic.Quotient x y),
  γ = γ_1 → ∀ {x' y' : X} (hx : x' = x) (hy : y' = y), γ.cast hx hy = γ_1.cast hx hy
-- Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Multiset.le_prod_of_submultiplicative_on_pred_of_nonneg : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : CommMonoidWithZero β] [inst_2 : PartialOrder β]
  [PosMulMono β] (f : α → β) (p : α → Prop),
  (∀ (a : α), 0 ≤ f a) →
    f 1 ≤ 1 →
      (∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b) →
        (∀ (a b : α), p a → p b → p (a * b)) → ∀ (s : Multiset α), (∀ a ∈ s, p a) → f s.prod ≤ (Multiset.map f s).prod
-- Mathlib.Algebra.Module.ZMod
/-- Reinterpret an additive homomorphism as a `ℤ/nℤ`-linear map.

See also:
`AddMonoidHom.toIntLinearMap`, `AddMonoidHom.toNatLinearMap`, `AddMonoidHom.toRatLinearMap`  -/
AddMonoidHom.toZModLinearMap : (n : ℕ) →
  {M : Type u_1} →
    {M₁ : Type u_2} →
      [inst : AddCommGroup M] →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : Module (ZMod n) M] → [inst_3 : Module (ZMod n) M₁] → (M →+ M₁) → M →ₗ[ZMod n] M₁
-- Mathlib.Topology.Algebra.StarSubalgebra
StarSubalgebra.instCompleteSpaceSubtypeMemTopologicalClosure : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : StarRing R] {A : Type u_4} [inst_2 : UniformSpace A]
  [CompleteSpace A] [inst_4 : Semiring A] [inst_5 : StarRing A] [inst_6 : IsSemitopologicalSemiring A]
  [inst_7 : ContinuousStar A] [inst_8 : Algebra R A] [inst_9 : StarModule R A] {S : StarSubalgebra R A},
  CompleteSpace ↥S.topologicalClosure
-- Mathlib.RingTheory.Congruence.Basic
_private.Mathlib.RingTheory.Congruence.Basic.0.RingCon.comap_ringConGen_equiv : {R : Type u_3} →
  {R' : Type u_4} →
    [inst : Add R] →
      [inst_1 : Mul R] →
        [inst_2 : Add R'] →
          [inst_3 : Mul R'] →
            {F : Type u_5} →
              [inst_4 : FunLike F R' R] →
                [inst_5 : MulHomClass F R' R] →
                  [inst_6 : AddHomClass F R' R] →
                    [EquivLike F R' R] →
                      (r : R → R → Prop) →
                        (f : F) → ProofWanted ((ringConGen r).comap f = ringConGen (Function.onFun r ⇑f))
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofDocElabInfo.inj : ∀ {i i_1 : Lean.Elab.DocElabInfo}, Lean.Elab.Info.ofDocElabInfo i = Lean.Elab.Info.ofDocElabInfo i_1 → i = i_1
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.IsQuasicoherent.nonempty_quasicoherentData : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat}
  {inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat} {M : SheafOfModules R}
  [self : M.IsQuasicoherent], Nonempty M.QuasicoherentData
-- Mathlib.LinearAlgebra.Alternating.Basic
_private.Mathlib.LinearAlgebra.Alternating.Basic.0.MultilinearMap.alternization_map_eq_zero_of_eq_aux : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6}
  [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι]
  (m : MultilinearMap R (fun x => M) N') (v : ι → M) (i j : ι),
  i ≠ j → v i = v j → (∑ σ, Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ m) v = 0