mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_erase_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, (t.erase k).getKey! k = default
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.disjoint : ∀ {ι : Type u_1} {n : ℕ} [inst : NeZero n] {ν ν' : ι → ℤ},
  ν ≠ ν' ↔ Disjoint ↑(BoxIntegral.unitPartition.box n ν) ↑(BoxIntegral.unitPartition.box n ν')
-- Mathlib.Order.Category.FinBddDistLat
/-- `OrderDual` as a functor.  -/
FinBddDistLat.dual : CategoryTheory.Functor FinBddDistLat FinBddDistLat
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `get?` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.Const.get?ₘ : {α : Type u} → {β : Type v} → [Ord α] → (Std.DTreeMap.Internal.Impl α fun x => β) → α → Option β
-- Init.GrindInstances.Ring.SInt
Lean.Grind.ISize.intCast_neg : ∀ (i : ℤ), ↑(-i) = -↑i
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.mk₀_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} [inst_3 : HasDerivedCategory C] (f : X ⟶ Y),
  (CategoryTheory.Abelian.Ext.mk₀ f).hom =
    CategoryTheory.ShiftedHom.mk₀ (↑0) CategoryTheory.Abelian.Ext.mk₀._proof_1
      ((DerivedCategory.singleFunctor C 0).map f)
-- Mathlib.AlgebraicGeometry.Morphisms.LocalFlatDescent
AlgebraicGeometry.instDescendsAlongSchemeSmoothMinMorphismPropertySurjectiveFlatQuasiCompact : CategoryTheory.MorphismProperty.DescendsAlong (@AlgebraicGeometry.Smooth)
  (@AlgebraicGeometry.Surjective ⊓ @AlgebraicGeometry.Flat ⊓ @AlgebraicGeometry.QuasiCompact)
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- The `p`-adic norm respects the triangle inequality: the norm of `p + q` is at most the norm of
`p` plus the norm of `q`.  -/
padicNorm.triangle_ineq : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (q r : ℚ), padicNorm p (q + r) ≤ padicNorm p q + padicNorm p r
-- Mathlib.RingTheory.Flat.Basic
/-- A direct sum of flat `R`-modules is flat.  -/
Module.Flat.directSum : ∀ {R : Type u} [inst : CommSemiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [∀ (i : ι), Module.Flat R (M i)], Module.Flat R (DirectSum ι fun i => M i)
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.isUnit_iff_degree_eq_zero : ∀ {R : Type u} [inst : Field R] {p : Polynomial R}, IsUnit p ↔ p.degree = 0
-- Mathlib.Topology.Algebra.TopologicallyNilpotent
topologicalNilradical.eq_1 : ∀ (R : Type u_1) [inst : TopologicalSpace R] [inst_1 : CommRing R] [inst_2 : IsLinearTopology R R],
  topologicalNilradical R =
    { carrier := {a | IsTopologicallyNilpotent a}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- An expression for the inverse of an upper block-triangular matrix, when either both elements of
diagonal are invertible, or both are not.  -/
Matrix.inv_fromBlocks_zero₂₁_of_isUnit_iff : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] (A : Matrix m m α) (B : Matrix m n α) (D : Matrix n n α),
  (IsUnit A ↔ IsUnit D) → (Matrix.fromBlocks A B 0 D)⁻¹ = Matrix.fromBlocks A⁻¹ (-(A⁻¹ * B * D⁻¹)) 0 D⁻¹
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- **Alias** of the reverse direction of `SimpleGraph.isContained_iff_exists_iso_subgraph`.

---

`B` contains `A` if and only if `B` has a subgraph `B'` and `B'` is isomorphic to `A`.  -/
SimpleGraph.IsContained.of_exists_iso_subgraph : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β},
  (∃ B', Nonempty (A ≃g B'.coe)) → A.IsContained B
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasSumLocallyUniformlyOn.hasSum : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α} {x : β} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  HasSumLocallyUniformlyOn f g s → x ∈ s → HasSum (fun x_1 => f x_1 x) (g x)
-- Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent
MeasureTheory.projectiveFamilyContent_ne_top : ∀ {ι : Type u_1} {α : ι → Type u_2} {mα : (i : ι) → MeasurableSpace (α i)}
  {P : (J : Finset ι) → MeasureTheory.Measure ((j : ↥J) → α ↑j)} {s : Set ((i : ι) → α i)}
  [∀ (J : Finset ι), MeasureTheory.IsFiniteMeasure (P J)] (hP : MeasureTheory.IsProjectiveMeasureFamily P),
  (MeasureTheory.projectiveFamilyContent hP) s ≠ ⊤
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.subtype_comp_inclusion : ∀ {M : Type u_1} [inst : MulOneClass M] {S T : Submonoid M} (h : S ≤ T),
  T.subtype.comp (Submonoid.inclusion h) = S.subtype
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Decl.castPurity! : {pu1 : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.Decl pu1 → (pu2 : Lean.Compiler.LCNF.Purity) → Lean.Compiler.LCNF.Decl pu2
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_ushiftRight_eq_extractLsb : ∀ {w w' w'' : ℕ} {b : BitVec w}, BitVec.setWidth w'' (b >>> w') = BitVec.extractLsb' w' w'' b
-- Mathlib.LinearAlgebra.PiTensorProduct.Basis
Basis.piTensorProduct.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : ι → Type u_3} {κ : ι → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M i)] [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Finite ι]
  (b b_1 : (i : ι) → Module.Basis (κ i) R (M i)), b = b_1 → Basis.piTensorProduct b = Basis.piTensorProduct b_1
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.algebraMap_residueField_eq_zero : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} [inst_1 : I.IsPrime] {x : R},
  (algebraMap R I.ResidueField) x = 0 ↔ x ∈ I
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_inter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, (t₁ ∩ t₂).getKeyD k fallback = if k ∈ t₂ then t₁.getKeyD k fallback else fallback
-- Mathlib.Dynamics.Flow
Flow.map_add : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddZero τ]
  (ϕ : Flow τ α) (t₁ t₂ : τ) (x : α), ϕ.toFun (t₁ + t₂) x = ϕ.toFun t₁ (ϕ.toFun t₂ x)
