mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.assocIsometry_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (x : TensorProduct 𝕜 (TensorProduct 𝕜 E F) G),
  (TensorProduct.assocIsometry 𝕜 E F G) x = (TensorProduct.assoc 𝕜 E F G) x
-- Mathlib.Algebra.Notation.Prod
Prod.vadd_mk : ∀ {E : Type u_8} {α : Type u_9} {β : Type u_10} [inst : VAdd E α] [inst_1 : VAdd E β] (c : E) (a : α) (b : β),
  c +ᵥ (a, b) = (c +ᵥ a, c +ᵥ b)
-- Mathlib.Data.Rel
SetRel.image_sUnion : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β) (S : Set (Set α)), R.image (⋃₀ S) = ⋃ s ∈ S, R.image s
-- Init.Data.Vector.Attach
Vector.attach.eq_1 : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n), xs.attach = xs.attachWith (Membership.mem xs) ⋯
-- Std.Http.Data.URI.Basic
Std.Http.URI.UserInfo.mk.injEq : ∀ (username : Std.Http.URI.EncodedUserInfo) (password : Option Std.Http.URI.EncodedUserInfo)
  (username_1 : Std.Http.URI.EncodedUserInfo) (password_1 : Option Std.Http.URI.EncodedUserInfo),
  ({ username := username, password := password } = { username := username_1, password := password_1 }) =
    (username = username_1 ∧ password = password_1)
-- Mathlib.Algebra.Category.MonCat.Basic
_private.Mathlib.Algebra.Category.MonCat.Basic.0.AddCommMonCat.Hom.mk.inj : ∀ {A B : AddCommMonCat} {hom' hom'_1 : ↑A →+ ↑B}, { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.GroupTheory.MonoidLocalization.Cardinality
AddLocalization.cardinalMk_le : ∀ {M : Type u} [inst : AddCommMonoid M] (S : AddSubmonoid M), Cardinal.mk (AddLocalization S) ≤ Cardinal.mk M
-- Init.Data.Slice.Array.Lemmas
Subarray.mkSlice_rci_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : Subarray α} {lo : ℕ},
  Std.Rci.Sliceable.mkSlice xs lo...* = Std.Rco.Sliceable.mkSlice xs lo...Std.Slice.size xs
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.isEmbedding_toWeakDualBCNN : ∀ (Ω : Type u_1) [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [HasOuterApproxClosed Ω]
  [inst_3 : BorelSpace Ω], Topology.IsEmbedding MeasureTheory.FiniteMeasure.toWeakDualBCNN
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.forIn'_eq_forIn'_toArray : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_3 : Std.Rxi.IsAlwaysFinite α]
  [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_5 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r → γ → m (ForInStep γ)},
  forIn' r init f = forIn' r.toArray init fun a x acc => f a ⋯ acc
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_eq_true_iff_exists_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.containsKey a l = true ↔ ∃ p ∈ l, (p.fst == a) = true
-- Mathlib.Algebra.Category.ModuleCat.Algebra
ModuleCat.linearOverField : {k : Type u} →
  [inst : Field k] → {A : Type w} → [inst_1 : Ring A] → [Algebra k A] → CategoryTheory.Linear k (ModuleCat A)
-- Mathlib.Topology.Order.DenselyOrdered
interior_Ici : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMinOrder α] {a : α}, interior (Set.Ici a) = Set.Ioi a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp]
  {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} {fallback : β k'},
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → (Std.DTreeMap.ofList l cmp).getD k' fallback = cast ⋯ v
-- Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
Subgroup.Commensurable.discreteTopology_iff : ∀ {G : Type u_2} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [T2Space G] {H K : Subgroup G},
  H.Commensurable K → (DiscreteTopology ↥H ↔ DiscreteTopology ↥K)
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f_aux : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G}
  [inst_2 : ∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))]
  (A : adj.toComonad.Coalgebra),
  ((CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction adj).counit.app A).f =
    (adj.homEquiv (CategoryTheory.Limits.equalizer (G.map A.a) (adj.unit.app (G.obj A.A))) A.A).symm
      (CategoryTheory.Limits.equalizer.ι (G.map A.a) (adj.unit.app (G.obj A.A)))
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.RightHomologyData.homologyIso_inv_comp_homologyι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] (h : S.RightHomologyData),
  CategoryTheory.CategoryStruct.comp h.homologyIso.inv S.homologyι =
    CategoryTheory.CategoryStruct.comp h.ι h.opcyclesIso.inv
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.prod_bot_sup_bot_prod : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] (s : Submonoid M) (t : Submonoid N),
  s.prod ⊥ ⊔ ⊥.prod t = s.prod t
