mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.LocalRing.NonLocalRing
/-- If two non-units sum to 1 in a (semi)ring `R` then `R` is not local.  -/
IsLocalRing.not_isLocalRing_def : ∀ {R : Type u_1} [inst : Semiring R] {a b : R}, ¬IsUnit a → ¬IsUnit b → a + b = 1 → ¬IsLocalRing R
-- Mathlib.LinearAlgebra.CliffordAlgebra.Prod
CliffordAlgebra.ofProd_comp_toProd : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] (Q₁ : QuadraticForm R M₁)
  (Q₂ : QuadraticForm R M₂),
  (CliffordAlgebra.ofProd Q₁ Q₂).comp (CliffordAlgebra.toProd Q₁ Q₂) =
    AlgHom.id R (GradedTensorProduct R (CliffordAlgebra.evenOdd Q₁) (CliffordAlgebra.evenOdd Q₂))
-- Mathlib.Algebra.FiniteSupport.Basic
Multiset.hasFiniteSupport_count : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), Function.HasFiniteSupport fun x => Multiset.count x s
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_top_right_eq_bot_iff_le_center : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, ⁅H, ⊤⁆ = ⊥ ↔ H ≤ AddSubgroup.center G
-- Mathlib.Tactic.FunProp.FunctionData
Mathlib.Meta.FunProp.MaybeFunctionData.letE.inj : ∀ {f f_1 : Lean.Expr},
  Mathlib.Meta.FunProp.MaybeFunctionData.letE f = Mathlib.Meta.FunProp.MaybeFunctionData.letE f_1 → f = f_1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.coreOfNat : Lean.Expr → Lean.Expr → ℕ → Int.Internal.Linear.Expr → Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof
-- Mathlib.LinearAlgebra.PiTensorProduct.Dual
/-- A linear equivalence between `⨂[R] i, Dual R (M i)` and `Dual R (⨂[R] i, M i)`
given bases for all `M i`. If `f : (i : ι) → Dual R (s i)`, then this equivalence sends
`⨂ₜ[R] i, f i` to the composition of `PiTensorProduct.map f` with the natural
isomorphism `⨂[R] i, R ≃ R` given by multiplication (`constantBaseRingEquiv`).  -/
PiTensorProduct.dualDistribEquivOfBasis : {ι : Type u_1} →
  {R : Type u_2} →
    {κ : ι → Type u_3} →
      {M : ι → Type u_4} →
        [inst : CommRing R] →
          [inst_1 : (i : ι) → AddCommGroup (M i)] →
            [inst_2 : (i : ι) → Module R (M i)] →
              [Finite ι] →
                [∀ (i : ι), Finite (κ i)] →
                  ((i : ι) → Module.Basis (κ i) R (M i)) →
                    (PiTensorProduct R fun i => Module.Dual R (M i)) ≃ₗ[R]
                      Module.Dual R (PiTensorProduct R fun i => M i)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftEq.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] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (l l' : L₁ ⟶ L₂) (h : l = l'),
  CategoryTheory.Comma.mapLeftEq R l l' h = CategoryTheory.Comma.mapLeftEq R l l' h
-- Mathlib.RingTheory.Nullstellensatz
MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton : ∀ {K : Type u_2} [inst : Field K] {σ : Type u_3} [IsAlgClosed K] [Finite σ] {I : Ideal (MvPolynomial σ K)},
  I.IsMaximal ↔ ∃ x, I = MvPolynomial.vanishingIdeal K {x}
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.foldlM.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    {δ : Type u_4} →
      (motive : δ → Std.DHashMap.Internal.AssocList α β → Sort u_3) →
        (x : δ) →
          (x_1 : Std.DHashMap.Internal.AssocList α β) →
            ((d : δ) → motive d Std.DHashMap.Internal.AssocList.nil) →
              ((d : δ) →
                  (a : α) →
                    (b : β a) →
                      (es : Std.DHashMap.Internal.AssocList α β) →
                        motive d (Std.DHashMap.Internal.AssocList.cons a b es)) →
                motive x x_1
