mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.zero_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : Zero γ] (g : C(α, β)), ContinuousMap.comp 0 g = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.desc.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPushout f g] (h h_1 : Y ⟶ W) (e_h : h = h_1) (k k_1 : Z ⟶ W) (e_k : k = k_1)
  (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k),
  CategoryTheory.Limits.pushout.desc h k w = CategoryTheory.Limits.pushout.desc h_1 k_1 ⋯
-- Std.Http.Data.Method
/-- Access control list for a resource.
Source: https://www.rfc-editor.org/rfc/rfc3744#section-8.1
 -/
Std.Http.Method.acl : Std.Http.Method
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.comp_inj' : ∀ {V : Type u} [inst : Quiver V] {a b c : V} {p₁ p₂ : Quiver.Path a b} {q₁ q₂ : Quiver.Path b c},
  p₁.length = p₂.length → (p₁.comp q₁ = p₂.comp q₂ ↔ p₁ = p₂ ∧ q₁ = q₂)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_coe_sort : ∀ {ι : Type u_1} {M : Type u_4} (s : Finset ι) [inst : CommMonoid M] (f : ι → M), ∏ i, f ↑i = ∏ i ∈ s, f i
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- Reindexing a matrix preserves column-stochasticity.  -/
Matrix.reindex_mem_colStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {m : Type u_3} [inst_5 : Fintype m] [inst_6 : DecidableEq m]
  {M : Matrix n n R} {e₁ e₂ : n ≃ m}, M ∈ Matrix.colStochastic R n → (Matrix.reindex e₁ e₂) M ∈ Matrix.colStochastic R m
-- Init.Data.List.Sublist
List.Sublist.tail : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁.tail.Sublist l₂.tail
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- **Alias** of `zero_apply`. -/
QuadraticMap.zero_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Zero β}
  {inst_2 : Zero F} [self : IsZeroApply F α β] (x : α), 0 x = 0
-- Init.Notation
/-- A pipe operator that feeds values from the right into functions on the left.

`f <| x` means the same as `f x`, except that it parses `x` with lower precedence, which means that
`f <| g <| x` is interpreted as `f (g x)` rather than `(f g) x`.
 -/
«term_<|_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.map.eq_1 : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : X ⟶ Y),
  CategoryTheory.Under.map f =
    CategoryTheory.Comma.mapLeft (CategoryTheory.Functor.id T) (CategoryTheory.Discrete.natTrans fun x => f)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.parallelPairOpIso_inv_app_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f g : X ⟶ Y),
  (CategoryTheory.Limits.parallelPairOpIso f g).inv.app CategoryTheory.Limits.WalkingParallelPair.zero =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Limits.walkingParallelPairOpEquiv.functor.comp (CategoryTheory.Limits.parallelPair f g).op).obj
        CategoryTheory.Limits.WalkingParallelPair.zero)
-- Mathlib.Algebra.Star.Unitary
Unitary.toUnits_comp_map : ∀ {R : Type u_2} {S : Type u_3} [inst : Monoid R] [inst_1 : StarMul R] [inst_2 : Monoid S] [inst_3 : StarMul S]
  (f : R →⋆* S), Unitary.toUnits.comp (Unitary.map f).toMonoidHom = (Units.map f.toMonoidHom).comp Unitary.toUnits
-- Mathlib.Algebra.Order.Module.Defs
smul_nonneg_iff_neg_imp_nonpos : ∀ {α : Type u_1} {β : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [PosSMulStrictMono α β] {a : α} {b : β}, 0 ≤ a • b ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
Std.Iterators.Types.ArrayIterator.stepAsHetT_iterFromIdxM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} [LawfulMonad m] {array : Array β} {pos : ℕ},
  (array.iterFromIdxM m pos).stepAsHetT =
    if x : pos < array.size then pure (Std.IterStep.yield (array.iterFromIdxM m (pos + 1)) array[pos])
    else pure Std.IterStep.done
-- Mathlib.NumberTheory.Height.Projectivization
Projectivization.logHeight_mk : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [inst_2 : Finite ι] {x : ι → K}
  (hx : x ≠ 0), (Projectivization.mk K x hx).logHeight = Height.logHeight x
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.hasLimit_cospan_forget_of_right' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.SheafedSpace C} (f : X ⟶ Z)
  (g : Y ⟶ Z) [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f],
  CategoryTheory.Limits.HasLimit
    (CategoryTheory.Limits.cospan
      (((CategoryTheory.Limits.cospan g f).comp AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace).map
        CategoryTheory.Limits.WalkingCospan.Hom.inl)
      (((CategoryTheory.Limits.cospan g f).comp AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace).map
        CategoryTheory.Limits.WalkingCospan.Hom.inr))
