mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.isAddUnit_detp_mul_detp : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R]
  {A B : Matrix n n R} {d : n → R},
  A * B = Matrix.diagonal d → IsAddUnit (Matrix.detp 1 A * Matrix.detp (-1) B + Matrix.detp (-1) A * Matrix.detp 1 B)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.specTargetImageFactorization_comp : ∀ {X : AlgebraicGeometry.Scheme} {A : CommRingCat} (f : X ⟶ AlgebraicGeometry.Spec A),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.specTargetImageFactorization f)
      (AlgebraicGeometry.Spec.map (AlgebraicGeometry.specTargetImageRingHom f)) =
    f
-- Std.Data.HashMap.IteratorLemmas
_private.Std.Data.HashMap.IteratorLemmas.0.Std.HashMap.iter.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.HashMap α β),
  m.iter = Std.Iter.map (fun e => (e.fst, e.snd)) m.inner.iter
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
SimpleGraph.vertexCoverNum_ne_top_of_finite : ∀ {V : Type u_1} {G : SimpleGraph V} [Finite V], G.vertexCoverNum ≠ ⊤
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor_obj_left_hom : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T × T)
  (Y : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.diag T) X),
  ((CategoryTheory.CostructuredArrow.ofDiagEquivalence.functor X).obj Y).left.hom = Y.hom.1
-- Mathlib.Analysis.Convolution
MeasureTheory.integral_convolution : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'} [inst_3 : RCLike 𝕜]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace ℝ F] [inst_7 : NormedSpace 𝕜 F]
  [inst_8 : MeasurableSpace G] {μ ν : MeasureTheory.Measure G} (L : E →L[𝕜] E' →L[𝕜] F) [CompleteSpace F]
  [inst_10 : AddGroup G] [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] [μ.IsAddRightInvariant] [MeasurableAdd₂ G]
  [MeasurableNeg G] [inst_16 : NormedSpace ℝ E] [inst_17 : NormedSpace ℝ E'] [CompleteSpace E] [CompleteSpace E'],
  MeasureTheory.Integrable f ν →
    MeasureTheory.Integrable g μ →
      ∫ (x : G), MeasureTheory.convolution f g L ν x ∂μ = (L (∫ (x : G), f x ∂ν)) (∫ (x : G), g x ∂μ)
-- Init.Data.String.Basic
String.Pos.ofSliceFrom_le_ofSliceFrom_iff : ∀ {s : String} {p : s.Pos} {q r : (s.sliceFrom p).Pos}, String.Pos.ofSliceFrom q ≤ String.Pos.ofSliceFrom r ↔ q ≤ r
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.iIndepSets.of_subsingleton : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure α} [Subsingleton ι] {m : ι → Set (Set Ω)} {κ : ProbabilityTheory.Kernel α Ω}
  [ProbabilityTheory.IsMarkovKernel κ], ProbabilityTheory.Kernel.iIndepSets m κ μ
-- Mathlib.LinearAlgebra.Matrix.Basis
Module.Basis.toMatrix_transpose_apply : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (e : Module.Basis ι R M) (v : ι' → M) (j : ι'), (e.toMatrix v).transpose j = ⇑(e.repr (v j))
-- Mathlib.NumberTheory.ModularForms.QExpansion
CuspFormClass.cuspFunction_apply_zero : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F)
  [CuspFormClass F Γ k], 0 < h → h ∈ Γ.strictPeriods → UpperHalfPlane.cuspFunction h (⇑f) 0 = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β} {fallback : α},
      (t.insertIfNew k v).minKeyD fallback = t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Lean.Elab.Tactic.Config
Lean.Elab.Tactic.ConfigItemView.mk.inj : ∀ {ref : Lean.Syntax} {option : Lean.Ident} {value : Lean.Term} {bool : Bool} {ref_1 : Lean.Syntax}
  {option_1 : Lean.Ident} {value_1 : Lean.Term} {bool_1 : Bool},
  { ref := ref, option := option, value := value, bool := bool } =
      { ref := ref_1, option := option_1, value := value_1, bool := bool_1 } →
    ref = ref_1 ∧ option = option_1 ∧ value = value_1 ∧ bool = bool_1
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- If `f x` equals `a` on for every point of the circle, then the circle average of `f` equals `a`.
 -/