-- Init.Data.Nat.Div.Lemmas
Nat.succ_div_of_dvd : ∀ {a b : ℕ}, b ∣ a + 1 → (a + 1) / b = a / b + 1
-- Mathlib.Analysis.RCLike.Lemmas
RCLike.ofRealCLM_norm : ∀ {K : Type u_1} [inst : RCLike K], ‖RCLike.ofRealCLM‖ = 1
-- Mathlib.Analysis.Normed.Ring.Lemmas
NonUnitalSeminormedRing.toContinuousMul : ∀ {α : Type u_1} [inst : NonUnitalSeminormedRing α], ContinuousMul α
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_eq_getD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {a fallback : α}
  {h : a ∈ t}, t.get a h = t.getD a fallback
-- Mathlib.Topology.Algebra.Group.Basic
instContinuousNegULift : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Neg G] [ContinuousNeg G], ContinuousNeg (ULift.{u_1, w} G)
-- Mathlib.Data.FunLike.Basic
DFunLike.congr_fun : ∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f g : F}, f = g → ∀ (x : α), f x = g x
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
/-- If `s : X.S` and `t : X.S` are simplices of a simplicial set, `s ≤ t` means
that the subcomplex generated by `s` is contained in the subcomplex generated by `t`,
see `SSet.S.le_def` and `SSet.S.le_iff`. Note that the
category structure on `X.S` induced by this preorder is not
the "category of simplices" of `X` (which is see `X.Elementsᵒᵖ`);
see `SSet.S.le_iff_nonempty_hom` for the precise relation.  -/
SSet.S.instPreorder : {X : SSet} → Preorder X.S
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
AddAction.IsMultiplyPreprimitive.of_bijective_map : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {N : Type u_3} {β : Type u_4}
  [inst_2 : AddGroup N] [inst_3 : AddAction N β] {φ : M → N} {f : α →ₑ[φ] β},
  Function.Bijective ⇑f → ∀ {n : ℕ}, AddAction.IsMultiplyPreprimitive M α n → AddAction.IsMultiplyPreprimitive N β n
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
AlgebraicGeometry.ValuativeCommSq.mk.injEq : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (R : Type u) [commRing : CommRing R] [domain : IsDomain R]
  [valuationRing : ValuationRing R] (K : Type u) [field : Field K] [algebra : Algebra R K]
  [isFractionRing : IsFractionRing R K] (i₁ : AlgebraicGeometry.Spec (CommRingCat.of K) ⟶ X)
  (i₂ : AlgebraicGeometry.Spec (CommRingCat.of R) ⟶ Y)
  (commSq : CategoryTheory.CommSq i₁ (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R K))) f i₂)
  (R_1 : Type u) (commRing_1 : CommRing R_1) (domain_1 : IsDomain R_1) (valuationRing_1 : ValuationRing R_1)
  (K_1 : Type u) (field_1 : Field K_1) (algebra_1 : Algebra R_1 K_1) (isFractionRing_1 : IsFractionRing R_1 K_1)
  (i₁_1 : AlgebraicGeometry.Spec (CommRingCat.of K_1) ⟶ X) (i₂_1 : AlgebraicGeometry.Spec (CommRingCat.of R_1) ⟶ Y)
  (commSq_1 : CategoryTheory.CommSq i₁_1 (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (algebraMap R_1 K_1))) f i₂_1),
  ({ R := R, commRing := commRing, domain := domain, valuationRing := valuationRing, K := K, field := field,
        algebra := algebra, isFractionRing := isFractionRing, i₁ := i₁, i₂ := i₂, commSq := commSq } =
      { R := R_1, commRing := commRing_1, domain := domain_1, valuationRing := valuationRing_1, K := K_1,
        field := field_1, algebra := algebra_1, isFractionRing := isFractionRing_1, i₁ := i₁_1, i₂ := i₂_1,
        commSq := commSq_1 }) =
    (R = R_1 ∧ commRing ≍ commRing_1 ∧ K = K_1 ∧ field ≍ field_1 ∧ algebra ≍ algebra_1 ∧ i₁ ≍ i₁_1 ∧ i₂ ≍ i₂_1)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.toGraphviz.invEdgeStyle : Bool → String
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.coneOfPreserves_pt_right : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (F : CategoryTheory.Functor J (CategoryTheory.Comma L R))
  [inst_4 : CategoryTheory.Limits.PreservesLimit (F.comp (CategoryTheory.Comma.snd L R)) R]
  (c₁ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.fst L R)))
  {c₂ : CategoryTheory.Limits.Cone (F.comp (CategoryTheory.Comma.snd L R))} (t₂ : CategoryTheory.Limits.IsLimit c₂),
  (CategoryTheory.Comma.coneOfPreserves F c₁ t₂).pt.right = c₂.pt
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.coe_addMonoidHom_id : ∀ {α : Type u_2} [inst : NonUnitalNonAssocSemiring α], ↑(NonUnitalRingHom.id α) = AddMonoidHom.id α
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioo_inter_Ioc_of_right_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a₁ a₂ b₁ b₂ : α},
  b₂ < b₁ → Set.Ioo a₁ b₁ ∩ Set.Ioc a₂ b₂ = Set.Ioc (max a₁ a₂) b₂
