mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Polynomial.Basic
/-- `polynomial` solves equalities of `Polynomial`s and similar types.

Given a goal which is an equality in `Polynomial R` with a commutative ring `R`, `polynomial`
turns both sides of the equation into a normal form by expanding out the brackets. It then closes
the goal if both sides contain the same terms and fails otherwise. `polynomial_nf` normalizes all
subexpressions at a given location.

Variants of `polynomial` include:
* `polynomial`: normalize both sides of an equation and close the goal if they are equal
* `polynomial!`: run `polynomial` at default transparency
* `polynomial_nf`: normalize all subexpression of the goal
* `polynomial_nf at h₁ h₂ ⊢`: normalize all subexpressions at hypotheses `h₁` `h₁` and the goal
* `polynomial_nf at *`: normalize all subexpressions of all local hypotheses and the goal
* `polynomial_nf!`: run `polynomial_nf` at default transparency

The `polynomial` tactic can be extended to work with algebras other than `Polynomial` using the
attributes `polynomial_infer_base`, `polynomial_pre` and `polynomial_post`. This is only possible
if the base ring can be inferred from the structure of the type.

Examples:

```
example (a : ℚ) : (X + C a) * (X - C a) = X^2 + C (a^2) := by polynomial

example {P : ℚ[X] → Prop} (h : P (X ^ 2 + X + C 4⁻¹)) : P ((X + C 2⁻¹) ^ 2) := by
  polynomial_nf at h ⊢
  exact h
```

 -/
Mathlib.Tactic.Polynomial.tacticPolynomial! : Lean.ParserDescr
-- Init.Data.Option.Lemmas
Option.isSome_iff_ne_none : ∀ {α : Type u_1} {o : Option α}, o.isSome = true ↔ o ≠ none
-- Lean.Meta.Sym.InstantiateS
/-- Similar to `Lean.Expr.instantiateRev`.
It assumes the input is maximally shared, and ensures the output is too.
 -/
Lean.Meta.Sym.instantiateRevS : Lean.Expr → Array Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Init.Prelude
/-- The value must be a legal scalar value.  -/
Char.valid : ∀ (self : Char), self.val.isValidChar
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_lt_of_lt_ofReal : ∀ {a : ENNReal} {b : ℝ}, a < ENNReal.ofReal b → a.toReal < b
-- Mathlib.RingTheory.Valuation.RankOne
/-- A nontrivial unit of `Γ₀`, given that there exists a rank one `v : Valuation R Γ₀`.  -/
Valuation.RankOne.unit : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : Ring R] → [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → (v : Valuation R Γ₀) → [hv : v.RankOne] → Γ₀ˣ
-- ProofWidgets.Component.PenroseDiagram
ProofWidgets.Penrose.DiagramProps.mk.sizeOf_spec : ∀ (embeds : Array (String × ProofWidgets.Html)) (dsl sty sub : String) (maxOptSteps : ℕ),
  sizeOf { embeds := embeds, dsl := dsl, sty := sty, sub := sub, maxOptSteps := maxOptSteps } =
    1 + sizeOf embeds + sizeOf dsl + sizeOf sty + sizeOf sub + sizeOf maxOptSteps
-- Mathlib.GroupTheory.Goursat
AddSubgroup.goursatFst_prod_goursatSnd_le : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (I : AddSubgroup (G × H)),
  I.goursatFst.prod I.goursatSnd ≤ I
-- Batteries.Data.AssocList
Batteries.AssocList.mapKey.eq_1 : ∀ {α : Type u_1} {δ : Type u_2} {β : Type u_3} (f : α → δ),
  Batteries.AssocList.mapKey f Batteries.AssocList.nil = Batteries.AssocList.nil
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
SeminormFamily.withSeminorms_of_nhds : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [t : TopologicalSpace E] [IsTopologicalAddGroup E] (p : SeminormFamily 𝕜 E ι),
  nhds 0 = p.moduleFilterBasis.filter → WithSeminorms p
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey!_eq_getElem!_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.minKey! = t.keysArray[0]!
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.div_eq_empty : ∀ {α : Type u_2} [inst : Div α] {s t : Set α}, s / t = ∅ ↔ s = ∅ ∨ t = ∅
-- Init.Data.Array.Erase
Array.set_eraseIdx_gt : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {w : i < xs.size} {j : ℕ} {a : α} (h : j < i) (hj : j < (xs.eraseIdx i w).size),
  (xs.eraseIdx i w).set j a hj = (xs.set j a ⋯).eraseIdx i ⋯
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey!_eq_get!_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {a : α}, t.getKey! a = (t.getKey? a).get!
-- Mathlib.CategoryTheory.Limits.Skeleton
CategoryTheory.Limits.hasLimitsOfSize_skeleton : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] [CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₂, u₂} C],
  CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₂, u₂} (CategoryTheory.Skeleton C)
