mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.natAbs_valMinAbs_neg : ∀ {n : ℕ} (a : ZMod n), (-a).valMinAbs.natAbs = a.valMinAbs.natAbs
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.xor_right_inj' : ∀ {w : ℕ} (a b c : BitVec w), (c ^^^ a == b ^^^ c) = (a == b)
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.QuasiMeasurePreserving.prod_of_left : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {f : α × β → γ} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β}
  {τ : MeasureTheory.Measure γ},
  Measurable f →
    ∀ [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν],
      (∀ᵐ (y : β) ∂ν, MeasureTheory.Measure.QuasiMeasurePreserving (fun x => f (x, y)) μ τ) →
        MeasureTheory.Measure.QuasiMeasurePreserving f (μ.prod ν) τ
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.IsLocallyInjective.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] {J : CategoryTheory.GrothendieckTopology C}
  {F₁ F₂ : CategoryTheory.Functor Cᵒᵖ D} {φ : F₁ ⟶ F₂},
  (∀ {X : Cᵒᵖ} (x y : CategoryTheory.ToType (F₁.obj X)),
      (CategoryTheory.ConcreteCategory.hom (φ.app X)) x = (CategoryTheory.ConcreteCategory.hom (φ.app X)) y →
        CategoryTheory.Presheaf.equalizerSieve x y ∈ J (Opposite.unop X)) →
    CategoryTheory.Presheaf.IsLocallyInjective J φ
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.isUnit_det_of_right_inverse : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A B : Matrix n n α},
  A * B = 1 → IsUnit A.det
-- Mathlib.Algebra.Homology.HomologicalComplex
CochainComplex.mk_d_1_0 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (X₀ X₁ X₂ : V) (d₀ : X₀ ⟶ X₁) (d₁ : X₁ ⟶ X₂) (s : CategoryTheory.CategoryStruct.comp d₀ d₁ = 0)
  (succ :
    (S : CategoryTheory.ShortComplex V) →
      (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' CategoryTheory.CategoryStruct.comp S.g d₂ = 0),
  (CochainComplex.mk X₀ X₁ X₂ d₀ d₁ s succ).d 0 1 = d₀
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
/-- If an additive group satisfies the universal property of an additive free group with respect to
a given type, then it admits an additive free group basis based on this type. Here
the universal property is expressed as in `IsFreeAddGroup.unique_lift`.  -/
FreeAddGroupBasis.ofUniqueLift : {G : Type u} →
  [inst : AddGroup G] →
    (X : Type u) →
      (of : X → G) →
        (∀ {H : Type u} [inst_1 : AddGroup H] (f : X → H), ∃! F, ∀ (a : X), F (of a) = f a) → FreeAddGroupBasis X G
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_filter_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    ∀ {h₁ : Std.Internal.List.containsKey k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) = true}
      {h₂ : Std.Internal.List.containsKey k l₁ = true},
      Std.Internal.List.getKey k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) h₁ =
        Std.Internal.List.getKey k l₁ h₂