-- Mathlib.Topology.LocallyClosed
IsLocallyClosed.isOpen_preimage_val_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsLocallyClosed s → IsOpen (Subtype.val ⁻¹' s)
-- Batteries.CodeAction.Match
/-- Invoking tactic code action `Generate a list of alternatives for this match.` in the
following:
```lean
def myfun2 (n : Nat) : Nat :=
  match n
```
produces:
```lean
def myfun2 (n : Nat) : Nat :=
  match n with
  | 0 => _
  | n + 1 => _
```
Also has support for multiple discriminants, e.g.
```
def myfun3 (o : Option Bool) (m : Nat) : Nat :=
  match o, m with
```
can be expanded into
```
def myfun3 (o : Option Bool) (m : Nat) : Nat :=
  match o, m with
  | none, 0 => _
  | none, n_2 + 1 => _
  | some val_1, 0 => _
  | some val_1, n_2 + 1 => _
```
If it makes sense to use at least one of the constructors with `@` (i.e. iff it has an
implicit non-parameter argument) then we also show a codeaction that expands every such constructor
with implicit arguments filled in with the syntax `implicitArg := implicitArg`.
E.g. invoking `Generate a list of equations with implicit arguments for this match.` in
the following
```lean
inductive TermWithImplicit (F : Nat → Type u) (α : Type w)
  | var (x : α) : TermWithImplicit F α
  | func {l : Nat} (f : F l) (ts : Fin l → TermWithImplicit F α) : TermWithImplicit F α

def myfun4 (t : TermWithImplicit F α) : Nat := by
  match t with
```
produces
```lean
def myfun4 (t : TermWithImplicit F α) : Nat := by
  match t with
  | .var x => _
  | .func (l := l) f ts => _
```
where the implicit argument `{l : Nat}` is now usable.
Note that the arguments `F` and `α` are not filled since they are `parameters`
(a parameter is an argument to an inductive type that is fixed over constructors), i.e.
they are already determined by the match discriminant `t`. This means they don't provide any
new information for you.
 -/
Batteries.CodeAction.matchExpand : Lean.CodeAction.CommandCodeAction
-- Mathlib.Data.Fintype.Basic
/-- Short-circuit instance to decrease search for `Unique.fintype`,
since that relies on a subsingleton elimination for `Unique`.  -/
Fintype.subtypeEq' : {α : Type u_1} → (y : α) → Fintype { x // y = x }
-- Batteries.Data.Char.AsciiCasing
Char.isAlpha_toUpper_eq_isAlpha : ∀ (c : Char), c.toUpper.isAlpha = c.isAlpha
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.comp_toLinearMap_symm_eq : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₂₃ : R₂ →+* R₃} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} [inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂}
  [inst_7 : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₃] M₃),
  g ∘ₛₗ ↑e₁₂.symm = f ↔ g = f ∘ₛₗ ↑e₁₂
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.toCoalgEquiv : {R : Type u} →
  [inst : CommSemiring R] →
    {A : Type v} →
      {B : Type w} →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → (A ≃ₐc[R] B) → A ≃ₗc[R] B
