mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Finiteness.FiniteTypeLocal
/-- Let `S` be an `R`-algebra, `M` a submonoid of `S`, `S' = M⁻¹S`.
Suppose the image of some `x : S` falls in the adjoin of some finite `s ⊆ S'` over `R`,
and `A` is an `R`-subalgebra of `S` containing both `M` and the numerators of `s`.
Then, there exists some `m : M` such that `m • x` falls in `A`.
 -/
IsLocalization.exists_smul_mem_of_mem_adjoin : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {S' : Type u_4}
  [inst_3 : CommRing S'] [inst_4 : Algebra S S'] [inst_5 : Algebra R S'] [IsScalarTower R S S'] (M : Submonoid S)
  [inst_7 : IsLocalization M S'] (x : S) (s : Finset S') (A : Subalgebra R S),
  ↑(IsLocalization.finsetIntegerMultiple M s) ⊆ ↑A →
    M ≤ A.toSubmonoid → (algebraMap S S') x ∈ Algebra.adjoin R ↑s → ∃ m, m • x ∈ A
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.instIsScalarTower : ∀ {𝕜 : Type u_2} {𝕝 : Type u_3} {𝕞 : Type u_4} {α : Type u_5} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α]
  [inst_2 : AddCommMonoid 𝕜] [inst_3 : Monoid 𝕜] [inst_4 : Semiring 𝕝] [inst_5 : AddCommMonoid 𝕞] [inst_6 : SMul 𝕜 𝕝]
  [inst_7 : Module 𝕝 𝕞] [inst_8 : DistribMulAction 𝕜 𝕞] [IsScalarTower 𝕜 𝕝 𝕞],
  IsScalarTower (IncidenceAlgebra 𝕜 α) (IncidenceAlgebra 𝕝 α) (IncidenceAlgebra 𝕞 α)
-- Lean.ProjFns
Lean.instInhabitedProjectionFunctionInfo.default : Lean.ProjectionFunctionInfo
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
/-- `preCDF` is the Radon-Nikodym derivative of `ρ.IicSnd` with respect to `ρ.fst` at each
`r : ℚ`. This function `ℚ → α → ℝ≥0∞` is such that for almost all `a : α`, the function `ℚ → ℝ≥0∞`
satisfies the properties of a cdf (monotone with limit 0 at -∞ and 1 at +∞, right-continuous).

We define this function on `ℚ` and not `ℝ` because `ℚ` is countable, which allows us to prove
properties of the form `∀ᵐ a ∂ρ.fst, ∀ q, P (preCDF q a)`, instead of the weaker
`∀ q, ∀ᵐ a ∂ρ.fst, P (preCDF q a)`.  -/
ProbabilityTheory.preCDF : {α : Type u_1} → {mα : MeasurableSpace α} → MeasureTheory.Measure (α × ℝ) → ℚ → α → ENNReal
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.isoMk_hom_right : ∀ {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] {L₁ : CategoryTheory.Functor A T}
  {R₁ : CategoryTheory.Functor B T} {X Y : CategoryTheory.Comma L₁ R₁} (l : X.left ≅ Y.left) (r : X.right ≅ Y.right)
  (h :
    autoParam
      (CategoryTheory.CategoryStruct.comp (L₁.map l.hom) Y.hom =
        CategoryTheory.CategoryStruct.comp X.hom (R₁.map r.hom))
      CategoryTheory.Comma.isoMk._auto_1),
  (CategoryTheory.Comma.isoMk l r h).hom.right = r.hom
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.add : {α : Type u} → [Add α] → Add (WithBot α)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.OplaxMonoidal.δ_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] (X Y : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)
      (CategoryTheory.SemiCartesianMonoidalCategory.fst (F.obj X) (F.obj Y)) =
    F.map (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y)
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.dFrom_eq_zero : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i : ι},
  ¬c.Rel i (c.next i) → C.dFrom i = 0
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min_eq_min! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {he : t ≠ ∅}, t.min he = t.min!
-- Mathlib.Order.SuccPred.Limit
Order.isPredPrelimit_toDual_iff : ∀ {α : Type u_1} {a : α} [inst : LT α], Order.IsPredPrelimit (OrderDual.toDual a) ↔ Order.IsSuccPrelimit a
-- Mathlib.Algebra.BigOperators.Ring.Finset
Nat.cast_multiset_sum : ∀ {R : Type u_4} [inst : AddCommMonoidWithOne R] (s : Multiset ℕ), ↑s.sum = (Multiset.map Nat.cast s).sum
-- Mathlib.RingTheory.Derivation.DifferentialRing
/-- Transfer a `Differential` instance across a `RingEquiv`.  -/
Differential.equiv : {R : Type u_1} →
  {R₂ : Type u_2} → [inst : CommRing R] → [inst_1 : CommRing R₂] → [Differential R₂] → R ≃+* R₂ → Differential R
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffOn.congr : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f f₁ : E → F} {n : WithTop ℕ∞}, ContDiffOn 𝕜 n f s → (∀ x ∈ s, f₁ x = f x) → ContDiffOn 𝕜 n f₁ s
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max!_eq_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {km : α}, t.max! = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Algebra.Lie.Basic
/-- An equivalence of Lie algebras (denoted as `L₁ ≃ₗ⁅R⁆ L₂`) is a morphism
which is also a linear equivalence.
We could instead define an equivalence to be a morphism which is also a (plain) equivalence.
However, it is more convenient to define via linear equivalence to get `.toLinearEquiv` for free.  -/
«term_≃ₗ⁅_⁆_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- If `s` is locally closed (e.g. open or closed), then `f` is locally integrable on `s` iff it is
integrable on every compact subset contained in `s`.  -/
MeasureTheory.locallyIntegrableOn_iff : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} {s : Set X}
  [TopologicalSpace.PseudoMetrizableSpace ε] [LocallyCompactSpace X],
  IsLocallyClosed s →
    (MeasureTheory.LocallyIntegrableOn f s μ ↔ ∀ k ⊆ s, IsCompact k → MeasureTheory.IntegrableOn f k μ)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
