mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, k ∉ m₂ → (m₁ \ m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_lt_subst_cert.eq_1 : ∀ (x : Lean.Grind.Linarith.Var) (p₁ p₂ p₃ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.eq_lt_subst_cert x p₁ p₂ p₃ =
    (decide (p₁.coeff x > 0) && p₃ == (p₂.mul (p₁.coeff x)).combine (p₁.mul (-p₂.coeff x)))
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- Category structure on the strong natural transformations between oplax functors.

Note that this a scoped instance in the `Oplax.StrongTrans` namespace.  -/
CategoryTheory.Oplax.StrongTrans.homCategory : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          CategoryTheory.Category.{max u₁ w₂, max (max (max u₁ v₁) v₂) w₂} (F ⟶ G)
-- Mathlib.CategoryTheory.Equivalence
/-- Construct an isomorphism `H ≅ G.inverse ⋙ F` from an isomorphism `G.functor ⋙ H ≅ F`.  -/
CategoryTheory.Iso.isoInverseComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            {F : CategoryTheory.Functor C E} →
              {H : CategoryTheory.Functor D E} → {G : C ≌ D} → (G.functor.comp H ≅ F) → (H ≅ G.inverse.comp F)
-- Mathlib.Topology.Instances.NNReal.Lemmas
continuous_real_toNNReal : Continuous Real.toNNReal
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.continuous : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsOpenEmbedding f → Continuous f
-- Init.Data.UInt.Bitwise
UInt16.ofFin_shiftLeft : ∀ (a b : Fin UInt16.size), ↑b < 16 → UInt16.ofFin (a <<< b) = UInt16.ofFin a <<< UInt16.ofFin b
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.of_isScalarTower : ∀ {R : Type u_1} [inst : CommSemiring R] {f : Polynomial R} {A : Type u_2} (B : Type u_3) [inst_1 : CommSemiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B],
  (Polynomial.map (algebraMap R A) f).Splits → (Polynomial.map (algebraMap R B) f).Splits
-- Mathlib.Algebra.Order.GroupWithZero.Defs
PosMulReflectLT.toContravariantClass : ∀ {α : Type u_1} {inst : Mul α} {inst_1 : Zero α} {inst_2 : Preorder α} [self : PosMulReflectLT α],
  ContravariantClass { x // 0 ≤ x } α (fun x y => ↑x * y) fun x1 x2 => x1 < x2
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
/-- Reinterpret an inner product space `E` over `ℂ` as a `CStarModule` over `ℂ`.

Note: this instance requires `SMul ℂᵐᵒᵖ E` and `IsCentralScalar ℂ E` instances to exist on `E`,
which is unlikely to occur in practice. However, in practice one could either add those instances
to the type `E` in question, or else supply them to this instance manually, which is reason behind
the naming of these two instance arguments.  -/
WithCStarModule.instCStarModuleComplex : {E : Type u_2} → [inst : NormedAddCommGroup E] → [inst_1 : InnerProductSpace ℂ E] → CStarModule ℂ E
-- Init.Data.Float.Float32
instReprFloat32 : Repr Float32
-- Mathlib.FieldTheory.AxGrothendieck
/-- A slight generalization of the **Ax-Grothendieck** theorem

If `K` is an algebraically closed field, `ι` is a finite type, and `S` is a definable subset of
`ι → K`, then any injective polynomial map `S → S`  is also surjective on `S`.  -/
ax_grothendieck_of_definable : ∀ {K : Type u_1} {ι : Type u_2} [inst : Field K] [IsAlgClosed K] [Finite ι] [inst_3 : FirstOrder.Ring.CompatibleRing K]
  {c : Set K} (S : Set (ι → K)),
  c.Definable FirstOrder.Language.ring S →
    ∀ (ps : ι → MvPolynomial ι K),
      Set.MapsTo (fun v i => (MvPolynomial.eval v) (ps i)) S S →
        Set.InjOn (fun v i => (MvPolynomial.eval v) (ps i)) S → Set.SurjOn (fun v i => (MvPolynomial.eval v) (ps i)) S S
-- Mathlib.Algebra.Group.Prod
AddHom.coprod.eq_1 : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Add M] [inst_1 : Add N] [inst_2 : AddCommSemigroup P]
  (f : M →ₙ+ P) (g : N →ₙ+ P), f.coprod g = f.comp (AddHom.fst M N) + g.comp (AddHom.snd M N)
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.IsWeakLimit.mk.injEq : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F}
  (lift : (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt)
  (fac :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cone F) (j : J),
        CategoryTheory.CategoryStruct.comp (lift s) (t.π.app j) = s.π.app j)
      CategoryTheory.Limits.IsWeakLimit.fac._autoParam)
  (lift_1 : (s : CategoryTheory.Limits.Cone F) → s.pt ⟶ t.pt)
  (fac_1 :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cone F) (j : J),
        CategoryTheory.CategoryStruct.comp (lift_1 s) (t.π.app j) = s.π.app j)
      CategoryTheory.Limits.IsWeakLimit.fac._autoParam),
  ({ lift := lift, fac := fac } = { lift := lift_1, fac := fac_1 }) = (lift = lift_1)
