mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.fun_sub : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β} [inst_1 : AddGroup β] [IsTopologicalAddGroup β],
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (fun i => f i - g i) μ
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.eval_apply_eq_zero_iff : ∀ (K : Type uK) {V : Type uV} [inst : CommSemiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [Module.Projective K V] (v : V), (Module.Dual.eval K V) v = 0 ↔ v = 0
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.congr : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {f g : α → ε}, MeasureTheory.Integrable f μ → f =ᵐ[μ] g → MeasureTheory.Integrable g μ
-- Mathlib.Algebra.Category.Grp.Basic
CategoryTheory.Iso.addCommGroupIsoToAddEquiv_symm_apply : ∀ {X Y : AddCommGrpCat} (i : X ≅ Y) (a : ↑Y), i.addCommGroupIsoToAddEquiv.symm a = (AddCommGrpCat.Hom.hom i.inv) 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₂)
  (α : CategoryTheory.CategoryStruct.comp g l₂ ⟶ CategoryTheory.CategoryStruct.comp l₁ h),
  (CategoryTheory.Bicategory.mateEquiv adj₁ adj₂) α =
    CategoryTheory.bicategoricalComp (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp r₁ g))
      (CategoryTheory.bicategoricalComp
        (CategoryTheory.Bicategory.whiskerLeft r₁ (CategoryTheory.Bicategory.whiskerLeft g adj₂.unit))
        (CategoryTheory.bicategoricalComp
          (CategoryTheory.Bicategory.whiskerLeft r₁ (CategoryTheory.Bicategory.whiskerRight α r₂))
          (CategoryTheory.bicategoricalComp
            (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight adj₁.counit h) r₂)
            (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp h r₂)))))
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_insert_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  (m.insert k).size ≤ m.size + 1
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_apply_one_sub : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (p₀ p₁ : P1) (c : k), (AffineMap.lineMap p₀ p₁) (1 - c) = (AffineMap.lineMap p₁ p₀) c
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.congrHash.go : Lean.Meta.Grind.ENodeMap → Lean.Expr → UInt64 → UInt64
-- Mathlib.Algebra.Group.Action.Units
/-- Transfer `VAddAssocClass G M α` to `VAddAssocClass G (AddUnits M) α`.  -/
AddUnits.vaddAssocClass'_left : ∀ {G : Type u_1} {M : Type u_3} {α : Type u_5} [inst : AddGroup G] [inst_1 : AddMonoid M] [inst_2 : AddAction G M]
  [inst_3 : VAdd M α] [inst_4 : VAdd G α] [inst_5 : VAddCommClass G M M] [inst_6 : VAddAssocClass G M M]
  [VAddAssocClass G M α], VAddAssocClass G (AddUnits M) α
