mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Tauto
Mathlib.Tactic.Tauto.DistribNotState.mk.injEq : ∀ (fvars : List Lean.Expr) (currentGoal : Lean.MVarId) (fvars_1 : List Lean.Expr) (currentGoal_1 : Lean.MVarId),
  ({ fvars := fvars, currentGoal := currentGoal } = { fvars := fvars_1, currentGoal := currentGoal_1 }) =
    (fvars = fvars_1 ∧ currentGoal = currentGoal_1)
-- Mathlib.GroupTheory.Index
/-- Relative version of `Subgroup.index_eq_two_iff`.  -/
Subgroup.relIndex_eq_two_iff : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H.relIndex K = 2 ↔ ∃ a ∈ K, ∀ b ∈ K, Xor (b * a ∈ H) (b ∈ H)
-- Mathlib.Analysis.Normed.Affine.MazurUlam
IsometryEquiv.toRealLinearIsometryEquiv_apply : ∀ {E : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (f : E ≃ᵢ F) (x : E), f.toRealLinearIsometryEquiv x = f x - f 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∩ t₂).contains k = (t₁.contains k && t₂.contains k)
-- Mathlib.Algebra.WithConv
WithConv.toConv.sizeOf_spec : ∀ {A : Sort u_1} [inst : SizeOf A] (ofConv : A), sizeOf (WithConv.toConv ofConv) = 1 + sizeOf ofConv
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey!_insertManyIfNewUnit!_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [inst : BEq α] [Std.LawfulBEqOrd α]
  [Std.TransOrd α] [inst_3 : Inhabited α],
  t.WF →
    ∀ {l : List α} {k : α},
      k ∉ t → l.contains k = false → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l)).getKey! k = default
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.δ_natural : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X X')
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (F.map f) (F.map g)) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))
      (CategoryTheory.Functor.OplaxMonoidal.δ F Y Y')
-- Mathlib.Control.Traversable.Basic
ApplicativeTransformation.coe_mk : ∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
  (f : (α : Type u) → F α → G α) (pp : ∀ {α : Type u} (x : α), f α (pure x) = pure x)
  (ps : ∀ {α β : Type u} (x : F (α → β)) (y : F α), f β (x <*> y) = f (α → β) x <*> f α y),
  (fun {α} => { app := f, preserves_pure' := pp, preserves_seq' := ps }.app α) = f
-- Lean.Data.Lsp.Window
Lean.Lsp.instFromJsonMessageActionItem : Lean.FromJson Lean.Lsp.MessageActionItem
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.congrRight_unitIso_inv_app : ∀ {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] (e : C ≌ D) (X : CategoryTheory.Functor E C),
  e.congrRight.unitIso.inv.app X =
    CategoryTheory.CategoryStruct.comp (X.associator e.functor e.inverse).inv
      (CategoryTheory.CategoryStruct.comp (X.whiskerLeft e.unitIso.inv) X.rightUnitor.hom)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ideal_iSup : ∀ {X : AlgebraicGeometry.Scheme} {ι : Type u_1} {I : ι → X.IdealSheafData}, (iSup I).ideal = ⨆ i, (I i).ideal
-- Mathlib.Analysis.Calculus.ContDiff.RCLike
/-- If a function is `C^n` with `1 ≤ n` around a point, then the derivative of `f` at this point
is also a strict derivative.  -/
ContDiffAt.hasStrictFDerivAt : ∀ {n : WithTop ℕ∞} {𝕂 : Type u_1} [inst : RCLike 𝕂] {E' : Type u_2} [inst_1 : NormedAddCommGroup E']
  [inst_2 : NormedSpace 𝕂 E'] {F' : Type u_3} [inst_3 : NormedAddCommGroup F'] [inst_4 : NormedSpace 𝕂 F'] {f : E' → F'}
  {x : E'}, ContDiffAt 𝕂 n f x → n ≠ 0 → HasStrictFDerivAt f (fderiv 𝕂 f x) x
-- Mathlib.Algebra.Group.Submonoid.Basic
AddSubmonoid.iSup_eq_closure : ∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Sort u_4} (p : ι → AddSubmonoid M),
  ⨆ i, p i = AddSubmonoid.closure (⋃ i, ↑(p i))
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.forIn.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {m : Type w → Type w₂} [inst : Monad m] [inst_1 : LawfulMonad m]
  [inst_2 : Std.TransCmp cmp] (f f_1 : α → δ → m (ForInStep δ)),
  f = f_1 →
    ∀ (init init_1 : δ),
      init = init_1 →
        ∀ (t t_1 : Std.ExtTreeSet α cmp), t = t_1 → Std.ExtTreeSet.forIn f init t = Std.ExtTreeSet.forIn f_1 init_1 t_1
-- Mathlib.Order.Basic
/-- **Alias** of `le_of_le_of_eq''`. -/
LE.le.trans_eq' : ∀ {α : Type u_1} {a b c : α} [inst : LE α], b ≤ a → b = c → c ≤ a
-- Mathlib.Order.WellFounded
/-- **Alias** of `WellFounded.irrefl`. -/
WellFounded.isIrrefl : ∀ {α : Type u_1} {r : α → α → Prop}, WellFounded r → Std.Irrefl r
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.exists_le_of_prod_le' : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : LinearOrder M] {f g : ι → M} {s : Finset ι}
  [IsOrderedCancelMonoid M], s.Nonempty → ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i → ∃ i ∈ s, f i ≤ g i
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_diff_eq_size_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    (∀ (a : α), Std.DTreeMap.Internal.Impl.contains a m₁ = true → Std.DTreeMap.Internal.Impl.contains a m₂ = false) →
      (m₁.diff m₂ ⋯).size = m₁.size
-- Init.Data.Nat.Lcm
Nat.lcm_pos : ∀ {m n : ℕ}, 0 < m → 0 < n → 0 < m.lcm n
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiffAt_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5} [inst_3 : NormedCommRing 𝔸']
  [inst_4 : NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ι → E → 𝔸'},
  (∀ i ∈ t, ContDiffAt 𝕜 n (f i) x) → ContDiffAt 𝕜 n (fun y => ∏ i ∈ t, f i y) x
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- `ContinuousLinearMap.applyModule` is faithful.  -/
ContinuousLinearMap.applyFaithfulSMul : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : ContinuousAdd M₁], FaithfulSMul (M₁ →L[R₁] M₁) M₁
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_compl : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], x \ yᶜ = x ⊓ y
-- Mathlib.Combinatorics.Matroid.Basic
/-- Matroids obey the maximality axiom  -/
Matroid.existsMaximalSubsetProperty_indep : ∀ {α : Type u_1} (M : Matroid α), ∀ X ⊆ M.E, Matroid.ExistsMaximalSubsetProperty M.Indep X
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_le_of_ne_zero : ∀ {R : Type u} {n : ℕ} [inst : Semiring R] {p : Polynomial R}, p.coeff n ≠ 0 → p.natTrailingDegree ≤ n
-- Mathlib.Analysis.InnerProductSpace.LinearMap
innerSLFlip_apply_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), ((innerSLFlip 𝕜) x) y = inner 𝕜 y x
-- Std.Tactic.BVDecide.LRAT.Parser
Std.Tactic.BVDecide.LRAT.Parser.Text.skipNewline : Std.Internal.Parsec.ByteArray.Parser Unit
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.sinh_le_sinh : ∀ {x y : ℝ}, Real.sinh x ≤ Real.sinh y ↔ x ≤ y
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.interSmallerFn.match_3.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3) (kv' : (a : α) × β a)
  (h_1 : (kv' : (a : α) × β a) → motive (some kv')) (h_2 : Unit → motive none),
  (match some kv' with
    | some kv' => h_1 kv'
    | none => h_2 ()) =
    h_1 kv'
-- Mathlib.RepresentationTheory.Basic
Representation.self_norm_apply : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring k] [inst_1 : Group G] [inst_2 : Fintype G]
  [inst_3 : AddCommMonoid V] [inst_4 : Module k V] (ρ : Representation k G V) (g : G) (x : V),
  (ρ g) (ρ.norm x) = ρ.norm x
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {l : List α} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    k ∉ t → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertMany l).getD k' fallback = k
-- Mathlib.Computability.PartrecCode
Nat.unpaired.eq_1 : ∀ {α : Sort u_1} (f : ℕ → ℕ → α) (n : ℕ), Nat.unpaired f n = f (Nat.unpair n).1 (Nat.unpair n).2
-- Mathlib.GroupTheory.Transfer
AddSubgroup.leftTransversals.vadd_diff_vadd : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {A : Type u_2} [inst_1 : AddCommGroup A] (ϕ : ↥H →+ A)
  (S T : H.LeftTransversal) [inst_2 : H.FiniteIndex] (g : G),
  AddSubgroup.leftTransversals.diff ϕ (g +ᵥ S) (g +ᵥ T) = AddSubgroup.leftTransversals.diff ϕ S T