-- Mathlib.Data.Nat.Log
Nat.clog_eq_clog_succ_iff : ∀ {b n : ℕ}, 1 < b → (Nat.clog b n = Nat.clog b (n + 1) ↔ b ^ Nat.clog b n ≠ n)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- The second map of a short complex, as a functor.  -/
CategoryTheory.ShortComplex.gFunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      CategoryTheory.Functor (CategoryTheory.ShortComplex C) (CategoryTheory.Arrow C)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.compCLMOfContinuousLinearEquiv_apply : ∀ (𝕜 : Type u_2) {D : Type u_4} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : RCLike 𝕜] [inst_5 : NormedAddCommGroup D]
  [inst_6 : NormedSpace ℝ D] [inst_7 : NormedSpace 𝕜 F] (g : D ≃L[ℝ] E) (f : SchwartzMap E F),
  ⇑((SchwartzMap.compCLMOfContinuousLinearEquiv 𝕜 g) f) = ⇑f ∘ ⇑g
-- Mathlib.Topology.UniformSpace.UniformConvergence
tendstoUniformly_iff_seq_tendstoUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {l : Filter ι}
  [l.IsCountablyGenerated],
  TendstoUniformly F f l ↔
    ∀ (u : ℕ → ι), Filter.Tendsto u Filter.atTop l → TendstoUniformly (fun n => F (u n)) f Filter.atTop
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothPartitionOfUnity.locallyFinite : ∀ {ι : Type uι} {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH}
  [inst_2 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M]
  [inst_4 : ChartedSpace H M] {s : Set M} (f : SmoothPartitionOfUnity ι I M s),
  LocallyFinite fun i => Function.support ⇑(f i)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.codeSupp'.eq_3 : ∀ (x : Turing.PartrecToTM2.Cont'),
  Turing.PartrecToTM2.codeSupp' Turing.ToPartrec.Code.tail x =
    Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.trNormal Turing.ToPartrec.Code.tail x)
-- Mathlib.Algebra.Polynomial.RingDivision
/-- See `Polynomial.rootMultiplicity_eq_natTrailingDegree'` for the special case of `t = 0`.  -/
Polynomial.rootMultiplicity_eq_natTrailingDegree : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R},
  Polynomial.rootMultiplicity t p = (p.comp (Polynomial.X + Polynomial.C t)).natTrailingDegree
-- Mathlib.Data.Finset.Erase
Finset.mem_of_mem_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a b : α}, b ∈ s.erase a → b ∈ s
-- Mathlib.Order.LiminfLimsup
Filter.HasBasis.limsInf_eq_iSup_sInf : ∀ {α : Type u_1} {ι : Type u_4} [inst : CompleteLattice α] {p : ι → Prop} {s : ι → Set α} {f : Filter α},
  f.HasBasis p s → f.limsInf = ⨆ i, ⨆ (_ : p i), sInf (s i)