-- Mathlib.Order.Interval.Set.ProjIcc
Set.IccExtend.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] {a b : α} (h : a ≤ b) (f : ↑(Set.Icc a b) → β),
  Set.IccExtend h f = f ∘ Set.projIcc a b h
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Returns `ULift.up true` if the iterator `it` yields no values.

`O(|it|)` since the iterator may skip an unknown number of times before returning a result.
Short-circuits upon encountering the first result. Only the first element of `it` is examined.

If the iterator is not productive, this function might run forever. The variant
`it.ensureTermination.isEmpty` always terminates after finitely many steps.
 -/
Std.IterM.isEmpty : {α β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] → [inst : Std.Iterator α m β] → [Std.IteratorLoop α m m] → Std.IterM m β → m (ULift.{w, 0} Bool)
-- Lean.Util.FindExpr
/-- Returns type for `findExt?` function argument.
 -/
Lean.Expr.FindStep : Type
-- Mathlib.Algebra.Group.Subgroup.Actions
AddSubgroup.vadd_def : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {S : AddSubgroup G} (g : ↥S) (m : α),
  g +ᵥ m = ↑g +ᵥ m
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
MultilinearMap.iteratedFDerivComponent.eq_1 : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] {α : Type u_1} (f : MultilinearMap R M₁ M₂) {s : Set ι} (e : α ≃ ↑s)
  [inst_5 : DecidablePred fun x => x ∈ s],
  f.iteratedFDerivComponent e =
    {
      toFun := fun z =>
        { toFun := fun v => ((f.domDomRestrictₗ fun i => i ∈ s) z) fun i => v (e.symm i) ↑i, map_update_add' := ⋯,
          map_update_smul' := ⋯ },
      map_update_add' := ⋯, map_update_smul' := ⋯ }
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.closure.eq_1 : ∀ {R : Type u} [inst : NonAssocRing R] (s : Set R), Subring.closure s = sInf {S | s ⊆ ↑S}
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.verts_inf : ∀ {V : Type u} {G : SimpleGraph V} (G₁ G₂ : G.Subgraph), (G₁ ⊓ G₂).verts = G₁.verts ∩ G₂.verts
-- Mathlib.Data.Finset.Card
Finset.card_insert_of_mem : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], a ∈ s → (insert a s).card = s.card
-- Mathlib.Analysis.Calculus.ContDiff.Defs
_private.Mathlib.Analysis.Calculus.ContDiff.Defs.0.ContDiffWithinAt.match_1.eq_1 : ∀ (motive : WithTop ℕ∞ → Sort u_1) (h_1 : Unit → motive none) (h_2 : (n : ℕ∞) → motive (some n)),
  (match none with
    | none => h_1 ()
    | some n => h_2 n) =
    h_1 ()