-- Lean.Meta.Basic
Lean.Meta.AbstractMVarsResult.mk.injEq : ∀ (paramNames : Array Lean.Name) (mvars : Array Lean.Expr) (expr : Lean.Expr) (paramNames_1 : Array Lean.Name)
  (mvars_1 : Array Lean.Expr) (expr_1 : Lean.Expr),
  ({ paramNames := paramNames, mvars := mvars, expr := expr } =
      { paramNames := paramNames_1, mvars := mvars_1, expr := expr_1 }) =
    (paramNames = paramNames_1 ∧ mvars = mvars_1 ∧ expr = expr_1)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
UniqueFactorizationMonoid.hasFiniteMulSupport_fun_pow_multiplicity : ∀ {R : Type u_2} [inst : CommMonoidWithZero R] [UniqueFactorizationMonoid R] {α : Type u_3} {M : Type u_4}
  [inst_2 : CommMonoid M] [Subsingleton Rˣ] (f : α → M) {g : α → R},
  Function.Injective g →
    (∀ (s : α), Irreducible (g s)) → ∀ {r : R}, r ≠ 0 → Function.HasFiniteMulSupport fun s => f s ^ multiplicity (g s) r
-- Mathlib.Order.Interval.Set.Basic
Set.Iio_eq_empty_iff : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Iio a = ∅ ↔ IsMin a
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unop_tensorHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X₁ Y₁ X₂ Y₂ : Cᵒᵖ} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).unop =
    CategoryTheory.MonoidalCategoryStruct.tensorHom f.unop g.unop
-- Init.Data.Int.Lemmas
Int.neg_negSucc : ∀ (n : ℕ), -Int.negSucc n = ↑(n + 1)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey!_union : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, (m₁ ∪ m₂).getKey! k = m₂.getKeyD k (m₁.getKey! k)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaValues
riemannZeta_four : riemannZeta 4 = ↑Real.pi ^ 4 / 90
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.addEntryImpl : Lean.Parser.ParserExtension.State → Lean.Parser.ParserExtension.Entry → Lean.Parser.ParserExtension.State
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- The composition of right adjoint mates is the adjoint mate of the composition.  -/
CategoryTheory.comp_rightAdjointMate : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
  [inst_2 : CategoryTheory.HasRightDual X] [inst_3 : CategoryTheory.HasRightDual Y]
  [inst_4 : CategoryTheory.HasRightDual Z] {f : X ⟶ Y} {g : Y ⟶ Z},
  CategoryTheory.CategoryStruct.comp f gᘁ = CategoryTheory.CategoryStruct.comp (gᘁ) (fᘁ)
-- Mathlib.Data.Set.Insert
Prop.compl_singleton : ∀ (p : Prop), {p}ᶜ = {¬p}
-- Init.Data.Nat.Lemmas
Nat.one_shiftLeft : ∀ (n : ℕ), 1 <<< n = 2 ^ n
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
/-- The `P`-`qc`-topology on the category of schemes wrt. to a morphism property `P` is the
topology generated by quasi-compact covers satisfying `P`.  -/
AlgebraicGeometry.Scheme.propQCTopology : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme → CategoryTheory.GrothendieckTopology AlgebraicGeometry.Scheme
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Node.entries.injEq : ∀ {α : Type u} {β : Type v} (es es_1 : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))),
  (Lean.PersistentHashMap.Node.entries es = Lean.PersistentHashMap.Node.entries es_1) = (es = es_1)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.mem_of_get_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {k v : α} {w : k ∈ t}, t.get k w = v → k ∈ t
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- The doubling constant `σ[A, B]` of two finsets `A` and `B` in a group is `|A + B| / |A|`.