-- Mathlib.Algebra.Order.Ring.StandardPart
/-- The standard part of `x` is the unique real `r` such that `x - r` is infinitesimal.  -/
ArchimedeanClass.mk_sub_pos_iff : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x : K} (f : ℝ →+*o K) {r : ℝ},
  0 ≤ ArchimedeanClass.mk x → (0 < ArchimedeanClass.mk (x - f r) ↔ ArchimedeanClass.stdPart x = r)
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₂₃_inv_app_assoc : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁) (f₁₂ : b₁ ⟶ b₂)
  (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃) (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂)
  (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃) (hf : CategoryTheory.CategoryStruct.comp f₀₂ f₂₃ = f)
  (X : ↑(F.obj b₀)) {Z : ↑(F.obj b₃)} (h : (F.map f).toFunctor.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₂ f₂₃ f ⋯).inv.toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((F.map f₂₃).toFunctor.map ((F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom.toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp
        ((F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv.toNatTrans.app ((F.map f₀₁).toFunctor.obj X))
        (CategoryTheory.CategoryStruct.comp ((F.mapComp' f₀₁ f₁₃ f ⋯).inv.toNatTrans.app X) h))
-- Mathlib.Data.Prod.Basic
Function.Surjective.prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ},
  Function.Surjective f → Function.Surjective g → Function.Surjective (Prod.map f g)
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IsIndObject.finallySmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)},
  CategoryTheory.Limits.IsIndObject A →
    CategoryTheory.FinallySmall (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.equiv_iff_toList_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁.Equiv t₂ ↔ Std.DTreeMap.Raw.Const.toList t₁ = Std.DTreeMap.Raw.Const.toList t₂)
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_neg : ∀ {R' : Type u_2} {A : Type u_3} {B : Type u_5} [inst : Ring R'] [inst_1 : SemilatticeSup B] [inst_2 : OrderBot B]
  {D : A → B} {f : AddMonoidAlgebra R' A}, AddMonoidAlgebra.supDegree D (-f) = AddMonoidAlgebra.supDegree D f
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.or_congr : ∀ {σs : List (Type u)} {P P' Q Q' : Std.Do.SPred σs}, (P ⊣⊢ₛ P') → (Q ⊣⊢ₛ Q') → P ∨ Q ⊣⊢ₛ P' ∨ Q'
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.State.continue.injEq : ∀ {dir : Std.Http.Protocol.H1.Direction} (a a_1 : Std.Http.Protocol.H1.Reader.State dir),
  (a.continue = a_1.continue) = (a = a_1)
-- Mathlib.Order.Category.PartOrdEmb
_private.Mathlib.Order.Category.PartOrdEmb.0.PartOrdEmb.Hom.mk.injEq : ∀ {X Y : PartOrdEmb} (hom' hom'_1 : ↑X ↪o ↑Y), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.Pattern.Model.splitFromSteps.eq_2 : ∀ {s : String.Slice} (currPos startPos endPos : s.Pos) (l_2 : List (String.Slice.Pattern.SearchStep s)),
  String.Slice.Pattern.Model.splitFromSteps✝ currPos (String.Slice.Pattern.SearchStep.rejected startPos endPos :: l_2) =
    String.Slice.Pattern.Model.splitFromSteps✝ currPos l_2
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
algebraMap_le_cfc_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalRing R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A]
  (f : R → R) (r : R) (a : A),
  autoParam (ContinuousOn f (spectrum R a)) algebraMap_le_cfc_iff._auto_1 →
    autoParam (p a) algebraMap_le_cfc_iff._auto_3 → ((algebraMap R A) r ≤ cfc f a ↔ ∀ x ∈ spectrum R a, r ≤ f x)
-- Init.Grind.AC
Lean.Grind.AC.Seq.eraseDup_k.eq_1 : ∀ (s : Lean.Grind.AC.Seq),
  s.eraseDup_k =
    Lean.Grind.AC.Seq.rec (fun x => Lean.Grind.AC.Seq.var x)
      (fun x x_1 ih =>
        Lean.Grind.AC.Seq.rec
          (fun y =>
            Bool.rec (Lean.Grind.AC.Seq.cons x (Lean.Grind.AC.Seq.var y)) (Lean.Grind.AC.Seq.var x) (Nat.beq x y))
          (fun y s' x_2 =>
            Bool.rec (Lean.Grind.AC.Seq.cons x (Lean.Grind.AC.Seq.cons y s')) (Lean.Grind.AC.Seq.cons y s')
              (Nat.beq x y))
          ih)
      s
-- Mathlib.Algebra.Homology.Bifunctor
HomologicalComplex.mapBifunctor.d₁_eq_zero' : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [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] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : K₁.HasMapBifunctor K₂ F c] [inst_10 : DecidableEq J] {i₁ i₁' : I₁},
  c₁.Rel i₁ i₁' →
    ∀ (i₂ : I₂) (j : J), c₁.π c₂ c (i₁', i₂) ≠ j → HomologicalComplex.mapBifunctor.d₁ K₁ K₂ F c i₁ i₂ j = 0
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.pack.eq_1 : ∀ (spec : Float.Model.Format),
  Float.Model.UnpackedFloat.pack spec Float.Model.UnpackedFloat.notANumber = Float.Model.UnpackedFloat.packedNaN spec
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.EMatchTheoremKind.isEqLhs : Lean.Meta.Grind.EMatchTheoremKind → Bool
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
/-- [Stacks Tag 030H](https://stacks.math.columbia.edu/tag/030H) -/
lift_trdeg_add_eq : ∀ (R : Type u_1) (S : Type v) (A : Type w) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] [Nontrivial R]
  [NoZeroDivisors A] [FaithfulSMul R S] [FaithfulSMul S A],
  Cardinal.lift.{w, v} (Algebra.trdeg R S) + Cardinal.lift.{v, w} (Algebra.trdeg S A) =
    Cardinal.lift.{v, w} (Algebra.trdeg R A)
-- Lean.Expr
Lean.Expr.appArg! : Lean.Expr → Lean.Expr
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
_private.Mathlib.RingTheory.SimpleModule.WedderburnArtin.0.IsSemiprimaryRing.mulOpposite : {R : Type u} → [inst : Ring R] → [IsSemiprimaryRing R] → ProofWanted (IsSemiprimaryRing Rᵐᵒᵖ)
-- Lean.Elab.Term.TermElabM
/-- Extracts a `BodyInfo` custom info.  -/
Lean.Elab.Term.getBodyInfo? : Lean.Elab.Info → Option Lean.Elab.Term.BodyInfo
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- Constants (and let-declaration `FVarId`) to unfold.
When `zetaDelta := false`, the simplifier will expand a let-declaration if it is in this set.
 -/
Lean.Meta.SimpTheorems.toUnfold : Lean.Meta.SimpTheorems → Lean.PHashSet Lean.Name
-- Mathlib.NumberTheory.Height.Basic
/-- The multiplicative height of a product of field elements is bounded above by the product
of their multiplicative heights.  -/
Height.mulHeight₁_prod_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} (s : Finset ι) (x : ι → K),
  Height.mulHeight₁ (∏ i ∈ s, x i) ≤ ∏ i ∈ s, Height.mulHeight₁ (x i)
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec.toPresheafedSpace_map_op : ∀ (R S : CommRingCat) (f : R ⟶ S),
  AlgebraicGeometry.Spec.toPresheafedSpace.map f.op = (AlgebraicGeometry.Spec.sheafedSpaceMap f).hom
-- Mathlib.Algebra.Order.Module.Defs
smul_eq_smul_iff_eq_and_eq_of_pos' : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b₁ b₂ : β} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β]
  [inst_3 : PartialOrder α] [inst_4 : PartialOrder β] [PosSMulStrictMono α β] [SMulPosStrictMono α β],
  a₁ ≤ a₂ → b₁ ≤ b₂ → 0 < a₂ → 0 < b₁ → (a₁ • b₁ = a₂ • b₂ ↔ a₁ = a₂ ∧ b₁ = b₂)
-- Mathlib.Topology.MetricSpace.Bounded
Metric.comap_dist_left_atTop : ∀ {α : Type u} [inst : PseudoMetricSpace α] (c : α), Filter.comap (dist c) Filter.atTop = Bornology.cobounded α
-- Mathlib.Topology.Order.LeftRight
continuousWithinAt_Ioi_iff_Ici : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : PartialOrder α] [inst_2 : TopologicalSpace β]
  {a : α} {f : α → β}, ContinuousWithinAt f (Set.Ioi a) a ↔ ContinuousWithinAt f (Set.Ici a) a
-- Mathlib.Data.List.Forall2
List.rel_foldl : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {R : α → β → Prop} {P : γ → δ → Prop},
  Relator.LiftFun (Relator.LiftFun P (Relator.LiftFun R P)) (Relator.LiftFun P (Relator.LiftFun (List.Forall₂ R) P))
    List.foldl List.foldl
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- The restriction map from `α →ᵤ[𝔖] β` to `⋃₀ 𝔖 → β` is uniformly continuous.  -/
UniformOnFun.uniformContinuous_restrict_toFun : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace β] {𝔖 : Set (Set α)},
  UniformContinuous ((⋃₀ 𝔖).domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖))
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.addConst.eq_2 : ∀ (k k_1 : ℤ) (v : Int.Internal.Linear.Var) (p_2 : Int.Internal.Linear.Poly),
  (Int.Internal.Linear.Poly.add k_1 v p_2).addConst k = Int.Internal.Linear.Poly.add k_1 v (p_2.addConst k)
-- Mathlib.Data.Nat.Factorization.Root
Nat.floorRoot_ne_zero : ∀ {a n : ℕ}, n.floorRoot a ≠ 0 ↔ n ≠ 0 ∧ a ≠ 0
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.flipFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  CategoryTheory.Square.flipFunctor.obj sq = sq.flip
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.d : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.Day.Ordinal
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainTopCoeff_chainTopIdx : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  RootPairing.chainTopCoeff i (RootPairing.chainTopIdx i j) = 0
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.BasicConstructibleSetData.toSet.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (C : PrimeSpectrum.BasicConstructibleSetData R),
  C.toSet = PrimeSpectrum.zeroLocus (Set.range C.g) \ PrimeSpectrum.zeroLocus {C.f}
-- Mathlib.LinearAlgebra.Matrix.Trace
/-- Matrices `A` and `B` are equal iff `(x * A).trace = (x * B).trace` for all `x`.  -/
Matrix.ext_iff_trace_mul_left : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_6} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : NonAssocSemiring R]
  {A B : Matrix m n R}, A = B ↔ ∀ (x : Matrix n m R), (x * A).trace = (x * B).trace
