mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Tannaka
/-- For `v : X` and `G` a finite group, the `G`-equivariant linear map from the right
regular representation `rightFDRep` to `X` sending `single 1 1` to `v`.  -/
TannakaDuality.FiniteGroup.sumSMulInv : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → [Fintype G] → {X : FDRep k G} → ↑X.V → (G → k) →ₗ[k] ↑X.V
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_succ_Iic : ∀ {n : ℕ} (i : Fin n), Finset.image Fin.succ (Finset.Iic i) = Finset.Ioc 0 i.succ
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.card_interedges_finpartition : ∀ {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)] {s : Finset α} {t : Finset β}
  [inst_1 : DecidableEq α] [inst_2 : DecidableEq β] (P : Finpartition s) (Q : Finpartition t),
  (Rel.interedges r s t).card = ∑ ab ∈ P.parts ×ˢ Q.parts, (Rel.interedges r ab.1 ab.2).card
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.ext_hom : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g}
  (i : s.pt ≅ t.pt)
  (w : autoParam (CategoryTheory.CategoryStruct.comp i.hom t.ι = s.ι) CategoryTheory.Limits.Fork.ext._auto_1),
  (CategoryTheory.Limits.Fork.ext i w).hom = CategoryTheory.Limits.Fork.mkHom i.hom w
-- Init.Data.BitVec.Bitblast
BitVec.cpopTree.eq_def : ∀ {len w : ℕ} (l : BitVec (len * w)),
  l.cpopTree = if h : len = 0 then 0#w else if h : len = 1 then BitVec.cast ⋯ l else (l.cpopLayer 0#(0 * w) ⋯).cpopTree
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.reindex_refl : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P), b.reindex (Equiv.refl ι) = b
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.isVonNBounded_iUnion : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : Zero E]
  [inst_3 : TopologicalSpace E] {ι : Sort u_6} [Finite ι] {s : ι → Set E},
  Bornology.IsVonNBounded 𝕜 (⋃ i, s i) ↔ ∀ (i : ι), Bornology.IsVonNBounded 𝕜 (s i)
-- Mathlib.Order.BooleanAlgebra.Set
Set.inter_compl_nonempty_iff : ∀ {α : Type u_1} {s t : Set α}, (s ∩ tᶜ).Nonempty ↔ ¬s ⊆ t
-- Mathlib.Data.Nat.Factorization.Divisors
Nat.divisors_eq_image_Iic_factorization_prod_pow : ∀ {n : ℕ}, n ≠ 0 → n.divisors = Finset.image (fun x => x.prod fun x1 x2 => x1 ^ x2) (Finset.Iic n.factorization)
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsRankOneDiscrete.generator_eq_neg_exp_one_of_surjective : ∀ {A : Type u_2} [inst : Ring A] {v : Valuation A (WithZero (Multiplicative ℤ))} [hv : v.IsRankOneDiscrete],
  Function.Surjective ⇑v →
    Valuation.IsRankOneDiscrete.generator v =
      Units.mk0 (WithZero.exp (-1)) Valuation.IsRankOneDiscrete.generator_eq_exp_neg_one_of_mem_range._proof_1
-- Mathlib.Topology.Covering.Basic
isLocalHomeomorph_iff_isCoveringMap : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} [T2Space E]
  [T2Space X] [CompactSpace E], IsLocalHomeomorph f ↔ IsCoveringMap f
-- Lean.Util.LeanOptions
Lean.LeanOptions.toOptions : Lean.LeanOptions → Lean.Options
-- Mathlib.Logic.Equiv.Defs
Equiv.refl_apply : ∀ {α : Sort u} (x : α), (Equiv.refl α) x = x
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.inv.eq_2 : ∀ {ι : Type u_1} {G : ι → Type u_4} [inst : (i : ι) → Group (G i)] (x x_1 j k : ι) (h : j ≠ k)
  (w₁ : Monoid.CoprodI.NeWord G x j) (w₂ : Monoid.CoprodI.NeWord G k x_1), (w₁.append h w₂).inv = w₂.inv.append ⋯ w₁.inv