-- Mathlib.Data.ENat.Basic
/-- Version of `WithTop.forall_natCast_le_iff_le` using `Nat.cast` rather than `WithTop.some`.  -/
ENat.forall_natCast_le_iff_le : ∀ {m n : ℕ∞}, (∀ (a : ℕ), ↑a ≤ m → ↑a ≤ n) ↔ m ≤ n
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
SimpContFract.of_isContFract : ∀ {K : Type u_1} (v : K) [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [inst_3 : FloorRing K],
  (SimpContFract.of v).IsContFract
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.limit_ext_iff : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  [inst_1 : CategoryTheory.Limits.HasLimit F] {x y : CategoryTheory.Limits.limit F},
  x = y ↔
    ∀ (j : J),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) x =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) y
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
hasFPowerSeriesAt_log_one : HasFPowerSeriesAt Real.log (FormalMultilinearSeries.ofScalars ℝ fun n => -(-1) ^ n / ↑n) 1
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.Stream'.dist_le_one : ∀ {α : Type u_1} (s t : Stream' α), dist s t ≤ 1
-- Mathlib.Algebra.Group.Defs
DivisionMonoid.toInvolutiveInv : {G : Type u} → [self : DivisionMonoid G] → InvolutiveInv G
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.cardinal_eq_of_isSeparable : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsSeparable F E],
  Cardinal.mk (Field.Emb F E) = (fun c => if Cardinal.aleph0 ≤ c then 2 ^ c else c) (Module.rank F E)
-- Mathlib.RingTheory.PowerSeries.Ideal
/-- Given a prime ideal `I` of `R⟦X⟧` such that `X ∉ I`, if `I.map constantCoeff` is generated by a
finite set `S : Set T`, then there exists `T : Set R`, of the same cardinality as `S`, that
generates `I`.  -/
PowerSeries.exist_eq_span_eq_ncard_of_X_notMem : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal (PowerSeries R)} [I.IsPrime],
  PowerSeries.X ∉ I →
    ∀ {S : Set R},
      Ideal.span S = Ideal.map PowerSeries.constantCoeff I →
        S.Finite → ∃ T, I = Ideal.span T ∧ T.Finite ∧ T.ncard = S.ncard
-- Mathlib.Probability.Moments.IntegrableExpMul
ProbabilityTheory.integrable_rpow_mul_cexp_of_re_mem_interior_integrableExpSet : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {z : ℂ},
  z.re ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ {p : ℝ}, 0 ≤ p → MeasureTheory.Integrable (fun ω => ↑(X ω ^ p) * Complex.exp (z * ↑(X ω))) μ
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.reflexivePair.mkNatIso_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C}
  (e₀ : F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ≅ G.obj CategoryTheory.Limits.WalkingReflexivePair.zero)
  (e₁ : F.obj CategoryTheory.Limits.WalkingReflexivePair.one ≅ G.obj CategoryTheory.Limits.WalkingReflexivePair.one)
  (h₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left) e₀.hom =
        CategoryTheory.CategoryStruct.comp e₁.hom (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left))
      CategoryTheory.Limits.reflexivePair.mkNatIso._auto_1)
  (h₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) e₀.hom =
        CategoryTheory.CategoryStruct.comp e₁.hom (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right))
      CategoryTheory.Limits.reflexivePair.mkNatIso._auto_3)
  (h₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion) e₁.hom =
        CategoryTheory.CategoryStruct.comp e₀.hom (G.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion))
      CategoryTheory.Limits.reflexivePair.mkNatIso._auto_5)
  (x : CategoryTheory.Limits.WalkingReflexivePair),
  (CategoryTheory.Limits.reflexivePair.mkNatIso e₀ e₁ h₁ h₂ h₃).inv.app x =
    match x with
    | CategoryTheory.Limits.WalkingReflexivePair.zero => e₀.inv
    | CategoryTheory.Limits.WalkingReflexivePair.one => e₁.inv
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertMany_empty_list_cons_eq_insertMany! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {k : α} {v : β} {tl : List (α × β)},
  ↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty ((k, v) :: tl) ⋯) =
    ↑(Std.DTreeMap.Internal.Impl.Const.insertMany!
        (Std.DTreeMap.Internal.Impl.insert! k v Std.DTreeMap.Internal.Impl.empty) tl)
