mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.d_comp_d : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (n m p : ℤ),
  CategoryTheory.CategoryStruct.comp (h.d n m) (h.d m p) = 0
-- Std.Data.ExtHashMap.Basic
Std.ExtHashMap.instReflBEq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  [inst_2 : BEq β] [ReflBEq β], ReflBEq (Std.ExtHashMap α β)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
FundamentalGroupoidFunctor.prodIso_inv : ∀ (A : TopCat) (B : TopCat),
  (FundamentalGroupoidFunctor.prodIso A B).inv =
    (FundamentalGroupoidFunctor.projLeft A B).prod' (FundamentalGroupoidFunctor.projRight A B)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSignatureHelpOptions : Lean.FromJson Lean.Lsp.SignatureHelpOptions
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsCartesian.map_isHomLift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsCartesian f φ] {a' : 𝒳}
  (φ' : a' ⟶ b) [inst_3 : p.IsHomLift f φ'],
  p.IsHomLift (CategoryTheory.CategoryStruct.id R) (CategoryTheory.Functor.IsCartesian.map p f φ φ')
-- Mathlib.Topology.LocallyFinsupp
/-- The positive part of a sum is less than or equal to the sum of the positive parts.
 -/
Function.locallyFinsuppWithin.posPart_add : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddCommGroup Y]
  [inst_2 : LinearOrder Y] [IsOrderedAddMonoid Y] (f₁ f₂ : Function.locallyFinsuppWithin U Y), (f₁ + f₂)⁺ ≤ f₁⁺ + f₂⁺
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.inv.eq_1 : ∀ (G : Type u_1) [inst : TopologicalSpace G] [inst_1 : InvolutiveInv G] [inst_2 : ContinuousInv G],
  Homeomorph.inv G = { toEquiv := Equiv.inv G, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_add_Icc : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b c : α),
  (fun x => a + x) ⁻¹' Set.Icc b c = Set.Icc (b - a) (c - a)
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIcc_eq_right : ∀ {α : Type u_1} [inst : LinearOrder α] {a b x : α} (h : a < b), Set.projIcc a b ⋯ x = ⟨b, ⋯⟩ ↔ b ≤ x
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.max?.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeSet α cmp),
  t = t_1 → t.max? = t_1.max?
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.filter_eq_self_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {f : α → Bool},
  Std.ExtTreeSet.filter f t = t ↔ ∀ (k : α) (h : k ∈ t), f (t.get k h) = true
-- Mathlib.Data.ENat.Basic
ENat.natCast_lt_top : ∀ (n : ℕ), ↑n < ⊤
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.Adjunction.homEquiv₁_apply : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {b c d : B} {l : b ⟶ c} {r : c ⟶ b}
  (adj : CategoryTheory.Bicategory.Adjunction l r) {g : b ⟶ d} {h : c ⟶ d}
  (γ : g ⟶ CategoryTheory.CategoryStruct.comp l h),
  adj.homEquiv₁ γ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft r γ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator r l h).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight adj.counit h)
          (CategoryTheory.Bicategory.leftUnitor h).hom))
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey!_eq_of_equiv : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β)
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α],
  (↑m₁).WF → (↑m₂).WF → (↑m₁).Equiv ↑m₂ → ∀ {k : α}, m₁.getKey! k = m₂.getKey! k
-- Mathlib.RingTheory.RingHom.Etale
RingHom.etale_algebraMap : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (algebraMap R S).Etale ↔ Algebra.Etale R S
-- Std.Time.Date.Unit.Year
Std.Time.Year.instDecidableLeOffset : {x y : Std.Time.Year.Offset} → Decidable (x ≤ y)
-- Mathlib.AlgebraicGeometry.Restrict
/-- The global sections of the restriction is isomorphic to the sections on the open set.  -/
AlgebraicGeometry.Scheme.Opens.topIso : {X : AlgebraicGeometry.Scheme} → (U : X.Opens) → (↑U).presheaf.obj (Opposite.op ⊤) ≅ X.presheaf.obj (Opposite.op U)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.eq_of_coeff_monomial_ne_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {m n : σ →₀ ℕ} {a : R},
  (MvPowerSeries.coeff m) ((MvPowerSeries.monomial n) a) ≠ 0 → m = n
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.toArray_eq_match_step.match_1.eq_1 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β) (out : β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it' out with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_1 it' out
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.IsEquiv.rfl : ∀ {R : Type u_1} [inst : Semiring R] {S : Type u_2} [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {v : AbsoluteValue R S}, v.IsEquiv v
-- Mathlib.CategoryTheory.MorphismProperty.Concrete
CategoryTheory.MorphismProperty.bijective_respectsIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type u_2}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC],
  (CategoryTheory.MorphismProperty.bijective C).RespectsIso