-- Std.Data.ByteSlice
instSliceableByteArrayNatByteSlice_1 : Std.Rco.Sliceable ByteArray ℕ ByteSlice
-- Mathlib.Algebra.Category.Grp.EpiMono
AddGrpCat.mono_iff_ker_eq_bot : ∀ {A B : AddGrpCat} (f : A ⟶ B), CategoryTheory.Mono f ↔ (AddGrpCat.Hom.hom f).ker = ⊥
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.mulEquivHaarChar_smul_preimage : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalGroup G] [inst_5 : LocallyCompactSpace G] (μ : MeasureTheory.Measure G) [μ.IsHaarMeasure]
  [μ.Regular] {X : Set G} (φ : G ≃ₜ* G), MeasureTheory.mulEquivHaarChar φ • μ (⇑φ ⁻¹' X) = μ X
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.IsImage.closure : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y}, e.IsImage s t → e.IsImage (closure s) (closure t)
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.basisSets_nonempty : ∀ {R : Type u_1} {E : Type u_6} {ι : Type u_9} [inst : SeminormedRing R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  (p : SeminormFamily R E ι), p.basisSets.Nonempty
-- Mathlib.Topology.UniformSpace.DiscreteUniformity
discreteUniformity_iff_setRelId_mem_uniformity : ∀ {X : Type u_2} [inst : UniformSpace X], DiscreteUniformity X ↔ SetRel.id ∈ uniformity X
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.throw_EStateM : ∀ {ε α σ : Type} (err : ε) (post : α → σ → Prop) (epost : ε → σ → Prop),
  ⦃ epost err ⦄ MonadExceptOf.throw err ⦃ post; epost ⦄
-- Mathlib.Algebra.Homology.HomotopyCategory.KInjective
CochainComplex.IsKInjective.rightOrthogonal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (L : CochainComplex C ℤ) [L.IsKInjective],
  (HomotopyCategory.subcategoryAcyclic C).rightOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.instFaithfulCompPreLeft : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (F : CategoryTheory.Functor C A) (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) [F.Faithful], (CategoryTheory.Comma.preLeft F L R).Faithful
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinOnBall.congr : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  HasFPowerSeriesWithinOnBall f p s x r →
    Set.EqOn g f (s ∩ Metric.eball x r) → g x = f x → HasFPowerSeriesWithinOnBall g p s x r
-- Mathlib.Order.Atoms
isSimpleOrder_iff : ∀ (α : Type u_4) [inst : LE α] [inst_1 : BoundedOrder α], IsSimpleOrder α ↔ Nontrivial α ∧ ∀ (a : α), a = ⊥ ∨ a = ⊤
-- Mathlib.RingTheory.PowerBasis
PowerBasis.equivOfMinpoly_map : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] {S' : Type u_7} [inst_2 : CommRing S']
  [inst_3 : Algebra A S] [inst_4 : Algebra A S'] (pb : PowerBasis A S) (e : S ≃ₐ[A] S')
  (h : minpoly A pb.gen = minpoly A (pb.map e).gen), pb.equivOfMinpoly (pb.map e) h = e
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.Context : Type
-- Mathlib.CategoryTheory.Abelian.FreydMitchell
/-- Given an abelian category `C`, this is a ring such that there is a full, faithful and exact
embedding `C ⥤ ModuleCat (EmbeddingRing C)`.

It is probably not a good idea to unfold this.  -/
CategoryTheory.Abelian.FreydMitchell.EmbeddingRing : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Abelian C] → Type (max u v)
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_lt : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R} {n : ℕ},
  0 ≤ a → (⌊a⌋₊ < n ↔ a < ↑n)
-- Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
CategoryTheory.Functor.mapCocone₂_ι_app : ∀ {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] (G : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C))
  {K₁ : CategoryTheory.Functor J₁ C₁} {K₂ : CategoryTheory.Functor J₂ C₂} (c₁ : CategoryTheory.Limits.Cocone K₁)
  (c₂ : CategoryTheory.Limits.Cocone K₂) (x : J₁ × J₂),
  (G.mapCocone₂ c₁ c₂).ι.app x =
    CategoryTheory.CategoryStruct.comp ((G.map (c₁.ι.app x.1)).app (K₂.obj x.2)) ((G.obj c₁.pt).map (c₂.ι.app x.2))
-- Mathlib.Data.Multiset.Dedup
Multiset.dedup_ext : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s.dedup = t.dedup ↔ ∀ (a : α), a ∈ s ↔ a ∈ t
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.forM_eq_forM : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : (a : α) → β a → m PUnit.{w + 1}},
  Std.DTreeMap.Raw.forM f t = forM t fun a => f a.fst a.snd
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
/-- The property that is satisfied by cofibrant objects.
(This is only introduced in order to consider the full subcategory
`CofibrantObject`. Otherwise, the typeclass `IsCofibrant`
is preferred.)  -/
HomotopicalAlgebra.cofibrantObjects : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [HomotopicalAlgebra.CategoryWithCofibrations C] →
      [CategoryTheory.Limits.HasInitial C] → CategoryTheory.ObjectProperty C