CStarAlgebra.preimage_inr_Icc_zero_one : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A],
  Unitization.inr ⁻¹' Set.Icc 0 1 = {x | 0 ≤ x} ∩ Metric.closedBall 0 1
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.polar_add_left : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticMap R M N) (x x' y : M),
  QuadraticMap.polar (⇑Q) (x + x') y = QuadraticMap.polar (⇑Q) x y + QuadraticMap.polar (⇑Q) x' y
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons counted by weight, strict inequality version:
if the total weight of a finite set of pigeons is greater than `n • b`, and they are sorted into
`n` pigeonholes, then for some pigeonhole, the total weight of the pigeons in this pigeonhole is
greater than `b`.  -/
Finset.exists_lt_sum_fiber_of_maps_to_of_nsmul_lt_sum : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β} {w : α → M}
  {b : M} [inst_1 : AddCommMonoid M] [inst_2 : LinearOrder M] [IsOrderedCancelAddMonoid M],
  (∀ a ∈ s, f a ∈ t) → t.card • b < ∑ x ∈ s, w x → ∃ y ∈ t, b < ∑ x ∈ s with f x = y, w x
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.det_invOf : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α)
  [inst_3 : Invertible A] [inst_4 : Invertible A.det], (⅟A).det = ⅟A.det
-- Std.Time.Time.HourMarker
/-- `ofOrdinal` converts an `Hour.Ordinal` value to an `HourMarker`, indicating whether it is AM or PM.
 -/