-- Plausible.Testable
Plausible.Testable.mk : {p : Prop} → (Plausible.Configuration → Bool → Plausible.Gen (Plausible.TestResult p)) → Plausible.Testable p
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_of_im_pos : ∀ {z : ℂ}, 0 < z.im → z.arg = Real.arccos (z.re / ‖z‖)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.continuousAt_arctan : ∀ {x : ℝ}, ContinuousAt Real.arctan x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.congr_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeMap.Raw α β cmp},
  t₁.Equiv t₂ → (t₁.Equiv t₃ ↔ t₂.Equiv t₃)
-- Batteries.Data.List.Perm
List.Subperm.idxInj.congr_simp : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : ReflBEq α] {xs ys : List α} (h : xs.Subperm ys) (i i_1 : Fin xs.length),
  i = i_1 → h.idxInj i = h.idxInj i_1
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.comap_map_mk : ∀ {R : Type u} [inst : Ring R] {I J : Ideal R} [inst_1 : I.IsTwoSided],
  I ≤ J → Ideal.comap (Ideal.Quotient.mk I) (Ideal.map (Ideal.Quotient.mk I) J) = J
-- Mathlib.Algebra.Polynomial.GroupRingAction
prodXSubSMul.eval : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Fintype G] (R : Type u_3) [inst_2 : CommRing R]
  [inst_3 : MulSemiringAction G R] (x : R), Polynomial.eval x (prodXSubSMul G R x) = 0
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
/-- A set equipped with an operation of finite convex combinations,
where the coefficients must be non-negative and sum to 1.
 -/
Convexity.ConvexSpace : (R : Type u) →
  Type v → [inst₁ : PartialOrder R] → [inst₂ : Semiring R] → [inst₃ : IsStrictOrderedRing R] → Type (max u v)
-- Mathlib.Order.Concept
/-- **Alias** of the forward direction of `Order.isIntent_iff`. -/
Order.IsIntent.eq : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {t : Set β}, Order.IsIntent r t → upperPolar r (lowerPolar r t) = t
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.toAlgHom_monomial : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {P : Algebra.Generators R S ι} {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] {P' : Algebra.Generators R' S' ι'} [inst_6 : Algebra R R']
  [inst_7 : Algebra S S'] (f : P.Hom P') (v : ι →₀ ℕ) (r : R),
  f.toAlgHom ((MvPolynomial.monomial v) r) = r • v.prod fun x1 x2 => f.val x1 ^ x2
-- Lean.Meta.Tactic.Grind.Types
/-- Goal modification time.  -/
Lean.Meta.Grind.EMatch.State.gmt : Lean.Meta.Grind.EMatch.State → ℕ
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
/-- A morphism is weakly étale if it is flat and the diagonal map is flat.  -/
AlgebraicGeometry.WeaklyEtale : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Mathlib.Data.Set.Function
Set.InjOn.eq_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {x y : α}, Set.InjOn f s → x ∈ s → y ∈ s → (f x = f y ↔ x = y)
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_insertList_disj_of_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.containsKey k (Std.Internal.List.insertList l toInsert) =
    (Std.Internal.List.containsKey k l || Std.Internal.List.containsKey k toInsert)
-- Mathlib.Analysis.Convex.Segment
left_mem_segment : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [ZeroLEOneClass 𝕜] [inst_4 : MulActionWithZero 𝕜 E] (x y : E), x ∈ segment 𝕜 x y
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasImage f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage f) (CategoryTheory.Limits.image.ι f) = f
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddCommMonoidOfAddOpposite : {M : Type u_1} → [AddCommMonoid Mᵃᵒᵖ] → AddCommMonoid Mᵈᵃᵃ
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.generatorIndex.congr_simp : ∀ {K : Type u_1} [inst : Field K] {E E_1 : IntermediateField K (RatFunc K)} (e_E : E = E_1) (h : E ≠ ⊥),
  RatFunc.Luroth.generatorIndex✝ h = RatFunc.Luroth.generatorIndex✝ ⋯