-- Std.Time.Duration
_private.Std.Time.Duration.0.Std.Time.Duration.ofNanoseconds.mod_nonpos : ∀ {a : ℤ} (b : ℤ), a ≤ 0 → b ≥ 0 → 0 ≥ a.tmod b
-- Mathlib.RingTheory.Ideal.Height
Ideal.height_add_one_le_of_lt_of_isPrime : ∀ {R : Type u_1} [inst : CommRing R] {I J : Ideal R} [I.IsPrime] [J.IsPrime], I < J → I.height + 1 ≤ J.height
-- Mathlib.Data.FP.Basic
FP.RMode.NE : FP.RMode
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.TypeDefinitionParams.mk : Lean.Lsp.TextDocumentPositionParams → Lean.Lsp.TypeDefinitionParams
-- Mathlib.Topology.UniformSpace.Cauchy
SequentiallyComplete.setSeq_mono : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α} (hf : Cauchy f) {U : ℕ → SetRel α α}
  (U_mem : ∀ (n : ℕ), U n ∈ uniformity α) ⦃m n : ℕ⦄,
  m ≤ n → SequentiallyComplete.setSeq hf U_mem n ⊆ SequentiallyComplete.setSeq hf U_mem m
-- Mathlib.Data.Set.Prod
Set.inter_prod : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β}, (s₁ ∩ s₂) ×ˢ t = s₁ ×ˢ t ∩ s₂ ×ˢ t
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.liftOpcycles_fromOpcycles : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) {A : C} {n : ℤ}
  (x : A ⟶ (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg))
  (hx : CategoryTheory.CategoryStruct.comp x ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) = 0),
  CategoryTheory.CategoryStruct.comp (X.liftOpcycles f g fg h x hx) (X.fromOpcycles f g fg h n) = x
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
instMeasurableSingletonClassOfMeasurableEq : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableEq α], MeasurableSingletonClass α
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.lawfulFunctor : ∀ {R : Type u_3} [inst : CommSemiring R], LawfulFunctor fun σ => MvPolynomial σ R
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.set.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → ℕ → α → Sort u_2) (x : ℕ) (x_1 : α)
  (h_1 : (head : α) → (as : List α) → (b : α) → motive (head :: as) 0 b)
  (h_2 : (a : α) → (as : List α) → (n : ℕ) → (b : α) → motive (a :: as) n.succ b)
  (h_3 : (x : ℕ) → (x_2 : α) → motive [] x x_2),
  (match [], x, x_1 with
    | head :: as, 0, b => h_1 head as b
    | a :: as, n.succ, b => h_2 a as n b
    | [], x, x_2 => h_3 x x_2) =
    h_3 x x_1
-- Mathlib.Logic.Function.Basic
Function.symm_apply_eq_iff : ∀ {α : Sort u_1} {f : α → α}, (Std.Symm fun x1 x2 => f x1 = x2) ↔ Function.Involutive f
-- Mathlib.NumberTheory.LSeries.Convolution
/-- We give an expression of the `LSeries.term` of the convolution of two functions
in terms of an a priori infinite sum over all pairs `(k, m)` with `k * m = n`
(the set we sum over is infinite when `n = 0`). This is the version needed for the
proof that `L (f ⍟ g) = L f * L g`.  -/
LSeries.term_convolution' : ∀ (f g : ℕ → ℂ) (s : ℂ),
  LSeries.term (LSeries.convolution f g) s = fun n =>
    ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {n})), LSeries.term f s (↑b).1 * LSeries.term g s (↑b).2