Std.Time.HourMarker.ofOrdinal : Std.Time.Hour.Ordinal → Std.Time.HourMarker
-- Mathlib.Algebra.GroupWithZero.Prod
Prod.instMulZeroOneClass : {M₀ : Type u_1} → {N₀ : Type u_2} → [MulZeroOneClass M₀] → [MulZeroOneClass N₀] → MulZeroOneClass (M₀ × N₀)
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
/-- The equivalence from the image of the `GoodProducts` in `LocallyConstant (π C (ord I · < o)) ℤ` to
`smaller C o`
 -/
Profinite.NobelingProof.GoodProducts.range_equiv_smaller : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] →
        (o : Ordinal.{u}) →
          ↑(Profinite.NobelingProof.GoodProducts.range
                (Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o)) ≃
            ↑(Profinite.NobelingProof.GoodProducts.smaller C o)
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
CommAlgCat.braiding_hom_hom : ∀ {R : Type u} [inst : CommRing R] (A B : CommAlgCat R),
  CommAlgCat.Hom.hom (β_ A B).hom = ↑(Algebra.TensorProduct.comm R ↑A ↑B)
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.Hom.mk.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  {X Y : CategoryTheory.Triangulated.SpectralObject C ι} (hom hom_1 : X.ω₁ ⟶ Y.ω₁) (e_hom : hom = hom_1)
  (comm :
    ∀ {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
      CategoryTheory.CategoryStruct.comp (X.δ f g)
          ((CategoryTheory.shiftFunctor C 1).map (hom.app (CategoryTheory.ComposableArrows.mk₁ f))) =
        CategoryTheory.CategoryStruct.comp (hom.app (CategoryTheory.ComposableArrows.mk₁ g)) (Y.δ f g)),
  { hom := hom, comm := comm } = { hom := hom_1, comm := ⋯ }
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_replaceEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k},
  Std.Internal.List.containsKey a (Std.Internal.List.replaceEntry k v l) = Std.Internal.List.containsKey a l
-- Mathlib.Data.Set.Lattice
Set.iInter_coe_set : ∀ {α : Type u_12} {β : Type u_13} (s : Set α) (f : ↑s → Set β), ⋂ i, f i = ⋂ i, ⋂ (h : i ∈ s), f ⟨i, h⟩
-- Mathlib.Algebra.Group.Hom.Instances
instIsRightCancelAddAddMonoidHom : ∀ {M : Type uM} {N : Type uN} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] [IsRightCancelAdd N],
  IsRightCancelAdd (M →+ N)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
PseudoMetricSpace.dist_triangle : ∀ {α : Type u} [self : PseudoMetricSpace α] (x y z : α), dist x z ≤ dist x y + dist y z
-- Qq.Match
Qq.Impl.mkInstantiateMVars : (decls : List Qq.Impl.PatVarDecl) →
  List Qq.Impl.PatVarDecl →
    Lean.MetaM
      (have a := Qq.Impl.mkIsDefEqType decls;
      Q(Lean.MetaM «$a»))
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- The exponent of a generalized eigenvalue is never 0.  -/
Module.End.exp_ne_zero_of_hasGenEigenvalue : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {k : ℕ}, f.HasGenEigenvalue μ k → k ≠ 0
-- Mathlib.Logic.Small.Defs
small_map : ∀ {α : Type u_1} {β : Type u_2} [hβ : Small.{w, u_2} β] (e : α ≃ β), Small.{w, u_1} α
-- Init.Data.Array.Find
Array.findSome?_push : ∀ {α : Type u_1} {a : α} {α_1 : Type u_2} {f : α → Option α_1} {xs : Array α},
  Array.findSome? f (xs.push a) = (Array.findSome? f xs).or (f a)
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_mono : ∀ {Γ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : Zero S]
  {x : HahnSeries Γ R} {y : HahnSeries Γ S}, x.support ⊆ y.support → x.cardSupp ≤ y.cardSupp