-- Mathlib.MeasureTheory.Measure.Haar.Basic
/-- This is the "limit" of `prehaar K₀ U K` as `U` becomes a smaller and smaller open
neighborhood of `(1 : G)`. More precisely, it is defined to be an arbitrary element
in the intersection of all the sets `clPrehaar K₀ V` in `haarProduct K₀`.
This is roughly equal to the Haar measure on compact sets,
but it can differ slightly. We do know that
`haarMeasure K₀ (interior K) ≤ chaar K₀ K ≤ haarMeasure K₀ K`.  -/
MeasureTheory.Measure.haar.chaar : {G : Type u_1} →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] →
      [IsTopologicalGroup G] → TopologicalSpace.PositiveCompacts G → TopologicalSpace.Compacts G → ℝ
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.neg_mk : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Neg R] (a₁ a₂ a₃ a₄ : R),
  -{ re := a₁, imI := a₂, imJ := a₃, imK := a₄ } = { re := -a₁, imI := -a₂, imJ := -a₃, imK := -a₄ }
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
CategoryTheory.Iso.inv.hcongr_5 : ∀ (C C' : Type u),
  C = C' →
    ∀ (inst : CategoryTheory.Category.{v, u} C) (inst' : CategoryTheory.Category.{v, u} C'),
      inst ≍ inst' →
        ∀ (X : C) (X' : C'),
          X ≍ X' → ∀ (Y : C) (Y' : C'), Y ≍ Y' → ∀ (self : X ≅ Y) (self' : X' ≅ Y'), self ≍ self' → self.inv ≍ self'.inv
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.forall_mem_dualAnnihilator_apply_eq_zero_iff : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (W : Subspace K V)
  (v : V), (∀ φ ∈ Submodule.dualAnnihilator W, φ v = 0) ↔ v ∈ W
-- Mathlib.Algebra.Order.Archimedean.Class
/-- An `OrderMonoidHom` can be lifted to an `OrderHom` over archimedean classes.  -/
MulArchimedeanClass.orderHom : {M : Type u_1} →
  [inst : CommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedMonoid M] →
        {N : Type u_2} →
          [inst_3 : CommGroup N] →
            [inst_4 : LinearOrder N] →
              [inst_5 : IsOrderedMonoid N] → (M →*o N) → MulArchimedeanClass M →o MulArchimedeanClass N
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.eq_of_valuation_isEquiv_valuation : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] {p q : IsDedekindDomain.HeightOneSpectrum R},
  (IsDedekindDomain.HeightOneSpectrum.valuation K p).IsEquiv (IsDedekindDomain.HeightOneSpectrum.valuation K q) → p = q
-- Mathlib.AlgebraicGeometry.Morphisms.Immersion
AlgebraicGeometry.IsImmersion.instLiftSchemeId : ∀ {X : AlgebraicGeometry.Scheme},
  AlgebraicGeometry.IsImmersion
    (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))
-- Mathlib.Probability.Decision.Risk.Countable
ProbabilityTheory.bayesRisk_countable : ∀ {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ}
  [Countable Θ] [MeasurableSingletonClass Θ],
  ProbabilityTheory.bayesRisk ℓ P π =
    ⨅ κ, ⨅ (_ : ProbabilityTheory.IsMarkovKernel κ), ∑' (θ : Θ), (∫⁻ (y : 𝓨), ℓ θ y ∂(κ.comp P) θ) * π {θ}
-- Mathlib.Order.WithBot
WithTop.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : β → γ) (g : α → β) (a : WithTop α),
  WithTop.map h (WithTop.map g a) = WithTop.map (h ∘ g) a
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.extendUpdatedVarsAux : Lean.Elab.Term.Do.Code → Lean.Elab.Term.Do.VarSet → Lean.Elab.TermElabM Lean.Elab.Term.Do.Code
-- Mathlib.Analysis.Analytic.Order
AnalyticAt.analyticOrderAt_deriv_add_one : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜},
  AnalyticAt 𝕜 f x →
    ∀ [CompleteSpace E] [CharZero 𝕜], analyticOrderAt (deriv f) x + 1 = analyticOrderAt (fun x_1 => f x_1 - f x) x
-- Mathlib.Order.JordanHolder
JordanHolderLattice.isMaximal_inf_right_of_isMaximal_sup : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {x y : X},
  JordanHolderLattice.IsMaximal x (x ⊔ y) →
    JordanHolderLattice.IsMaximal y (x ⊔ y) → JordanHolderLattice.IsMaximal (x ⊓ y) y
-- Mathlib.Combinatorics.Matroid.Circuit
/-- A stronger version of `Matroid.ext_isCircuit`:
two matroids on the same ground set are equal if no circuit of one is independent in the other.  -/
Matroid.ext_isCircuit_not_indep : ∀ {α : Type u_1} {M₁ M₂ : Matroid α},
  M₁.E = M₂.E → (∀ (C : Set α), M₁.IsCircuit C → ¬M₂.Indep C) → (∀ (C : Set α), M₂.IsCircuit C → ¬M₁.Indep C) → M₁ = M₂
