mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Internal.Parsec.String
/-- Takes a fixed amount of chars from the iterator.
 -/
Std.Internal.Parsec.String.take : ℕ → Std.Internal.Parsec.String.Parser String
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- A continuous linear equivalence of codomains
defines an equivalence between continuous alternating maps.  -/
ContinuousLinearEquiv.continuousAlternatingMapCongrRightEquiv : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_4} →
      {N' : Type u_5} →
        {ι : Type u_6} →
          [inst : Semiring R] →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : Module R M] →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : AddCommMonoid N] →
                    [inst_5 : Module R N] →
                      [inst_6 : TopologicalSpace N] →
                        [inst_7 : AddCommMonoid N'] →
                          [inst_8 : Module R N'] →
                            [inst_9 : TopologicalSpace N'] → (N ≃L[R] N') → M [⋀^ι]→L[R] N ≃ M [⋀^ι]→L[R] N'
-- Mathlib.Data.Finset.Sups
Finset.forall_mem_compls : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Finset α} {p : α → Prop}, (∀ a ∈ s.compls, p a) ↔ ∀ a ∈ s, p aᶜ
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.pairwise_toList_lt : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [inst_7 : Std.Rxc.IsAlwaysFinite α],
  List.Pairwise (fun a b => a < b) r.toList
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.toFun_eq_coe : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (f : Π₀ (i : ι), β i), f.toFun = ⇑f
-- Lean.Data.SMap
Lean.SMap.find? : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.SMap α β → α → Option β
-- Mathlib.RingTheory.Polynomial.UniqueFactorization
/-- A polynomial over a field which is not a unit must have a monic irreducible factor.
See also `WfDvdMonoid.exists_irreducible_factor`.  -/
Polynomial.exists_monic_irreducible_factor : ∀ {F : Type u_1} [inst : Field F] (f : Polynomial F), ¬IsUnit f → ∃ g, g.Monic ∧ Irreducible g ∧ g ∣ f
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
addMonoidAlgebraRingEquivDirectSum_apply : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Semiring M]
  [inst_3 : (m : M) → Decidable (m ≠ 0)], ⇑addMonoidAlgebraRingEquivDirectSum = AddMonoidAlgebra.toDirectSum
-- Mathlib.Algebra.Group.Prod
/-- `Prod.map` as a `MonoidHom`.  -/
MulHom.prodMap : {M : Type u_3} →
  {N : Type u_4} →
    {M' : Type u_6} →
      {N' : Type u_7} →
        [inst : Mul M] →
          [inst_1 : Mul N] → [inst_2 : Mul M'] → [inst_3 : Mul N'] → (M →ₙ* M') → (N →ₙ* N') → M × N →ₙ* M' × N'
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α}, k ∉ t₂ → (t₁ ∪ t₂).get? k = t₁.get? k
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.below.insert : ∀ {α : Type u} [inst : Ord α] {motive : {β : α → Type v} → (a : Std.DTreeMap.Internal.Impl α β) → a.WF → Prop}
  {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} {h : t.Balanced} {k : α} {v : x k} (a : t.WF),
  Std.DTreeMap.Internal.Impl.WF.below a → motive t a → Std.DTreeMap.Internal.Impl.WF.below ⋯
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.exactAt_iff_isZero_homology : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i : ι) [inst_2 : K.HasHomology i],
  K.ExactAt i ↔ CategoryTheory.Limits.IsZero (K.homology i)
-- Mathlib.NumberTheory.Divisors
/-- `n : ℕ` is perfect if and only the sum of the proper divisors of `n` is `n` and `n`
is positive.  -/
Nat.Perfect : ℕ → Prop
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.lift.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 ℤ}
  (α α_1 : CochainComplex.HomComplex.Cocycle K F 1) (e_α : α = α_1) (β β_1 : CochainComplex.HomComplex.Cochain K G 0)
  (e_β : β = β_1)
  (eq : CochainComplex.HomComplex.δ 0 1 β + (↑α).comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯ = 0),
  CochainComplex.mappingCone.lift φ α β eq = CochainComplex.mappingCone.lift φ α_1 β_1 ⋯
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → (t₁ ∩ t₂).getKey? k = t₁.getKey? k
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {t₁ t₂ : Std.TreeMap α Unit cmp},
  t₁.Equiv t₂ → ∀ (l : List α), (t₁.insertManyIfNewUnit l).Equiv (t₂.insertManyIfNewUnit l)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.diff_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₃.WF → m₂.Equiv m₃ → (m₁ \ m₂).Equiv (m₁ \ m₃)
