mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Tactics
/-- `contradiction` closes the main goal if its hypotheses are "trivially contradictory".

- Inductive type/family with no applicable constructors
  ```lean
  example (h : False) : p := by contradiction
  ```
- Injectivity of constructors
  ```lean
  example (h : none = some true) : p := by contradiction  --
  ```
- Decidable false proposition
  ```lean
  example (h : 2 + 2 = 3) : p := by contradiction
  ```
- Contradictory hypotheses
  ```lean
  example (h : p) (h' : ¬ p) : q := by contradiction
  ```
- Other simple contradictions such as
  ```lean
  example (x : Nat) (h : x ≠ x) : p := by contradiction
  ```
 -/
Lean.Parser.Tactic.contradiction : Lean.ParserDescr
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableLocallyUniformlyOn_congr : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {s : Set β} [inst_1 : UniformSpace α]
  [inst_2 : TopologicalSpace β] {f f' : ι → β → α},
  (∀ (i : ι), Set.EqOn (f i) (f' i) s) → MultipliableLocallyUniformlyOn f s → MultipliableLocallyUniformlyOn f' s
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.classifyNumberMax : ℕ → ℕ → Option Std.Time.Number
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.addValuationDef.eq_1 : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (x : ℚ_[p]), x.addValuationDef = if x = 0 then ⊤ else ↑x.valuation
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleOf_inv : ∀ {α : Type u_2} (f : Equiv.Perm α) [inst : DecidableRel f.SameCycle] (x : α), (f.cycleOf x)⁻¹ = f⁻¹.cycleOf x
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instStarMul : StarMul Complex.UnitClosedDisc
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.IsTriangulated.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C],
  (∀ {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
      (comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃) {v₁₂ : X₂ ⟶ Z₁₂}
      {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
      (h₁₂ :
        CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
      {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
      (h₂₃ :
        CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
      {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
      (h₁₃ :
        CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
      Nonempty (CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)) →
    CategoryTheory.IsTriangulated C
-- Init.Data.SInt.Lemmas
Int16.add_comm : ∀ (a b : Int16), a + b = b + a
-- Mathlib.LinearAlgebra.Eigenspace.Minpoly
Module.End.hasEigenvalue_iff_isRoot : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} [IsDomain R] [Module.Finite R M] [Module.IsTorsionFree R M], f.HasEigenvalue μ ↔ (minpoly R f).IsRoot μ
-- Mathlib.Analysis.Complex.AbsMax
/-- **Maximum modulus principle** on a connected set. Let `U` be a (pre)connected open set in a
complex normed space.  Let `f : E → F` be a function that is complex differentiable on `U` and is
continuous on its closure. Suppose that `‖f x‖` takes its maximum value on `U` at `c ∈ U`. Then
`‖f x‖ = ‖f c‖` for all `x ∈ closure U`.  -/
Complex.norm_eqOn_closure_of_isPreconnected_of_isMaxOn : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {f : E → F} {U : Set E} {c : E},
  IsPreconnected U →
    IsOpen U →
      DiffContOnCl ℂ f U → c ∈ U → IsMaxOn (norm ∘ f) U c → Set.EqOn (norm ∘ f) (Function.const E ‖f c‖) (closure U)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote : Int.Internal.Linear.Context → Int.Internal.Linear.Poly → ℤ
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- An `RCLike` field is a real inner product space.  -/
RCLike.toInnerProductSpaceReal : {𝕜 : Type u_1} → [inst : RCLike 𝕜] → InnerProductSpace ℝ 𝕜
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKeyD_le_maxKeyD_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {k : α} {v : β k} {fallback : α},
        (compare (Std.Internal.List.maxKeyD l fallback)
              (Std.Internal.List.maxKeyD (Std.Internal.List.insertEntryIfNew k v l) fallback)).isLE =
          true
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_read_MonadReader_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ρ : Type u}
  {post : ρ → Pred} {epost : EPred} [inst_4 : MonadReaderOf ρ m],
  Std.Internal.Do.wp read post epost = Std.Internal.Do.wp MonadReaderOf.read post epost
-- Mathlib.Topology.LocallyFinite
/-- A family of sets in `Set X` is locally finite if at every point `x : X`,
there is a neighborhood of `x` which meets only finitely many sets in the family.  -/
LocallyFinite : {ι : Type u_1} → {X : Type u_4} → [TopologicalSpace X] → (ι → Set X) → Prop
-- Init.Data.BitVec.Lemmas
BitVec.ushiftRight_self : ∀ {w : ℕ} (n : BitVec w), n >>> n.toNat = 0#w
-- Mathlib.Algebra.Module.FinitePresentation
/-- Let `M` `N` be a finitely presented `R`-modules.
Any `Mₛ ≃ₗ[R] Nₛ` between the localizations at `S : Submonoid R` can be lifted to an
isomorphism between `Mᵣ ≃ₗ[R] Nᵣ` for some `r ∈ S`.
 -/
Module.FinitePresentation.exists_lift_equiv_of_isLocalizedModule : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (S : Submonoid R) {M' : Type u_1} [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] (f : M →ₗ[R] M') [inst_7 : IsLocalizedModule S f] {N' : Type u_2} [inst_8 : AddCommGroup N']
  [inst_9 : Module R N'] (g : N →ₗ[R] N') [inst_10 : IsLocalizedModule S g] [Module.FinitePresentation R M]
  [Module.FinitePresentation R N] (l : M' ≃ₗ[R] N'),
  ∃ r,
    ∃ (hr : r ∈ S),
      ∃ l',
        LocalizedModule.lift (Submonoid.powers r) g ⋯ ∘ₗ ↑R ↑l' = ↑l ∘ₗ LocalizedModule.lift (Submonoid.powers r) f ⋯
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_updateBucket_alter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : Option (β a) → Option (β a)},
      Std.DHashMap.Internal.Raw.WFImp
        (Std.DHashMap.Internal.withComputedSize
          (Std.DHashMap.Internal.updateBucket (↑m).buckets ⋯ a (Std.DHashMap.Internal.AssocList.alter a f)))
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.instRefl : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M},
  Std.Refl (SModEq U)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_prodProdProdComm : ∀ (R : Type u_8) (M₁ : Type u_9) (M₂ : Type u_10) (M₃ : Type u_11) (M₄ : Type u_12) [inst : Semiring R]
  [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : AddCommMonoid M₄]
  [inst_5 : Module R M₁] [inst_6 : Module R M₂] [inst_7 : Module R M₃] [inst_8 : Module R M₄]
  [inst_9 : TopologicalSpace M₁] [inst_10 : TopologicalSpace M₂] [inst_11 : TopologicalSpace M₃]
  [inst_12 : TopologicalSpace M₄],
  ⇑(ContinuousLinearEquiv.prodProdProdComm R M₁ M₂ M₃ M₄) = ⇑(Equiv.prodProdProdComm M₁ M₂ M₃ M₄)
-- Mathlib.Analysis.Convex.Between
Wbtw.trans_right_ne : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V]
  {w x y z : P}, Wbtw R w x z → Wbtw R x y z → w ≠ x → w ≠ y
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.ext_from_X' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (i : ι),
  ¬c.Rel i (c.next i) →
    ∀ {A : C} {f g : HomologicalComplex.homotopyCofiber.X φ i ⟶ A},
      CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i) f =
          CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX φ i) g →
        f = g
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.instInhabitedNonUnitalSubalgebra : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring A] →
        [inst_2 : Module R A] → [IsScalarTower R A A] → [SMulCommClass R A A] → Inhabited (NonUnitalSubalgebra R A)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
pow_lt_pow_iff_right' : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulLeftStrictMono M] {a : M} {m n : ℕ},
  1 < a → (a ^ m < a ^ n ↔ m < n)
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- `val_v(1) = 0`.  -/
FractionalIdeal.count_one : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R),
  FractionalIdeal.count K v 1 = 0
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mul_mem_mul_rev : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R} {r s : R}, r ∈ I → s ∈ J → s * r ∈ I * J
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform.0.EisensteinSeries.G2Term_prod_summable : ∀ (z : UpperHalfPlane), Summable fun p => EisensteinSeries.G2Term✝ z ![p.1, p.2]
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.adjMatrix_hadamard_natCast : ∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq V]
  [inst_2 : MulZeroOneClass α] [inst_3 : NatCast α] (a : ℕ), (SimpleGraph.adjMatrix α G).hadamard ↑a = 0
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.adjoin_range_ι : ∀ (R : Type u_1) (X : Type u_2) [inst : CommSemiring R], Algebra.adjoin R (Set.range (FreeAlgebra.ι R)) = ⊤
-- Mathlib.Algebra.BigOperators.Finprod
/-- **Alias** of `finprod_mem_mul_sdiff`.