-- Mathlib.Data.List.Shortlex
List.shortlex_cons_iff : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Irrefl r] {a : α} {s t : List α},
  List.Shortlex r (a :: s) (a :: t) ↔ List.Shortlex r s t
-- Mathlib.Logic.Relation
Relation.ReflTransGen.brecOn : ∀ {α : Type u_1} {r : α → α → Prop} {a : α} {motive : (a_1 : α) → Relation.ReflTransGen r a a_1 → Prop} {a_1 : α}
  (t : Relation.ReflTransGen r a a_1),
  (∀ (a_2 : α) (t : Relation.ReflTransGen r a a_2), Relation.ReflTransGen.below t → motive a_2 t) → motive a_1 t
-- Mathlib.Algebra.Group.End
/-- Group conjugation, `AddAut.addConj g h = g + h + -g`, as an additive homomorphism
mapping addition in `G` into addition in the additive automorphism group `AddAut G`.  -/
AddAut.addConj : {G : Type u_3} → [inst : AddGroup G] → G →+ AddAut G
-- Mathlib.CategoryTheory.Presentable.Adjunction
CategoryTheory.Adjunction.isCardinalLocallyPresentable : ∀ {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) (κ : Cardinal.{w})
  [inst_2 : Fact κ.IsRegular] [CategoryTheory.IsCardinalLocallyPresentable C κ] [G.IsCardinalAccessible κ] [G.Full]
  [G.Faithful], CategoryTheory.IsCardinalLocallyPresentable D κ
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.insert_not_isBase : ∀ {α : Type u_1} {M : Matroid α} {B : Set α} {e : α}, M.IsBase B → e ∉ B → ¬M.IsBase (insert e B)
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_apply_ite_of_false : ∀ {ι : Type u_1} {M : Type u_3} {γ : Type u_5} {s : Finset ι} [inst : CommMonoid M] {p : ι → Prop}
  [inst_1 : DecidablePred p] (f g : ι → γ) (k : γ → M),
  (∀ x ∈ s, ¬p x) → ∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (g x)