-- Std.Data.DTreeMap.Internal.Ordered
Std.DTreeMap.Internal.Impl.Ordered.compare_left : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {sz : ℕ} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.inner sz k v l r).Ordered →
    ∀ {k' : (a : α) × β a}, k' ∈ l.toListModel → compare k'.fst k = Ordering.lt
-- Mathlib.Data.Finsupp.Basic
/-- **Alias** of `Finsupp.filter_add_filter_not`. -/
Finsupp.filter_pos_add_filter_neg : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α →₀ M) (p : α → Prop) [inst_1 : DecidablePred p],
  Finsupp.filter p f + Finsupp.filter (fun x => ¬p x) f = f
-- Mathlib.Order.SymmDiff
Pi.symmDiff_def : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : (i : ι) → GeneralizedCoheytingAlgebra (π i)] (a b : (i : ι) → π i),
  symmDiff a b = fun i => symmDiff (a i) (b i)
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
CommAlgCat.lift_unop_hom : ∀ {R : Type u} [inst : CommRing R] {A B C : (CommAlgCat R)ᵒᵖ} (f : C ⟶ A) (g : C ⟶ B),
  CommAlgCat.Hom.hom (CategoryTheory.CartesianMonoidalCategory.lift f g).unop =
    Algebra.TensorProduct.lift (CommAlgCat.Hom.hom f.unop) (CommAlgCat.Hom.hom g.unop) ⋯
