mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Interval.Finset.Basic
Finset.image_add_left_Ioc : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α]
  [inst_4 : LocallyFiniteOrder α] [inst_5 : DecidableEq α] (a b c : α),
  Finset.image (fun x => c + x) (Finset.Ioc a b) = Finset.Ioc (c + a) (c + b)
-- Mathlib.Topology.Maps.Basic
Topology.IsQuotientMap.of_comp_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Topology.IsQuotientMap f → (Topology.IsQuotientMap (g ∘ f) ↔ Topology.IsQuotientMap g)
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.instIsCardinalFilteredToTypeOrd : ∀ (κ : Cardinal.{w}) [hκ : Fact κ.IsRegular], CategoryTheory.IsCardinalFiltered κ.ord.ToType κ
-- Mathlib.RingTheory.Smooth.AdicCompletion
/-- (Implementation): Lift `A →ₐ[R] S ⧸ I` inductively to `A →ₐ[R] S ⧸ I ^ m` using formal
smoothness.
 -/
_private.Mathlib.RingTheory.Smooth.AdicCompletion.0.Algebra.FormallySmooth.liftAdicCompletionAux : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] →
          {S : Type u_3} →
            [inst_3 : CommRing S] →
              [inst_4 : Algebra R S] →
                (I : Ideal S) → (A →ₐ[R] S ⧸ I) → [Algebra.FormallySmooth R A] → (m : ℕ) → A →ₐ[R] S ⧸ I ^ m
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.coe_prodComm : ∀ (X : Type u) (Y : Type v) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  ⇑(Homeomorph.prodComm X Y) = Prod.swap
-- Mathlib.CategoryTheory.Sites.Point.Presheaf
/-- The functor `C ⥤ Point.{w} (⊥ : GrothendieckTopology C)` which sends
`X : C` to the point corresponding to `X`.  -/
CategoryTheory.GrothendieckTopology.pointBotFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.LocallySmall.{w, v, u} C] → CategoryTheory.Functor C ⊥.Point
-- Mathlib.Order.Category.Preord
_private.Mathlib.Order.Category.Preord.0.Preord.Hom.mk.injEq : ∀ {X Y : Preord} (hom' hom'_1 : ↑X →o ↑Y), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.Data.Set.Function
Set.BijOn.subset_left : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {r : Set α},
  Set.BijOn f s t → r ⊆ s → Set.BijOn f r (f '' r)
-- Mathlib.Algebra.Order.Ring.Int
Int.isCompl_even_odd : IsCompl {n | Even n} {n | Odd n}
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivWithinAt_iff_isLittleO : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x ↔ (fun x' => f x' - f x - (x' - x) • f') =o[nhdsWithin x s] fun x' => x' - x
-- Mathlib.Analysis.Normed.Group.Constructions
nnnorm_ofDual : ∀ {E : Type u_2} [inst : NNNorm E] (x : Eᵒᵈ), ‖OrderDual.ofDual x‖₊ = ‖x‖₊
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.pi_apply : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : AddTorsor V1 P1]
  [inst_3 : Module k V1] {ι : Type u_9} {φv : ι → Type u_10} {φp : ι → Type u_11}
  [inst_4 : (i : ι) → AddCommGroup (φv i)] [inst_5 : (i : ι) → Module k (φv i)]
  [inst_6 : (i : ι) → AddTorsor (φv i) (φp i)] (fp : (i : ι) → P1 →ᵃ[k] φp i) (c : P1) (i : ι),
  (AffineMap.pi fp) c i = (fp i) c
-- Mathlib.MeasureTheory.Integral.Bochner.VitaliCaratheodory
/-- Given a simple function `f` with values in `ℝ≥0`, there exists an upper semicontinuous
function `g ≤ f` with integral arbitrarily close to that of `f`. Formulation in terms of
`lintegral`.
Auxiliary lemma for Vitali-Carathéodory theorem `exists_lt_lower_semicontinuous_integral_lt`.  -/
MeasureTheory.SimpleFunc.exists_upperSemicontinuous_le_lintegral_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [BorelSpace α] {μ : MeasureTheory.Measure α}
  [μ.WeaklyRegular] (f : MeasureTheory.SimpleFunc α NNReal),
  ∫⁻ (x : α), ↑(f x) ∂μ ≠ ⊤ →
    ∀ {ε : ENNReal},
      ε ≠ 0 → ∃ g, (∀ (x : α), g x ≤ f x) ∧ UpperSemicontinuous g ∧ ∫⁻ (x : α), ↑(f x) ∂μ ≤ ∫⁻ (x : α), ↑(g x) ∂μ + ε