Real.circleAverage_const_on_circle : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℂ → E} {c : ℂ} {R : ℝ} [CompleteSpace E]
  {a : E}, (∀ x ∈ Metric.sphere c |R|, f x = a) → Real.circleAverage f c R = a
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
BddAbove.mul : ∀ {M : Type u_3} [inst : Mul M] [inst_1 : Preorder M] [MulLeftMono M] [MulRightMono M] {s t : Set M},
  BddAbove s → BddAbove t → BddAbove (s * t)
-- Std.Time.Format.Modifier
Std.Time.Modifier.a.sizeOf_spec : ∀ (presentation : Std.Time.Text), sizeOf (Std.Time.Modifier.a presentation) = 1 + sizeOf presentation
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.mk : {R : Type u_1} →
  [inst : CommRing R] →
    {I : Ideal R} →
      {M : Type u_3} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            (N : ℕ → Submodule R M) → (∀ (i : ℕ), N (i + 1) ≤ N i) → (∀ (i : ℕ), I • N i ≤ N (i + 1)) → I.Filtration M
-- Mathlib.Data.Fintype.Defs
OrderDual.finite : ∀ (α : Type u_4) [Finite α], Finite αᵒᵈ
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.PresheafedSpace.GlueData.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : SizeOf C]
  (toGlueData : CategoryTheory.GlueData (AlgebraicGeometry.PresheafedSpace C))
  (f_open : ∀ (i j : toGlueData.J), AlgebraicGeometry.PresheafedSpace.IsOpenImmersion (toGlueData.f i j)),
  sizeOf { toGlueData := toGlueData, f_open := f_open } = 1 + sizeOf toGlueData
-- Mathlib.Data.Multiset.Filter
Multiset.countP_eq_countP_filter_add : ∀ {α : Type u_1} (s : Multiset α) (p q : α → Prop) [inst : DecidablePred p] [inst_1 : DecidablePred q],
  Multiset.countP p s = Multiset.countP p (Multiset.filter q s) + Multiset.countP p (Multiset.filter (fun a => ¬q a) s)
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCat_pOpcycles_eq_iff : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (x y : ↑S.X₂),
  (CategoryTheory.ConcreteCategory.hom S.pOpcycles) x = (CategoryTheory.ConcreteCategory.hom S.pOpcycles) y ↔
    x - y ∈ (ModuleCat.Hom.hom S.f).range
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.equivMapDomain_trans : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {G' : Type u_4} {G'' : Type u_5} (f : G ≃ G') (g : G' ≃ G'')
  (l : SkewMonoidAlgebra k G),
  SkewMonoidAlgebra.equivMapDomain (f.trans g) l =
    SkewMonoidAlgebra.equivMapDomain g (SkewMonoidAlgebra.equivMapDomain f l)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_castAdd_Iio_castAdd : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Fin.castAdd m ⁻¹' Set.Iio (Fin.castAdd m i) = Set.Iio i
-- Init.Data.Nat.Gcd
Nat.gcd_eq_zero_iff : ∀ {i j : ℕ}, i.gcd j = 0 ↔ i = 0 ∧ j = 0
-- Mathlib.Data.Setoid.Partition
Setoid.IsPartition.pairwiseDisjoint : ∀ {α : Type u_1} {c : Set (Set α)}, Setoid.IsPartition c → c.PairwiseDisjoint id
-- Mathlib.Algebra.Group.Semiconj.Basic
AddSemiconjBy.neg_symm_left_iff : ∀ {G : Type u_1} [inst : AddGroup G] {a x y : G}, AddSemiconjBy (-a) y x ↔ AddSemiconjBy a x y
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.inr_comp_inl_comp_associator : ∀ (x y z : AugmentedSimplexCategory),
  CategoryTheory.CategoryStruct.comp (x.inr y)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj x y).inl z)
        (CategoryTheory.MonoidalCategoryStruct.associator x y z).hom) =
    CategoryTheory.CategoryStruct.comp (y.inl z) (x.inr (CategoryTheory.MonoidalCategoryStruct.tensorObj y z))