-- Std.Http.Protocol.H1
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.BodyMode.eof : Std.Http.Protocol.H1.Machine.BodyMode✝
-- Lean.Elab.Calc
_private.Lean.Elab.Calc.0.Lean.Elab.Term.annotateFirstHoleWithType.go : Lean.Expr → Lean.Syntax → StateT Bool Lean.Elab.TermElabM Lean.Syntax
-- Mathlib.Topology.Covering.Quotient
IsAddQuotientCoveringMap.map_vadd : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E], IsAddQuotientCoveringMap f G → ∀ (g : G) {e : E}, f (g +ᵥ e) = f e
-- Mathlib.Data.List.Pi
List.Pi.cons_def : ∀ {ι : Type u_1} [inst : DecidableEq ι] {α : ι → Sort u_2} {i : ι} {l : List ι} (a : α i) (f : (j : ι) → j ∈ l → α j),
  List.Pi.cons i l a f = fun j hj => if h : j = i then ⋯ ▸ a else f j ⋯
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftUnshift_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n' a : ℤ}
  (γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ)
  (hn : n + a = n'), (-γ).leftUnshift n hn = -γ.leftUnshift n hn
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
/-- Turn a morphism in `HopfAlgCat` back into a `BialgHom`.  -/
HopfAlgCat.Hom.toBialgHom : {R : Type u} → [inst : CommRing R] → {X Y : HopfAlgCat R} → X.Hom Y → X.carrier →ₐc[R] Y.carrier
-- Mathlib.Algebra.Group.Prod
Prod.instCommGroup : {G : Type u_1} → {H : Type u_2} → [CommGroup G] → [CommGroup H] → CommGroup (G × H)
-- Mathlib.Order.CountableSupClosed
countableSupClosure_univ : ∀ {α : Type u_2} [inst : Preorder α], countableSupClosure Set.univ = Set.univ
-- Mathlib.Tactic.Simps.Basic
/-- A hiding rule `-fieldName`  -/
Simps.ProjectionRule.erase : Lean.Name → Lean.Syntax → Simps.ProjectionRule
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp_ofNat : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) [inst_1 : n.AtLeastTwo], { toFinsupp := OfNat.ofNat n } = OfNat.ofNat n
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : ι → α → β}
  {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} (hf : ∀ (i : ι), AEMeasurable (f i) μ) {x : α},
  x ∈ aeSeqSet hf p → ∀ (i : ι), aeSeq hf p i x = f i x
-- Mathlib.CategoryTheory.Abelian.FunctorCategory
CategoryTheory.Abelian.FunctorCategory.functor_category_isIso_coimageImageComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type w} [inst_1 : CategoryTheory.Category.{z, w} D]
  [inst_2 : CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} (α : F ⟶ G),
  CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison α)
-- Mathlib.Algebra.Order.Group.OrderIso
/-- `x ↦ a - x` as an order-reversing equivalence.  -/
OrderIso.subLeft : {α : Type u} → [inst : AddGroup α] → [inst_1 : LE α] → [AddLeftMono α] → [AddRightMono α] → α → α ≃o αᵒᵈ
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- The domain of the truth morphism  -/
CategoryTheory.Subobject.Classifier.Ω₀ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Subobject.Classifier C → C
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative : ∀ {R : Type u} [inst : CommRing R] [NoZeroDivisors R] [CharZero R] {p : Polynomial R} {t : R} {n : ℕ},
  p ≠ 0 → (n < Polynomial.rootMultiplicity t p ↔ ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t)