-- Lean.Environment
/-- Like `findAsync?` but returns a task instead of resorting to blocking.  -/
Lean.Environment.findTask : Lean.Environment → Lean.Name → optParam Bool false → Task (Option Lean.AsyncConstantInfo)
-- Init.Data.Vector.Algebra
Vector.mul_assoc : ∀ {α : Type u_1} {n : ℕ} [inst : Mul α],
  (∀ (x y z : α), x * (y * z) = x * y * z) → ∀ (xs ys zs : Vector α n), xs * ys * zs = xs * (ys * zs)
-- Mathlib.Order.Completion
DedekindCut.principal_le_principal : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, DedekindCut.principal a ≤ DedekindCut.principal b ↔ a ≤ b
-- Mathlib.NumberTheory.Dioph
Dioph.abs_poly_dioph : ∀ {α : Type u} (p : Poly α), Dioph.DiophFn fun v => (p v).natAbs
-- Mathlib.Data.ZMod.Basic
ZMod.ringEquivCongr_val : ∀ {a b : ℕ} (h : a = b) (x : ZMod a), ((ZMod.ringEquivCongr h) x).val = x.val
-- Mathlib.Data.Seq.Defs
Stream'.Seq.get?_zero_eq_none : ∀ {α : Type u} {s : Stream'.Seq α}, s.get? 0 = none ↔ s = Stream'.Seq.nil
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instNonUnitalRing : {n : Type u_2} → {A : Type u_5} → [Fintype n] → [NonUnitalRing A] → NonUnitalRing (CStarMatrix n n A)
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.separatesPoints_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α],
  MeasurableSpace.SeparatesPoints α ↔ ∀ (x y : α), (∀ (s : Set α), MeasurableSet s → (x ∈ s ↔ y ∈ s)) → x = y
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.of_isEmpty : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal} {f : X → Y}
  [IsEmpty X], HolderWith C r f
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.le_dual_iff : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B] {I J : FractionalIdeal (nonZeroDivisors B) L},
  J ≠ 0 → (I ≤ FractionalIdeal.dual A K J ↔ I * J ≤ FractionalIdeal.dual A K 1)
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.endPos_le : ∀ {s : String.Slice} (p : s.Pos), s.endPos ≤ p ↔ p = s.endPos
-- Lean.Util.ParamMinimizer
/-- **Pruning (minimization phase).**

Starting from a configuration `cur` known to satisfy `test`, this procedure
iterates through the indices stored in `added` **in reverse order**, removing
each one temporarily to check if it is necessary.

For each recorded index `i` (except the last one added, which is known to be
required since its removal made `test` fail during `init`):

1. sets `cur[i] := false`;
2. re-evaluates `tryCur`;
3. if `test` remains true, keeps `i` cleared;
   otherwise restores `cur[i] := true`.

After this phase, `cur` is guaranteed to be *1-minimal*: removing any single
`true` bit would make `test` return `false`.
 -/
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.prune : {m : Type → Type} → [Monad m] → Lean.Util.ParamMinimizer.M✝ m Unit
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_symm_comp_lid_symm : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N],
  ↑(TensorProduct.assoc R R M N).symm ∘ₗ ↑(TensorProduct.lid R (TensorProduct R M N)).symm =
    TensorProduct.map (↑(TensorProduct.lid R M).symm) LinearMap.id