-- Mathlib.Algebra.Order.Group.Defs
lt_neg_self_iff : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {a : α}, a < -a ↔ a < 0
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.outerSkip_flatMap : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [inst_3 : Std.Iterator α₂ m γ] {f : β → Std.IterM m γ} {it₁ it₁' : Std.IterM m β},
  it₁.IsPlausibleStep (Std.IterStep.skip it₁') →
    (Std.IterM.flatMapAfter f it₁ none).IsPlausibleStep (Std.IterStep.skip (Std.IterM.flatMapAfter f it₁' none))
-- Mathlib.Data.Quot
Quotient.induction_on_pi : ∀ {ι : Type u_3} {α : ι → Sort u_4} {s : (i : ι) → Setoid (α i)} {p : ((i : ι) → Quotient (s i)) → Prop}
  (f : (i : ι) → Quotient (s i)), (∀ (a : (i : ι) → α i), p fun i => ⟦a i⟧) → p f
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- If a set `s : Set α` is in `fixedBy (Set α) g`, then all points of `s` will stay
in `s` after being moved by `g`.  -/
AddAction.set_mem_fixedBy_iff : ∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (s : Set α) (g : G),
  s ∈ AddAction.fixedBy (Set α) g ↔ ∀ (x : α), g +ᵥ x ∈ s ↔ x ∈ s
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgHom.mem_equalizer : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (φ ψ : A →ₐ[R] B) (x : A), x ∈ φ.equalizer ψ ↔ φ x = ψ x
-- Init.Data.SInt.Lemmas
Int8.ofBitVec_mul : ∀ (a b : BitVec 8), Int8.ofBitVec (a * b) = Int8.ofBitVec a * Int8.ofBitVec b
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Expand
/-- If `p` is a prime such that `¬ p ∣ n`, then
`expand R p (cyclotomic n R) = (cyclotomic (n * p) R) * (cyclotomic n R)`.  -/
Polynomial.cyclotomic_expand_eq_cyclotomic_mul : ∀ {p n : ℕ},
  Nat.Prime p →
    ¬p ∣ n →
      ∀ (R : Type u_1) [inst : CommRing R],
        (Polynomial.expand R p) (Polynomial.cyclotomic n R) =
          Polynomial.cyclotomic (n * p) R * Polynomial.cyclotomic n R
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose.eq_1 : ∀ (x : ℕ), x.choose 0 = 1
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
HomotopicalAlgebra.PathObject.IsVeryGood.cofibration_ι : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {A : C}
  {inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C} {P : HomotopicalAlgebra.PathObject A}
  {inst_2 : CategoryTheory.Limits.HasBinaryProduct A A} {inst_3 : HomotopicalAlgebra.CategoryWithFibrations C}
  {inst_4 : HomotopicalAlgebra.CategoryWithCofibrations C} [self : P.IsVeryGood], HomotopicalAlgebra.Cofibration P.ι
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
jacobiSym.eq_1 : ∀ (a : ℤ) (b : ℕ), jacobiSym a b = (List.pmap (fun p pp => legendreSym p a) b.primeFactorsList ⋯).prod
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwiseDisjoint_singleton : ∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] (i : ι) (f : ι → α),
  {i}.PairwiseDisjoint f
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtSource.top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}, ⊤.IsLocalAtSource K
-- Mathlib.Topology.UniformSpace.Basic
ball_entourageProd : ∀ {α : Type ua} {β : Type ub} (u : SetRel α α) (v : SetRel β β) (x : α × β),
  UniformSpace.ball x (entourageProd u v) = UniformSpace.ball x.1 u ×ˢ UniformSpace.ball x.2 v
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.ofHom_comp : ∀ {R : Type u} [inst : Semiring R] {M N O : Type v} [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : AddCommMonoid O] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R O] (f : M →ₗ[R] N)
  (g : N →ₗ[R] O),
  SemimoduleCat.ofHom (g ∘ₗ f) = CategoryTheory.CategoryStruct.comp (SemimoduleCat.ofHom f) (SemimoduleCat.ofHom g)
-- Mathlib.MeasureTheory.Function.ConvergenceInDistribution
MeasureTheory.tendstoInDistribution_unique : ∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {Ω'' : Type u_4} {Ω : ι → Type u_5}
  {m : (i : ι) → MeasurableSpace (Ω i)} {μ : (i : ι) → MeasureTheory.Measure (Ω i)}
  [inst : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {m' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'}
  [inst_1 : MeasureTheory.IsProbabilityMeasure μ'] {m'' : MeasurableSpace Ω''} {μ'' : MeasureTheory.Measure Ω''}
  [inst_2 : MeasureTheory.IsProbabilityMeasure μ''] {mE : MeasurableSpace E} {l : Filter ι}
  [inst_3 : TopologicalSpace E] [HasOuterApproxClosed E] [inst_5 : BorelSpace E] (X : (i : ι) → Ω i → E) {Z : Ω' → E}
  {W : Ω'' → E} [l.NeBot],
  MeasureTheory.TendstoInDistribution X l Z μ μ' →
    MeasureTheory.TendstoInDistribution X l W μ μ'' → MeasureTheory.Measure.map Z μ' = MeasureTheory.Measure.map W μ''
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.eval_curry : ∀ (c : Nat.Partrec.Code) (n x : ℕ), (c.curry n).eval x = c.eval (Nat.pair n x)
-- Mathlib.Algebra.Category.ModuleCat.Colimits
ModuleCat.hasColimitsOfShape : ∀ (R : Type w) [inst : Ring R] (J : Type u) [inst_1 : CategoryTheory.Category.{v, u} J]
  [CategoryTheory.Limits.HasColimitsOfShape J AddCommGrpCat], CategoryTheory.Limits.HasColimitsOfShape J (ModuleCat R)
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsRestriction.isBasis_iff : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α} {N : Matroid α},
  N.IsRestriction M → (N.IsBasis I X ↔ M.IsBasis I X ∧ X ⊆ N.E)
-- Init.Data.Nat.Div.Basic
Nat.modCore.go.eq_def : ∀ (y : ℕ) (hy : 0 < y) (fuel x : ℕ) (hfuel : x < fuel),
  Nat.modCore.go y hy fuel x hfuel =
    match fuel, hfuel with
    | fuel.succ, hfuel => if h : y ≤ x then Nat.modCore.go y hy fuel (x - y) ⋯ else x
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
OpenPartialHomeomorph.eventually_right_inverse : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : Y}, x ∈ e.target → ∀ᶠ (y : Y) in nhds x, ↑e (↑e.symm y) = y
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.reindexₐ.eq_1 : ∀ {m : Type u_1} {n : Type u_2} (R : Type u_7) (A : Type u_8) [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid A] [inst_4 : Mul A] [inst_5 : Module R A] [inst_6 : Star A] (e : m ≃ n),
  CStarMatrix.reindexₐ R A e =
    { toFun := (↑(CStarMatrix.reindexₗ R A e e)).toFun, invFun := (CStarMatrix.reindexₗ R A e e).invFun, left_inv := ⋯,
      right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, map_star' := ⋯, map_smul' := ⋯ }
-- Mathlib.Data.Finset.Empty
Finset.forall_mem_const : ∀ {α : Type u_1} {s : Finset α} [Nonempty ↥s] {p : Prop}, (∀ x ∈ s, p) ↔ p
-- Mathlib.CategoryTheory.Shift.Twist
/-- Given `t : TwistShiftData C A`, this is a type synonym for the category `C`,
which the same shift functors as `C` but where the `shiftFunctorAdd` isomorphisms
have been modified using `t`.  -/
CategoryTheory.TwistShiftData.Category : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type w} →
      [inst_1 : AddMonoid A] → [inst_2 : CategoryTheory.HasShift C A] → CategoryTheory.TwistShiftData C A → Type u
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.ι_D₁ : ∀ {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₁₂]
  (i₁₂ i₁₂' : I₁₂) (i₁ : I₁) (i₂ : I₂) (h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂),
  CategoryTheory.CategoryStruct.comp (K.ιTotal c₁₂ i₁ i₂ i₁₂ h) (K.D₁ c₁₂ i₁₂ i₁₂') = K.d₁ c₁₂ i₁ i₂ i₁₂'
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- `L` with the spectral norm is a `NormedAlgebra` over `K`.  -/
spectralNorm.normedAlgebra : (K : Type u) →
  [inst : NontriviallyNormedField K] →
    (L : Type v) →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          [inst_3 : Algebra.IsAlgebraic K L] →
            [hu : IsUltrametricDist K] → [inst_4 : CompleteSpace K] → NormedAlgebra K L
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.pairSet.eq_1 : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] [inst_1 : DecidableEq T] (J : Finset T) (a c : ENNReal),
  PairReduction.pairSet J a c = (Finset.range J.card).biUnion (PairReduction.pairSetSeq J a c)
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.associated_content_mul : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] (p q : Polynomial R),
  Associated (p * q).content (p.content * q.content)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv.eq_1 : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDedekindDomain A] {I : Ideal R}
  {J : Ideal A} [inst_3 : IsDedekindDomain R] (f : R ⧸ I ≃+* A ⧸ J) (hI : I ≠ ⊥) (hJ : J ≠ ⊥),
  IsDedekindDomain.normalizedFactorsEquivOfQuotEquiv f hI hJ =
    { toFun := fun j => ⟨↑((IsDedekindDomain.idealFactorsEquivOfQuotEquiv f) ⟨↑j, ⋯⟩), ⋯⟩,
      invFun := fun j => ⟨↑((IsDedekindDomain.idealFactorsEquivOfQuotEquiv f).symm ⟨↑j, ⋯⟩), ⋯⟩, left_inv := ⋯,
      right_inv := ⋯ }
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.prod_unitsSMul : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B}
  (u : ℤˣ) (w : HNNExtension.NormalWord d),
  HNNExtension.NormalWord.ReducedWord.prod φ (HNNExtension.NormalWord.unitsSMul φ u w).toReducedWord =
    HNNExtension.t ^ ↑u * HNNExtension.NormalWord.ReducedWord.prod φ w.toReducedWord
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.nhds_F : ∀ {α : Type u_1} [inst : TopologicalSpace α] (F : Ctop.Realizer α) (a : α) (s : (F.nhds a).σ),
  (F.nhds a).F.f s = F.F.f ↑s
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.homologyData₀_left_i : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C),
  (X.homologyData₀ R).left.i = CategoryTheory.CategoryStruct.id ((X.chainComplex R).X 0)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.trivial.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.AddMon.trivial C =
    { X := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, addMon := CategoryTheory.AddMonObj.instTensorAddUnit }