-- Mathlib.Data.Fintype.Sets
Fintype.coe_finsetEquivSet : ∀ {α : Type u_1} [inst : Fintype α], ⇑Fintype.finsetEquivSet = SetLike.coe
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.DerivedLitsInvariant.congr_simp : ∀ {n : ℕ} (f f_1 : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (e_f : f = f_1)
  (fassignments_size : f.assignments.size = n)
  (assignments assignments_1 : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (e_assignments : assignments = assignments_1) (assignments_size : assignments.size = n)
  (derivedLits derivedLits_1 : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  derivedLits = derivedLits_1 →
    f.DerivedLitsInvariant fassignments_size assignments assignments_size derivedLits =
      f_1.DerivedLitsInvariant ⋯ assignments_1 ⋯ derivedLits_1
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.size_reverse.go : ∀ {α : Type u_1} (as : Array α) (i : ℕ) (j : Fin as.size), (Array.reverse.loop as i j).size = as.size
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- The natural `AddActionHom` over `R` from a `SubAddAction` of `M` to `M`.  -/
SubAddAction.SMulMemClass.subtype : {R : Type u} →
  {M : Type v} →
    [inst : AddMonoid R] →
      [inst_1 : AddAction R M] →
        {A : Type u_1} → [inst_2 : SetLike A M] → [hA : VAddMemClass A R M] → (S' : A) → ↥S' →ₑ[id] M
-- Mathlib.LinearAlgebra.Finsupp.Pi
/-- Forget that a function is finitely supported.

This is the linear version of `Finsupp.toFun`.  -/
Finsupp.lcoeFun : {α : Type u_1} →
  {M : Type u_2} →
    {R : Type u_5} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (α →₀ M) →ₗ[R] α → M
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.Functor.ranges_directed : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofilteredOrEmpty C]
  (F : CategoryTheory.Functor C (Type u_1)) (j : C),
  Directed (fun x1 x2 => x1 ⊇ x2) fun f => Set.range ⇑(CategoryTheory.ConcreteCategory.hom (F.map f.snd))
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RoiSliceData.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : SizeOf α] [inst_2 : (a : α) → SizeOf (β a)]
  (treeMap : Std.DTreeMap.Internal.Impl α β) (range : Std.Roi α),
  sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pushout.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  [inst_1 : CategoryTheory.Limits.HasPushout f g] {W : C} {k l : CategoryTheory.Limits.pushout f g ⟶ W},
  k = l ↔
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) k =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g) l ∧
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) k =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g) l
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.Hom.isoOfComponents_hom_f : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ : HomologicalComplex V c}
  (f : (i : ι) → C₁.X i ≅ C₂.X i)
  (hf :
    autoParam
      (∀ (i j : ι),
        c.Rel i j →
          CategoryTheory.CategoryStruct.comp (f i).hom (C₂.d i j) =
            CategoryTheory.CategoryStruct.comp (C₁.d i j) (f j).hom)
      HomologicalComplex.Hom.isoOfComponents._auto_1)
  (i : ι), (HomologicalComplex.Hom.isoOfComponents f hf).hom.f i = (f i).hom
-- Std.Do.Triple.SpecLemmas
List.Cursor.tail.eq_1 : ∀ {α : Type u_1} {l : List α} (s : l.Cursor) (h : 0 < s.suffix.length),
  s.tail h = { «prefix» := s.prefix ++ [s.current h], suffix := s.suffix.tail, property := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.whiskerLeft_curry'_ihom_ev_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.Closed X] (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalClosed.curry' f))
      ((CategoryTheory.ihom.ev X).app Y) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom f
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.comap_le_comap_iff_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N},
  Function.Surjective ⇑f → ∀ {S T : Subsemigroup N}, Subsemigroup.comap f S ≤ Subsemigroup.comap f T ↔ S ≤ T
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.H0π.eq_1 : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  groupHomology.H0π A = CategoryTheory.CategoryStruct.comp (groupHomology.cyclesIso₀ A).inv (groupHomology.π A 0)
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.ext_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
  [inst_3 : MulZeroOneClass β] {f g : α →*₀o β}, f = g ↔ ∀ (a : α), f a = g a