-- Mathlib.AlgebraicTopology.SimplicialSet.Basic
SSet.δ_comp_δ_self_apply : ∀ {S : SSet} {n : ℕ} {i : Fin (n + 2)} (x : S.obj (Opposite.op { len := n + 2 })),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i.castSucc)) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ S i.succ)) x)
-- Mathlib.Tactic.ITauto
/-- Constructor for `¬ p`.  -/
Mathlib.Tactic.ITauto.IProp.not : Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp
-- Mathlib.Data.Nat.Choose.Lucas
/-- For primes `p` and positive integer `n`, assume that for all `i ∈ Icc 1 (n - 1)`,
`choose n i` congruent to `0` module `p`, then `n = p ^ multiplicity p n`.
Also see `eq_pow_multiplicity_of_choose_modEq_zero_nat` for the version with `MOD`.  -/
Choose.eq_pow_multiplicity_of_choose_modEq_zero : ∀ {n p : ℕ} [Fact (Nat.Prime p)],
  0 < n → (∀ i ∈ Finset.Icc 1 (n - 1), ↑(n.choose i) ≡ 0 [ZMOD ↑p]) → n = p ^ multiplicity p n
-- Mathlib.Topology.UniformSpace.Defs
comp_mem_uniformity_sets : ∀ {α : Type ua} [inst : UniformSpace α] {s : SetRel α α}, s ∈ uniformity α → ∃ t ∈ uniformity α, SetRel.comp t t ⊆ s
-- Lean.Expr
/-- A dependent arrow `(a : α) → β)` (aka forall-expression) where `β` may depend
on `a`. Note that this constructor is also used to represent non-dependent arrows
where `β` does not depend on `a`.