-- Mathlib.Algebra.Order.Field.Basic
one_div_lt_one_div_of_lt : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α},
  0 < a → a < b → 1 / b < 1 / a
-- Mathlib.Tactic.NormNum.Ineq
/-- Identify (as `true` or `false`) expressions of the form `a ≤ b`, where `a` and `b` are numeric
expressions whose evaluations to `NormNum.Result` have already been computed.  -/
_private.Mathlib.Tactic.NormNum.Ineq.0.Mathlib.Meta.NormNum.evalLE.core : {u : Lean.Level} →
  {α : Q(Type u)} →
    (lα : Q(LE «$α»)) →
      {a b : Q(«$α»)} →
        Mathlib.Meta.NormNum.Result a →
          Mathlib.Meta.NormNum.Result b → Lean.MetaM (Mathlib.Meta.NormNum.Result q(«$a» ≤ «$b»))
-- Mathlib.AlgebraicGeometry.Normalization
CategoryTheory.MorphismProperty.monomorphisms.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (x x_1 : C) (f : x ⟶ x_1),
  CategoryTheory.MorphismProperty.monomorphisms C f = CategoryTheory.Mono f
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.empty.eq_1 : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ},
  Monoid.PushoutI.NormalWord.empty = { toWord := Monoid.CoprodI.Word.empty, head := 1, normalized := ⋯ }
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.normalCore_eq_self : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [H.Normal], H.normalCore = H
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_extractLsb : ∀ {n hi lo : ℕ} {x : BitVec n} {i : ℕ},
  (BitVec.extractLsb hi lo x).getLsbD i = (decide (i < hi - lo + 1) && x.getLsbD (lo + i))
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Certify `a.subject + b.subject` from certificates for `a` and `b`.  -/
Mathlib.Tactic.Determinant.certAdd : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} →
      Mathlib.Tactic.Determinant.Cert rα →
        Mathlib.Tactic.Determinant.Cert rα → Mathlib.Tactic.Determinant.CertM rα (Mathlib.Tactic.Determinant.Cert rα)
-- Batteries.Data.Array.Merge
/-- `O(|xs| + |ys|)`. Merge arrays `xs` and `ys`, which must be sorted according to `compare` and must
not contain duplicates. If an element appears in both `xs` and `ys`, only one copy is kept.
 -/
Array.mergeDedup : {α : Type u_1} → [ord : Ord α] → Array α → Array α → Array α
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.pf_sub_c : ∀ {α : Type u_1} {a b : α} [inst : Sub α], a = b → ∀ (c : α), a - c = b - c
-- Mathlib.Data.Sym.Basic
Sym.mem_cast : ∀ {α : Type u_1} {n m : ℕ} {s : Sym α n} {a : α} (h : n = m), a ∈ (Sym.cast h) s ↔ a ∈ s
-- Mathlib.Data.Fintype.Prod
Finset.product_eq_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : Fintype β] {s : Finset α} {t : Finset β} [Nonempty α]
  [Nonempty β], s ×ˢ t = Finset.univ ↔ s = Finset.univ ∧ t = Finset.univ
-- Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Mathlib.Tactic.Bicategory.instMonadNormalizeNaturalityBicategoryM : Mathlib.Tactic.BicategoryLike.MonadNormalizeNaturality Mathlib.Tactic.Bicategory.BicategoryM
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.lcongr_single : ∀ {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] {σ : R →+* R₂}
  {σ_inv : R₂ →+* R} [inst_6 : RingHomInvPair σ σ_inv] [inst_7 : RingHomInvPair σ_inv σ] {ι : Type u_9} {κ : Type u_10}
  (e₁ : ι ≃ κ) (e₂ : M ≃ₛₗ[σ] N) (i : ι) (m : M), ((Finsupp.lcongr e₁ e₂) fun₀ | i => m) = fun₀ | e₁ i => e₂ m