-- Batteries.Recycling.RBTree.Alter
RBTree.RBNode.Path.Balanced.below.redR : ∀ {c₀ : RBTree.RBColor} {n₀ : ℕ} {α : Type u_1}
  {motive :
    (a : RBTree.RBNode.Path α) →
      (a_1 : RBTree.RBColor) → (a_2 : ℕ) → RBTree.RBNode.Path.Balanced c₀ n₀ a a_1 a_2 → Prop}
  {x : RBTree.RBNode α} {n : ℕ} {v : α} {parent : RBTree.RBNode.Path α} (a : x.Balanced RBTree.RBColor.black n)
  (a_1 : RBTree.RBNode.Path.Balanced c₀ n₀ parent RBTree.RBColor.red n),
  RBTree.RBNode.Path.Balanced.below a_1 → motive parent RBTree.RBColor.red n a_1 → RBTree.RBNode.Path.Balanced.below ⋯
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_two : Cardinal.lift.{u, v} 2 = 2
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingFieldAux.scalar_tower' : ∀ {K : Type v} [inst : Field K] {n : ℕ} {f : Polynomial K},
  IsScalarTower K (AdjoinRoot f.factor) (Polynomial.SplittingFieldAux n f.removeFactor)
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.limitUncurryIsoLimitCompLim_inv_π : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasLimit (CategoryTheory.Functor.uncurry.obj F)]
  [inst_5 : CategoryTheory.Limits.HasLimit (F.comp CategoryTheory.Limits.lim)] {j : J} {k : K},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitUncurryIsoLimitCompLim F).inv
      (CategoryTheory.Limits.limit.π (CategoryTheory.Functor.uncurry.obj F) (j, k)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp CategoryTheory.Limits.lim) j)
      (CategoryTheory.Limits.limit.π (F.obj j) k)
-- Mathlib.Algebra.Group.Action.TypeTags
Multiplicative.mulAction : {α : Type u_2} → {β : Type u_3} → [inst : AddMonoid α] → [AddAction α β] → MulAction (Multiplicative α) β
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.toBitVec_val_assemble₄ : ∀ {w x y z : UInt8} (c : Char),
  ByteArray.utf8DecodeChar?.assemble₄ w x y z = some c →
    c.val.toBitVec =
      BitVec.setWidth 32
        (BitVec.setWidth 3 w.toBitVec ++ BitVec.setWidth 6 x.toBitVec ++ BitVec.setWidth 6 y.toBitVec ++
          BitVec.setWidth 6 z.toBitVec)
-- Init.Data.Nat.Fold
Nat.dfold_zero : ∀ {α : (i : ℕ) → autoParam (i ≤ 0) Nat.dfold_zero._auto_1 → Type u} (f : (i : ℕ) → (h : i < 0) → α i ⋯ → α (i + 1) ⋯)
  (init : α 0 Nat.dfold_zero._proof_7), Nat.dfold 0 f init = init
-- Init.Data.SInt.Lemmas
USize.toISize_mul : ∀ (a b : USize), (a * b).toISize = a.toISize * b.toISize
-- Mathlib.Order.CompleteLattice.Lemmas
iInf_iSup_ge_nat_add : ∀ {α : Type u_1} [inst : CompleteLattice α] (f : ℕ → α) (k : ℕ),
  ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), f (i + k) = ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), f i
-- Mathlib.CategoryTheory.Limits.IndYoneda
/-- Ind-Yoneda lemma: morphisms from colimit of yoneda of diagram `D` to `F` is limit of `F`
evaluated at `D`. This version is for covariant diagrams, see `colimitYonedaHomIsoLimit'` for a
contravariant version.  -/
CategoryTheory.Limits.colimitYonedaHomIsoLimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    {I : Type v₁} →
      [inst_1 : CategoryTheory.Category.{v₂, v₁} I] →
        (D : CategoryTheory.Functor Iᵒᵖ Cᵒᵖ) →
          (F : CategoryTheory.Functor Cᵒᵖ (Type u₂)) →
            [inst_2 : CategoryTheory.Limits.HasColimit (D.unop.comp CategoryTheory.yoneda)] →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))] →
                (CategoryTheory.Limits.colimit (D.unop.comp CategoryTheory.yoneda) ⟶ F) ≅
                  CategoryTheory.Limits.limit (D.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂}))