-- Mathlib.Order.SupClosed
ofDual_preimage_latticeClosure : ∀ {α : Type u_3} [inst : Lattice α] (s : Set α),
  ⇑OrderDual.ofDual ⁻¹' latticeClosure s = latticeClosure (⇑OrderDual.ofDual ⁻¹' s)
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.instToMessageDataRelevantArg : Lean.ToMessageData Mathlib.Tactic.Translate.RelevantArg
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normal_subgroupOf : ∀ {G : Type u_1} [inst : Group G] {H N : Subgroup G} [N.Normal], (N.subgroupOf H).Normal
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_Ioc_castLE : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n m : ℕ} (h : n ≤ m) (f : Fin m → M) (a b : Fin n),
  ∑ i ∈ Finset.Ioc (Fin.castLE h a) (Fin.castLE h b), f i = ∑ i ∈ Finset.Ioc a b, f (Fin.castLE h i)
-- Mathlib.GroupTheory.FiniteAbelian.Duality
CommGroup.mem_subgroupOrderIsoSubgroupMonoidHom_iff : ∀ {G : Type u_1} (M : Type u_2) [inst : CommGroup G] [inst_1 : Finite G] [inst_2 : CommMonoid M]
  [hM : HasEnoughRootsOfUnity M (Monoid.exponent G)] (H : Subgroup G) (φ : G →* Mˣ),
  φ ∈ OrderDual.ofDual ((CommGroup.subgroupOrderIsoSubgroupMonoidHom G M) H) ↔ ∀ g ∈ H, φ g = 1