-- Mathlib.ModelTheory.Order
FirstOrder.Language.noBotOrderSentence.eq_1 : ∀ (L : FirstOrder.Language) [inst : L.IsOrdered],
  L.noBotOrderSentence = (((FirstOrder.Language.var ∘ Sum.inr) 0).le ((FirstOrder.Language.var ∘ Sum.inr) 1)).not.ex.all
-- Mathlib.Data.Fin.Tuple.Take
/-- Taking the first `n + m` elements of an `addCases u v`, where `v` is a `n'`-tuple and `m ≤ n'`,
is the same as appending `u` with the first `m` elements of `v`.  -/
Fin.take_addCases_right : ∀ {n n' : ℕ} {motive : Fin (n + n') → Sort u_2} (m : ℕ) (h : m ≤ n') (u : (i : Fin n) → motive (Fin.castAdd n' i))
  (v : (i : Fin n') → motive (Fin.natAdd n i)),
  (Fin.take (n + m) ⋯ fun i => Fin.addCases u v i) = fun i => Fin.addCases u (Fin.take m h v) i
-- Mathlib.Algebra.Lie.Sl2
IsSl2Triple.HasPrimitiveVectorWith.lie_h : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {h e f : L} {t : IsSl2Triple h e f} {m : M} {μ : R},
  t.HasPrimitiveVectorWith m μ → ⁅h, m⁆ = μ • m
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
/-- The smallest cardinality of a `(U, n)`-dynamical cover of `F`. Takes values in `ℕ∞`, and is
infinite if and only if `F` admits no finite dynamical cover.  -/
Dynamics.coverMincard : {X : Type u_1} → (X → X) → Set X → SetRel X X → ℕ → ℕ∞
-- Mathlib.CategoryTheory.Monoidal.Internal.Module
/-- The ring structure on a monoid object.
This instance is dangerous as it doesn't round trip from a ring to a monoid object and then back
to a ring, since the `npow` field is lost in the middle. Therefore, it is scoped.  -/
ModuleCat.MonModuleEquivalenceAlgebra.MonObj.toRing : {R : Type u} → [inst : CommRing R] → (A : ModuleCat R) → [CategoryTheory.MonObj A] → Ring ↑A
-- Mathlib.Algebra.Order.Floor.Defs
/-- A version of `Nat.cast_nonneg'` for floor semirings, whose addition is not necessarily
monotone.  -/
FloorSemiring.natCast_nonneg : ∀ {α : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [FloorSemiring α] (n : ℕ), 0 ≤ ↑n
-- Mathlib.GroupTheory.GroupAction.IterateAct
/-- The value of `n : IterateMulAct f`.  -/
IterateMulAct.val : {α : Type u_1} → {f : α → α} → IterateMulAct f → ℕ
-- Mathlib.Analysis.Calculus.TangentCone.Real
uniqueDiffWithinAt_Ioo : ∀ {a b t : ℝ}, t ∈ Set.Ioo a b → UniqueDiffWithinAt ℝ (Set.Ioo a b) t
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.comp'_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A₁ A₂ A₃ : CategoryTheory.Grp C} (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) {Z : CategoryTheory.Mon C} (h : A₃.toMon ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).hom h =
    CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp g.hom h)
-- Mathlib.Algebra.Group.Subgroup.ZPowers.Basic
Subgroup.decidableMemZPowers : {G : Type u_1} → [inst : Group G] → {a : G} → DecidablePred fun x => x ∈ Subgroup.zpowers a
-- Mathlib.GroupTheory.FreeAbelianGroup
/-- See note [partially-applied ext lemmas].  -/
FreeAbelianGroup.lift_ext : ∀ {α : Type u} {β : Type v} [inst : AddCommGroup β] (g h : FreeAbelianGroup α →+ β),
  (∀ (x : α), g (FreeAbelianGroup.of x) = h (FreeAbelianGroup.of x)) → g = h
-- Mathlib.RingTheory.Ideal.MinimalPrime.Localization
Ideal.minimalPrimes_comap_subset : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S) (J : Ideal S),
  (Ideal.comap f J).minimalPrimes ⊆ Ideal.comap f '' J.minimalPrimes
-- Init.Data.SInt.Lemmas
ISize.toBitVec_neg : ∀ (x : ISize), (-x).toBitVec = -x.toBitVec
-- Mathlib.Analysis.Convex.Integral
/-- If an integrable function `f : α → E` takes values in a strictly convex closed set `s`, then
either it is a.e. equal to its average value, or its average value belongs to the interior of
`s`.  -/
StrictConvex.ae_eq_const_or_average_mem_interior : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {f : α → E} [MeasureTheory.IsFiniteMeasure μ],
  StrictConvex ℝ s →
    IsClosed s →
      (∀ᵐ (x : α) ∂μ, f x ∈ s) →
        MeasureTheory.Integrable f μ → f =ᵐ[μ] Function.const α (⨍ (x : α), f x ∂μ) ∨ ⨍ (x : α), f x ∂μ ∈ interior s
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
/-- **Alias** of `AlgebraicGeometry.LocallyQuasiFinite.of_fiberToSpecResidueField`. -/
AlgebraicGeometry.LocallyQuasiFinite.of_isFinite_fiberToSpecResidueField : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  (∀ (x : ↥Y), AlgebraicGeometry.LocallyQuasiFinite (AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField f x)) →
    AlgebraicGeometry.LocallyQuasiFinite f
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtAllPlaces_norm_at_real_places : ∀ {K : Type u_1} [inst : Field K] (x : NumberField.mixedEmbedding.mixedSpace K),
  NumberField.mixedEmbedding.normAtAllPlaces (fun w => ‖x.1 w‖, x.2) = NumberField.mixedEmbedding.normAtAllPlaces x
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.opNNNorm_prod : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : SeminormedAddCommGroup G']
  [inst_6 : NormedSpace 𝕜 G'] [inst_7 : Fintype ι] (f : ContinuousMultilinearMap 𝕜 E G)
  (g : ContinuousMultilinearMap 𝕜 E G'), ‖f.prod g‖₊ = max ‖f‖₊ ‖g‖₊
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.getElem?_eq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁[k]? = m₂[k]?
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.coe_sub : ∀ {M : Type u_2} {N : Type u_3} {X : Type u_4} {Y : Type u_5} {σ : M → N} [inst : SMul M X] [inst_1 : AddGroup Y]
  [inst_2 : DistribSMul N Y] (f g : X →ₑ[σ] Y), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderivWithin_sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {s : Set E} {ι : Type u_4} {u : Finset ι} {A : ι → E → F},
  UniqueDiffWithinAt 𝕜 s x →
    (∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x) →
      fderivWithin 𝕜 (∑ i ∈ u, A i) s x = ∑ i ∈ u, fderivWithin 𝕜 (A i) s x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.epi_desc_of_epi_right : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] (f : X ⟶ W) (g : Y ⟶ W) [CategoryTheory.Epi g],
  CategoryTheory.Epi (CategoryTheory.Limits.biprod.desc f g)
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.instInhabitedSearchStep : {a : String.Slice} → Inhabited (String.Slice.Pattern.SearchStep a)
-- Mathlib.Algebra.Order.SuccPred
Order.lt_add_one_iff_of_not_isMax : ∀ {α : Type u_1} {x y : α} [inst : LinearOrder α] [inst_1 : Add α] [inst_2 : One α] [SuccAddOrder α],
  ¬IsMax y → (x < y + 1 ↔ x ≤ y)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioi_sdiff_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioi a \ Set.Ioc a b = Set.Ioi (max a b)
-- Mathlib.Topology.Order
map_nhds_induced_of_surjective : ∀ {α : Type u} {β : Type v} [T : TopologicalSpace α] {f : β → α},
  Function.Surjective f → ∀ (a : β), Filter.map f (nhds a) = nhds (f a)
-- Mathlib.FieldTheory.RatFunc.Valuation
RatFunc.inftyValuation.X_zpow : ∀ (F : Type u_1) [inst : Field F] [inst_1 : DecidableEq (RatFunc F)] (m : ℤ),
  (RatFunc.inftyValuation F) (RatFunc.X ^ m) = WithZero.exp m
-- Lean.Meta.Tactic.Grind.Split
_private.Lean.Meta.Tactic.Grind.Split.0.Lean.Meta.Grind.mkGrindEM : Lean.Expr → Lean.Expr
-- Mathlib.Combinatorics.SetFamily.Shadow
/-- The upper shadow of the empty set is empty.  -/
Finset.upShadow_empty : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α], ∅.upShadow = ∅
-- Mathlib.Order.Antisymmetrization
OrderEmbedding.ofAntisymmetrization_apply : ∀ (α : Type u_1) [inst : Preorder α] (a : Antisymmetrization α fun x1 x2 => x1 ≤ x2),
  (OrderEmbedding.ofAntisymmetrization α) a = ofAntisymmetrization (fun x1 x2 => x1 ≤ x2) a
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.posPart_mul_negPart : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] (a : A), a⁺ * a⁻ = 0
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Take.0.Std.Iterators.Types.Take.instIterator.match_1.eq_3 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.internalState.inner.Step → Sort u_3) (h' : it.internalState.inner.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) →
        (h' : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
          motive ⟨Std.IterStep.yield it' out, h'⟩)
  (h_2 :
    (it' : Std.IterM m β) →
      (h' : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h'⟩)
  (h_3 : (h' : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h'⟩),
  (match ⟨Std.IterStep.done, h'⟩ with
    | ⟨Std.IterStep.yield it' out, h'⟩ => h_1 it' out h'
    | ⟨Std.IterStep.skip it', h'⟩ => h_2 it' h'
    | ⟨Std.IterStep.done, h'⟩ => h_3 h') =
    h_3 h'
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.integrable_prod : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} {F : Type u_9}
  [inst : NormedAddCommGroup E] [NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [NormedSpace ℝ F] {f : α → E × F},
  MeasureTheory.Integrable f μ ↔
    MeasureTheory.Integrable (fun x => (f x).1) μ ∧ MeasureTheory.Integrable (fun x => (f x).2) μ
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- Given `R`-module X and `S`-module Y, any `g : (restrictScalars f).obj Y ⟶ X`
corresponds to `Y ⟶ (coextendScalars f).obj X` by sending `y ↦ (s ↦ g (s • y))`
 -/
ModuleCat.RestrictionCoextensionAdj.HomEquiv.fromRestriction : {R : Type u₁} →
  {S : Type u₂} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        (f : R →+* S) →
          {X : ModuleCat R} →
            {Y : ModuleCat S} → ((ModuleCat.restrictScalars f).obj Y ⟶ X) → (Y ⟶ (ModuleCat.coextendScalars f).obj X)
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trPosNum.match_1.splitter : (motive : PosNum → Sort u_1) →
  (x : PosNum) → (Unit → motive PosNum.one) → ((n : PosNum) → motive n.bit0) → ((n : PosNum) → motive n.bit1) → motive x
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.MonadGetStruct.getStruct : {m : Type → Type} → [self : Lean.Meta.Grind.AC.MonadGetStruct m] → m Lean.Meta.Grind.AC.Struct
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.compare_minKey_modify_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β} {he : (t.modify k f).isEmpty = false}, cmp ((t.modify k f).minKey he) (t.minKey ⋯) = Ordering.eq
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.coe_top : ∀ {α : Type u_2} [inst : BooleanAlgebra α], ↑⊤ = Set.univ
-- Lean.Meta.Tactic.Grind.Internalize
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.addDefaultSplitCandidate : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
/-- The base change of `R[M]` to an `R`-algebra `A` is isomorphic to `A[M]` as an `A`-algebra.  -/
MonoidAlgebra.scalarTensorEquiv : (R : Type u_1) →
  {M : Type u_2} →
    (A : Type u_5) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : CommMonoid M] → TensorProduct R A (MonoidAlgebra R M) ≃ₐ[A] MonoidAlgebra A M
-- Mathlib.NumberTheory.ZetaValues
hasDerivAt_bernoulliFun : ∀ (k : ℕ) (x : ℝ), HasDerivAt (bernoulliFun k) (↑k * bernoulliFun (k - 1) x) x
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than the given key,
panicking if no such pair exists.
 -/
Std.TreeMap.getEntryLT! : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Inhabited (α × β)] → Std.TreeMap α β cmp → α → α × β
-- Init.Control.Lawful.Instances
StateT.run_modify : ∀ {m : Type u_1 → Type u_2} {σ : Type u_1} [inst : Monad m] (f : σ → σ) (s : σ),
  (modify f).run s = pure (PUnit.unit, f s)
-- Mathlib.Tactic.FieldSimp.Lemmas
/-- Given an expression `y : Q($M)` with specified sign (either + or -), construct a proof that
the inverse of (± `y`) (here taking the specified sign) is ± `y⁻¹`.  -/
Mathlib.Tactic.FieldSimp.Sign.inv : {v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(CommGroupWithZero «$M»)) →
      (y : Q(«$M»)) →
        (g : Mathlib.Tactic.FieldSimp.Sign M) →
          Lean.MetaM
            (have a := g.expr q(«$y»⁻¹);
            have a_1 := g.expr y;
            Q(«$a_1»⁻¹ = «$a»))
-- Mathlib.CategoryTheory.Limits.Preserves.Finite
CategoryTheory.Limits.instPreservesLimitsOfShapeDiscreteOfFiniteOfPreservesFiniteProducts : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (J : Type u) [Finite J] [CategoryTheory.Limits.PreservesFiniteProducts F],
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete J) F
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.val_awayMap_mk : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] (𝒜 : ι → σ)
  [inst_5 : GradedRing 𝒜] {e : ι} {f g : A} (hg : g ∈ 𝒜 e) {x : A} (hx : x = f * g) (n : ι) (a : ↥(𝒜 n)) (i : ℕ)
  (hi : f ^ i ∈ 𝒜 n),
  HomogeneousLocalization.val
      ((HomogeneousLocalization.awayMap 𝒜 hg hx)
        (HomogeneousLocalization.mk { deg := n, num := a, den := ⟨f ^ i, hi⟩, den_mem := ⋯ })) =
    Localization.mk (↑a * g ^ i) ⟨x ^ i, ⋯⟩