---

Given a finite set `t` and a subset `s` of `t`, the product of `f i` over `i ∈ s`
times the product of `f i` over `t \ s` equals the product of `f i` over `i ∈ t`.  -/
finprod_mem_mul_diff : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] {f : α → M} {s t : Set α},
  s ⊆ t → t.Finite → (∏ᶠ (i : α) (_ : i ∈ s), f i) * ∏ᶠ (i : α) (_ : i ∈ t \ s), f i = ∏ᶠ (i : α) (_ : i ∈ t), f i
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.restrict_coeSubgraph : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} (G'' : G'.coe.Subgraph),
  SimpleGraph.Subgraph.restrict (SimpleGraph.Subgraph.coeSubgraph G'') = G''
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- The natural inclusion induced by implications of morphism properties.  -/
CategoryTheory.MorphismProperty.Over.changeProp : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P Q : CategoryTheory.MorphismProperty T} →
      (X : T) →
        [inst_1 : Q.IsMultiplicative] →
          {P' Q' : CategoryTheory.MorphismProperty T} →
            [inst_2 : Q'.IsMultiplicative] → P ≤ P' → Q ≤ Q' → CategoryTheory.Functor (P.Over Q X) (P'.Over Q' X)
-- Mathlib.Analysis.SpecialFunctions.Pochhammer
deriv_descPochhammer_eval_eq_sum_prod_range_erase : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] (n : ℕ) (k : 𝕜),
  deriv (fun x => Polynomial.eval x (descPochhammer 𝕜 n)) k =
    ∑ i ∈ Finset.range n, ∏ j ∈ (Finset.range n).erase i, (k - ↑j)
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
AlgebraicGeometry.universallyInjective_eq_diagonal : @AlgebraicGeometry.UniversallyInjective = CategoryTheory.MorphismProperty.diagonal @AlgebraicGeometry.Surjective
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulETransformRight_one : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Group α] (x : Finset α × Finset α), Finset.mulETransformRight 1 x = x
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.mul_star_self : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (x : ↥(spinGroup Q)), x * star x = 1
-- Mathlib.CategoryTheory.Functor.Derived.Adjunction
CategoryTheory.Adjunction.derivedη.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [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} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj adj_1 : G ⊣ F),
  adj = adj_1 →
    ∀ {L₁ : CategoryTheory.Functor C₁ D₁} {L₂ : CategoryTheory.Functor C₂ D₂}
      (W₁ W₁_1 : CategoryTheory.MorphismProperty C₁) (e_W₁ : W₁ = W₁_1) [inst_4 : L₁.IsLocalization W₁]
      {G' : CategoryTheory.Functor D₁ D₂} {F' : CategoryTheory.Functor D₂ D₁} (α α_1 : L₁.comp G' ⟶ G.comp L₂)
      (e_α : α = α_1) (β β_1 : F.comp L₁ ⟶ L₂.comp F'),
      β = β_1 →
        ∀
          [inst_5 :
            (G'.comp F').IsLeftDerivedFunctor
              (CategoryTheory.CategoryStruct.comp (L₁.associator G' F').inv (CategoryTheory.Functor.whiskerRight α F'))
              W₁],
          adj.derivedη W₁ α β = adj_1.derivedη W₁_1 α_1 β_1
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.refl_trans : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (f : α ≃*o β), (OrderMonoidIso.refl α).trans f = f
-- Mathlib.Algebra.Category.Grp.LeftExactFunctor
/-- Implementation, see `leftExactFunctorForgetEquivalence`.  -/
AddCommGrpCat.leftExactFunctorForgetEquivalence.inverse : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasFiniteBiproducts C] → CategoryTheory.Functor (C ⥤ₗ Type v) (C ⥤ₗ AddCommGrpCat)
-- Init.Data.Float.Model.Float
/-- Return a `Float.Model` with positive sign.
 -/
Float.Model.abs : Float.Model → Float.Model
-- Mathlib.Analysis.SpecificLimits.Normed
hasSum_geometric_of_abs_lt_one : ∀ {r : ℝ}, |r| < 1 → HasSum (fun n => r ^ n) (1 - r)⁻¹
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformFun.instBoundedSpace : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : BoundedSpace β], BoundedSpace (UniformFun α β)
-- Mathlib.Order.Preorder.Chain
IsChain.insert : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α},
  IsChain r s → (∀ b ∈ s, a ≠ b → r a b ∨ r b a) → IsChain r (insert a s)
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.instNonemptySubtypeIsMarkovKernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [Nonempty β],
  Nonempty { κ // ProbabilityTheory.IsMarkovKernel κ }
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.ceil_intCast : ∀ {R : Type u_3} [inst : Ring R] [inst_1 : LinearOrder R] [IsOrderedRing R] [inst_3 : FloorSemiring R] (z : ℤ),
  ⌈↑z⌉₊ = z.toNat
-- Mathlib.Order.Filter.AtTopBot.Tendsto
/-- If `f` is a monotone function and `g` tends to `atBot` along a nontrivial filter.
then the lower bounds of the range of `f ∘ g`
are the same as the lower bounds of the range of `f`.  -/
Monotone.lowerBounds_range_comp_tendsto_atBot : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : Preorder γ] {l : Filter α} [l.NeBot]
  {f : β → γ},
  Monotone f →
    ∀ {g : α → β}, Filter.Tendsto g l Filter.atBot → lowerBounds (Set.range (f ∘ g)) = lowerBounds (Set.range f)
-- Mathlib.CategoryTheory.Limits.Types.Images
/-- Given surjections `⋯ ⟶ Xₙ₊₁ ⟶ Xₙ ⟶ ⋯ ⟶ X₀`, the projection map `lim Xₙ ⟶ X₀` is surjective.
 -/
CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map : ∀ {F : CategoryTheory.Functor ℕᵒᵖ (Type u)} {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c),
  (∀ (n : ℕ), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op))) →
    Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (c.π.app (Opposite.op 0)))
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_eq : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (g : R →+* S₁)
  (X : σ → S₁) (f : MvPolynomial σ R),
  MvPolynomial.eval₂ g X f = ∑ d ∈ f.support, g (MvPolynomial.coeff d f) * ∏ i ∈ d.support, X i ^ d i
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.OplaxRightLinear.δᵣ_naturality_left_assoc : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'} [self : F.OplaxRightLinear C] {d d' : D}
  (f : d ⟶ d') (c : C) {Z : D'}
  (h : CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj (F.obj d') c ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (F.map (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f c))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d' c) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (F.map f) c) h)