-- Init.GrindInstances.Ring.SInt
Lean.Grind.instIsCharPISizeHPowNatOfNatNumBits : Lean.Grind.IsCharP ISize (2 ^ System.Platform.numBits)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_nat_mul_pi : ∀ (n : ℕ), Complex.sin (↑n * ↑Real.pi) = 0
-- Mathlib.Algebra.Ring.Action.ConjAct
ConjAct.unitsMulSemiringAction : {R : Type u_1} → [inst : Semiring R] → MulSemiringAction (ConjAct Rˣ) R
-- Init.Internal.Order.Basic
Lean.Order.instCompleteLatticePProd : {α : Sort u} →
  {β : Sort v} → [Lean.Order.CompleteLattice α] → [Lean.Order.CompleteLattice β] → Lean.Order.CompleteLattice (α ×' β)
-- Mathlib.Topology.Perfect
PerfectSpace.univ_preperfect : ∀ {α : Type u_1} {inst : TopologicalSpace α} [self : PerfectSpace α], Preperfect Set.univ
-- Mathlib.Data.Int.Sqrt
Int.sqrt_eq : ∀ (n : ℤ), Int.sqrt (n * n) = ↑n.natAbs
-- Std.Time.Format.Basic
Std.Time.instFormatGenericFormatFormatTypeString : {aw : Std.Time.Awareness} → Std.Time.Format (Std.Time.GenericFormat aw) fun x1 x2 => Std.Time.FormatType x1 x2.string
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
/-- A morphism in `SimplexCategory` is a monomorphism precisely when it is an injective function
 -/
SimplexCategory.mono_iff_injective : ∀ {n m : SimplexCategory} {f : n ⟶ m}, CategoryTheory.Mono f ↔ Function.Injective ⇑(SimplexCategory.Hom.toOrderHom f)
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- A graph induced from an acyclic graph is acyclic.  -/
SimpleGraph.IsAcyclic.induce : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsAcyclic → ∀ (s : Set V), (SimpleGraph.induce s G).IsAcyclic
-- Init.Data.Array.Find
Array.findFinIdx?_empty : ∀ {α : Type u_1} {p : α → Bool}, Array.findFinIdx? p #[] = none
-- Mathlib.NumberTheory.Modular
ModularGroup.exists_eq_T_zpow_of_c_eq_zero : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ}, ↑g 1 0 = 0 → ∃ n, ∀ (z : UpperHalfPlane), g • z = ModularGroup.T ^ n • z
-- Mathlib.Logic.Embedding.Set
Function.Embedding.codRestrict_apply : ∀ {α : Sort u_1} {β : Type u_2} (p : Set β) (f : α ↪ β) (H : ∀ (a : α), f a ∈ p) (a : α),
  (Function.Embedding.codRestrict p f H) a = ⟨f a, ⋯⟩
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.neg_le : ∀ {G : Type u_2} [inst : AddGroup G] (S T : AddSubmonoid G), -S ≤ T ↔ S ≤ -T
-- Std.Http.Data.Status
/-- 407 Proxy Authentication Required
 -/
Std.Http.Status.proxyAuthenticationRequired : Std.Http.Status
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Functor.projective_of_map_projective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] [F.PreservesEpimorphisms] {P : C},
  CategoryTheory.Projective (F.obj P) → CategoryTheory.Projective P
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.trunc_one : ∀ {σ : Type u_1} {R : Type u_2} [inst : DecidableEq σ] [inst_1 : CommSemiring R] (n : σ →₀ ℕ),
  n ≠ 0 → (MvPowerSeries.trunc R n) 1 = 1
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.lratChecker.match_3.congr_eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : List (Std.Tactic.BVDecide.LRAT.Action β α) → Sort u_3)
  (prf : List (Std.Tactic.BVDecide.LRAT.Action β α)) (h_1 : Unit → motive [])
  (h_2 :
    (id : ℕ) →
      (rupHints : Array ℕ) →
        (tail : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
          motive (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail))
  (h_3 :
    (id : ℕ) →
      (c : β) →
        (rupHints : Array ℕ) →
          (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
            motive (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf))
  (h_4 :
    (id : ℕ) →
      (c : β) →
        (pivot : Std.Sat.Literal α) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
                motive (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf))
  (h_5 :
    (ids : Array ℕ) →
      (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)) →
        motive (Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf))
  (id : ℕ) (rupHints : Array ℕ) (tail : List (Std.Tactic.BVDecide.LRAT.Action β α)),
  prf = Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail →
    (match prf with
      | [] => h_1 ()
      | Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints :: tail => h_2 id rupHints tail
      | Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints :: restPrf => h_3 id c rupHints restPrf
      | Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints :: restPrf =>
        h_4 id c pivot rupHints ratHints restPrf
      | Std.Tactic.BVDecide.LRAT.Action.del ids :: restPrf => h_5 ids restPrf) ≍
      h_2 id rupHints tail
-- Lean.Data.Options
Lean.Options.get? : {α : Type} → [Lean.KVMap.Value α] → Lean.Options → Lean.Name → Option α
-- Mathlib.RingTheory.Kaehler.Polynomial
KaehlerDifferential.mvPolynomialBasis_repr_D : ∀ (R : Type u) [inst : CommRing R] (σ : Type u_1) (x : MvPolynomial σ R),
  (KaehlerDifferential.mvPolynomialBasis R σ).repr ((KaehlerDifferential.D R (MvPolynomial σ R)) x) =
    (MvPolynomial.mkDerivation R fun x => fun₀ | x => 1) x
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeAddGroup.reduceCyclically.eq_1 : ∀ {α : Type u} [inst : DecidableEq α] (l : List (α × Bool)),
  FreeAddGroup.reduceCyclically l =
    List.bidirectionalRec [] (fun x => [x]) (fun a L b rC => if b.1 = a.1 ∧ (!b.2) = a.2 then rC else a :: L ++ [b]) l
-- Batteries.Data.ByteArray
ByteArray.get_extract_aux : ∀ {i : ℕ} {a : ByteArray} {start stop : ℕ}, i < (a.extract start stop).size → start + i < a.size
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.ofNat : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : DecidableEq n] (d : ℕ) [inst_5 : d.AtLeastTwo], (OfNat.ofNat d).PosSemidef
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k a : α} {v : β}, (t.insert k v).getKey! a = if cmp k a = Ordering.eq then k else t.getKey! a
-- Mathlib.Data.List.TakeDrop
List.takeI_left' : ∀ {α : Type u} [inst : Inhabited α] {l₁ l₂ : List α} {n : ℕ}, l₁.length = n → List.takeI n (l₁ ++ l₂) = l₁
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_eq_getKeyD : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {a fallback : α} {h : a ∈ m}, m.getKey a h = m.getKeyD a fallback
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.epi_v₂₃_τ₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.Epi S.v₂₃.τ₂
-- Mathlib.Analysis.Convex.Continuous
ConcaveOn.continuousOn_interior : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {C : Set E} {f : E → ℝ}
  [FiniteDimensional ℝ E], ConcaveOn ℝ C f → ContinuousOn f (interior C)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