-- Init.Data.Rat.Lemmas
Rat.mul_lt_mul_of_pos_right : ∀ {a b c : ℚ}, a < b → 0 < c → a * c < b * c
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.module' : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] →
              [inst_4 : LieRingModule L M] →
                {N : LieSubmodule R L M} →
                  {S : Type u_1} →
                    [inst_5 : Semiring S] →
                      [inst_6 : SMul S R] → [inst_7 : Module S M] → [IsScalarTower S R M] → Module S (M ⧸ N)
-- Mathlib.Order.ConditionallyCompleteLattice.Group
ciSup_add_ciSup_le : ∀ {α : Type u_1} {ι : Sort u_2} {ι' : Sort u_3} [Nonempty ι] [Nonempty ι'] [inst : ConditionallyCompleteLattice α]
  [inst_1 : AddGroup α] [AddLeftMono α] [AddRightMono α] {a : α} {g : ι → α} {h : ι' → α},
  (∀ (i : ι) (j : ι'), g i + h j ≤ a) → iSup g + iSup h ≤ a
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
CategoryTheory.Bicategory.mateEquiv_apply : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d e f : B} {g : c ⟶ e} {h : d ⟶ f} {l₁ : c ⟶ d} {r₁ : d ⟶ c}
  {l₂ : e ⟶ f} {r₂ : f ⟶ e} (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁)
  (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂)
  (a : CategoryTheory.CategoryStruct.comp g l₂ ⟶ CategoryTheory.CategoryStruct.comp l₁ h),
  (CategoryTheory.Bicategory.mateEquiv adj₁ adj₂) a =
    adj₁.homEquiv₁
      (CategoryTheory.CategoryStruct.comp (adj₂.homEquiv₂ a) (CategoryTheory.Bicategory.associator l₁ h r₂).hom)
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.copy_eq : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃) (f' : M → M₃) (h : f' = ⇑f), f.copy f' h = f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.minKeyD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {fallback : α}, t₁.Equiv t₂ → t₁.minKeyD fallback = t₂.minKeyD fallback
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedObj.default : Mathlib.Tactic.BicategoryLike.Obj
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.foldlM_eq_foldlM_keysArray : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldlM (fun d a x => f d a) init t = Array.foldlM f init t.keysArray
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
Units.continuousOn_inv₀_spectrum : ∀ {R : Type u_3} {A : Type u_4} [inst : Semifield R] [inst_1 : Ring A] [inst_2 : TopologicalSpace R] [ContinuousInv₀ R]
  [inst_4 : Algebra R A] (a : Aˣ), ContinuousOn (fun x => x⁻¹) (spectrum R ↑a)
-- Mathlib.Data.Set.Finite.Monad
Set.Finite.seq : ∀ {α : Type u} {β : Type v} {f : Set (α → β)} {s : Set α}, f.Finite → s.Finite → (f.seq s).Finite
-- Init.Data.String.Length
Nat.repeat.eq_def : ∀ {α : Type u} (f : α → α) (x : ℕ) (x_1 : α),
  Nat.repeat f x x_1 =
    match x, x_1 with
    | 0, a => a
    | n.succ, a => f (Nat.repeat f n a)
-- Mathlib.ModelTheory.Syntax
/-- Maps a sentence's symbols along a language map.  -/
FirstOrder.Language.LHom.onSentence : {L : FirstOrder.Language} → {L' : FirstOrder.Language} → (L →ᴸ L') → L.Sentence → L'.Sentence
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolRing_zero : ∀ {α : Type u_1} [inst : BooleanAlgebra α], ofBoolRing 0 = ⊥
-- Mathlib.Combinatorics.Hindman
Hindman.FP.brecOn : ∀ {M : Type u_1} [inst : Semigroup M] {motive : (a : Stream' M) → (a_1 : M) → Hindman.FP a a_1 → Prop} {a : Stream' M}
  {a_1 : M} (t : Hindman.FP a a_1),
  (∀ (a : Stream' M) (a_2 : M) (t : Hindman.FP a a_2), Hindman.FP.below t → motive a a_2 t) → motive a a_1 t
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.coprodMonad.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X X_1 : C),
  X = X_1 →
    ∀ [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C],
      CategoryTheory.coprodMonad X = CategoryTheory.coprodMonad X_1
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.totalDesc.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  {c₁₂ : ComplexShape I₁₂} [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  {A : C} {i₁₂ : I₁₂} (f : (i₁ : I₁) → (i₂ : I₂) → c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂ → ((K.X i₁).X i₂ ⟶ A)),
  K.totalDesc f =
    K.toGradedObject.descMapObj (c₁.π c₂ c₁₂) fun x hi =>
      match x, hi with
      | (i₁, i₂), hi => f i₁ i₂ hi
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.instIsIsoCommaHom : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (f : X ⟶ Y)
  [CategoryTheory.IsIso f], CategoryTheory.IsIso (CategoryTheory.MorphismProperty.Comma.Hom.hom f)
-- Lean.Meta.Eqns
Lean.Meta.eqn1ThmSuffix : String
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of the reverse direction of `ValuativeRel.not_vle`. -/
ValuativeRel.vlt.not_vle : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R}, y <ᵥ x → ¬x ≤ᵥ y
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.neg_univ : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveNeg α] [inst_2 : Fintype α], -Finset.univ = Finset.univ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_eq_some_maxKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {he : t.isEmpty = false}, t.maxKey? = some (t.maxKey he)
-- Mathlib.Control.Basic
pure_id'_seq : ∀ {α : Type u} {F : Type u → Type v} [inst : Applicative F] [LawfulApplicative F] (x : F α), (pure fun x => x) <*> x = x
-- Mathlib.RingTheory.ZariskisMainTheorem
_private.Mathlib.RingTheory.ZariskisMainTheorem.0.Algebra.ZariskisMainProperty.of_algHom_mvPolynomial : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal S) [inst_3 : p.IsPrime]
  [Algebra.WeaklyQuasiFiniteAt R p] {n : ℕ} (f : MvPolynomial (Fin n) R →ₐ[R] S),
  f.Finite → Algebra.ZariskisMainProperty R p
-- Mathlib.Probability.Distributions.Uniform
/-- Uniform distribution taking the same non-zero probability on the nonempty finset `s`  -/
PMF.uniformOfFinset : {α : Type u_1} → (s : Finset α) → s.Nonempty → PMF α
-- Mathlib.Data.Complex.Basic
Complex.div_ratCast_im : ∀ (z : ℂ) (x : ℚ), (z / ↑x).im = z.im / ↑x
-- Mathlib.Algebra.Category.Grp.Preadditive
AddCommGrpCat.hom_add : ∀ {M N : AddCommGrpCat} (f g : M ⟶ N), AddCommGrpCat.Hom.hom (f + g) = AddCommGrpCat.Hom.hom f + AddCommGrpCat.Hom.hom g
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_eq_self_iff_disjoint : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, s \ t = s ↔ Disjoint s t
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
ContravariantClass.mk : ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop}, Contravariant M N μ r → ContravariantClass M N μ r
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.N.subcomplex_injective_iff : ∀ {X : SSet} {x y : X.N}, x.subcomplex = y.subcomplex ↔ x = y
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.Walk.IsHamiltonianCycle.isCycle : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {a : α} {p : G.Walk a a}, p.IsHamiltonianCycle → p.IsCycle
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
DirichletCharacter.completedLFunction.congr_simp : ∀ {N : ℕ} [inst : NeZero N] (χ χ_1 : DirichletCharacter ℂ N),
  χ = χ_1 →
    ∀ (s s_1 : ℂ), s = s_1 → DirichletCharacter.completedLFunction χ s = DirichletCharacter.completedLFunction χ_1 s_1