-- Mathlib.CategoryTheory.Products.Basic
/-- `F` composed with evaluation is the same as evaluating `F.flip`.  -/
CategoryTheory.compEvaluation : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor A (CategoryTheory.Functor B C)) →
              (b : B) → F.comp ((CategoryTheory.evaluation B C).obj b) ≅ F.flip.obj b
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Context.mk.inj : ∀ {maxResultSize maxHeartbeats maxResultSize_1 maxHeartbeats_1 : ℕ},
  { maxResultSize := maxResultSize, maxHeartbeats := maxHeartbeats } =
      { maxResultSize := maxResultSize_1, maxHeartbeats := maxHeartbeats_1 } →
    maxResultSize = maxResultSize_1 ∧ maxHeartbeats = maxHeartbeats_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.minKey!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.minKey! = t₂.minKey!
-- Mathlib.Topology.Homotopy.Lifting
IsQuotientCoveringMap.fundamentalGroupToMulOpposite_eq_one_iff : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hp : IsQuotientCoveringMap p G) {x : X} {e : ↑(p ⁻¹' {x})}
  {γ : FundamentalGroup X x}, (hp.fundamentalGroupToMulOpposite e) γ = 1 ↔ ⋯.monodromy γ e = e
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_le_minKey?_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k km kme : α} (hkme : (t.erase k).minKey? = some kme), t.minKey?.get ⋯ = km → (cmp km kme).isLE = true
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
/-- The length of an object in `SimplexCategory`  -/
SimplexCategory.len : SimplexCategory → ℕ
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roo_succ_right_eq_push : ∀ {m n : ℤ}, m < n → (m<...n + 1).toArray = (m<...n).toArray.push n
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.isZero_of_hasProjectiveDimensionLT_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C)
  [CategoryTheory.HasProjectiveDimensionLT X 0], CategoryTheory.Limits.IsZero X
-- Lean.Meta.IndPredBelow
/-- Returns `@XYZ.below params... motives...`  -/
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.mkBelowAppOfIdx : ℕ → Lean.Meta.IndPredBelow.Context✝ → Lean.Expr
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- A sum can be partitioned into a sum of sums, each equivalent under a setoid.  -/
Finset.sum_partition : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] {f : ι → M} (R : Setoid ι)
  [inst_1 : DecidableRel ⇑R], ∑ x ∈ s, f x = ∑ xbar ∈ Finset.image (Quotient.mk R) s, ∑ y ∈ s with ⟦y⟧ = xbar, f y
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.opEquiv.match_15.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : CategoryTheory.WithTerminal Cᵒᵖ) → (x ⟶ y) → Sort u_3) (x y : C)
  (f : CategoryTheory.WithTerminal.of (Opposite.op x) ⟶ CategoryTheory.WithTerminal.of (Opposite.op y))
  (h_1 :
    (x y : C) →
      (f : CategoryTheory.WithTerminal.of (Opposite.op x) ⟶ CategoryTheory.WithTerminal.of (Opposite.op y)) →
        motive (CategoryTheory.WithTerminal.of (Opposite.op x)) (CategoryTheory.WithTerminal.of (Opposite.op y)) f)
  (h_2 :
    (unop : C) →
      (x : CategoryTheory.WithTerminal.of (Opposite.op unop) ⟶ CategoryTheory.WithTerminal.star) →
        motive (CategoryTheory.WithTerminal.of (Opposite.op unop)) CategoryTheory.WithTerminal.star x)
  (h_3 :
    (x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
      motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x),
  (match CategoryTheory.WithTerminal.of (Opposite.op x), CategoryTheory.WithTerminal.of (Opposite.op y), f with
    | CategoryTheory.WithTerminal.of (Opposite.op x), CategoryTheory.WithTerminal.of (Opposite.op y), f => h_1 x y f
    | CategoryTheory.WithTerminal.of (Opposite.op unop), CategoryTheory.WithTerminal.star, x => h_2 unop x
    | CategoryTheory.WithTerminal.star, CategoryTheory.WithTerminal.star, x => h_3 x) =
    h_1 x y f
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getKey!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Inhabited α] (a : α),
  Std.DHashMap.Internal.AssocList.getKey! a Std.DHashMap.Internal.AssocList.nil =
    panicWithPosWithDecl "Std.Data.DHashMap.Internal.AssocList.Basic" "Std.DHashMap.Internal.AssocList.getKey!" 168 11
      "key is not present in hash table"