-- Std.Time.Format.Modifier
Std.Time.OffsetO.short.sizeOf_spec : sizeOf Std.Time.OffsetO.short = 1
-- Init.Data.UInt.Lemmas
UInt32.toNat_toUInt16 : ∀ (x : UInt32), x.toUInt16.toNat = x.toNat % 2 ^ 16
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- **Alias** of `FunLike.coe_smul`. -/
ContDiffMapSupportedIn.coe_smul : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- The morphism of presheaves of modules `M₁ ⟶ M₂` given by a morphism
of abelian presheaves `M₁.presheaf ⟶ M₂.presheaf`
which satisfy a suitable linearity condition.  -/
PresheafOfModules.homMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {M₁ M₂ : PresheafOfModules R} →
        (φ : M₁.presheaf ⟶ M₂.presheaf) →
          (∀ (X : Cᵒᵖ) (r : ↑(R.obj X)) (m : ↑(M₁.obj X)),
              (CategoryTheory.ConcreteCategory.hom (φ.app X)) (r • m) =
                r • (CategoryTheory.ConcreteCategory.hom (φ.app X)) m) →
            (M₁ ⟶ M₂)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.get.congr_simp : ∀ {α : Type u} {β : Type v} [inst : BEq α] (a a_1 : α) (e_a : a = a_1)
  (l l_1 : Std.DHashMap.Internal.AssocList α fun x => β) (e_l : l = l_1)
  (a_2 : Std.DHashMap.Internal.AssocList.contains a l = true),
  Std.DHashMap.Internal.AssocList.get a l a_2 = Std.DHashMap.Internal.AssocList.get a_1 l_1 ⋯
-- Mathlib.Algebra.Order.Monoid.Associated
Associates.instCanonicallyOrderedMul : ∀ {M : Type u_1} [inst : CommMonoidWithZero M], CanonicallyOrderedMul (Associates M)
-- Mathlib.Analysis.Normed.Group.Basic
/-- **Alias** of `mem_eball_zero_iff`. -/
mem_emetric_ball_zero_iff : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a : E} {r : ENNReal}, a ∈ Metric.eball 0 r ↔ ‖a‖ₑ < r
-- Mathlib.Topology.Algebra.WithZeroTopology
WithZeroTopology.isOpen_Iio : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {a : Γ₀}, IsOpen (Set.Iio a)
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_Ici : ∀ {a : ℝ}, MeasureTheory.volume (Set.Ici a) = ⊤
-- Mathlib.Logic.Nontrivial.Basic
/-- As a convenience, provide an instance automatically if `(f default)` is nontrivial.

If a different index has the non-trivial type, then use `haveI := nontrivial_at that_index`.
 -/
Pi.nontrivial : ∀ {I : Type u_3} {f : I → Type u_4} [inst : Inhabited I] [∀ (i : I), Nonempty (f i)] [Nontrivial (f default)],
  Nontrivial ((i : I) → f i)
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegalCore.spineToSimplex_spine : ∀ {X : SSet} (h : (n : ℕ) → X.StrictSegalCore n) {n : ℕ} (s : X.obj (Opposite.op { len := n })),
  SSet.StrictSegalCore.spineToSimplex h (X.spine n s) = s
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.card_roots_le_map_of_injective : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : IsDomain A] [inst_3 : IsDomain B]
  {p : Polynomial A} {f : A →+* B}, Function.Injective ⇑f → p.roots.card ≤ (Polynomial.map f p).roots.card
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instZero : {m : Type u_1} → {n : Type u_2} → {A : Type u_5} → [Zero A] → Zero (CStarMatrix m n A)
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- If `F G : Presheaf C X` are isomorphic presheaves,
then the `fork F U`, the canonical cone of the sheaf condition diagram for `F`,
is isomorphic to `fork F G` postcomposed with the corresponding isomorphism between
sheaf condition diagrams.
 -/