-- Mathlib.CategoryTheory.Limits.Preorder
/-- If a partial order has binary coproducts, then it is a sup-semilattice  -/
Preorder.semilatticeSupOfHasBinaryCoproducts : (C : Type u) → [inst : PartialOrder C] → [CategoryTheory.Limits.HasBinaryCoproducts C] → SemilatticeSup C
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsUniversal.all : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {φ : L.BoundedFormula α (n + 1)}, φ.IsUniversal → φ.all.IsUniversal
-- Mathlib.Algebra.Algebra.Operations
Submodule.instIsReduced : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [IsReduced A], IsReduced (Submodule R A)
-- Mathlib.Topology.Order.PartialSups
Continuous.partialSups : ∀ {L : Type u_1} [inst : SemilatticeSup L] [inst_1 : TopologicalSpace L] [ContinuousSup L] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : ℕ → X → L} {n : ℕ}, (∀ k ≤ n, Continuous (f k)) → Continuous ((partialSups f) n)
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_add_measureReal_compl₀ : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.NullMeasurableSet s μ → μ.real s + μ.real sᶜ = μ.real Set.univ
-- Mathlib.GroupTheory.Index
Subgroup.mul_mem_iff_of_index_two : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, H.index = 2 → ∀ {a b : G}, a * b ∈ H ↔ (a ∈ H ↔ b ∈ H)
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.pow_lt_pow_left : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : CommSemiring α] [inst_2 : PartialOrder α] [OrderBot α]
  [inst_4 : CanonicallyOrderedAdd α] [PosMulStrictMono α] [inst_6 : NoZeroDivisors α] [inst_7 : Nontrivial α]
  {a b : WithTop α}, a < b → ∀ {n : ℕ}, n ≠ 0 → a ^ n < b ^ n
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.lie_le_inf : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I J : LieIdeal R L),
  ⁅I, J⁆ ≤ I ⊓ J
-- Batteries.Data.String.Lemmas
String.Pos.Raw.extract.go₁_cons_addChar : ∀ (c : Char) (cs : List Char) (b e : String.Pos.Raw),
  String.Pos.Raw.extract.go₁ (c :: cs) 0 (b + c) (e + c) = String.Pos.Raw.extract.go₁ cs 0 b e
-- Mathlib.Algebra.Group.Action.Defs
/-- An instance of `IsScalarTower M N α` states that the multiplicative
action of `M` on `α` is determined by the multiplicative actions of `M` on `N`
and `N` on `α`.  -/
IsScalarTower : (M : Type u_9) → (N : Type u_10) → (α : Type u_11) → [SMul M N] → [SMul N α] → [SMul M α] → Prop
-- Batteries.Data.MLList.Basic
MLList.instInhabited : {m : Type u_1 → Type u_1} → {α : Type u_1} → Inhabited (MLList m α)
-- Mathlib.Order.Hom.BoundedLattice
instCoeTCInfTopHomOfInfTopHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Min α] →
          [inst_2 : Min β] → [inst_3 : Top α] → [inst_4 : Top β] → [InfTopHomClass F α β] → CoeTC F (InfTopHom α β)
-- Mathlib.Algebra.Ring.SumsOfSquares
/-- In an additive unital magma with multiplication, `x * x` is a sum of squares for all `x`.  -/
IsSumSq.mul_self : ∀ {R : Type u_1} [inst : AddZeroClass R] [inst_1 : Mul R] (a : R), IsSumSq (a * a)