-- Mathlib.Topology.Category.Stonean.Basic
Stonean.instHasPropExtremallyDisconnectedCarrier : ∀ (X : Type u_1) [inst : TopologicalSpace X] [ExtremallyDisconnected X],
  CompHausLike.HasProp (fun Y => ExtremallyDisconnected ↑Y) X
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.PackedBitVec.mk : {w : ℕ} → BitVec w → Std.Tactic.BVDecide.BVExpr.PackedBitVec
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
VonNeumannAlgebra.instSetLike : {H : Type u} →
  [inst : NormedAddCommGroup H] →
    [inst_1 : InnerProductSpace ℂ H] → [inst_2 : CompleteSpace H] → SetLike (VonNeumannAlgebra H) (H →L[ℂ] H)
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.StartsWithResult.exact.sizeOf_spec : sizeOf Lean.Grind.AC.StartsWithResult.exact✝ = 1
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_le_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t → ∀ {fallback : α}, (cmp (t.minKeyD fallback) k).isLE = true
-- Init.Data.SInt.Lemmas
Int32.toInt16_add : ∀ (a b : Int32), (a + b).toInt16 = a.toInt16 + b.toInt16
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- A subalgebra is isomorphic to its image under an injective `AlgHom`  -/
Subalgebra.equivMapOfInjective : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Semiring B] →
              [inst_4 : Algebra R B] →
                (S : Subalgebra R A) → (f : A →ₐ[R] B) → Function.Injective ⇑f → ↥S ≃ₐ[R] ↥(Subalgebra.map f S)
-- Init.Data.Iterators.Lemmas.Combinators.Append
Std.Iter.Intermediate.appendSnd.eq_1 : ∀ {α₂ β : Type w} [inst : Std.Iterator α₂ Id β] (α₁ : Type w) (it₂ : Std.Iter β),
  Std.Iter.Intermediate.appendSnd α₁ it₂ = (Std.IterM.Intermediate.appendSnd α₁ it₂.toIterM).toIter
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.symm_comp_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (e : α ≃*o β) (f : α → α) (g : α → β), ⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f
-- Mathlib.Data.ENNReal.Real
/-- `ENNReal.toReal` as a `MonoidHom`.  -/
ENNReal.toRealHom : ENNReal →*₀ ℝ
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.orderOf_isConj_two_of_ne_one : ∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] [inst_2 : Algebra k K] {φ : K →+* ℂ} {σ : Gal(K/k)},
  NumberField.ComplexEmbedding.IsConj φ σ → σ ≠ 1 → orderOf σ = 2
-- Mathlib.Algebra.Field.Defs
/-- However `NNRat.cast` is defined, it must be propositionally equal to `a / b`.