TopCat.Presheaf.SheafConditionEqualizerProducts.fork.isoOfIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} →
        {F : TopCat.Presheaf C X} →
          {ι : Type v'} →
            (U : ι → TopologicalSpace.Opens ↑X) →
              {G : TopCat.Presheaf C X} →
                (α : F ≅ G) →
                  TopCat.Presheaf.SheafConditionEqualizerProducts.fork F U ≅
                    (CategoryTheory.Limits.Cone.postcompose
                          (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram.isoOfIso U α).inv).obj
                      (TopCat.Presheaf.SheafConditionEqualizerProducts.fork G U)
-- Std.Data.DTreeMap.Basic
/-- Returns the `n`-th smallest key, or panics if `n` is at least `t.size`.  -/
Std.DTreeMap.keyAtIdx! : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.DTreeMap α β cmp → ℕ → α
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_eq_Ico_same_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Icc b a = Set.Ico b a ↔ ¬b ≤ a
-- Mathlib.Order.Basic
Pi.instHImp.eq_1 : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → HImp (π i)], Pi.instHImp = { himp := fun y x i => y i ⇨ x i }
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.extend_comp_eq' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  (f₁ : MeasureTheory.SimpleFunc α γ) {g : α → β} (hg : MeasurableEmbedding g) (f₂ : MeasureTheory.SimpleFunc β γ),
  ⇑(f₁.extend g hg f₂) ∘ g = ⇑f₁
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Pi.hasSum : ∀ {α : Type u_1} {ι : Type u_4} {X : α → Type u_5} [inst : (x : α) → AddCommMonoid (X x)]
  [inst_1 : (x : α) → TopologicalSpace (X x)] {L : SummationFilter ι} {f : ι → (x : α) → X x} {g : (x : α) → X x},
  HasSum f g L ↔ ∀ (x : α), HasSum (fun i => f i x) (g x) L
-- Mathlib.SetTheory.Ordinal.Veblen
/-- For any given `x`, there exists a unique pair `(o, a)` such that `ω ^ x = veblen o a` and
`a < ω ^ x`. `invVeblen₁ x` and `invVeblen₂ x` return the first and second entries of this pair,
respectively. See `veblen_eq_opow_iff` for a proof.

Composing this function with `Ordinal.CNF` yields a predicative ordinal notation up to `Γ₀`.  -/
Ordinal.invVeblen₁ : Ordinal.{u_1} → Ordinal.{u_1}
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.Cell.preimage_map : ∀ {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : SSet.relativeCellComplexOfMono.Cell i d),
  ((SSet.skeletonOfMono i) d).preimage c.map = SSet.boundary d
-- Mathlib.Data.Nat.Choose.Bounds
Nat.choose_le_pow_div : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (r n : ℕ),
  ↑(n.choose r) ≤ ↑n ^ r / ↑r.factorial
-- Mathlib.Topology.IsLocalHomeomorph
IsLocalHomeomorphOn.continuousAt : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set X},
  IsLocalHomeomorphOn f s → ∀ {x : X}, x ∈ s → ContinuousAt f x
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.instMonoid : {R : Type u_1} → [inst : Semiring R] → Monoid (ArithmeticFunction R)
-- Mathlib.Tactic.Bound.Attribute
/-- Attribute for `forward` rules for the `bound` tactic.

`@[bound_forward]` lemmas should produce inequalities given other hypotheses that might be in the
context. A typical example is exposing an inequality field of a structure, such as
`HasPowerSeriesOnBall.r_pos`.  -/
Mathlib.Tactic.Bound.attrBound_forward : Lean.ParserDescr
-- Std.Data.HashSet.Lemmas
Std.HashSet.inter_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α}, m₁.inter m₂ = m₁ ∩ m₂
-- Mathlib.Data.Fin.Tuple.Reflection
/-- This can be used to prove
```lean
example {f : α → β} (a₁ a₂ : α) : f ∘ ![a₁, a₂] = ![f a₁, f a₂] :=
  (map_eq _ _).symm
```
 -/