-- Mathlib.Algebra.Module.GradedModule
DirectSum.Gmodule.smulAddMonoidHom.eq_1 : ∀ {ιA : Type u_1} {ιB : Type u_2} (A : ιA → Type u_3) (M : ιB → Type u_4) [inst : AddMonoid ιA] [inst_1 : VAdd ιA ιB]
  [inst_2 : (i : ιA) → AddCommMonoid (A i)] [inst_3 : (i : ιB) → AddCommMonoid (M i)] [inst_4 : DecidableEq ιA]
  [inst_5 : DecidableEq ιB] [inst_6 : GradedMonoid.GMonoid A] [inst_7 : DirectSum.Gmodule A M],
  DirectSum.Gmodule.smulAddMonoidHom A M =
    DirectSum.toAddMonoid fun _i =>
      (DirectSum.toAddMonoid fun _j =>
          ((AddMonoidHom.compHom (DirectSum.of M (_i +ᵥ _j))).comp (DirectSum.gsmulHom A M)).flip).flip
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- `map f` is left adjoint to `pullback f` when `f` is a monomorphism  -/
CategoryTheory.MonoOver.mapPullbackAdj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Mono f] → CategoryTheory.MonoOver.map f ⊣ CategoryTheory.MonoOver.pullback f
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Mon.mul_nc.match_1.eq_1 : ∀ (motive : Lean.Grind.CommRing.Mon → Sort u_1) (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit)
  (h_2 : (pw : Lean.Grind.CommRing.Power) → motive (Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit))
  (h_3 :
    (pw : Lean.Grind.CommRing.Power) → (m₁ : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult pw m₁)),
  (match Lean.Grind.CommRing.Mon.unit with
    | Lean.Grind.CommRing.Mon.unit => h_1 ()
    | Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit => h_2 pw
    | Lean.Grind.CommRing.Mon.mult pw m₁ => h_3 pw m₁) =
    h_1 ()
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.map_add_toList_roo : ∀ {m n k : ℕ}, List.map (fun x => x + k) (m<...n).toList = ((m + k)<...n + k).toList
-- Mathlib.CategoryTheory.Sites.LocalSite
/-- The presheaf fibre functor of `point J` is given by evaluation at the terminal
object.  -/
CategoryTheory.GrothendieckTopology.IsLocalSite.pointPresheafFiberNatIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
        [inst_2 : J.IsLocalSite] →
          (A : Type u') →
            [inst_3 : CategoryTheory.Category.{v', u'} A] →
              [inst_4 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
                (CategoryTheory.GrothendieckTopology.IsLocalSite.point J).presheafFiber ≅
                  (CategoryTheory.evaluation Cᵒᵖ A).obj (Opposite.op (⊤_ C))
-- Mathlib.Topology.Convenient.GeneratedBy
Topology.IsGeneratedBy.homeomorph.congr_simp : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y : Type v} [tY : TopologicalSpace Y]
  [inst_1 : Topology.IsGeneratedBy X Y], Topology.IsGeneratedBy.homeomorph = Topology.IsGeneratedBy.homeomorph
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_diff_add_size_inter_eq_size_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (t₁ \ t₂).size + (t₁ ∩ t₂).size = t₁.size
-- Mathlib.Analysis.Convex.StdSimplex
/-- `stdSimplex 𝕜 ι` is closed.  -/
isClosed_stdSimplex : ∀ (𝕜 : Type u_1) (ι : Type u_2) [inst : Fintype ι] [inst_1 : TopologicalSpace 𝕜] [inst_2 : Semiring 𝕜]
  [inst_3 : PartialOrder 𝕜] [OrderClosedTopology 𝕜] [ContinuousAdd 𝕜], IsClosed (stdSimplex 𝕜 ι)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.isoMk.congr_simp : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L₁ : CategoryTheory.Functor A T}
  {R₁ : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L₁ R₁} (l l_1 : X.left ≅ Y.left) (e_l : l = l_1)
  (r r_1 : X.right ≅ Y.right) (e_r : r = r_1)
  (h :
    CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom = CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom)),
  CategoryTheory.Comma.isoMk l r h = CategoryTheory.Comma.isoMk l_1 r_1 ⋯