-- Mathlib.Topology.Instances.Rat
Rat.instIsTopologicalAddGroup : IsTopologicalAddGroup ℚ
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.norm_eq_zero_iff : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.mixedEmbedding.mixedSpace K},
  NumberField.mixedEmbedding.norm x = 0 ↔ ∃ w, (NumberField.mixedEmbedding.normAtPlace w) x = 0
-- Init.Data.UInt.Bitwise
USize.toUInt16_or : ∀ (a b : USize), (a ||| b).toUInt16 = a.toUInt16 ||| b.toUInt16
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.MkTableKey.State.lmap : Lean.Meta.SynthInstance.MkTableKey.State → Std.HashMap Lean.LMVarId Lean.Level
-- Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure
AlgebraicIndependent.extendScalars : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_4} {x : ι → A} (S : Type u_5) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : CommRing A] [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A]
  [NoZeroDivisors S], AlgebraicIndependent R x → ∀ [alg : Algebra.IsAlgebraic R S], AlgebraicIndependent S x
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The underlying function.  -/
MulActionHom.toFun : {M : Type u_2} →
  {N : Type u_3} →
    {φ : M → N} → {X : Type u_5} → [inst : SMul M X] → {Y : Type u_6} → [inst_1 : SMul N Y] → (X →ₑ[φ] Y) → X → Y
-- Lean.Server.FileSource
Lean.Lsp.instFileSourcePlainTermGoalParams : Lean.Lsp.FileSource Lean.Lsp.PlainTermGoalParams
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.brecOn_2.go : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      {motive_1 : Lean.PrefixTreeNode α β cmp → Sort u_1} →
        {motive_2 : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp → Sort u_1} →
          {motive_3 : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp → Sort u_1} →
            {motive_4 : (Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) → Sort u_1} →
              (t : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp) →
                ((t : Lean.PrefixTreeNode α β cmp) → t.below → motive_1 t) →
                  ((t : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp) →
                      Lean.PrefixTreeNode.below_1 t → motive_2 t) →
                    ((t : Std.DTreeMap.Raw α (fun x => Lean.PrefixTreeNode α β cmp) cmp) →
                        Lean.PrefixTreeNode.below_2 t → motive_3 t) →
                      ((t : Std.DTreeMap.Internal.Impl α fun x => Lean.PrefixTreeNode α β cmp) →
                          Lean.PrefixTreeNode.below_3 t → motive_4 t) →
                        motive_3 t ×' Lean.PrefixTreeNode.below_2 t
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Simprocs.post : Lean.Meta.Simprocs → Lean.Meta.Simp.SimprocTree
-- Init.Prelude
/-- Congruence in the function argument: if `a₁ = a₂` then `f a₁ = f a₂` for
any (nondependent) function `f`. This is more powerful than it might look at first, because
you can also use a lambda expression for `f` to prove that
`<something containing a₁> = <something containing a₂>`. This function is used
internally by tactics like `congr` and `simp` to apply equalities inside
subterms.

For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
 -/
congrArg : ∀ {α : Sort u} {β : Sort v} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.coe_quotQuotEquivQuotOfLEₐ : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {I J : Ideal A}
  (h : I ≤ J), ⇑(DoubleQuot.quotQuotEquivQuotOfLEₐ R h) = ⇑(DoubleQuot.quotQuotEquivQuotOfLE h)
-- Mathlib.Algebra.Order.Hom.Basic
/-- `MulRingNormClass F α` states that `F` is a type of `β`-valued multiplicative norms on the
ring `α`.

You should extend this class when you extend `MulRingNorm`.  -/
MulRingNormClass : (F : Type u_7) →
  (α : outParam (Type u_8)) →
    (β : outParam (Type u_9)) → [NonAssocRing α] → [Semiring β] → [PartialOrder β] → [FunLike F α β] → Prop