FinVec.map_eq : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {m : ℕ} (v : Fin m → α), FinVec.map f v = f ∘ v
-- Mathlib.Order.Basic
lt_iff_lt_of_le_iff_le' : ∀ {α : Type u_2} {β : Type u_5} [inst : Preorder α] [inst_1 : Preorder β] {a b : α} {c d : β},
  (a ≤ b ↔ c ≤ d) → (b ≤ a ↔ d ≤ c) → (b < a ↔ d < c)
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.Iter.step_take.match_3.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((k : ℕ) → motive k.succ) → motive n
-- Mathlib.NumberTheory.FLT.Basic
fermatLastTheoremWith'_nat_int_tfae : ∀ (n : ℕ), [FermatLastTheoremFor n, FermatLastTheoremWith' ℕ n, FermatLastTheoremWith' ℤ n].TFAE
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts
CategoryTheory.Limits.HasFiniteCoproducts.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ (n : ℕ), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (Fin n)) C) →
    CategoryTheory.Limits.HasFiniteCoproducts C
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.reflective : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → [CategoryTheory.Limits.HasImages C] → CategoryTheory.Reflective (CategoryTheory.MonoOver.forget X)
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.one_def : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [inst_2 : One β], 1 = MeasureTheory.AEEqFun.mk (fun x => 1) ⋯
-- Mathlib.Algebra.Category.Grp.Adjunctions
AddCommGrpCat.instIsRightAdjointForgetAddMonoidHomCarrier : (CategoryTheory.forget AddCommGrpCat).IsRightAdjoint
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.lift_surjective_of_surjective : ∀ {G : Type u_1} {M : Type u_4} [inst : Group G] [inst_1 : Monoid M] (N : Subgroup G) [nN : N.Normal] (φ : G →* M),
  Function.Surjective ⇑φ → ∀ (HN : N ≤ φ.ker), Function.Surjective ⇑(QuotientGroup.lift N φ HN)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.instDistribMulAction : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module A M] →
                [inst_5 : Module R M] →
                  {S : Type u_5} →
                    [inst_6 : Monoid S] →
                      [inst_7 : DistribMulAction S M] →
                        [SMulCommClass R S M] → [SMulCommClass S A M] → DistribMulAction S (Derivation R A M)
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addRightCancelMonoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → AddRightCancelMonoid (f i)] → AddRightCancelMonoid ((i : I) → f i)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.vanishingIdeal_mem_minimalPrimes : ∀ {R : Type u} [inst : CommSemiring R] {s : Set (PrimeSpectrum R)},
  PrimeSpectrum.vanishingIdeal s ∈ minimalPrimes R ↔ closure s ∈ irreducibleComponents (PrimeSpectrum R)
-- Mathlib.FieldTheory.Separable
Algebra.IsSeparable.mk : ∀ {F : Type u_1} {K : Type u_3} [inst : CommRing F] [inst_1 : Ring K] [inst_2 : Algebra F K],
  (∀ (x : K), IsSeparable F x) → Algebra.IsSeparable F K