-- Mathlib.NumberTheory.JacobiSum.Basic
/-- If `χ` and `φ` are multiplicative characters on a finite field `F` such that
`χφ` is nontrivial, then `g(χφ) * J(χ,φ) = g(χ) * g(φ)`.  -/
jacobiSum_mul_nontrivial : ∀ {F : Type u_1} {R : Type u_2} [inst : Field F] [inst_1 : Fintype F] [inst_2 : CommRing R] [IsDomain R]
  {χ φ : MulChar F R}, χ * φ ≠ 1 → ∀ (ψ : AddChar F R), gaussSum (χ * φ) ψ * jacobiSum χ φ = gaussSum χ ψ * gaussSum φ ψ
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.categoryFreeMonoidalCategory : {C : Type u} → CategoryTheory.Category.{u, u} (CategoryTheory.FreeMonoidalCategory C)
-- Init.Data.Nat.Lemmas
Nat.add_eq_right : ∀ {a b : ℕ}, a + b = b ↔ a = 0
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Stats.mk.injEq : ∀ (usedTheorems : Lean.Meta.Simp.UsedSimps) (diag : Lean.Meta.Simp.Diagnostics)
  (usedTheorems_1 : Lean.Meta.Simp.UsedSimps) (diag_1 : Lean.Meta.Simp.Diagnostics),
  ({ usedTheorems := usedTheorems, diag := diag } = { usedTheorems := usedTheorems_1, diag := diag_1 }) =
    (usedTheorems = usedTheorems_1 ∧ diag = diag_1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.not_mem_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {a : α}, t.isEmpty = true → a ∉ t
-- Mathlib.Data.Tree.Basic
BinaryTree.numNodes.eq_def : ∀ {α : Type u} (x : BinaryTree α),
  x.numNodes =
    match x with
    | BinaryTree.nil => 0
    | BinaryTree.node value a b => a.numNodes + b.numNodes + 1
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
/-- The linear equivalence between `(𝓞 K)ˣ ⧸ (torsion K)` as an additive `ℤ`-module and
`unitLattice` .  -/
NumberField.Units.logEmbeddingEquiv : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      Additive ((NumberField.RingOfIntegers K)ˣ ⧸ NumberField.Units.torsion K) ≃ₗ[ℤ] ↥(NumberField.Units.unitLattice K)