The notation `σ[A, B]` is available in scope `Combinatorics.Additive`.  -/
Finset.addConst : {G : Type u_1} → [AddGroup G] → [DecidableEq G] → Finset G → Finset G → ℚ≥0
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.stabilizerAddSubmonoid.eq_1 : ∀ (M : Type u_1) {α : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M α] (a : α),
  AddAction.stabilizerAddSubmonoid M a = { carrier := {m | m +ᵥ a = a}, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.ofι_π_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) (P : C) (ι : (a : J.L) → P ⟶ I.left a)
  (w :
    ∀ (b : J.R),
      CategoryTheory.CategoryStruct.comp (ι (J.fst b)) (I.fst b) =
        CategoryTheory.CategoryStruct.comp (ι (J.snd b)) (I.snd b))
  (x : CategoryTheory.Limits.WalkingMulticospan J),
  (CategoryTheory.Limits.Multifork.ofι I P ι w).π.app x =
    match x with
    | CategoryTheory.Limits.WalkingMulticospan.left a => ι a
    | CategoryTheory.Limits.WalkingMulticospan.right b => CategoryTheory.CategoryStruct.comp (ι (J.fst b)) (I.fst b)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- A functor which preserves homology preserves kernels.  -/
CategoryTheory.Functor.PreservesHomology.preservesKernel : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] [F.PreservesHomology] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F
-- Mathlib.Topology.Order.LocalExtr
isLocalExtrOn_const : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {s : Set α} {a : α} {b : β},
  IsLocalExtrOn (fun x => b) s a
-- Init.Data.Vector.Lemmas
Vector.mem_iff_getElem : ∀ {α : Type u_1} {n : ℕ} {a : α} {xs : Vector α n}, a ∈ xs ↔ ∃ i, ∃ (h : i < n), xs[i] = a
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.algEquivCMulXAddC_symm_apply : ∀ {R : Type u_3} [inst : CommRing R] (a b : R) [inst_1 : Invertible a] (a_1 : Polynomial R),
  (Polynomial.algEquivCMulXAddC a b).symm a_1 =
    (Polynomial.aeval (Polynomial.C ⅟a * (Polynomial.X - Polynomial.C b))) a_1
-- Mathlib.NumberTheory.FLT.Basic
fermatLastTheoremWith'_of_semifield : ∀ (𝕜 : Type u_2) [inst : Semifield 𝕜] (n : ℕ), FermatLastTheoremWith' 𝕜 n
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {k a : α}, (t.insert k).get! a = if cmp k a = Ordering.eq ∧ k ∉ t then k else t.get! a
-- Mathlib.Data.Ordmap.Ordnode
/-- Auxiliary definition for `drop`. (Can also be used in lieu of `drop` if you know the
index is within the range of the data structure.)

```
drop_aux {a, b, c, d} 2 = {c, d}
drop_aux {a, b, c, d} 5 = ∅
```  -/
Ordnode.dropAux : {α : Type u_1} → Ordnode α → ℕ → Ordnode α
-- Mathlib.Algebra.GCDMonoid.Nat
/-- `ℕ` is a `GCDMonoid`.  -/
instGCDMonoidNat : GCDMonoid ℕ
-- Mathlib.Algebra.Order.Sub.Defs
lt_tsub_of_add_lt_right : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftReflectLE α], a + c < b → a < b - c
-- Mathlib.Topology.Semicontinuity.Defs
lowerSemicontinuousAt_const : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {x : α} {z : β},
  LowerSemicontinuousAt (fun _x => z) x
-- Mathlib.Data.Rat.Init
NNRat.num_mk : ∀ (q : ℚ) (hq : 0 ≤ q), NNRat.num ⟨q, hq⟩ = q.num.natAbs
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- Taking the negative commutes with taking `meromorphicTrailingCoeffAt`.
 -/