Do not use this lemma directly. Use `NNRat.cast_def` instead.  -/
DivisionSemiring.nnratCast_def : ∀ {K : Type u_2} [self : DivisionSemiring K] (q : ℚ≥0), ↑q = ↑q.num / ↑q.den
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.continuous_comp : ∀ {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [inst : TopologicalSpace M₁] [inst_1 : TopologicalSpace M₂]
  [inst_2 : TopologicalSpace M₃] [inst_3 : AddCommMonoid M₁] {f : M₁ → M₂},
  IsCompactOperator f → ∀ {g : M₂ → M₃}, Continuous g → IsCompactOperator (g ∘ f)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
_private.Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic.0.CFC.termσₙ : Lean.ParserDescr
-- Mathlib.Algebra.Homology.HomologicalBicomplex
/-- Constructor for a morphism `K ⟶ L` in the category `HomologicalComplex₂ C c₁ c₂` which
takes as inputs a morphism `f : K.toGradedObject ⟶ L.toGradedObject` and
the compatibilities with both horizontal and vertical differentials.  -/
HomologicalComplex₂.homMk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          {c₁ : ComplexShape I₁} →
            {c₂ : ComplexShape I₂} →
              {K L : HomologicalComplex₂ C c₁ c₂} →
                (f : K.toGradedObject ⟶ L.toGradedObject) →
                  (∀ (i₁ i₁' : I₁) (i₂ : I₂),
                      c₁.Rel i₁ i₁' →
                        CategoryTheory.CategoryStruct.comp (f (i₁, i₂)) ((L.d i₁ i₁').f i₂) =
                          CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (f (i₁', i₂))) →
                    (∀ (i₁ : I₁) (i₂ i₂' : I₂),
                        c₂.Rel i₂ i₂' →
                          CategoryTheory.CategoryStruct.comp (f (i₁, i₂)) ((L.X i₁).d i₂ i₂') =
                            CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (f (i₁, i₂'))) →
                      (K ⟶ L)
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.subsingleton_of_subsingleton : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [Subsingleton A],
  Subsingleton (Subalgebra R A)
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instAddCommMonoid : {α : Type u} →
  {R : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace R] →
        [inst_2 : AddCommMonoid R] → [BoundedAdd R] → [ContinuousAdd R] → AddCommMonoid (BoundedContinuousFunction α R)
-- Mathlib.Algebra.GroupWithZero.Basic
mul_eq_left₀ : ∀ {M₀ : Type u_1} {a b : M₀} [inst : MulZeroOneClass M₀] [IsLeftCancelMulZero M₀], a ≠ 0 → (a * b = a ↔ b = 1)
-- Mathlib.FieldTheory.Perfect
frobeniusEquiv_def : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p] (x : R),
  (frobeniusEquiv R p) x = x ^ p
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.isUnit_singleton : ∀ {α : Type u_2} [inst : Group α] (a : α), IsUnit {a}
-- Mathlib.Algebra.Order.CompleteField
/-- `inducedMap` as an additive homomorphism.  -/
ConditionallyCompleteLinearOrderedField.inducedAddHom : (α : Type u_2) →
  (β : Type u_3) →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [IsStrictOrderedRing α] →
          [inst_3 : Field β] →
            [inst_4 : ConditionallyCompleteLinearOrder β] → [IsStrictOrderedRing β] → [Archimedean α] → α →+ β
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.whiskerLeft : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  (X : CategoryTheory.FreeMonoidalCategory C) {Y Z : CategoryTheory.FreeMonoidalCategory C} (f f' : Y.Hom Z)
  (a : CategoryTheory.FreeMonoidalCategory.HomEquiv f f'),
  CategoryTheory.FreeMonoidalCategory.HomEquiv.below a →
    motive f f' a → CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Init.GrindInstances.Ring.Nat
Lean.Grind.instIsPreorderNat : Std.IsPreorder ℕ
-- Mathlib.AlgebraicGeometry.Cover.Directed
/-- The transition maps of a directed cover.  -/
AlgebraicGeometry.Scheme.Cover.trans : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {X : AlgebraicGeometry.Scheme} →
    (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X) →
      [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] → [𝒰.LocallyDirected] → {i j : 𝒰.I₀} → (i ⟶ j) → (𝒰.X i ⟶ 𝒰.X j)
-- Mathlib.Topology.DiscreteSubset
/-- If a set is codiscrete within `U`, then it is codiscrete within any subset of `U`.  -/
Filter.codiscreteWithin_mono : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U₁ U : Set X},
  U₁ ⊆ U → Filter.codiscreteWithin U₁ ≤ Filter.codiscreteWithin U
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.VariableChange.instOne : {R : Type u} → [inst : CommRing R] → One (WeierstrassCurve.VariableChange R)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAlgebra : {R : Type u_1} →
  {ι : Type u_2} →
    [inst : Preorder ι] →
      {G : ι → Type u_3} →
        {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
          {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
            [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
              [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
                [inst_3 : IsDirectedOrder ι] →
                  [inst_4 : Nonempty ι] →
                    [inst_5 : CommSemiring R] →
                      [inst_6 : (i : ι) → Semiring (G i)] →
                        [inst_7 : (i : ι) → Algebra R (G i)] →
                          [inst_8 : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)] →
                            Algebra R (DirectLimit G f)
-- Mathlib.CategoryTheory.DinatTrans
CategoryTheory.DinatTrans.precompNatTrans_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C D)} (δ : CategoryTheory.DinatTrans G H) (α : F ⟶ G)
  (X : C), (δ.precompNatTrans α).app X = CategoryTheory.CategoryStruct.comp ((α.app (Opposite.op X)).app X) (δ.app X)
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.Receiver.tryRecv : {α : Type} → Std.Bounded.Receiver✝ α → BaseIO (Option α)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.mem_ofList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k : α}, k ∈ Std.DHashMap.Raw.Const.ofList l ↔ (List.map Prod.fst l).contains k = true
-- Init.Data.String.Slice
String.Slice.RevSplitIterator : {σ : String.Slice → Type} →
  {ρ : Type} → (pat : ρ) → String.Slice → [String.Slice.Pattern.ToBackwardSearcher pat σ] → Type
-- Init.Data.UInt.Basic
instOrOpUSize : OrOp USize
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `Irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is an odd
prime, then the norm of `ζ - 1` is `p`.  -/
IsPrimitiveRoot.norm_sub_one_of_prime_ne_two : ∀ {p : ℕ} {K : Type u} {L : Type v} [inst : Field L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L] {k : ℕ},
  IsPrimitiveRoot ζ (p ^ (k + 1)) →
    ∀ [hpri : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K L],
      Irreducible (Polynomial.cyclotomic (p ^ (k + 1)) K) → p ≠ 2 → (Algebra.norm K) (ζ - 1) = ↑p
-- Mathlib.FieldTheory.KummerExtension
/-- The equivalence between the roots of unity of `K` and `Gal(K[ⁿ√a]/K)`.  -/
autAdjoinRootXPowSubCEquiv : {K : Type u} →
  [inst : Field K] →
    {n : ℕ} →
      (primitiveRoots n K).Nonempty →
        {a : K} →
          Irreducible (Polynomial.X ^ n - Polynomial.C a) →
            [NeZero n] →
              ↥(rootsOfUnity n K) ≃*
                AdjoinRoot (Polynomial.X ^ n - Polynomial.C a) ≃ₐ[K] AdjoinRoot (Polynomial.X ^ n - Polynomial.C a)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
_private.Mathlib.Combinatorics.SimpleGraph.Walk.Operations.0.SimpleGraph.Walk.concatRecAux.match_1.splitter : {V : Type u_1} →
  {G : SimpleGraph V} →
    {u : V} →
      (motive : (v : V) → G.Walk u v → Sort u_2) →
        (v : V) →
          (x : G.Walk u v) →
            (Unit → motive u SimpleGraph.Walk.nil) →
              ((v v_1 : V) → (h : G.Adj u v_1) → (p : G.Walk v_1 v) → motive v (SimpleGraph.Walk.cons h p)) → motive v x
-- Mathlib.Algebra.Order.Hom.Submonoid
/-- The top submonoid is order isomorphic to the whole monoid.  -/
Submonoid.topOrderMonoidIso : {α : Type u_1} → [inst : Preorder α] → [inst_1 : Monoid α] → ↥⊤ ≃*o α
-- Mathlib.RingTheory.Ideal.Operations
Ideal.radical_isRadical : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal R), I.radical.IsRadical
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- An isomorphism `Over.mk p ≅ Over.mk (pullback.fst f g)` in `Over X` yields
an `IsPullback` square.  -/
CategoryTheory.IsPullback.of_over_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPullbacksAlong g] {P : C} {p : P ⟶ X}
  (e : CategoryTheory.Over.mk p ≅ CategoryTheory.Over.mk (CategoryTheory.Limits.pullback.fst f g)),
  CategoryTheory.IsPullback p
    (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left e.hom) (CategoryTheory.Limits.pullback.snd f g)) f
    g
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Finset.le_prod_max_one : ∀ {ι : Type u_1} {s : Finset ι} {M : Type u_4} [inst : CommMonoidWithZero M] [inst_1 : LinearOrder M] [ZeroLEOneClass M]
  [PosMulMono M] {i : ι}, i ∈ s → ∀ (f : ι → M), f i ≤ ∏ i ∈ s, max (f i) 1
-- Mathlib.LinearAlgebra.Prod
/-- **Line test** for module isomorphisms.

Let `f : G → H × I` be a linear (or semilinear) map to a product of modules. Assume that `f` is
surjective onto both factors and that the image of `f` intersects every "vertical line"
`{(h, i) | i : I}` and every "horizontal line" `{(h, i) | h : H}` at most once. Then the image of
`f` is the graph of some module isomorphism `f' : H ≃ I`.  -/
LinearMap.exists_linearEquiv_eq_graph : ∀ {R : Type u_3} {S : Type u_4} {G : Type u_5} {H : Type u_6} {I : Type u_7} [inst : Semiring R] [inst_1 : Semiring S]
  {σ : R →+* S} [inst_2 : RingHomSurjective σ] [inst_3 : AddCommMonoid G] [inst_4 : Module R G]
  [inst_5 : AddCommMonoid H] [inst_6 : Module S H] [inst_7 : AddCommMonoid I] [inst_8 : Module S I]
  {f : G →ₛₗ[σ] H × I},
  Function.Surjective (Prod.fst ∘ ⇑f) →
    Function.Surjective (Prod.snd ∘ ⇑f) →
      (∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2) → ∃ e, f.range = (↑e).graph
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.hom_comp : ∀ {X Y T : CommGrpCat} (f : X ⟶ Y) (g : Y ⟶ T),
  CommGrpCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (CommGrpCat.Hom.hom g).comp (CommGrpCat.Hom.hom f)
-- Mathlib.Data.Nat.Factors
Nat.eq_of_perm_primeFactorsList : ∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → a.primeFactorsList.Perm b.primeFactorsList → a = b
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.tryCatchPred : Lean.Elab.Term.Do.CodeBlock →
  Array Lean.Elab.Term.Do.ToCodeBlock.Catch →
    Option Lean.Elab.Term.Do.CodeBlock → (Lean.Elab.Term.Do.Code → Bool) → Bool
-- Mathlib.Algebra.Group.Action.Defs
VAddCommClass.of_add_vadd_zero : ∀ {M : Type u_9} {N : Type u_10} [inst : AddMonoid N] [inst_1 : VAdd M N],
  (∀ (x : M) (y : N), y + (x +ᵥ 0) = x +ᵥ y) → VAddCommClass M N N
-- Mathlib.LinearAlgebra.TensorProduct.Pi
/-- For any `R`-module `N`, index type `ι` and family of `R`-modules `Mᵢ`, there is a natural
linear map `N ⊗[R] (∀ i, M i) →ₗ ∀ i, N ⊗[R] M i`. This map is an isomorphism if `ι` is finite.  -/
TensorProduct.piRightHom : (R : Type u_1) →
  [inst : CommSemiring R] →
    (S : Type u_2) →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (N : Type u_3) →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] →
                [inst_5 : Module S N] →
                  [inst_6 : IsScalarTower R S N] →
                    {ι : Type u_4} →
                      (M : ι → Type u_5) →
                        [inst_7 : (i : ι) → AddCommMonoid (M i)] →
                          [inst_8 : (i : ι) → Module R (M i)] →
                            TensorProduct R N ((i : ι) → M i) →ₗ[S] (i : ι) → TensorProduct R N (M i)
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- Cells are up-left justified, witnessed by the fact that `cells` is a lower set in `ℕ × ℕ`.  -/
YoungDiagram.isLowerSet : ∀ (self : YoungDiagram), IsLowerSet ↑self.cells
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.SearchStep.cast_rfl : ∀ {s : String.Slice} {st : String.Slice.Pattern.SearchStep s}, String.Slice.Pattern.SearchStep.cast ⋯ st = st
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.specialLinearGroup_apply : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : Algebra R ℝ] (g : Matrix.SpecialLinearGroup (Fin 2) R)
  (z : UpperHalfPlane),
  g • z =
    {
      coe :=
        (↑((algebraMap R ℝ) (↑g 0 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 0 1))) /
          (↑((algebraMap R ℝ) (↑g 1 0)) * ↑z + ↑((algebraMap R ℝ) (↑g 1 1))),
      coe_im_pos := ⋯ }
-- Mathlib.Data.NNReal.Defs
NNReal.pow_antitone_exp : ∀ {a : NNReal} (m n : ℕ), m ≤ n → a ≤ 1 → a ^ n ≤ a ^ m
-- Mathlib.Algebra.Group.UniqueProds.Basic
/-- `UniqueProd` is preserved under multiplicative equivalences.  -/
MulEquiv.uniqueProds_iff : ∀ {G : Type u} {H : Type v} [inst : Mul G] [inst_1 : Mul H] (f : G ≃* H), UniqueProds G ↔ UniqueProds H