-- Mathlib.GroupTheory.OrderOfElement
zmultiplesEquivZMultiples.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {x y : G} [inst_1 : Finite G] (h : addOrderOf x = addOrderOf y),
  zmultiplesEquivZMultiples h = (finEquivZMultiples ⋯).symm.trans ((finCongr h).trans (finEquivZMultiples ⋯))
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.map_eq_one_iff : ∀ {β : Type v} {α : Type u_1} {f : α → β} {v : WithBot α} [inst : One β], WithBot.map f v = 1 ↔ ∃ x, v = ↑x ∧ f x = 1
-- Lean.CompactedRegion
_private.Lean.CompactedRegion.0.Lean.CompactedRegion.mk : System.FilePath → USize → Bool → USize → USize → NonScalar → Lean.CompactedRegion
-- Mathlib.Algebra.Module.Projective
/-- A module which satisfies the universal property is projective: If all surjections of
`R`-modules `(P →₀ R) →ₗ[R] P` have `R`-linear left inverse maps, then `P` is
projective.  -/
Module.Projective.of_lifting_property'' : ∀ {R : Type u} [inst : Semiring R] {P : Type v} [inst_1 : AddCommMonoid P] [inst_2 : Module R P],
  (∀ (f : (P →₀ R) →ₗ[R] P), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = LinearMap.id) → Module.Projective R P
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
DirectSum.lof.eq_1 : ∀ (R : Type u) [inst : Semiring R] (ι : Type v) (M : ι → Type w) [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι], DirectSum.lof R ι M = DFinsupp.lsingle
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars_pow : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (φ : MvPolynomial σ R) (n : ℕ), (φ ^ n).vars ⊆ φ.vars
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.MonadGetStruct : (Type → Type) → Type
-- Mathlib.Order.Heyting.Hom
BiheytingHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β]
  [inst_2 : BiheytingAlgebra γ] (f : BiheytingHom β γ) (g : BiheytingHom α β), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor'_obj_X₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)),
  (CategoryTheory.Square.fromArrowArrowFunctor'.obj f).X₂ = f.left.right
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.right.inj : ∀ {J : CategoryTheory.Limits.MultispanShape} {a a_1 : J.R},
  CategoryTheory.Limits.WalkingMultispan.right a = CategoryTheory.Limits.WalkingMultispan.right a_1 → a = a_1
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.X_ne_zero : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R], Polynomial.X ≠ 0
-- Mathlib.CategoryTheory.IsConnected
/-- If `J` and `K` are equivalent, then if `J` is connected then `K` is as well.  -/
CategoryTheory.isConnected_of_equivalent : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  (e : J ≌ K) [CategoryTheory.IsConnected J], CategoryTheory.IsConnected K
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
/-- This is [bourbaki2007] §9 Lemma 3.  -/
CliffordAlgebra.changeForm_changeForm : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q Q' Q'' : QuadraticForm R M} {B B' : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q)
  (h' : LinearMap.BilinMap.toQuadraticMap B' = Q'' - Q') (x : CliffordAlgebra Q),
  (CliffordAlgebra.changeForm h') ((CliffordAlgebra.changeForm h) x) = (CliffordAlgebra.changeForm ⋯) x
-- Init.Data.String.Basic
String.Pos.offset_cast : ∀ {s t : String} {pos : s.Pos} {h : s = t}, (pos.cast h).offset = pos.offset
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.subset_closure : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Set α}, s ⊆ ↑(BooleanSubalgebra.closure s)
-- Mathlib.Topology.Order.LeftRightNhds
/-- The following statements are equivalent:

0. `s` is a neighborhood of `a` within `(a, +∞)`;
1. `s` is a neighborhood of `a` within `(a, b]`;
2. `s` is a neighborhood of `a` within `(a, b)`;
3. `s` includes `(a, u)` for some `u ∈ (a, b]`;
4. `s` includes `(a, u)` for some `u > a`.
 -/
TFAE_mem_nhdsGT : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a b : α},
  a < b →
    ∀ (s : Set α),
      [s ∈ nhdsWithin a (Set.Ioi a), s ∈ nhdsWithin a (Set.Ioc a b), s ∈ nhdsWithin a (Set.Ioo a b),
          ∃ u ∈ Set.Ioc a b, Set.Ioo a u ⊆ s, ∃ u ∈ Set.Ioi a, Set.Ioo a u ⊆ s].TFAE