-- Mathlib.Analysis.Meromorphic.NormalForm
toMeromorphicNFAt_eventuallyEq_nhds_congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f g : 𝕜 → E},
  f =ᶠ[nhdsWithin x {x}ᶜ] g → toMeromorphicNFAt f x =ᶠ[nhds x] toMeromorphicNFAt g x
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β}, k ∉ m₁ → (m₁ \ m₂).getD k fallback = fallback
-- Mathlib.RingTheory.SimpleModule.Basic
instIsPrincipalIdealRingOfIsSemisimpleRing : ∀ {R : Type u_2} [inst : Ring R] [IsSemisimpleRing R], IsPrincipalIdealRing R
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKeyD_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β k} {fallback : α},
      (t.insert k v).maxKeyD fallback = t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k'
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.instLawfulSingletonProd : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering}, LawfulSingleton (α × β) (Std.TreeMap.Raw α β cmp)
-- Init.Data.Array.Extract
Array.extract_append_right : ∀ {α : Type u_1} {i : ℕ} {as bs : Array α}, (as ++ bs).extract as.size (as.size + i) = bs.extract 0 i
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- The pushforward of a cover along an isomorphism.  -/
AlgebraicGeometry.Scheme.Cover.pushforwardIso : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [P.RespectsIso] →
    [P.ContainsIdentities] →
      [P.IsStableUnderComposition] →
        {X Y : AlgebraicGeometry.Scheme} →
          AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X →
            (f : X ⟶ Y) →
              [CategoryTheory.IsIso f] → AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) Y
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.ofAbs_pow : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S) (x : WithAbs v) (n : ℕ), (x ^ n).ofAbs = x.ofAbs ^ n
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.LaxTrans.Modification.instInhabited : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η : F ⟶ G} → Inhabited (CategoryTheory.Oplax.LaxTrans.Modification η η)
-- Mathlib.Logic.Pairwise
Set.Pairwise.imp_on : ∀ {α : Type u_1} {r p : α → α → Prop} {s : Set α}, s.Pairwise r → (s.Pairwise fun ⦃a b⦄ => r a b → p a b) → s.Pairwise p
-- Mathlib.Data.List.Defs
_private.Mathlib.Data.List.Defs.0.List.map₂Left'.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (bs : List β) (h_1 : (bs : List β) → motive [] bs)
  (h_2 : (a : α) → (as : List α) → motive (a :: as) [])
  (h_3 : (a : α) → (as : List α) → (b : β) → (bs : List β) → motive (a :: as) (b :: bs)),
  (match [], bs with
    | [], bs => h_1 bs
    | a :: as, [] => h_2 a as
    | a :: as, b :: bs => h_3 a as b bs) =
    h_1 bs
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableOn.congr_mono : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {s t : Set M},
  MDiff[s] f → (∀ x ∈ t, f₁ x = f x) → t ⊆ s → MDiff[t] f₁
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Functor.coconeTypesEquiv_symm_apply_ι : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  (c : CategoryTheory.Limits.Cocone F) (j : J) (a : F.obj j),
  (F.coconeTypesEquiv.symm c).ι j a = (CategoryTheory.ConcreteCategory.hom (c.ι.app j)) a
-- Mathlib.Algebra.Order.BigOperators.Ring.Finset
Finset.PNat.coe_prod : ∀ {ι : Type u_4} (f : ι → ℕ+) (s : Finset ι), ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
-- Mathlib.Algebra.Order.Interval.Set.SuccPred
Set.insert_Ioc_right_eq_Ioc_add_one_of_not_isMax : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : Add α] [SuccAddOrder α] {a b : α},
  a ≤ b → ¬IsMax b → insert (b + 1) (Set.Ioc a b) = Set.Ioc a (b + 1)
-- Lean.AutoDecl
/-- Returns true if `decl` is an automatically generated declaration.

Also returns true if `decl` is an internal name or created during macro
expansion.
 -/
Lean.isAutoDeclOrPrivate_Internal : Lean.Name → Lean.CoreM Bool
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.erase_empty : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {k : α}, ∅.erase k = ∅
-- Mathlib.RingTheory.Polynomial.Nilpotent
Polynomial.isNilpotent_aeval_sub_of_isNilpotent_sub : ∀ {R : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (P : Polynomial R)
  {a b : S}, IsNilpotent (a - b) → IsNilpotent ((Polynomial.aeval a) P - (Polynomial.aeval b) P)
-- Batteries.Tactic.GeneralizeProofs
Batteries.Tactic.GeneralizeProofs.Config.mk.inj : ∀ {maxDepth : ℕ} {abstract debug : Bool} {maxDepth_1 : ℕ} {abstract_1 debug_1 : Bool},
  { maxDepth := maxDepth, abstract := abstract, debug := debug } =
      { maxDepth := maxDepth_1, abstract := abstract_1, debug := debug_1 } →
    maxDepth = maxDepth_1 ∧ abstract = abstract_1 ∧ debug = debug_1
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- The interior is the complement of the boundary.  -/
ModelWithCorners.compl_boundary : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M],
  (ModelWithCorners.boundary M)ᶜ = ModelWithCorners.interior M