meromorphicTrailingCoeffAt_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E}, meromorphicTrailingCoeffAt (-f) x = -meromorphicTrailingCoeffAt f x
-- Std.Time.Duration
/-- Second offset of the duration.
 -/
Std.Time.Duration.second : Std.Time.Duration → Std.Time.Second.Offset
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Append.0.Std.Iterators.Types.Append.instIterator.match_1.splitter : {m : Type u_1 → Type u_2} →
  {β α₁ : Type u_1} →
    [inst : Std.Iterator α₁ m β] →
      (it₁ : Std.IterM m β) →
        (motive : it₁.Step → Sort u_3) →
          (x : it₁.Step) →
            ((it₁' : Std.IterM m β) →
                (out : β) →
                  (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, h⟩) →
              ((it₁' : Std.IterM m β) →
                  (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩) →
                ((h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.prod_lt_one' : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {f : ι → M}
  {s : Finset ι} [MulLeftStrictMono M], (∀ i ∈ s, f i ≤ 1) → (∃ i ∈ s, f i < 1) → ∏ i ∈ s, f i < 1
-- Lean.Util.Recognizers
Lean.Expr.and? : Lean.Expr → Option (Lean.Expr × Lean.Expr)
-- Mathlib.CategoryTheory.Bicategory.LocallyDiscrete
/-- `LocallyDiscrete C` is equivalent to the original type `C`.  -/
CategoryTheory.LocallyDiscrete.locallyDiscreteEquiv : {C : Type u} → CategoryTheory.LocallyDiscrete C ≃ C
-- Mathlib.NumberTheory.ArithmeticFunction.Liouville
ArithmeticFunction.liouville_apply_mul : ∀ (m n : ℕ), ArithmeticFunction.liouville (m * n) = ArithmeticFunction.liouville m * ArithmeticFunction.liouville n
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm : ∀ {α : Type u_1} {F : Type u_3} {F' : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (T : Set α → F →L[ℝ] F') {C : ℝ},
  (∀ (s : Set α), MeasurableSet s → ‖T s‖ ≤ C * μ.real s) →
    ∀ (f : MeasureTheory.SimpleFunc α F),
      ‖MeasureTheory.SimpleFunc.setToSimpleFunc T f‖ ≤ C * ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) * ‖x‖
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instCommGroup : {α : Type u_1} → [CommGroup α] → CommGroup (Colex α)
-- Mathlib.Data.Sym.Sym2
/-- This is a predicate that determines whether a given term is a member of a term of the
symmetric square.  From this point of view, the symmetric square is the subtype of
cardinality-two multisets on `α`.
 -/
Sym2.Mem : {α : Type u_1} → α → Sym2 α → Prop
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_dvd_leadingCoeff_pow : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] (f g : Polynomial R),
  IsCoprime f g → ∃ n, f.resultant g ∣ f.leadingCoeff ^ n
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.prod.eq_1 : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] (s : AddSubmonoid M)
  (t : AddSubmonoid N), s.prod t = { carrier := ↑s ×ˢ ↑t, add_mem' := ⋯, zero_mem' := ⋯ }
-- Init.Data.Vector.Count
Vector.count_replicate : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α} {n : ℕ},
  Vector.count a (Vector.replicate n b) = if (b == a) = true then n else 0
-- Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology
/-- **Alias** of the reverse direction of `ContinuousLinearMapWOT.continuousOn_iff`. -/
ContinuousLinearMapWOT.continuousOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E]
  [inst_3 : Module 𝕜 E] [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F] [CompleteSpace F]
  {α : Type u_4} [inst_7 : TopologicalSpace α] {f : α → E →WOT[𝕜] F} {s : Set α},
  (∀ (x : E) (y : F), ContinuousOn (fun x_1 => inner 𝕜 y ((f x_1) x)) s) → ContinuousOn f s