-- Mathlib.Data.Fintype.Order
Finite.bddAbove_range : ∀ {ι : Sort u_1} {α : Type u_2} [Finite ι] [Nonempty α] [inst : Preorder α] [IsDirectedOrder α] (f : ι → α),
  BddAbove (Set.range f)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Util
_private.Lean.Meta.Tactic.Grind.Arith.Linear.Util.0.Lean.Grind.Linarith.Poly.updateOccs.go : Lean.Grind.Linarith.Var → Lean.Grind.Linarith.Poly → Lean.Meta.Grind.Arith.Linear.LinearM Unit
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.hasLiftingPropertyFixedBot_ι_app_bot : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c)
  {X Y : C} {p : X ⟶ Y} {g : c.pt ⟶ Y} [F.IsWellOrderContinuous] [inst_4 : SuccOrder J] [WellFoundedLT J],
  (∀ (j : J),
      ¬IsMax j →
        CategoryTheory.HasLiftingPropertyFixedBot (F.map (CategoryTheory.homOfLE ⋯)) p
          (CategoryTheory.CategoryStruct.comp (c.ι.app (Order.succ j)) g)) →
    CategoryTheory.HasLiftingPropertyFixedBot (c.ι.app ⊥) p g
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf_set_le : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {f : β → α} {s : Set β},
  BddBelow (f '' s) → ∀ {c : β}, c ∈ s → ⨅ i, f ↑i ≤ f c
-- Mathlib.Topology.Defs.Basic
/-- A one-field structure wrapper for `X` with the topology coinduced from `t`.  -/
WithTopology : (X : Type u_1) → TopologicalSpace X → Type u_1
-- Mathlib.Data.Sigma.Order
Sigma.preorder : {ι : Type u_1} → {α : ι → Type u_2} → [(i : ι) → Preorder (α i)] → Preorder ((i : ι) × α i)
-- Mathlib.Geometry.Group.Growth.LinearLowerBound
Finset.pow_right_strictMono : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {X : Finset G},
  1 ∈ X → (↑(Subgroup.closure ↑X)).Infinite → StrictMono fun n => X ^ n
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_right_inj₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : LinearOrder G₀] {a : G₀} {m n : ℤ} [PosMulStrictMono G₀]
  [ZeroLEOneClass G₀], 0 < a → a ≠ 1 → (a ^ m = a ^ n ↔ m = n)
-- Aesop.BuiltinRules.DestructProducts
Aesop.BuiltinRules.destructProductsCore : Lean.MVarId → Lean.Meta.TransparencyMode → Aesop.BaseM (Lean.MVarId × Array Aesop.Script.LazyStep)
-- Batteries.Data.Fin.Coding
Fin.encodeFun_decodeFun : ∀ {n m : ℕ} (x : Fin (n ^ m)), Fin.encodeFun (Fin.decodeFun x) = x
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkFVarS : {m : Type → Type} → [Lean.Meta.Sym.Internal.MonadShareCommon m] → Lean.FVarId → m Lean.Expr
-- Mathlib.Topology.Order
instDiscreteTopologyPEmpty : DiscreteTopology PEmpty.{u_1 + 1}
-- Mathlib.Data.Set.Basic
Set.decidableInsert : {α : Type u} → (s : Set α) → (a b : α) → [Decidable (a = b)] → [Decidable (a ∈ s)] → Decidable (a ∈ insert b s)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.liftCocycle.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α α_1 : CochainComplex.HomComplex.Cocycle K F m) (e_α : α = α_1)
  (β β_1 : CochainComplex.HomComplex.Cochain K G n) (e_β : β = β_1) (h : n + 1 = m)
  (eq : CochainComplex.HomComplex.δ n m β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0),
  CochainComplex.mappingCone.liftCocycle φ α β h eq = CochainComplex.mappingCone.liftCocycle φ α_1 β_1 h ⋯
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.condIndep_biSup_compl : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [inst : StandardBorelSpace Ω] (hm : m ≤ m0) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.iCondIndep m hm s μ →
      ∀ (t : Set ι), ProbabilityTheory.CondIndep m (⨆ n ∈ t, s n) (⨆ n ∈ tᶜ, s n) hm μ
-- Mathlib.GroupTheory.Exponent
Monoid.lcm_orderOf_eq_exponent : ∀ {G : Type u} [inst : Monoid G] [inst_1 : Fintype G], Finset.univ.lcm orderOf = Monoid.exponent G
-- Mathlib.Order.Interval.Set.SuccPred
Set.insert_Icc_right_eq_Icc_succ : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α},
  a ≤ Order.succ b → insert (Order.succ b) (Set.Icc a b) = Set.Icc a (Order.succ b)