-- Init.Data.SInt.Basic
/-- Converts 8-bit signed integers to 16-bit signed integers that denote the same number.

This function is overridden at runtime with an efficient implementation.
 -/
Int8.toInt16 : Int8 → Int16
-- Mathlib.Order.Category.BddDistLat
BddDistLat.forget_map : ∀ {X Y : BddDistLat} (f : X ⟶ Y),
  ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget BddDistLat).map f)) =
    ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.row_eq_prod : ∀ {μ : YoungDiagram} {i : ℕ}, μ.row i = {i} ×ˢ Finset.range (μ.rowLen i)
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.smul_apply : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M] (a : L)
  {S : Type u_4} [inst_7 : Monoid S] [inst_8 : DistribMulAction S M] [inst_9 : SMulCommClass R S M]
  [inst_10 : LieDerivation.SMulBracketCommClass S L M] (r : S) (D : LieDerivation R L M), (r • D) a = r • D a
-- Mathlib.Order.CompactlyGenerated.Basic
/-- See [Theorem 6.6][calugareanu].  -/
complementedLattice_of_isAtomistic : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] [IsAtomistic α],
  ComplementedLattice α
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.opEquiv.match_3.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C]
  (motive : (x y : (CategoryTheory.WithInitial C)ᵒᵖ) → (Opposite.unop y ⟶ Opposite.unop x) → (x ⟶ y) → Sort u_3)
  (x y : C)
  (f :
    Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of y)) ⟶
      Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of x)))
  (x_1 : Opposite.op (CategoryTheory.WithInitial.of x) ⟶ Opposite.op (CategoryTheory.WithInitial.of y))
  (h_1 :
    (x y : C) →
      (f :
          Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of y)) ⟶
            Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of x))) →
        (x_2 : Opposite.op (CategoryTheory.WithInitial.of x) ⟶ Opposite.op (CategoryTheory.WithInitial.of y)) →
          motive (Opposite.op (CategoryTheory.WithInitial.of x)) (Opposite.op (CategoryTheory.WithInitial.of y)) f x_2)
  (h_2 :
    (a : C) →
      (x :
          Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
            Opposite.unop (Opposite.op (CategoryTheory.WithInitial.of a))) →
        (x_2 : Opposite.op (CategoryTheory.WithInitial.of a) ⟶ Opposite.op CategoryTheory.WithInitial.star) →
          motive (Opposite.op (CategoryTheory.WithInitial.of a)) (Opposite.op CategoryTheory.WithInitial.star) x x_2)
  (h_3 :
    (x :
        Opposite.unop (Opposite.op CategoryTheory.WithInitial.star) ⟶
          Opposite.unop (Opposite.op CategoryTheory.WithInitial.star)) →
      (x_2 : Opposite.op CategoryTheory.WithInitial.star ⟶ Opposite.op CategoryTheory.WithInitial.star) →
        motive (Opposite.op CategoryTheory.WithInitial.star) (Opposite.op CategoryTheory.WithInitial.star) x x_2),
  (match Opposite.op (CategoryTheory.WithInitial.of x), Opposite.op (CategoryTheory.WithInitial.of y), f, x_1 with
    | Opposite.op (CategoryTheory.WithInitial.of x), Opposite.op (CategoryTheory.WithInitial.of y), f, x_2 =>
      h_1 x y f x_2
    | Opposite.op (CategoryTheory.WithInitial.of a), Opposite.op CategoryTheory.WithInitial.star, x, x_2 => h_2 a x x_2
    | Opposite.op CategoryTheory.WithInitial.star, Opposite.op CategoryTheory.WithInitial.star, x, x_2 => h_3 x x_2) =
    h_1 x y f x_1