-- Mathlib.Order.Ideal
/-- A (noncomputable) element of a cofinal set lying above a given element.  -/
Order.Cofinal.above : {P : Type u_1} → [inst : Preorder P] → Order.Cofinal P → P → P
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- The Jacobi symbol is multiplicative in its second argument.  -/
jacobiSym.mul_right' : ∀ (a : ℤ) {b₁ b₂ : ℕ}, b₁ ≠ 0 → b₂ ≠ 0 → jacobiSym a (b₁ * b₂) = jacobiSym a b₁ * jacobiSym a b₂
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- A rewrite lemma for `padicValRat p (q / r)` with conditions `q ≠ 0`, `r ≠ 0`.  -/
padicValRat.div : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {q r : ℚ}, q ≠ 0 → r ≠ 0 → padicValRat p (q / r) = padicValRat p q - padicValRat p r
-- Mathlib.Topology.Category.TopCommRingCat
/-- The forgetful functor to `TopCat`.  -/
TopCommRingCat.hasForgetToTopCat : CategoryTheory.HasForget₂ TopCommRingCat TopCat
-- Mathlib.Data.Set.Function
Set.mapsTo_univ : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α), Set.MapsTo f s Set.univ
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
/-- The continuous `σ`-semilinear maps between two vector bundles form a vector bundle.  -/
Bundle.ContinuousAlternatingMap.instVectorBundle : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : Fintype ι] {B : Type u_3}
  [inst_2 : TopologicalSpace B] {F₁ : Type u_4} [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁]
  {E₁ : B → Type u_5} [inst_5 : (x : B) → AddCommGroup (E₁ x)] [inst_6 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_8 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_9 : FiberBundle F₁ E₁] [inst_10 : VectorBundle 𝕜 F₁ E₁] {F₂ : Type u_6} [inst_11 : NormedAddCommGroup F₂]
  [inst_12 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_13 : (x : B) → AddCommGroup (E₂ x)]
  [inst_14 : (x : B) → Module 𝕜 (E₂ x)] [inst_15 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜 F₂ E₂]
  [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)] [inst_20 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)],
  VectorBundle 𝕜 (F₁ [⋀^ι]→L[𝕜] F₂) fun x => E₁ x [⋀^ι]→L[𝕜] E₂ x
-- Qq.Match
Qq.unpackParensIdent : Lean.Syntax → Option Lean.Syntax
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.flip_quotDualCoannihilatorToDual_bijective : ∀ {K : Type u_4} {V : Type u_5} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (W : Subspace K (Module.Dual K V)) [FiniteDimensional K ↥W],
  Function.Bijective ⇑(Submodule.quotDualCoannihilatorToDual W).flip
-- Init.Data.Int.Basic
Int.instAdd : Add ℤ
-- Mathlib.Tactic.TacticAnalysis.Declarations
/-- Debug `grind` by identifying places where it does not yet supersede `linarith`.  -/
linarithToGrindRegressions : Mathlib.TacticAnalysis.Config
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.funUnique_apply : ∀ (ι : Type u_7) (X : Type u_8) [inst : Unique ι] [inst_1 : TopologicalSpace X],
  ⇑(Homeomorph.funUnique ι X) = fun f => f default
-- Mathlib.Data.Finmap
Finmap.lookup_eq_none : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s : Finmap β}, Finmap.lookup a s = none ↔ a ∉ s
-- Mathlib.Algebra.Module.ZLattice.Basic
ZLattice.comap_refl : ∀ (K : Type u_1) [inst : NormedField K] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace K E]
  (L : Submodule ℤ E), ZLattice.comap K L 1 = L
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.constantCoeff_substInvOfIsUnit : ∀ {R : Type u_2} [inst : CommRing R] (P : PowerSeries R) (hP' : IsUnit ((PowerSeries.coeff 1) P)),
  PowerSeries.constantCoeff (P.substInvOfIsUnit hP') = 0
-- Lean.Elab.InfoTree.Main
Lean.Elab.Info.format : Lean.Elab.ContextInfo → Lean.Elab.Info → IO Std.Format
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.self_le_maxKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k} {fallback : α}, (cmp k ((t.insertIfNew k v).maxKeyD fallback)).isLE = true
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The current machine state.  -/
Turing.TM0.Cfg.q : {Γ : Type u_1} → {Λ : Type u_2} → [inst : Inhabited Γ] → Turing.TM0.Cfg Γ Λ → Λ
-- Init.Data.SInt.Bitwise
Int64.toISize_xor : ∀ (a b : Int64), (a ^^^ b).toISize = a.toISize ^^^ b.toISize
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.coprod.inl_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct X Y] {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.snd X Y) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_zero_right_deg : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (m : ℕ), f.resultant g m 0 = g.coeff 0 ^ m
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.leftUnitor_naturality : ∀ {R : Type u} [inst : CommSemiring R] {M N : SemimoduleCat R} (f : M ⟶ N),
  CategoryTheory.CategoryStruct.comp
      (SemimoduleCat.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (SemimoduleCat.of R R)) f)
      (SemimoduleCat.MonoidalCategory.leftUnitor N).hom =
    CategoryTheory.CategoryStruct.comp (SemimoduleCat.MonoidalCategory.leftUnitor M).hom f