-- Init.Data.Range.Polymorphic.PRange
Std.Rii.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α], sizeOf *...* = 1
-- Mathlib.Algebra.CharP.Two
CharTwo.add_eq_iff_eq_add : ∀ {R : Type u_1} [inst : Ring R] [CharP R 2] {a b c : R}, a + b = c ↔ a = c + b
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
CategoryTheory.Functor.IsCocartesian.toIsHomLift : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳}
  {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} {f : R ⟶ S} {φ : a ⟶ b} [self : p.IsCocartesian f φ],
  p.IsHomLift f φ
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- Unfolds the definition of the `p`-adic norm of `q` when `q ≠ 0`.  -/
padicNorm.eq_zpow_of_nonzero : ∀ {p : ℕ} {q : ℚ}, q ≠ 0 → padicNorm p q = ↑p ^ (-padicValRat p q)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblU_ne_zero_of_Y_eq : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P Q : Fin 3 → F},
  W.Nonsingular P →
    P 2 ≠ 0 →
      Q 2 ≠ 0 →
        P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 →
          P 1 * Q 2 ^ 3 = Q 1 * P 2 ^ 3 → P 1 * Q 2 ^ 3 = W.negY Q * P 2 ^ 3 → W.dblU P ≠ 0
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
MeasureTheory.condExp_stronglyMeasurable_simpleFunc_mul : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω},
  m ≤ mΩ →
    ∀ (f : MeasureTheory.SimpleFunc Ω ℝ) {g : Ω → ℝ}, MeasureTheory.Integrable g μ → μ[⇑f * g | m] =ᵐ[μ] ⇑f * μ[g | m]
-- Std.Data.DTreeMap.Internal.Lemmas
/-- Internal implementation detail  -/
Std.DTreeMap.Internal.Impl.decidableEquiv : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.TransOrd α] →
        [Std.LawfulEqOrd α] →
          [inst_3 : (k : α) → BEq (β k)] →
            [∀ (k : α), LawfulBEq (β k)] →
              (t₁ t₂ : Std.DTreeMap.Internal.Impl α β) → t₁.WF → t₂.WF → Decidable (t₁.Equiv t₂)
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.map_smul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
  {T : Submonoid P} {Q : Type u_4} [inst_5 : CommSemiring Q] [inst_6 : Algebra P Q] [inst_7 : IsLocalization T Q]
  (hy : M ≤ Submonoid.comap g T) (x : S) (z : R),
  (IsLocalization.map Q g hy) (z • x) = g z • (IsLocalization.map Q g hy) x