-- Mathlib.Topology.Algebra.FilterBasis
AddGroupFilterBasis.t2Space_iff : ∀ {G : Type u} [inst : AddGroup G] [t : TopologicalSpace G] (F : AddGroupFilterBasis G),
  F.topology = t → (T2Space G ↔ ⋂₀ F.sets = {0})
-- Init.Data.Fin.Lemmas
Fin.coe_cast : ∀ {n m : ℕ} (h : n = m) (i : Fin n), ↑(Fin.cast h i) = ↑i
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csInf_Ioc : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {a b : α} [DenselyOrdered α], b < a → sInf (Set.Ioc b a) = b
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.toArray_filter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {f : α → β → Bool},
  t.WF → (Std.TreeMap.Raw.filter f t).toArray = Array.filter (fun p => f p.1 p.2) t.toArray
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
Quiver.WeaklyConnectedComponent.eq : ∀ {V : Type u_1} [inst : Quiver V] (a b : V),
  Quiver.WeaklyConnectedComponent.mk a = Quiver.WeaklyConnectedComponent.mk b ↔ Nonempty (Quiver.Path a b)
-- Mathlib.Algebra.Homology.ExactSequence
/-- If `S : ComposableArrows C (n + 2)` is such that the first two arrows form
an exact sequence and that the tail `S.δ₀` is exact, then `S` is also exact.
See `ShortComplex.SnakeInput.snake_lemma` in `Algebra.Homology.ShortComplex.SnakeLemma`
for a use of this lemma.  -/
CategoryTheory.ComposableArrows.exact_of_δ₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 2)},
  (CategoryTheory.ComposableArrows.mk₂ (S.map' 0 1 CategoryTheory.ComposableArrows.isComplex₂_iff._proof_2 ⋯)
        (S.map' 1 2 CategoryTheory.ComposableArrows.isComplex₂_iff._proof_4 ⋯)).Exact →
    S.δ₀.Exact → S.Exact
-- Mathlib.CategoryTheory.Presentable.Finite
CategoryTheory.instPreservesFilteredColimitsOfSizeObjOppositeFunctorTypeCoyonedaOpOfIsFinitelyPresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [CategoryTheory.IsFinitelyPresentable X],
  CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v, v, u, v + 1}
    (CategoryTheory.coyoneda.obj (Opposite.op X))
-- Mathlib.Tactic.Widget.StringDiagram
/-- Display the string diagram for a given term.

Example usage:
```
/- String diagram for the equality theorem. -/
#string_diagram MonoidalCategory.whisker_exchange

/- String diagram for the morphism. -/
variable {C : Type u} [Category.{v} C] [MonoidalCategory C] {X Y : C} (f : 𝟙_ C ⟶ X ⊗ Y) in
#string_diagram f
```
 -/
Mathlib.Tactic.Widget.stringDiagram : Lean.ParserDescr
-- Mathlib.Data.Finset.Union
Finset.biUnion_insert : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : α → Finset β} [inst : DecidableEq β] [inst_1 : DecidableEq α]
  {a : α}, (insert a s).biUnion t = t a ∪ s.biUnion t
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.innerAnodyneExtensions_eq_retracts_transfiniteCompositionsOfShape : SSet.innerAnodyneExtensions =
  ((CategoryTheory.MorphismProperty.coproducts.{u, u, u + 1}
            SSet.innerHornInclusions).pushouts.transfiniteCompositionsOfShape
      ℕ).retracts
-- Mathlib.Analysis.RCLike.Basic
RCLike.mk : {K : semiOutParam (Type u_1)} →
  [toDenselyNormedField : DenselyNormedField K] →
    [toStarRing : StarRing K] →
      [toNormedAlgebra : NormedAlgebra ℝ K] →
        [toCompleteSpace : CompleteSpace K] →
          (re im : K →+ ℝ) →
            (I : K) →
              re I = 0 →
                I = 0 ∨ I * I = -1 →
                  (∀ (z : K), (algebraMap ℝ K) (re z) + (algebraMap ℝ K) (im z) * I = z) →
                    (∀ (r : ℝ), re ((algebraMap ℝ K) r) = r) →
                      (∀ (r : ℝ), im ((algebraMap ℝ K) r) = 0) →
                        (∀ (z w : K), re (z * w) = re z * re w - im z * im w) →
                          (∀ (z w : K), im (z * w) = re z * im w + im z * re w) →
                            (∀ (z : K), re ((starRingEnd K) z) = re z) →
                              (∀ (z : K), im ((starRingEnd K) z) = -im z) →
                                (starRingEnd K) I = -I →
                                  (∀ (z : K), ‖z‖ ^ 2 = re z * re z + im z * im z) →
                                    (∀ (z : K), im z * im I = im z) →
                                      [toPartialOrder : PartialOrder K] →
                                        (∀ {z w : K}, z ≤ w ↔ re z ≤ re w ∧ im z = im w) →
                                          [toDecidableEq : DecidableEq K] → RCLike K
-- Mathlib.FieldTheory.SeparableDegree
/-- If `E / F` is an algebraic extension, then the (finite) separable degree of `E / F`
is the number of `F`-algebra homomorphisms from `E` to the algebraic closure of `E`,
as a natural number. It is defined to be zero if there are infinitely many of them.
Note that if `E / F` is not algebraic, then this definition makes no mathematical sense.  -/
Field.finSepDegree : (F : Type u) → (E : Type v) → [inst : Field F] → [inst_1 : Field E] → [Algebra F E] → ℕ
-- Lean.MetavarContext
Lean.MetavarContext.getDecl : Lean.MetavarContext → Lean.MVarId → Lean.MetavarDecl
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.hom_inv_id_toNatTrans_assoc : ∀ {X Y : CategoryTheory.Cat} {F G : X ⟶ Y} (e : F ≅ G) {Z : CategoryTheory.Functor ↑X ↑Y} (h : F.toFunctor ⟶ Z),
  CategoryTheory.CategoryStruct.comp e.hom.toNatTrans (CategoryTheory.CategoryStruct.comp e.inv.toNatTrans h) = h
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.keys_map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} (m : Std.DHashMap.Internal.Raw₀ α β) {f : (a : α) → β a → γ a},
  (↑(Std.DHashMap.Internal.Raw₀.map f m)).keys.Perm (↑m).keys