-- Init.Data.Int.Gcd
Int.gcd_natCast_natCast : ∀ (a b : ℕ), (↑a).gcd ↑b = a.gcd b
-- Mathlib.Order.CompleteLattice.SetLike
CompleteSublattice.mem_top : ∀ {X : Type u_1} {L : CompleteSublattice (Set X)} {x : X}, x ∈ ⊤
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Comon.forget_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Comon C} (f : X ⟶ Y), (CategoryTheory.Comon.forget C).map f = f.hom
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimits.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Limits.HasColimits C = CategoryTheory.Limits.HasColimitsOfSize.{v, v, v, u} C
-- Mathlib.Data.Int.Interval
Int.uIcc_eq_finset_map : ∀ (a b : ℤ),
  Finset.uIcc a b =
    Finset.map (Nat.castEmbedding.trans (addLeftEmbedding (min a b))) (Finset.range (max a b + 1 - min a b).toNat)
-- Mathlib.RingTheory.Valuation.ValuationSubring
Valuation.valuationSubring_eq_top_iff : ∀ {K : Type u} [inst : Field K] {Γ : Type u_1} [inst_1 : LinearOrderedCommGroupWithZero Γ] (v : Valuation K Γ),
  v.valuationSubring = ⊤ ↔ ¬v.IsNontrivial
-- Init.Data.BitVec.Bootstrap
BitVec.ofNatLT.congr_simp : ∀ {w : ℕ} (i i_1 : ℕ) (e_i : i = i_1) (p : i < 2 ^ w), i#'p = i_1#'⋯
-- Init.Data.Range.Polymorphic.PRange
Std.Rci.LawfulRcoIntersection.mk : ∀ {α : Type w} [inst : LT α] [inst_1 : LE α] [inst_2 : Std.Rci.HasRcoIntersection α],
  (∀ {a : α} {r : Std.Rci α} {s : Std.Rco α}, a ∈ Std.Rci.HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s) →
    Std.Rci.LawfulRcoIntersection α
-- Init.Data.String.Iterator
/-- Gets the character at the iterator's current position.

This is a no-longer-supported legacy API that will be removed in a future release. You should use
`String.Pos` instead, which is similar, but safer. To iterate over a string `s`, start with
`p : s.startPos`, advance it using `p.next`, access the current character using `p.get` and
check if the position is at the end using `p = s.endPos` or `p.IsAtEnd`.

A run-time bounds check is performed. Use `String.Iterator.curr'` to avoid redundant bounds checks.

If the position is invalid, returns `(default : Char)`.
 -/
String.Legacy.Iterator.curr : String.Legacy.Iterator → Char
-- Mathlib.Topology.Algebra.InfiniteSum.Order
isLUB_hasSum : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α},
  (∀ (i : ι), 0 ≤ f i) → HasSum f a → IsLUB (Set.range fun s => ∑ i ∈ s, f i) a
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_prodMk_right : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {y : β}, Measurable fun x => (x, y)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_map : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited α] {f : (a : α) → β a → γ a} {k : α},
  (Std.DHashMap.map f m).getKey! k = m.getKey! k
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.pow_iff_coprime : ∀ {M : Type u_1} [inst : CommMonoid M] {k : ℕ} {ζ : M},
  IsPrimitiveRoot ζ k → 0 < k → ∀ (i : ℕ), IsPrimitiveRoot (ζ ^ i) k ↔ i.Coprime k