-- Mathlib.Algebra.Group.Prod
MulHom.prodMap_def : ∀ {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul M']
  [inst_3 : Mul N'] (f : M →ₙ* M') (g : N →ₙ* N'),
  f.prodMap g = (f.comp (MulHom.fst M N)).prod (g.comp (MulHom.snd M N))
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.inclusion'_top_functor : ∀ (X : TopCat), ⋯.functor = TopologicalSpace.Opens.map (TopologicalSpace.Opens.inclusionTopIso X).inv
-- Mathlib.Analysis.Complex.Trigonometric
Real.two_mul_sin_mul_sin : ∀ (x y : ℝ), 2 * Real.sin x * Real.sin y = Real.cos (x - y) - Real.cos (x + y)
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
rothNumberNat_spec : ∀ (n : ℕ), ∃ t ⊆ Finset.range n, t.card = rothNumberNat n ∧ ThreeAPFree ↑t
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.instHasDetOneMapSpecialLinearGroupGeneralLinearGroupMapGL : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : CommRing R] {S : Type u_3}
  [inst_3 : CommRing S] [inst_4 : Algebra R S] (Γ : Subgroup (Matrix.SpecialLinearGroup n R)),
  (Subgroup.map (Matrix.SpecialLinearGroup.mapGL S) Γ).HasDetOne
-- Std.Sat.AIG.Relabel
Std.Sat.AIG.unsat_relabel : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {β : Type} [inst_2 : Hashable β] [inst_3 : DecidableEq β]
  {idx : ℕ} {invert : Bool} {aig : Std.Sat.AIG α} (r : α → β) {hidx : idx < aig.decls.size},
  aig.UnsatAt idx invert hidx → (Std.Sat.AIG.relabel r aig).UnsatAt idx invert ⋯
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.frobenius_zmodp : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (x : WittVector p (ZMod p)), WittVector.frobenius x = x
-- Mathlib.Data.List.Nodup
/-- **Alias** of `List.Nodup.mem_sdiff_iff`. -/
List.Nodup.mem_diff_iff : ∀ {α : Type u} {l₁ l₂ : List α} {a : α} [inst : BEq α] [LawfulBEq α], l₁.Nodup → (a ∈ l₁.diff l₂ ↔ a ∈ l₁ ∧ a ∉ l₂)
-- Mathlib.Data.ULift
PLift.instNonempty_mathlib : ∀ {α : Sort u} [Nonempty α], Nonempty (PLift α)
-- Mathlib.Data.Nat.Choose.Factorization
Nat.factorization_choose_eq_zero_of_lt : ∀ {p n k : ℕ}, n < p → (n.choose k).factorization p = 0
-- Mathlib.Algebra.Order.Nonneg.Module
Nonneg.instIsOrderedModule : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : PartialOrder M] [inst_4 : SMulWithZero R M] [hM : IsOrderedModule R M], IsOrderedModule { c // 0 ≤ c } M
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.tanh_arsinh : ∀ (x : ℝ), Real.tanh (Real.arsinh x) = x / √(1 + x ^ 2)
-- Lean.Expr
/-- Return the type of a literal value.  -/
Lean.Literal.type : Lean.Literal → Lean.Expr
-- Mathlib.Tactic.Algebra.Basic
/-- `algebra` solves equalities in the language of algebras: ring operations and scalar
multiplications.

Given a goal which is an equality in a commutative `R`-algebra `A`, `algebra` parses the LHS and
RHS of the goal as polynomial expressions of `A`-atoms with coefficients in some semiring `R`, and
closes the goal if the two expressions are the same. The `R`-coefficients are put into ring normal
form.

By default, the scalar ring `R` is inferred automatically by looking for scalar multiplications and
`algebraMap`s present in the expressions. The inference procedure assumes that any two rings `R`
and `S` that appear are comparable, in the sense that either `R` is an `S`-algebra or `S` is an
`R`-algebra.

* `algebra with R` uses the term `R` as the scalar ring, instead of attempting to infer it
automatically.
 -/
Mathlib.Tactic.Algebra.algebra : Lean.ParserDescr
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.rightHomologyι_naturality' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.rightHomologyMap' φ h₁ h₂) h₂.ι =
    CategoryTheory.CategoryStruct.comp h₁.ι (CategoryTheory.ShortComplex.opcyclesMap' φ h₁ h₂)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocNatIso_hom_app_app_app : ∀ (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.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (X X_1 : C) (X_2 : D),
  (((CategoryTheory.MonoidalCategory.MonoidalRightAction.actionAssocNatIso C D).hom.app X).app X_1).app X_2 =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso X_2 X X_1).hom
-- Init.Data.List.Monadic
List.zipWithM'.eq_def : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type x} {γ : Type u} (f : α → β → m γ) (x : List α)
  (x_1 : List β),
  List.zipWithM' f x x_1 =
    match x, x_1 with
    | x :: xs, y :: ys => do
      let z ← f x y
      let zs ← List.zipWithM' f xs ys
      pure (z :: zs)
    | x, x_2 => pure []
-- Mathlib.Order.Interval.Set.Basic
Set.Icc_eq_empty_of_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a → Set.Icc a b = ∅
-- Lean.Meta.Tactic.Grind.Types
/-- Closes the current goal using the given proof of `False` and
marks it as inconsistent if it is not already marked so.
 -/
Lean.Meta.Grind.closeGoal : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Analysis.Calculus.FDeriv.Defs
/-- **Alias** of the reverse direction of `hasFDerivAt_iff_isLittleOTVS`. -/
HasFDerivAt.of_isLittleOTVS : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E},
  ((fun x' => f x' - f x - f' (x' - x)) =o[𝕜; nhds x] fun x' => x' - x) → HasFDerivAt f f' x