-- Mathlib.Topology.Closure
Dense.mono : ∀ {X : Type u} [inst : TopologicalSpace X] {s₁ s₂ : Set X}, s₁ ⊆ s₂ → Dense s₁ → Dense s₂
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.instIteratorLoop.loop.wf.eq_def : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α] {n : Type u → Type w}
  [inst_5 : Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop)
  (wf : Std.IteratorLoop.WellFounded (Std.Rxc.Iterator α) Id Pl) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), a ≤ b → LargeEnough a → LargeEnough b) (upperBound : α) (acc : γ) (next : α) (h : LargeEnough next)
  (f : (out : α) → LargeEnough out → out ≤ upperBound → (c : γ) → n { s // Pl out c s }),
  Std.Rxc.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc next h f =
    if hu : next ≤ upperBound then do
      let __do_lift ← f next h hu acc
      match __do_lift with
        | ⟨ForInStep.yield acc', property⟩ =>
          match hs : Std.PRange.succ? next with
          | some next' => Std.Rxc.Iterator.instIteratorLoop.loop.wf✝ γ Pl wf LargeEnough hl upperBound acc' next' ⋯ f
          | none => pure acc'
        | ⟨ForInStep.done acc', property⟩ => pure acc'
    else pure acc
-- Init.Data.UInt.Lemmas
UInt16.pow_succ : ∀ (x : UInt16) (n : ℕ), x ^ (n + 1) = x ^ n * x
-- Lean.Meta.Tactic.Grind.Types
/-- Returns `true` if `e` is in the equivalence class of `Bool.true`.  -/
Lean.Meta.Grind.isEqBoolTrue : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.Data.Real.ConjExponents
/-- For `r`, instead of `p`  -/
NNReal.HolderTriple.inv_nonneg' : ∀ {p q r : NNReal}, p.HolderTriple q r → 0 ≤ r⁻¹
-- Mathlib.Topology.Irreducible
IsPreirreducible.open_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] {t U : Set X}, IsPreirreducible t → IsOpen U → U ⊆ t → IsPreirreducible U
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsCharTwoJNeZeroNF.mk : ∀ {R : Type u_1} [inst : CommRing R] {W : WeierstrassCurve R}, W.a₁ = 1 → W.a₃ = 0 → W.a₄ = 0 → W.IsCharTwoJNeZeroNF
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
/-- See `star_mem_iff` for both directions.  -/
spinGroup.star_mem : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : CliffordAlgebra Q}, x ∈ spinGroup Q → star x ∈ spinGroup Q
-- Init.Data.Int.Lemmas
Int.subNatNat_of_lt : ∀ {m n : ℕ}, m < n → Int.subNatNat m n = Int.negSucc (n - m).pred
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.μ_pullback_left_snd' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X R Y Z : C} {f : R ⟶ X} (g₁ : Y ⟶ X) (g₂ : Z ⟶ X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left
        (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback f) (CategoryTheory.Over.mk g₁)
          (CategoryTheory.Over.mk g₂)))
      (CategoryTheory.Limits.pullback.snd
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g₁ g₂) g₁) f) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk g₁)).hom
        ((CategoryTheory.Over.pullback f).obj (CategoryTheory.Over.mk g₂)).hom)
      (CategoryTheory.Limits.pullback.snd (CategoryTheory.Over.mk g₂).hom f)
-- Lean.Elab.WhereFinally
Lean.Elab.instInhabitedWhereFinallyView : Inhabited Lean.Elab.WhereFinallyView
-- Init.Data.Array.Int
Array.sum_eq_foldl_int : ∀ {xs : Array ℤ}, xs.sum = Array.foldl (fun x1 x2 => x1 + x2) 0 xs
-- Lean.Meta.Tactic.Util
/-- Get the type of the given metavariable after instantiating metavariables and reducing to
weak head normal form.  -/
Lean.MVarId.getType' : Lean.MVarId → Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.rightAssocTensor_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C × C × C),
  (CategoryTheory.MonoidalCategory.rightAssocTensor C).obj X =
    CategoryTheory.MonoidalCategoryStruct.tensorObj X.1 (CategoryTheory.MonoidalCategoryStruct.tensorObj X.2.1 X.2.2)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- The forgetful functor from `PresheafedSpace` to `TopCat`.  -/