-- Mathlib.Dynamics.Ergodic.Action.Basic
ErgodicSMul.mk : ∀ {G : Type u_1} {α : Type u_2} [inst : SMul G α] {x : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [toSMulInvariantMeasure : MeasureTheory.SMulInvariantMeasure G α μ],
  (∀ {s : Set α},
      MeasurableSet s → (∀ (g : G), (fun x => g • x) ⁻¹' s =ᵐ[μ] s) → Filter.EventuallyConst s (MeasureTheory.ae μ)) →
    ErgodicSMul G α μ
-- Mathlib.LinearAlgebra.TensorPower.Symmetric
SymmetricPower.Rel.perm : ∀ {R ι : Type u} [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (e : Equiv.Perm ι) (f : ι → M),
  SymmetricPower.Rel R ι M ((PiTensorProduct.tprod R) fun i => f i) ((PiTensorProduct.tprod R) fun i => f (e i))
-- Mathlib.Topology.Algebra.Module.Basic
/-- A subspace is dense iff its topological closure is the entire space.  -/
Submodule.dense_iff_topologicalClosure_eq_top : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : ContinuousConstSMul R M] [inst_5 : ContinuousAdd M] {s : Submodule R M},
  Dense ↑s ↔ s.topologicalClosure = ⊤
-- Mathlib.Order.WellFoundedSet
Set.partiallyWellOrderedOn_union : ∀ {α : Type u_2} {r : α → α → Prop} {s t : Set α},
  (s ∪ t).PartiallyWellOrderedOn r ↔ s.PartiallyWellOrderedOn r ∧ t.PartiallyWellOrderedOn r
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
/-- If `0` is the least element in `α`, then `WithZero α` is an ordered `AddMonoid`.  -/
WithZero.isOrderedAddMonoid : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α],
  (∀ (a : α), 0 ≤ a) → IsOrderedAddMonoid (WithZero α)
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- The `p`-adic norm of `q` is `1` if `q` is prime and not equal to `p`.  -/
padicNorm.padicNorm_of_prime_of_ne : ∀ {p q : ℕ} [p_prime : Fact (Nat.Prime p)] [q_prime : Fact (Nat.Prime q)], p ≠ q → padicNorm p ↑q = 1
-- Mathlib.RingTheory.DedekindDomain.Different
Submodule.traceDual_top' : ∀ {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],
  Submodule.traceDual A K ⊤ = if Submodule.restrictScalars A (Algebra.trace K L).range ≤ 1 then ⊤ else ⊥
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsLoop.dep_of_mem : ∀ {α : Type u_1} {M : Matroid α} {e : α} {X : Set α},
  M.IsLoop e → e ∈ X → autoParam (X ⊆ M.E) Matroid.IsLoop.dep_of_mem._auto_1 → M.Dep X
-- Init.Data.FloatArray.Basic
_private.Init.Data.FloatArray.Basic.0.List.toFloatArray.loop : List Float → FloatArray → FloatArray
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.le_of_opNorm_le : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂) {c : ℝ}, ‖f‖ ≤ c → ∀ (x : V₁), ‖f x‖ ≤ c * ‖x‖
-- Mathlib.Analysis.Normed.Module.DoubleDual
/-- If one controls the norm of every `f x`, then one controls the norm of `x`.
Compare `ContinuousLinearMap.opNorm_le_bound`.  -/
NormedSpace.norm_le_dual_bound : ∀ (𝕜 : Type v) [inst : RCLike 𝕜] {E : Type u} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] (x : E)
  {M : ℝ}, 0 ≤ M → (∀ (f : StrongDual 𝕜 E), ‖f x‖ ≤ M * ‖f‖) → ‖x‖ ≤ M
-- Init.Data.SInt.Lemmas
ISize.minValue.eq_1 : ISize.minValue = ISize.ofInt (-2 ^ (System.Platform.numBits - 1))
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.toListRev.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} [inst : Monad m] {β : Type w} [inst_1 : Std.Iterator α m β] (it : Std.IterM m β),
  it.toListRev = Std.IterM.toListRev.go it []
-- Mathlib.Combinatorics.Additive.ETransform
Finset.addETransformLeft.card : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddGroup α] (e : α) (x : Finset α × Finset α),
  (Finset.addETransformLeft e x).1.card + (Finset.addETransformRight e x).1.card = 2 * x.1.card
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- The category of topological representations of a monoid `G` over a topological ring `k`, and
their morphisms.  -/
TopRep : (k : Type u) → (G : Type v) → [Ring k] → [TopologicalSpace k] → [Monoid G] → Type (max (max u v) (w + 1))
-- Mathlib.Analysis.Normed.Group.Defs
/-- The distance function is induced by the norm.  -/
SeminormedGroup.dist_eq : ∀ {E : Type u_8} [self : SeminormedGroup E] (x y : E), dist x y = ‖x⁻¹ * y‖
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Finset.multipliable_compl_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup α] [inst_1 : TopologicalSpace α] [IsTopologicalGroup α] {f : β → α}
  (s : Finset β), (Multipliable fun x => f ↑x) ↔ Multipliable f