-- Mathlib.RingTheory.Perfection
/-- Given rings `R` and `S` of characteristic `p`, with `R` being perfect,
any homomorphism `R →+* S` can be lifted to a homomorphism `R →+* P`,
where `P` is any perfection of `S`.  -/
PerfectionMap.lift : (p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    (R : Type u₁) →
      [inst_1 : CommSemiring R] →
        [CharP R p] →
          [PerfectRing R p] →
            (S : Type u₂) →
              [inst_4 : CommSemiring S] →
                [inst_5 : CharP S p] →
                  (P : Type u₃) →
                    [inst_6 : CommSemiring P] →
                      [inst_7 : CharP P p] →
                        [inst_8 : PerfectRing P p] → (π : P →+* S) → PerfectionMap p π → (R →+* S) ≃ (R →+* P)
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
/-- The inclusion of `(F.obj (X i)).obj (Y j)` in `mapBifunctorMapObj F p X Y k`
when `i + j = k`.  -/
CategoryTheory.GradedObject.ιMapBifunctorMapObj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : 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} C₃] →
            (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) →
              {I : Type u_4} →
                {J : Type u_5} →
                  {K : Type u_6} →
                    (p : I × J → K) →
                      (X : CategoryTheory.GradedObject I C₁) →
                        (Y : CategoryTheory.GradedObject J C₂) →
                          [inst_3 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X).obj Y).HasMap p] →
                            (i : I) →
                              (j : J) →
                                (k : K) →
                                  p (i, j) = k →
                                    ((F.obj (X i)).obj (Y j) ⟶ CategoryTheory.GradedObject.mapBifunctorMapObj F p X Y k)
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- If an additive group `G` acts on `X` by isometries,
then `IsometryEquiv.constVAdd` is the isometry of `X` given by addition of a constant element of the
group.  -/
IsometryEquiv.constVAdd : {G : Type v} →
  {X : Type w} →
    [inst : PseudoEMetricSpace X] →
      [inst_1 : AddGroup G] → [inst_2 : AddAction G X] → [IsIsometricVAdd G X] → G → X ≃ᵢ X
-- Mathlib.Combinatorics.Enumerative.Composition
/-- Induction (recursion) principle on `c : Composition _`
that corresponds to the reverse induction on the list of blocks of `c`.  -/
Composition.recOnAppendSingle : {motive : (n : ℕ) → Composition n → Sort u_1} →
  {n : ℕ} →
    (c : Composition n) →
      motive 0 (Composition.ones 0) →
        ((k n : ℕ) →
            (c : Composition n) → motive n c → motive (n + (k + 1)) (c.append (Composition.single (k + 1) ⋯))) →
          motive n c
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.surjective : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
  Function.Surjective ⇑h