AlgebraicGeometry.PresheafedSpace.forget : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.Functor (AlgebraicGeometry.PresheafedSpace C) TopCat
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.brecOn.eq : ∀ {motive_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr → Sort u}
  {motive_2 : Lean.Meta.Grind.Arith.Linear.EqCnstrProof → Sort u}
  {motive_3 : Lean.Meta.Grind.Arith.Linear.IneqCnstr → Sort u}
  {motive_4 : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof → Sort u}
  {motive_5 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Sort u}
  {motive_6 : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof → Sort u}
  {motive_7 : Lean.Meta.Grind.Arith.Linear.UnsatProof → Sort u} (t : Lean.Meta.Grind.Arith.Linear.EqCnstrProof)
  (F_1 : (t : Lean.Meta.Grind.Arith.Linear.EqCnstr) → t.below → motive_1 t)
  (F_2 : (t : Lean.Meta.Grind.Arith.Linear.EqCnstrProof) → t.below → motive_2 t)
  (F_3 : (t : Lean.Meta.Grind.Arith.Linear.IneqCnstr) → t.below → motive_3 t)
  (F_4 : (t : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof) → t.below → motive_4 t)
  (F_5 : (t : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) → t.below → motive_5 t)
  (F_6 : (t : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof) → t.below → motive_6 t)
  (F_7 : (t : Lean.Meta.Grind.Arith.Linear.UnsatProof) → t.below → motive_7 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 F_7 =
    F_2 t (Lean.Meta.Grind.Arith.Linear.EqCnstrProof.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
AlgebraicGeometry.QuasiCompactCover.homCover : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (hf : P f)
  [inst : AlgebraicGeometry.Surjective f] [AlgebraicGeometry.QuasiCompact f],
  AlgebraicGeometry.QuasiCompactCover (AlgebraicGeometry.Scheme.Hom.cover f hf).toPreZeroHypercover
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfLocalizedEquivalences
CategoryTheory.LocalizerMorphism.isLeftDerivabilityStructure_iff_of_isLocalizedEquivalence : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₁' : CategoryTheory.MorphismProperty D₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  {W₂' : CategoryTheory.MorphismProperty D₂} {T : CategoryTheory.LocalizerMorphism W₁ W₂}
  {L : CategoryTheory.LocalizerMorphism W₁ W₁'} {R : CategoryTheory.LocalizerMorphism W₂ W₂'}
  {B : CategoryTheory.LocalizerMorphism W₁' W₂'} [W₂'.RespectsIso] [L.IsLocalizedEquivalence] [R.IsLocalizedEquivalence]
  [R.functor.EssSurj] [L.functor.EssSurj] [R.functor.Full] [R.IsInduced]
  (iso : T.functor.comp R.functor ≅ L.functor.comp B.functor) [CategoryTheory.TwoSquare.GuitartExact iso.inv],
  T.IsLeftDerivabilityStructure ↔ B.IsLeftDerivabilityStructure
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.AddQuotientMeasureEqMeasurePreimage.mk : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  {ν : autoParam (MeasureTheory.Measure α) MeasureTheory.AddQuotientMeasureEqMeasurePreimage._auto_1}
  {μ : MeasureTheory.Measure (Quotient (AddAction.orbitRel G α))},
  (∀ (t : Set α),
      MeasureTheory.IsAddFundamentalDomain G t ν →
        μ = MeasureTheory.Measure.map (Quotient.mk (AddAction.orbitRel G α)) (ν.restrict t)) →
    MeasureTheory.AddQuotientMeasureEqMeasurePreimage ν μ
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.rightInverse_of_leftInverse : ∀ {R : Type u} {M : Type v} {N : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] [Module.Invertible R M] [Module.Invertible R N] {f : M →ₗ[R] N}
  {g : N →ₗ[R] M}, Function.LeftInverse ⇑f ⇑g → Function.RightInverse ⇑f ⇑g
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
/-- The invertible elements in the center of `D` that are equal
to `(z (0, n) (m, 0))⁻¹ * z (m, 0) (0, n)`.  -/
CategoryTheory.CommShift₂Setup.ε : {D : Type u_5} →
  [inst : CategoryTheory.Category.{v_5, u_5} D] →
    {M : Type u_6} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : CategoryTheory.HasShift D M] →
          CategoryTheory.CommShift₂Setup D M → M → M → (CategoryTheory.CatCenter D)ˣ
-- Mathlib.SetTheory.ZFC.PSet
PSet.notMem_of_subset : ∀ {x y : PSet.{u_1}}, x ⊆ y → y ∉ x
-- Lean.Meta.Transform
_private.Lean.Meta.Transform.0.Lean.Meta.transformWithCache.visit.visitLet : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT Lean.MetaM m] →
      [MonadControlT Lean.MetaM m] →
        (Lean.Expr → m Lean.TransformStep) →
          (Lean.Expr → m Lean.TransformStep) →
            Bool →
              Bool →
                Bool →
                  (x : STWorld IO.RealWorld m) →
                    MonadLiftT (ST IO.RealWorld) m →
                      Array Lean.Expr → Lean.Expr → Lean.MonadCacheT Lean.ExprStructEq Lean.Expr m Lean.Expr
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsKleinFour.mulEquiv'.eq_1 : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : Group G₁] [inst_1 : Group G₂] [inst_2 : IsKleinFour G₁] (e : G₁ ≃ G₂)
  (he : e 1 = 1) (h : Monoid.exponent G₂ = 2), IsKleinFour.mulEquiv' e he h = { toEquiv := e, map_mul' := ⋯ }