For example:
- `forall x : Prop, x ∧ x`:
  ```lean
  Expr.forallE `x (.sort .zero)
    (.app (.app (.const `And []) (.bvar 0)) (.bvar 0)) .default
  ```
- `Nat → Bool`:
  ```lean
  Expr.forallE `a (.const `Nat [])
    (.const `Bool []) .default
  ```
 -/
Lean.Expr.forallE : Lean.Name → Lean.Expr → Lean.Expr → Lean.BinderInfo → Lean.Expr
-- Mathlib.Geometry.Manifold.Instances.Real
modelWithCornersEuclideanHalfSpace.eq_1 : ∀ (n : ℕ) [inst : NeZero n],
  modelWithCornersEuclideanHalfSpace n =
    { toFun := Subtype.val, invFun := fun x => ⟨WithLp.toLp 2 (Function.update x.ofLp 0 (max (x.ofLp 0) 0)), ⋯⟩,
      source := Set.univ, target := {x | 0 ≤ x.ofLp 0}, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯,
      right_inv' := ⋯, source_eq := ⋯, convex_range' := ⋯, nonempty_interior' := ⋯, continuous_toFun := ⋯,
      continuous_invFun := ⋯ }
-- Mathlib.Algebra.Order.UpperLower
LowerSet.instAdd.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α],
  LowerSet.instAdd = { add := fun s t => { carrier := Set.image2 (fun x1 x2 => x1 + x2) ↑s ↑t, lower' := ⋯ } }
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_erase_eq_of_not_compare_minKey!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF → ∀ {k : α}, (t.erase k).isEmpty = false → ¬cmp k t.minKey! = Ordering.eq → (t.erase k).minKey! = t.minKey!
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_subset_Iic_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioc a b ⊆ Set.Iic b
-- Mathlib.Order.Hom.Lattice
InfHom.cancel_right : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Min α] [inst_1 : Min β] [inst_2 : Min γ] {g₁ g₂ : InfHom β γ}
  {f : InfHom α β}, Function.Surjective ⇑f → (g₁.comp f = g₂.comp f ↔ g₁ = g₂)
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
/-- The universal coprime factorization ring of a monic polynomial `p` of degree `n`.
This is the representing object of the functor
`S ↦ "factorizations of p into coprime (monic deg m) * (monic deg k) in S"`.
See `UniversalCoprimeFactorizationRing.homEquiv`.  -/
Polynomial.UniversalCoprimeFactorizationRing : {R : Type u_1} → [inst : CommRing R] → {n : ℕ} → (m k : ℕ) → n = m + k → Polynomial.MonicDegreeEq R n → Type u_1
-- Mathlib.Data.Set.Lattice.Image
Set.kernImage_preimage_eq_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, Set.kernImage f (f ⁻¹' s) = s ↔ (Set.range f)ᶜ ⊆ s
-- Mathlib.Algebra.Order.Sub.WithTop
WithTop.sub_ne_top_iff : ∀ {α : Type u_1} [inst : Sub α] [inst_1 : Bot α] {a b : WithTop α}, a - b ≠ ⊤ ↔ a ≠ ⊤ ∨ b = ⊤
-- Mathlib.Algebra.Ring.Defs
mul_one_sub : ∀ {α : Type u} [inst : NonAssocRing α] (a b : α), a * (1 - b) = a - a * b
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
RootPairing.coPolarization_apply_eq_zero_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : Fintype ι]
  (n : N), P.CoPolarization n = 0 ↔ P.CorootForm n = 0
-- Mathlib.Analysis.Convex.GaugeRescale
image_gaugeRescaleHomeomorph_closure : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
  [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul ℝ E] [inst_5 : T1Space E] {s t : Set E} (hsc : Convex ℝ s)
  (hs₀ : s ∈ nhds 0) (hsb : Bornology.IsVonNBounded ℝ s) (htc : Convex ℝ t) (ht₀ : t ∈ nhds 0)
  (htb : Bornology.IsVonNBounded ℝ t), ⇑(gaugeRescaleHomeomorph s t hsc hs₀ hsb htc ht₀ htb) '' closure s = closure t
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ring : {R : Type u_1} → {M : Type u_4} → [inst : Ring R] → [AddMonoid M] → Ring (AddMonoidAlgebra R M)
-- Mathlib.Logic.Equiv.List
/-- Explicit decoding function for `List α`  -/
Encodable.decodeList : {α : Type u_1} → [Encodable α] → ℕ → Option (List α)
-- Mathlib.RingTheory.Finiteness.Defs
RingHom.Finite.eq_1 : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] (f : A →+* B), f.Finite = Module.Finite A B
-- Mathlib.Order.RelIso.Basic
RelIso.relEmbeddingCongr_apply : ∀ {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop}
  {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₁ : r₁ ↪r s₁),
  (e₁.relEmbeddingCongr e₂) f₁ = (e₁.symm.toRelEmbedding.trans f₁).trans e₂.toRelEmbedding
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
CliffordAlgebra.foldr'_ι_mul : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N)
  (hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), (f m) ((CliffordAlgebra.ι Q) m * x, (f m) (x, fx)) = Q m • fx)
  (n : N) (m : M) (x : CliffordAlgebra Q),
  (CliffordAlgebra.foldr' Q f hf n) ((CliffordAlgebra.ι Q) m * x) = (f m) (x, (CliffordAlgebra.foldr' Q f hf n) x)
-- Mathlib.Order.Filter.IsBounded
Filter.isBoundedUnder_le_neg : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α] {l : Filter β}
  {u : β → α},
  (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => -u x) ↔ Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) l u
-- Init.Data.String.Iterate
/-- Creates an iterator over all valid positions within {name}`s`, starting from the last valid
position and iterating towards the first one.

Examples
 * {lean}`("abc".toSlice.revPositions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['c', 'b', 'a']`
 * {lean}`("abc".toSlice.revPositions.map (·.val.offset.byteIdx) |>.toList) = [2, 1, 0]`
 * {lean}`("ab∀c".toSlice.revPositions.map (fun ⟨p, h⟩ => p.get h) |>.toList) = ['c', '∀', 'b', 'a']`
 * {lean}`("ab∀c".toSlice.revPositions.map (·.val.offset.byteIdx) |>.toList) = [5, 2, 1, 0]`
 -/
String.Slice.revPositions : (s : String.Slice) → Std.Iter { p // p ≠ s.endPos }
-- Mathlib.Tactic.Ring.Common
/-- Exponentiates a polynomial `va` by a monomial `vb`, including several special cases.

* `a ^ 1 = a`
* `0 ^ e = 0` if `0 < e`
* `(a + 0) ^ b = a ^ b` computed using `evalPowProd`
* `a ^ b = (a ^ b') ^ k` if `b = b' * k` and `k > 1`

Otherwise `a ^ b` is just encoded as `a ^ b * 1 + 0` using `evalPowAtom`.
 -/
Mathlib.Tactic.Ring.Common.evalPow₁ : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        Mathlib.Tactic.Ring.Common.RingCompute bt sα →
          Mathlib.Tactic.Ring.Common.RingCompute Mathlib.Tactic.Ring.Common.btℕ Mathlib.Tactic.Ring.Common.sℕ →
            {a : Q(«$α»)} →
              {b : Q(ℕ)} →
                Mathlib.Tactic.Ring.Common.ExSum bt sα a →
                  Mathlib.Tactic.Ring.Common.ExProdNat b →
                    Lean.MetaM
                      (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum bt sα) q(«$a» ^ «$b»))
-- Lean.Environment
/-- Name of all imported modules (directly and indirectly).
The index of a module name in the array equals the `ModuleIdx` for the same module.
 -/
Lean.EnvironmentHeader.moduleNames : Lean.EnvironmentHeader → Array Lean.Name
-- Mathlib.FieldTheory.SeparableClosure
IntermediateField.insepDegree_bot' : ∀ {F : Type u} (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type v) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [inst_6 : IsScalarTower F E K],
  Field.insepDegree F ↥⊥ = Field.insepDegree F E
-- Init.Prelude
/-- The notation typeclass for heterogeneous division.
This enables the notation `a / b : γ` where `a : α`, `b : β`.
 -/
HDiv : Type u → Type v → outParam (Type w) → Type (max (max u v) w)
-- Mathlib.Topology.Semicontinuity.Defs
LowerHemicontinuousAt.const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {x : α} {z : Set β},
  LowerHemicontinuousAt (fun _x => z) x
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Infinite.orderOf_eq_zero_of_forall_mem_zpowers : ∀ {α : Type u_1} [inst : Group α] [Infinite α] {g : α}, (∀ (x : α), x ∈ Subgroup.zpowers g) → orderOf g = 0
-- Mathlib.Data.Fin.Basic
Fin.natCast_strictMono : ∀ {n a b : ℕ}, b ≤ n → a < b → ↑a < ↑b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKey!_unitOfList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] [inst_2 : Inhabited α]
  {l : List α} {k : α}, l.contains k = false → (Std.DTreeMap.Const.unitOfList l cmp).getKey! k = default
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyMapIso'_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  (CategoryTheory.ShortComplex.rightHomologyMapIso' e h₁ h₂).hom =
    CategoryTheory.ShortComplex.rightHomologyMap' e.hom h₁ h₂
-- Init.Data.BitVec.Lemmas
BitVec.getElem_fill : ∀ {w i : ℕ} {v : Bool} (h : i < w), (BitVec.fill w v)[i] = v
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.instMonoidalForget.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.AddMon.instMonoidalForget C =
    { εIso := CategoryTheory.Iso.refl (CategoryTheory.MonoidalCategoryStruct.tensorUnit C),
        μIso := fun x x_1 =>
          CategoryTheory.Iso.refl
            (CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.AddMon.forget C).obj x)
              ((CategoryTheory.AddMon.forget C).obj x_1)),
        μIso_hom_natural_left := ⋯, μIso_hom_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯,
        right_unitality := ⋯ }.toMonoidal
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexivePair.mkNatTrans_app_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C}
  (e₀ : F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ⟶ G.obj CategoryTheory.Limits.WalkingReflexivePair.zero)
  (e₁ : F.obj CategoryTheory.Limits.WalkingReflexivePair.one ⟶ G.obj CategoryTheory.Limits.WalkingReflexivePair.one)
  (h₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) e₀ =
        CategoryTheory.CategoryStruct.comp e₁ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left))
      _auto_153✝)
  (h₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) e₀ =
        CategoryTheory.CategoryStruct.comp e₁ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right))
      _auto_155✝)
  (h₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion) e₁ =
        CategoryTheory.CategoryStruct.comp e₀ (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion))
      _auto_157✝),
  (CategoryTheory.Limits.reflexivePair.mkNatTrans e₀ e₁ h₁ h₂ h₃).app CategoryTheory.Limits.WalkingReflexivePair.zero =
    e₀
-- Mathlib.Data.Erased
/-- Equivalence between `Erased α` and `α`.  -/
Erased.equiv : (α : Sort u_1) → Erased α ≃ α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_insert : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m).WF →
    ∀ {k a : α} {v : β},
      Std.DHashMap.Internal.Raw₀.Const.get! (m.insert k v) a =
        if (k == a) = true then v else Std.DHashMap.Internal.Raw₀.Const.get! m a
-- Mathlib.Tactic.NormNum.DivMod
Mathlib.Meta.NormNum.isInt_ediv : ∀ {a b q m a' : ℤ} {b' r : ℕ},
  Mathlib.Meta.NormNum.IsInt a a' →
    Mathlib.Meta.NormNum.IsNat b b' → q * ↑b' = m → ↑r + m = a' → r.blt b' = true → Mathlib.Meta.NormNum.IsInt (a / b) q
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.OuterMeasure.toMeasure.congr_simp : ∀ {α : Type u_1} [ms : MeasurableSpace α] (m m_1 : MeasureTheory.OuterMeasure α) (e_m : m = m_1)
  (h : ms ≤ m.caratheodory), m.toMeasure h = m_1.toMeasure ⋯
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- Cosine Hurwitz zeta kernel. See `cosKernel_def` for the defining formula, and
`hasSum_int_cosKernel` for expression as a sum.  -/
HurwitzZeta.cosKernel : UnitAddCircle → ℝ → ℝ
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearEquiv.lTensor_mul : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (f g : N ≃ₗ[R] N),
  LinearEquiv.lTensor M (f * g) = LinearEquiv.lTensor M f * LinearEquiv.lTensor M g
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.mkOfMemSupportIff_ideal : ∀ {X : AlgebraicGeometry.Scheme} (ideal : (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U)))
  (map_ideal_basicOpen :
    ∀ (U : ↑X.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))),
      Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (ideal U) =
        ideal (X.affineBasicOpen f))
  (supportSet : Set ↥X)
  (supportSet_inter : ∀ (U : ↑X.affineOpens), ∀ x ∈ ↑U, x ∈ supportSet ↔ x ∈ X.zeroLocus ↑(ideal U))
  (U : ↑X.affineOpens),
  (AlgebraicGeometry.Scheme.IdealSheafData.mkOfMemSupportIff ideal map_ideal_basicOpen supportSet
          supportSet_inter).ideal
      U =
    ideal U
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.EquivalenceRelation.symmetry₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.EquivalenceRelation p₁ p₂), CategoryTheory.CategoryStruct.comp self.s p₂ = p₁
-- Mathlib.Algebra.Category.AlgCat.Limits
AlgCat.limitAlgebra : {R : Type u} →
  [inst : CommRing R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.Category.{t, v} J] →
        (F : CategoryTheory.Functor J (AlgCat R)) →
          [inst_2 : Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (AlgCat R))).sections] →
            Algebra R (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget (AlgCat R)))).pt
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.alter.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashMap α β),
  m = m_1 → ∀ (a a_1 : α), a = a_1 → ∀ (f f_1 : Option β → Option β), f = f_1 → m.alter a f = m_1.alter a_1 f_1