/-- **Alias** of `WeierstrassCurve.HasGoodReduction`.

---

A minimal Weierstrass equation has good reduction if and only if
the valuation of its discriminant is 1.  -/
WeierstrassCurve.IsGoodReduction : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      [IsDiscreteValuationRing R] →
        {K : Type u_2} → [inst_3 : Field K] → [inst_4 : Algebra R K] → [IsFractionRing R K] → WeierstrassCurve K → Prop
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.le_logb_iff_rpow_le : ∀ {b x y : ℝ}, 1 < b → 0 < y → (x ≤ Real.logb b y ↔ b ^ x ≤ y)
-- Mathlib.Data.ENNReal.Inv
ENNReal.zpow_add : ∀ {x : ENNReal}, x ≠ 0 → x ≠ ⊤ → ∀ (m n : ℤ), x ^ (m + n) = x ^ m * x ^ n
-- Mathlib.Condensed.Epi
CondensedMod.epi_iff_locallySurjective_on_compHaus : ∀ (R : Type (u + 1)) [inst : Ring R] {X Y : CondensedMod R} (f : X ⟶ Y),
  CategoryTheory.Epi f ↔
    ∀ (S : CompHaus) (y : ↑(Y.obj.obj (Opposite.op S))),
      ∃ S' φ,
        ∃ (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom φ)),
          ∃ x,
            (CategoryTheory.ConcreteCategory.hom (f.hom.app (Opposite.op S'))) x =
              (CategoryTheory.ConcreteCategory.hom (Y.obj.map (Opposite.op φ))) y
-- Init.Data.Iterators.Lemmas.Consumers.Access
_private.Init.Data.Iterators.Lemmas.Consumers.Access.0.Std.Iter.atIdxSlow?_eq_match.match_3.splitter : {α β : Type u_1} →
  (motive : Std.IterStep (Std.Iter β) β → Sort u_2) →
    (x : Std.IterStep (Std.Iter β) β) →
      ((it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out)) →
        ((it' : Std.Iter β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.instDivisionRingNonZeroDivisors : {R : Type u_1} →
  [inst : Ring R] →
    [Nontrivial R] →
      [NoZeroDivisors R] →
        [inst_3 : OreLocalization.OreSet (nonZeroDivisors R)] → DivisionRing (OreLocalization (nonZeroDivisors R) R)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- If `f` is a regular mono, then any map `k : W ⟶ Y` equalizing `RegularMono.left` and
`RegularMono.right` induces a morphism `l : W ⟶ X` such that `l ≫ f = k`.  -/
CategoryTheory.RegularMono.lift' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y W : C} →
      {f : X ⟶ Y} →
        (hf : CategoryTheory.RegularMono f) →
          (k : W ⟶ Y) →
            CategoryTheory.CategoryStruct.comp k hf.left = CategoryTheory.CategoryStruct.comp k hf.right →
              { l // CategoryTheory.CategoryStruct.comp l f = k }
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.kerCotangentToTensor_injective_iff : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {P : Type u_2}
  [inst_3 : CommRing P] [inst_4 : Algebra R P] [Algebra.FormallySmooth R P] [inst_6 : Algebra P A]
  [IsScalarTower R P A],
  Function.Surjective ⇑(algebraMap P A) →
    (Function.Injective ⇑(KaehlerDifferential.kerCotangentToTensor R P A) ↔ Subsingleton (Algebra.H1Cotangent R A))
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanCompIso_hom_app_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  (CategoryTheory.Limits.spanCompIso F f g).hom.app CategoryTheory.Limits.WalkingSpan.zero =
    CategoryTheory.CategoryStruct.id
      (((CategoryTheory.Limits.span f g).comp F).obj CategoryTheory.Limits.WalkingSpan.zero)
-- Mathlib.NumberTheory.FunctionField
/-- **Alias** of `RatFunc.inftyValuation.X_zpow`. -/
FunctionField.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
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_inter_Ici : ∀ {α : Type u_1} [inst : SemilatticeSup α] {a b : α}, Set.Ici a ∩ Set.Ici b = Set.Ici (a ⊔ b)
-- Init.Data.Vector.Lemmas
/-- Variant of `map_id`, with a side condition that the function is pointwise the identity.  -/
Vector.map_id'' : ∀ {α : Type u_1} {n : ℕ} {f : α → α}, (∀ (x : α), f x = x) → ∀ (xs : Vector α n), Vector.map f xs = xs
-- Mathlib.Algebra.CharP.Frobenius
/-- The iterated Frobenius map of an algebra as an iterated-Frobenius-semilinear map.  -/
LinearMap.iterateFrobenius : (R : Type u_1) →
  [inst : CommSemiring R] →
    (S : Type u_2) →
      [inst_1 : CommSemiring S] →
        (p n : ℕ) → [inst_2 : ExpChar R p] → [ExpChar S p] → [inst_4 : Algebra R S] → S →ₛₗ[iterateFrobenius R p n] S
-- Mathlib.Analysis.Calculus.Gradient.Basic
inner_gradientWithin_right : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {x y : F} {s : Set F},
  inner 𝕜 x (gradientWithin f s y) = (starRingEnd 𝕜) ((fderivWithin 𝕜 f s y) x)
-- Mathlib.RingTheory.Congruence.Hom
RingCon.quotientKerEquivRangeₐ_comp_mkₐ : ∀ {M : Type u_1} {N : Type u_2} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring N] [inst_4 : Algebra R N] (φ : M →ₐ[R] N),
  (↑(RingCon.quotientKerEquivRangeₐ φ)).comp (RingCon.mkₐ R (RingCon.ker ↑φ)) = φ.rangeRestrict
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.mk.sizeOf_spec : ∀ {A : Type u_1} {B : Type u_2} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] [inst_4 : SizeOf A] [inst_5 : SizeOf B]
  (toNonUnitalRingHom : A →ₙ+* B)
  (map_star' : ∀ (a : A), toNonUnitalRingHom.toFun (star a) = star (toNonUnitalRingHom.toFun a)),
  sizeOf { toNonUnitalRingHom := toNonUnitalRingHom, map_star' := map_star' } = 1 + sizeOf toNonUnitalRingHom
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- The functor to another `CompHausLike` preserves pullbacks.  -/
CompHausLike.instPreservesLimitWalkingCospanCospanToCompHausLike : ∀ {P : TopCat → Prop} {X Y B : CompHausLike P} (f : X ⟶ B) (g : Y ⟶ B) [CompHausLike.HasExplicitPullback f g]
  {P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop),
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) (CompHausLike.toCompHausLike h)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
/-- the first projection  -/
CategoryTheory.Limits.ChosenPullback.p₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ S : C} →
      {f₁ : X₁ ⟶ S} → {f₂ : X₂ ⟶ S} → (self : CategoryTheory.Limits.ChosenPullback f₁ f₂) → self.pullback ⟶ X₁
-- Mathlib.Algebra.Group.Units.Defs
Units.mk_val : ∀ {α : Type u} [inst : Monoid α] (u : αˣ) (y : α) (h₁ : ↑u * y = 1) (h₂ : y * ↑u = 1),
  { val := ↑u, inv := y, val_inv := h₁, inv_val := h₂ } = u
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Outside the support, `config` takes the default value of `A`.  -/
SymbolicDynamics.FullShift.Pattern.condition : ∀ {A : Type u_1} {G : Type u_2} [inst : Inhabited A] (self : SymbolicDynamics.FullShift.Pattern A G),
  ∀ g ∉ self.support, self.config g = default
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.fFunctor_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S T : CategoryTheory.ShortComplex C} (f : S ⟶ T),
  CategoryTheory.ShortComplex.fFunctor.map f = CategoryTheory.Arrow.homMk f.τ₁ f.τ₂ ⋯