-- Mathlib.RingTheory.LocalProperties.InjectiveDimension
ModuleCat.localizedModule_hasInjectiveDimensionLE : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] [IsNoetherianRing R] (n : ℕ) (S : Submonoid R)
  (M : ModuleCat R) [CategoryTheory.HasInjectiveDimensionLE M n],
  CategoryTheory.HasInjectiveDimensionLE (M.localizedModule S) n
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Zipper.instToIterator : {α : Type u} →
  {β : α → Type v} →
    Std.ToIterator (Std.DTreeMap.Internal.Zipper α β) Id (Std.DTreeMap.Internal.Zipper α β) ((a : α) × β a)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isEmpty_filterMap_eq_false_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ},
  m.WF → ((Std.HashMap.Raw.filterMap f m).isEmpty = false ↔ ∃ k, ∃ (h : k ∈ m), (f (m.getKey k h) m[k]).isSome = true)
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanFinrank_eq_one_iff : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M),
  p.spanFinrank = 1 ↔ p.IsPrincipal ∧ p ≠ ⊥
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.mul : ∀ {α : Type u_2} [inst : Mul α] {f g : Filter α}, f.NeBot → g.NeBot → (f * g).NeBot
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.right_inv : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : Y}, x ∈ e.target → ↑e (↑e.symm x) = x
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.equivMvPolynomial.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R],
  Polynomial.Bivariate.equivMvPolynomial R =
    AlgEquiv.ofAlgHom (Polynomial.aevalAeval (MvPolynomial.X 0) (MvPolynomial.X 1))
      (MvPolynomial.aeval ![Polynomial.C Polynomial.X, Polynomial.X]) ⋯ ⋯