-- Mathlib.CategoryTheory.Monoidal.Closed.Zero
/-- If a Cartesian closed category has an initial object which is isomorphic to the terminal object,
then each homset has exactly one element.
 -/
CategoryTheory.uniqueHomsetOfInitialIsoUnit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      [CategoryTheory.MonoidalClosed C] →
        [inst_3 : CategoryTheory.Limits.HasInitial C] →
          (⊥_ C ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit C) → (X Y : C) → Unique (X ⟶ Y)
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.reset.injEq : ∀ (n : ℕ) (x : Lean.IR.VarId) (n_1 : ℕ) (x_1 : Lean.IR.VarId),
  (Lean.IR.Expr.reset n x = Lean.IR.Expr.reset n_1 x_1) = (n = n_1 ∧ x = x_1)
-- Mathlib.NumberTheory.PellMatiyasevic
/-- The Pell sequence can also be viewed as an element of `ℤ√d`  -/
Pell.pellZd : {a : ℕ} → (a1 : 1 < a) → ℕ → ℤ√↑(Pell.d✝ a1)
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.manyNoAntiquot.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.vanishingIdeal_irreducibleComponents : ∀ (R : Type u) [inst : CommSemiring R],
  PrimeSpectrum.vanishingIdeal '' irreducibleComponents (PrimeSpectrum R) = minimalPrimes R
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_insertMany_list_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {l : List α},
  (m.insertMany l).size ≤ m.size + l.length
-- Mathlib.NumberTheory.Real.Irrational
Irrational.natCast_mul : ∀ {x : ℝ}, Irrational x → ∀ {m : ℕ}, m ≠ 0 → Irrational (↑m * x)
-- Lean.Widget.InteractiveGoal
Lean.Widget.InteractiveHypothesisBundle.mk.sizeOf_spec : ∀ (names : Array String) (fvarIds : Array Lean.FVarId) (type : Lean.Widget.CodeWithInfos)
  (val? : Option Lean.Widget.CodeWithInfos) (isInstance? isType? isInserted? isRemoved? : Option Bool),
  sizeOf
      { names := names, fvarIds := fvarIds, type := type, val? := val?, isInstance? := isInstance?, isType? := isType?,
        isInserted? := isInserted?, isRemoved? := isRemoved? } =
    1 + sizeOf names + sizeOf fvarIds + sizeOf type + sizeOf val? + sizeOf isInstance? + sizeOf isType? +
        sizeOf isInserted? +
      sizeOf isRemoved?
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Cotrident.IsColimit.hom_ext : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J]
  {s : CategoryTheory.Limits.Cotrident f} (hs : CategoryTheory.Limits.IsColimit s) {W : C} {k l : s.pt ⟶ W},
  CategoryTheory.CategoryStruct.comp s.π k = CategoryTheory.CategoryStruct.comp s.π l → k = l
-- Mathlib.LinearAlgebra.Matrix.Echelon.Basic
/-- In an echelon matrix, rows below a zero row are zero.  -/
Matrix.IsRowEchelon.row_eq_zero_of_lt : ∀ {m : Type u_1} {n : Type u_2} {R : Type v} {A : Matrix m n R} [inst : Zero R] [inst_1 : LT m] [inst_2 : LT n]
  {i₁ i₂ : m}, A.IsRowEchelon → i₁ < i₂ → A i₁ = 0 → A i₂ = 0