-- Init.Data.Nat.ToString
Nat.digitChar_eq_six : ∀ {n : ℕ}, n.digitChar = '6' ↔ n = 6
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.absNorm_ne_zero_iff : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] (I : Ideal S),
  Ideal.absNorm I ≠ 0 ↔ Finite (S ⧸ I)
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
CategoryTheory.instIsIsoSSetProdComparisonCatCompNerveFunctorHoFunctorOf : ∀ (C D : Type u) [inst : CategoryTheory.Category.{u, u} C] [inst_1 : CategoryTheory.Category.{u, u} D],
  CategoryTheory.IsIso
    (CategoryTheory.Limits.prodComparison
      (CategoryTheory.nerveFunctor.comp (SSet.hoFunctor.comp CategoryTheory.nerveFunctor)) (CategoryTheory.Cat.of C)
      (CategoryTheory.Cat.of D))
-- Mathlib.Data.Setoid.Basic
Setoid.piQuotientEquiv_apply : ∀ {ι : Sort u_4} {α : ι → Sort u_5} (r : (i : ι) → Setoid (α i)) (x : (i : ι) → Quotient (r i)),
  (Setoid.piQuotientEquiv r) x = Quotient.mk'' fun i => (x i).out
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.SigmaFinite.out : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  MeasureTheory.SigmaFinite μ → Nonempty (μ.FiniteSpanningSetsIn Set.univ)
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.range_exp : Set.range Complex.exp = {0}ᶜ
-- Mathlib.Order.CompactlyGenerated.Basic
CompleteLattice.isSupFiniteCompact_iff_isSupClosedCompact : ∀ (α : Type u_2) [inst : CompleteLattice α], CompleteLattice.IsSupFiniteCompact α ↔ CompleteLattice.IsSupClosedCompact α
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.mk_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (f : CauSeq β abv),
  -CauSeq.Completion.mk f = CauSeq.Completion.mk (-f)
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsFiltered.SmallFilteredIntermediate.instOfNonempty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsFilteredOrEmpty C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C) [Nonempty D],
  CategoryTheory.IsFiltered (CategoryTheory.IsFiltered.SmallFilteredIntermediate F)