-- Mathlib.LinearAlgebra.Matrix.Adjugate
/-- Use linearity of `cramer` and vector evaluation to take `cramer A _ i` out of a summation.  -/
Matrix.sum_cramer_apply : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
  {β : Type u_1} (s : Finset β) (f : n → β → α) (i : n),
  ∑ x ∈ s, A.cramer (fun j => f j x) i = A.cramer (fun j => ∑ x ∈ s, f j x) i
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max?_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {k : α},
  t.WF → ((∀ (k' : α), t.max? = some k' → (cmp k' k).isLE = true) ↔ ∀ k' ∈ t, (cmp k' k).isLE = true)
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- `opZ^n(f, g)` identifies to the kernel of `H^n(f ≫ g) ⟶ H^n(g)`.  -/
CategoryTheory.Abelian.SpectralObject.kernelSequenceOpcycles_exact : ∀ {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) (n : ℤ), (X.kernelSequenceOpcycles f g fg h n).Exact
-- Init.Data.String.Substring
/-- Given a `Substring`, returns another one which has valid endpoints
and represents the same substring according to `Substring.toString`.
(Note, the substring may still be inverted, i.e. beginning greater than end.)
 -/
Substring.Raw.repair : Substring.Raw → Substring.Raw
-- Mathlib.LinearAlgebra.Multilinear.Basic
LinearMap.compMultilinearMap_smul : ∀ {R : Type uR} {S : Type uS} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : (i : ι) → Module R (M₁ i)] [inst_5 : Module R M₂] [inst_6 : Module R M₃] [inst_7 : DistribSMul S M₂]
  [inst_8 : DistribSMul S M₃] [inst_9 : SMulCommClass R S M₂] [inst_10 : SMulCommClass R S M₃]
  [LinearMap.CompatibleSMul M₂ M₃ S R] (g : M₂ →ₗ[R] M₃) (s : S) (f : MultilinearMap R M₁ M₂),
  g.compMultilinearMap (s • f) = s • g.compMultilinearMap f
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivAt.comp_hasFDerivAt_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  {h₂ : 𝕜' → 𝕜'} {h₂' y : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x : E),
  HasDerivAt h₂ h₂' y → HasFDerivAt f f' x → y = f x → HasFDerivAt (h₂ ∘ f) (h₂' • f') x
-- Mathlib.Combinatorics.Graph.Basic
Graph.Inc.isLink_other : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β} (h : G.Inc e x), G.IsLink e x h.other
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- The functor `RightExtension L F ⥤ RightExtension (G ⋙ L) (G ⋙ F)`
obtained by precomposition.  -/
CategoryTheory.Functor.RightExtension.precomp : {C : Type u_1} →
  {C' : Type u_2} →
    {H : 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} H] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                (L : CategoryTheory.Functor C D) →
                  (F : CategoryTheory.Functor C H) →
                    (G : CategoryTheory.Functor C' C) →
                      CategoryTheory.Functor (L.RightExtension F) ((G.comp L).RightExtension (G.comp F))
-- Mathlib.Order.SuccPred.Limit
PredOrder.prelimitRecOn_of_isPredPrelimit : ∀ {α : Type u_1} {b : α} {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : PredOrder α]
  [inst_2 : WellFoundedGT α] (pred : (a : α) → ¬IsMin a → motive a → motive (Order.pred a))
  (isPredPrelimit : (a : α) → Order.IsPredPrelimit a → ((b : α) → a < b → motive b) → motive a)
  (hb : Order.IsPredPrelimit b),
  PredOrder.prelimitRecOn b pred isPredPrelimit =
    isPredPrelimit b hb fun x x_1 => PredOrder.prelimitRecOn x pred isPredPrelimit
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.denote'.go.match_1.eq_1 : ∀ (motive : Lean.Grind.CommRing.Poly → Sort u_1) (h_1 : Unit → motive (Lean.Grind.CommRing.Poly.num 0))
  (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Poly.num k))
  (h_3 :
    (k : ℤ) →
      (m : Lean.Grind.CommRing.Mon) → (p : Lean.Grind.CommRing.Poly) → motive (Lean.Grind.CommRing.Poly.add k m p)),
  (match Lean.Grind.CommRing.Poly.num 0 with
    | Lean.Grind.CommRing.Poly.num 0 => h_1 ()
    | Lean.Grind.CommRing.Poly.num k => h_2 k
    | Lean.Grind.CommRing.Poly.add k m p => h_3 k m p) =
    h_1 ()
-- Mathlib.Combinatorics.Additive.Energy
Finset.mulEnergy.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Mul α] (s t : Finset α),
  s.mulEnergy t = {x ∈ (s ×ˢ s) ×ˢ t ×ˢ t | x.1.1 * x.2.1 = x.1.2 * x.2.2}.card
-- Mathlib.Topology.Path
Path.symm_bijective : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, Function.Bijective Path.symm
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → Option γ} {k : α} (h : m.WF),
  (Std.HashMap.Raw.filterMap f m)[k]? = m[k]?.pbind fun x h' => f (m.getKey k ⋯) x
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_le : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α}, s.Nonempty → (∀ b ∈ s, b ≤ a) → sSup s ≤ a
-- Mathlib.Order.Disjoint
codisjoint_inf_left : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderTop α] {a b c : α},
  Codisjoint (a ⊓ b) c ↔ Codisjoint a c ∧ Codisjoint b c
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiffWithinAt_prod' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {x : E} {n : WithTop ℕ∞} {𝔸' : Type u_4} {ι : Type u_5}
  [inst_3 : NormedCommRing 𝔸'] [inst_4 : NormedAlgebra 𝕜 𝔸'] {t : Finset ι} {f : ι → E → 𝔸'},
  (∀ i ∈ t, ContDiffWithinAt 𝕜 n (f i) s x) → ContDiffWithinAt 𝕜 n (∏ i ∈ t, f i) s x
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Literal.reify.prop : ∀ {v : Sat.Valuation} {l : Sat.Literal} {p : Prop}, Sat.Literal.reify v l p → v.neg l → p
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.toSubsemigroup_mono : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R], Monotone NonUnitalSubring.toSubsemigroup
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.IsWeaklyEisensteinAt.mk : ∀ {R : Type u} [inst : CommSemiring R] {f : Polynomial R} {𝓟 : Ideal R},
  (∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟) → f.IsWeaklyEisensteinAt 𝓟
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLoopAt.of_compatible : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G H : Graph α β},
  G.Compatible H → e ∈ H.edgeSet → G.IsLoopAt e x → H.IsLoopAt e x
-- Std.Time.Time.Unit.Second
Std.Time.Second.instDecidableLeOffset : {x y : Std.Time.Second.Offset} → Decidable (x ≤ y)