-- Mathlib.Algebra.Homology.BifunctorShift
CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_inv_f_f : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Preadditive C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (y i i_1 : ℤ),
  ((K₁.mapBifunctorHomologicalComplexShift₂Iso K₂ F y).inv.f i).f i_1 =
    CategoryTheory.CategoryStruct.id ((F.obj (K₁.X i)).obj (K₂.X (i_1 + y)))
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.SameCycle.toList_isRotated : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {f : Equiv.Perm α} {x y : α},
  f.SameCycle x y → f.toList x ~r f.toList y
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis'.contract_isBasis'_sdiff_sdiff_of_subset : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α}, M.IsBasis' I X → J ⊆ I → (M.contract J).IsBasis' (I \ J) (X \ J)
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_iInf : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {ι : Sort u_7} [Nonempty ι] (f : G →+ N),
  Function.Injective ⇑f → ∀ (s : ι → AddSubgroup G), AddSubgroup.map f (iInf s) = ⨅ i, AddSubgroup.map f (s i)
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.enorm : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f : α → ε}, MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun x => ‖f x‖ₑ) μ
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
/-- The isomorphism expressing that `extendToSucc hj F τ` extends `F`.  -/
CategoryTheory.SmallObject.SuccStruct.extendToSuccRestrictionLEIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {J : Type u} →
      [inst_1 : LinearOrder J] →
        [inst_2 : SuccOrder J] →
          {j : J} →
            (hj : ¬IsMax j) →
              (F : CategoryTheory.Functor (↑(Set.Iic j)) C) →
                {X : C} →
                  (τ : F.obj ⟨j, ⋯⟩ ⟶ X) →
                    CategoryTheory.SmallObject.restrictionLE (CategoryTheory.SmallObject.SuccStruct.extendToSucc hj F τ)
                        ⋯ ≅
                      F
-- Mathlib.Algebra.MvPolynomial.Counit
MvPolynomial.ACounit_surjective : ∀ (A : Type u_1) (B : Type u_2) [inst : CommSemiring A] [inst_1 : CommSemiring B] [inst_2 : Algebra A B],
  Function.Surjective ⇑(MvPolynomial.ACounit A B)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support_one : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [Nontrivial R], MvPolynomial.support 1 = {0}
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Every fork is isomorphic to one of the form `Fork.of_ι _ _`.  -/
CategoryTheory.Limits.Fork.isoForkOfι : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} → (c : CategoryTheory.Limits.Fork f g) → c ≅ CategoryTheory.Limits.Fork.ofι c.ι ⋯
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.contStack.eq_def : ∀ (x : Turing.ToPartrec.Cont),
  Turing.PartrecToTM2.contStack x =
    match x with
    | Turing.ToPartrec.Cont.halt => []
    | Turing.ToPartrec.Cont.cons₁ a ns k => ns :: Turing.PartrecToTM2.contStack k
    | Turing.ToPartrec.Cont.cons₂ ns k => ns :: Turing.PartrecToTM2.contStack k
    | Turing.ToPartrec.Cont.comp a k => Turing.PartrecToTM2.contStack k
    | Turing.ToPartrec.Cont.fix a k => Turing.PartrecToTM2.contStack k
-- Mathlib.Topology.Clopen
isClopen_range_inl : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], IsClopen (Set.range Sum.inl)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  AlgebraicGeometry.Scheme.Hom.app I.subschemeι ↑U =
    CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) (I.subschemeObjIso U).inv
-- Mathlib.RingTheory.Extension.Basic
/-- The canonical hom from `P` to its base change `P.baseChange`.  -/
Algebra.Extension.toBaseChange : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {P : Algebra.Extension R S} →
            (T : Type u_1) → [inst_3 : CommRing T] → [inst_4 : Algebra R T] → P.Hom P.baseChange
-- Mathlib.Algebra.Order.Group.Pointwise.Bounds
isGLB_inv : ∀ {G : Type u_2} [inst : Group G] [inst_1 : Preorder G] [MulLeftMono G] [MulRightMono G] {s : Set G} {a : G},
  IsGLB s⁻¹ a ↔ IsLUB s a⁻¹