-- Mathlib.Analysis.Normed.Order.Lattice
norm_sup_sub_sup_le_norm : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α] (x y z : α),
  ‖x ⊔ z - y ⊔ z‖ ≤ ‖x - y‖
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Implementation of `Mon.equivLaxMonoidalFunctorPUnit`.  -/
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Functor (CategoryTheory.Mon C)
        (CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C)
-- Mathlib.Order.Completion
DedekindCut.principal_lt_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a : α} {c : DedekindCut α}, DedekindCut.principal a < c ↔ ∃ b ∈ c.left, a < b
-- Mathlib.RingTheory.WittVector.IsPoly
/-- `ghost_calc` is a tactic for proving identities between polynomial functions.
Typically, when faced with a goal like
```lean
∀ (x y : 𝕎 R), verschiebung (x * frobenius y) = verschiebung x * y
```
you can
1. call `ghost_calc`
2. do a small amount of manual work -- maybe nothing, maybe `rintro`, etc
3. call `ghost_simp`

and this will close the goal.

`ghost_calc` cannot detect whether you are dealing with unary or binary polynomial functions.
You must give it arguments to determine this.
If you are proving a universally quantified goal like the above,
call `ghost_calc _ _`.
If the variables are introduced already, call `ghost_calc x y`.
In the unary case, use `ghost_calc _` or `ghost_calc x`.

`ghost_calc` is a light wrapper around type class inference.
All it does is apply the appropriate extensionality lemma and try to infer the resulting goals.
This is subtle and Lean's elaborator doesn't like it because of the HO unification involved,
so it is easier (and prettier) to put it in a tactic script.
 -/
WittVector.Tactic.ghostCalc : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.eccent_eq_top_of_not_connected : ∀ {α : Type u_1} {G : SimpleGraph α}, ¬G.Connected → ∀ (u : α), G.eccent u = ⊤
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.σ : {α : Type u_1} → {f : Filter α} → f.Realizer → Type u_5
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.instInhabited : (α : Type u_2) → [inst : Preorder α] → [inst_1 : MulZeroOneClass α] → Inhabited (α →*₀o α)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.instIsEmptyOfForall : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [IsEmpty (V → W)], IsEmpty (G →g H)