-- Mathlib.Topology.Homotopy.HSpaces
IsTopologicalAddGroup.hSpace.eq_1 : ∀ (G : Type u) [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G],
  IsTopologicalAddGroup.hSpace G = IsTopologicalAddGroup.toHSpace G
-- Init.Data.List.Perm
List.foldl.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β → α) (x : α), List.foldl f x [] = x
-- Mathlib.Order.LiminfLimsup
Filter.mono_blimsup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p : β → Prop} {u v : β → α},
  (∀ (x : β), p x → u x ≤ v x) → Filter.blimsup u f p ≤ Filter.blimsup v f p
-- Mathlib.Algebra.Star.Basic
StarHomClass.mk : ∀ {F : Type u_1} {R : outParam (Type u_2)} {S : outParam (Type u_3)} [inst : Star R] [inst_1 : Star S]
  [inst_2 : FunLike F R S], (∀ (f : F) (r : R), f (star r) = star (f r)) → StarHomClass F R S
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.coe_refl : ∀ (M : Type u_1) [inst : TopologicalSpace M] [inst_1 : Mul M], ⇑(ContinuousMulEquiv.refl M) = id
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.tensorHomImpl_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X₁ X₂ Y₁ Y₂ : CategoryTheory.Dial C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂),
  (CategoryTheory.Dial.tensorHomImpl f g).F =
    CategoryTheory.Limits.prod.lift
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) f.F)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.prod.map CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd) g.F)
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
CategoryTheory.Limits.instHasLimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesLimit₂ : ∀ {J₁ : Type u_1} {J₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} J₂] {C₁ : Type u_3} {C₂ : Type u_4} {C : Type u_5}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} C] {K₁ : CategoryTheory.Functor J₁ C₁}
  {K₂ : CategoryTheory.Functor J₂ C₂} (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  [CategoryTheory.Limits.HasLimit K₁] [CategoryTheory.Limits.HasLimit K₂]
  [CategoryTheory.Limits.PreservesLimit₂ K₁ K₂ G],
  CategoryTheory.Limits.HasLimit
    (CategoryTheory.Functor.uncurry.obj ((((CategoryTheory.Functor.whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.le_norm_expr : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] [inst_1 : LE α] [inst_2 : LT α] [inst_3 : Std.IsPreorder α]
  [Lean.Grind.OrderedRing α] (ctx : Lean.Grind.CommRing.Context α) (lhs rhs lhs' rhs' : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.norm_cnstr_cert lhs rhs lhs' rhs' = true →
    (Lean.Grind.CommRing.Expr.denote ctx lhs ≤ Lean.Grind.CommRing.Expr.denote ctx rhs) =
      (Lean.Grind.CommRing.Expr.denote ctx lhs' ≤ Lean.Grind.CommRing.Expr.denote ctx rhs')
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.alter_eq_empty_iff_erase_eq_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β}, m.alter k f = ∅ ↔ m.erase k = ∅ ∧ f m[k]? = none
-- Mathlib.Probability.Moments.CovarianceBilinDual
ProbabilityTheory.uncenteredCovarianceBilinDual_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E}
  [inst_1 : NormedSpace ℝ E] [inst_2 : OpensMeasurableSpace E],
  MeasureTheory.MemLp id 2 μ →
    ∀ (L₁ L₂ : StrongDual ℝ E), ((ProbabilityTheory.uncenteredCovarianceBilinDual μ) L₁) L₂ = ∫ (x : E), L₁ x * L₂ x ∂μ