-- Mathlib.Algebra.Group.Graph
/-- **Vertical line test** for monoid homomorphisms.

Let `f : G → H × I` be a homomorphism to a product of monoids. Assume that `f` is surjective on the
first factor and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` at most
once. Then the image of `f` is the graph of some monoid homomorphism `f' : H → I`.  -/
AddMonoidHom.exists_mrange_eq_mgraph : ∀ {G : Type u_1} {H : Type u_2} {I : Type u_3} [inst : AddMonoid G] [inst_1 : AddMonoid H] [inst_2 : AddMonoid I]
  {f : G →+ H × I},
  Function.Surjective (Prod.fst ∘ ⇑f) →
    (∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) → ∃ f', AddMonoidHom.mrange f = f'.mgraph
-- Init.SimpLemmas
/-- We move `!` from the left hand side of an equality to the right hand side.
This helps confluence, and also helps combining pairs of `!`s.
 -/
Bool.not_eq_eq_eq_not : ∀ {a b : Bool}, (!a) = b ↔ a = !b
-- Lean.Elab.Do.Control
_private.Lean.Elab.Do.Control.0.Lean.Elab.Do.ControlStack.exceptT.stM : Lean.Elab.Do.MonadInfo → Lean.Elab.Do.DoElabM Lean.Elab.Do.ReturnCont → Lean.Expr → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_apply_self : ∀ {α : Type u_2} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α), (μ.restrict s) s = μ s
-- Mathlib.AlgebraicTopology.DoldKan.Degeneracies
AlgebraicTopology.DoldKan.degeneraciesVanish_iff_QInfty_f_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} {n : ℕ} {T : C} (f : X.obj (Opposite.op { len := n }) ⟶ T),
  AlgebraicTopology.DoldKan.DegeneraciesVanish f ↔
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.QInfty.f n) f = 0
-- Init.Data.Array.Lemmas
Array.filter_empty : ∀ {α : Type u_1} {p : α → Bool}, Array.filter p #[] = #[]
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The left homology in the opposite category of the opposite of a short complex identifies
to the right homology of this short complex.  -/
CategoryTheory.ShortComplex.leftHomologyOpIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        [inst_2 : S.HasRightHomology] → S.op.leftHomology ≅ Opposite.op S.rightHomology
-- Mathlib.Order.RelClasses
instIsPartialOrderLe : ∀ {α : Type u} [inst : PartialOrder α], IsPartialOrder α fun x1 x2 => x1 ≤ x2
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.hasExt_iff_small_ext : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C],
  CategoryTheory.HasExt C ↔ ∀ (X Y : C) (n : ℕ), Small.{w', w} (CategoryTheory.Abelian.Ext X Y n)
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
instIsInertiaFieldOfIsGaloisGroupSubtypeAlgEquivMemSubgroupInertia : ∀ (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing B] (P : Ideal B) (E : Type u_6) [inst_4 : Field E] [inst_5 : Algebra E L]
  [inst_6 : MulSemiringAction Gal(L/K) B] [h : IsGaloisGroup (↥(Ideal.inertia Gal(L/K) P)) E L], IsInertiaField K L P E
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.normalizationObjIso_hom_val : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U : Y.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationObjIso f hU).hom
      (CommRingCat.ofHom
        (integralClosure ↑(Y.presheaf.obj (Opposite.op U))
              ↑(X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)))).val.toRingHom) =
    AlgebraicGeometry.Scheme.Hom.appLE (AlgebraicGeometry.Scheme.Hom.toNormalization f)
      ((TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.Hom.fromNormalization f).base).obj U)
      ((TopologicalSpace.Opens.map f.base).obj U) ⋯
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.realizeValue.unsafe_15 : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PersistentHashMap α (Task Dynamic) → NonScalar
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousAt.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] (r : α → β → Prop) (x : α),
  SemicontinuousAt r x = ∀ (y : β), r x y → ∀ᶠ (x' : α) in nhds x, r x' y