mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.PartialHomeomorph.Basic
PartialHomeomorph.ofContinuousOpen_toPartialEquiv : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : PartialEquiv X Y)
  (hc : ContinuousOn (↑e) e.source) (ho : IsOpenMap ↑e) (hs : IsOpen e.source),
  (PartialHomeomorph.ofContinuousOpen e hc ho hs).toPartialEquiv = e
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k : α} {f : Option β → Option β},
  Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.Const.alter t k f) k = f (Std.ExtDTreeMap.Const.get? t k)
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.isNextOutParamOfLocalInstanceAndResult.isResultType : Lean.Expr → ℕ → Bool
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.forMUncurried_eq_forM_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {m : Type w → Type w'} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : α × β → m PUnit.{w + 1}},
  Std.ExtDTreeMap.Const.forMUncurried f t = (Std.ExtDTreeMap.Const.toList t).forM f
-- Mathlib.Analysis.Normed.Algebra.Spectrum
quasispectrum.instCompactSpaceNNReal : ∀ {B : Type u_3} [inst : NonUnitalNormedRing B] [inst_1 : NormedSpace ℝ B] [IsScalarTower ℝ B B] [SMulCommClass ℝ B B]
  (a : B) [CompactSpace ↑(quasispectrum ℝ a)], CompactSpace ↑(quasispectrum NNReal a)
-- Mathlib.Condensed.TopComparison
TopCat.toSheafCompHausLike_obj_obj : ∀ (P : TopCat → Prop) (X : TopCat) [inst : CompHausLike.HasExplicitFiniteCoproducts P]
  [inst_1 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  (X_1 : (CompHausLike P)ᵒᵖ),
  (TopCat.toSheafCompHausLike P X hs).obj.obj X_1 = C(↑((CompHausLike.compHausLikeToTop P).obj (Opposite.unop X_1)), ↑X)
-- Lean.Structure
Lean.StructureInfo.getProjFn? : Lean.StructureInfo → ℕ → Option Lean.Name
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
/-- Create new `PMF` by filtering on a set with non-zero measure and normalizing.  -/
PMF.filter : {α : Type u_1} → (p : PMF α) → (s : Set α) → (∃ a ∈ s, a ∈ p.support) → PMF α
-- Init.Core
DoResultBC.break.inj : ∀ {σ : Type u} {a a_1 : σ}, DoResultBC.break a = DoResultBC.break a_1 → a = a_1
-- Std.Time.Format.Modifier
Std.Time.instReprYear.repr : Std.Time.Year → ℕ → Std.Format
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_eraseKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {fallback : β},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueD a (Std.Internal.List.eraseKey k l) fallback =
      if (k == a) = true then fallback else Std.Internal.List.getValueD a l fallback
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_mul_inv_iff_mul_lt : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulRightStrictMono α] {a b c : α}, c < a * b⁻¹ ↔ c * b < a
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.map_range_eq_span_tprod : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] (f : (i : ι) → s i →ₗ[R] t i),
  (PiTensorProduct.map f).range = Submodule.span R {t_1 | ∃ m, (⨂ₜ[R] (i : ι), (f i) (m i)) = t_1}
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
Set.Countable.measure_restrict_compl : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {s : Set α},
  s.Countable → ∀ (μ : MeasureTheory.Measure α) [MeasureTheory.NullSingletonClass μ], μ.restrict sᶜ = μ
-- Std.Data.DTreeMap.Internal.Cell
Std.DTreeMap.Internal.Cell.mk.injEq : ∀ {α : Type u} [inst : Ord α] {β : α → Type v} {k : α → Ordering} (inner : Option ((a : α) × β a))
  (property : ∀ [Std.OrientedOrd α] (p : (a : α) × β a), inner = some p → k p.fst = Ordering.eq)
  (inner_1 : Option ((a : α) × β a))
  (property_1 : ∀ [Std.OrientedOrd α] (p : (a : α) × β a), inner_1 = some p → k p.fst = Ordering.eq),
  ({ inner := inner, property := property } = { inner := inner_1, property := property_1 }) = (inner = inner_1)
-- Mathlib.Order.CompleteBooleanAlgebra
CompletelyDistribLattice.iInf_iSup_eq : ∀ {α : Type u} [self : CompletelyDistribLattice α] {ι : Type u} {κ : ι → Type u} (f : (a : ι) → κ a → α),
  ⨅ a, ⨆ b, f a b = ⨆ g, ⨅ a, f a (g a)
-- Mathlib.Tactic.Order.CollectFacts
/-- Collects facts from the local context. `negGoal` is the negated goal, `hyps` is the expressions
passed to the tactic using square brackets. If `only?` is true, we collect facts only from `hyps`
and `negGoal`, otherwise we also use the local context.

For each occurring type `α`, the returned map contains an array containing all collected
`AtomicFact`s about atoms of type `α`.  -/
Mathlib.Tactic.Order.collectFacts : Bool →
  Array Lean.Expr → Lean.Expr → Mathlib.Tactic.AtomM (Std.HashMap Lean.Expr (Array Mathlib.Tactic.Order.AtomicFact))
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_erase_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β}, (m.erase k).getD k fallback = fallback
-- Std.Async.Basic
/-- Returns the `EAsync` computation inside an `ETask ε α`, so it can be awaited.
 -/
Std.Async.EAsync.async : {ε α : Type} →
  Std.Async.EAsync ε α → optParam Task.Priority Task.Priority.default → Std.Async.EAsync ε (Std.Async.ETask ε α)
-- Mathlib.Probability.Kernel.Defs
/-- A kernel from a measurable space `α` to another measurable space `β` is a measurable function
`κ : α → Measure β`. The measurable space structure on `MeasureTheory.Measure β` is given by
`MeasureTheory.Measure.instMeasurableSpace`. A map `κ : α → MeasureTheory.Measure β` is measurable
iff `∀ s : Set β, MeasurableSet s → Measurable (fun a ↦ κ a s)`.  -/
ProbabilityTheory.Kernel : (α : Type u_1) → (β : Type u_2) → [MeasurableSpace α] → [MeasurableSpace β] → Type (max u_1 u_2)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.equiv_of_forall_contains_unit_eq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => Unit},
  (↑m₁).WF → (↑m₂).WF → (∀ (k : α), m₁.contains k = m₂.contains k) → (↑m₁).Equiv ↑m₂
-- Mathlib.Order.Hom.Basic
OrderHom.uliftLeftMap_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β) (i : ULift.{u_8, u_2} α),
  f.uliftLeftMap i = f i.down
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.map_leftRightHomologyComparison' : ∀ {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] {S : CategoryTheory.ShortComplex C}
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] (hₗ : S.LeftHomologyData)
  (hᵣ : S.RightHomologyData) [inst_5 : hₗ.IsPreservedBy F] [inst_6 : hᵣ.IsPreservedBy F],
  F.map (CategoryTheory.ShortComplex.leftRightHomologyComparison' hₗ hᵣ) =
    CategoryTheory.ShortComplex.leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F)
-- Mathlib.AlgebraicGeometry.Morphisms.FlatRank
_private.Mathlib.AlgebraicGeometry.Morphisms.FlatRank.0.AlgebraicGeometry.IsAffine.finrank_comp_left_of_isIso : ∀ {X S Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine S] (f : X ⟶ Y) (g : Y ⟶ S)
  [CategoryTheory.IsIso f] [AlgebraicGeometry.IsFinite g] [AlgebraicGeometry.Flat g],
  AlgebraicGeometry.IsAffine.finrank✝ (CategoryTheory.CategoryStruct.comp f g) = AlgebraicGeometry.IsAffine.finrank✝ g
-- Lean.Meta.Tactic.Simp.Attr
Lean.Meta.Simp.Context.mkDefault : Lean.MetaM Lean.Meta.Simp.Context
-- Mathlib.Algebra.Category.Grp.Yoneda
AddCommGrpCat.coyonedaType_obj_map : ∀ (X : Type uᵒᵖ) {X_1 Y : AddCommGrpCat} (f : X_1 ⟶ Y),
  (AddCommGrpCat.coyonedaType.obj X).map f =
    AddCommGrpCat.ofHom
      (AddMonoidHom.pi fun i => (AddCommGrpCat.Hom.hom f).comp (Pi.evalAddMonoidHom (fun a => ↑X_1) i))
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_units_conj' : ∀ {m : Type u_2} {R : Type u_6} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : CommSemiring R]
  (M : (Matrix m m R)ˣ) (N : Matrix m m R), (↑M⁻¹ * N * ↑M).trace = N.trace
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
Lean.Elab.ConfigEval.EvalConfigItemView : Type
-- Mathlib.Data.Set.Basic
Set.PiSetCoe.canLift : ∀ (ι : Type u) (α : ι → Type v) [∀ (i : ι), Nonempty (α i)] (s : Set ι),
  CanLift ((i : ↑s) → α ↑i) ((i : ι) → α i) (fun f i => f ↑i) fun x => True
-- Mathlib.Topology.VectorBundle.Riemannian
/-- Given two continuous maps into the same fibers of a continuous Riemannian bundle,
their inner product is continuous. Version with `ContinuousOn`.  -/
ContinuousOn.inner_bundle : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F : Type u_2} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  {E : B → Type u_3} [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (x : B) → NormedAddCommGroup (E x)]
  [inst_5 : (x : B) → InnerProductSpace ℝ (E x)] [inst_6 : FiberBundle F E] [inst_7 : VectorBundle ℝ F E] {M : Type u_4}
  [inst_8 : TopologicalSpace M] [h : IsContinuousRiemannianBundle F E] {b : M → B} {v w : (x : M) → E (b x)}
  {s : Set M},
  ContinuousOn (fun m => ⟨b m, v m⟩) s →
    ContinuousOn (fun m => ⟨b m, w m⟩) s → ContinuousOn (fun b_1 => inner ℝ (v b_1) (w b_1)) s
-- Mathlib.Data.Vector.Basic
/-- Variant of `List.Vector.sum_set` that subtracts the inverse of the replaced element  -/
List.Vector.sum_set' : ∀ {α : Type u_1} {n : ℕ} [inst : AddCommGroup α] (v : List.Vector α n) (i : Fin n) (a : α),
  (v.set i a).toList.sum = v.toList.sum + -v.get i + a
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.toList.eq_2 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] (x x_1 j k : ι) (_hne : j ≠ k)
  (w₁ : Monoid.CoprodI.NeWord M x j) (w₂ : Monoid.CoprodI.NeWord M k x_1),
  (w₁.append _hne w₂).toList = w₁.toList ++ w₂.toList
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.uncurry_natural_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X X' Y : C}
  [inst_2 : CategoryTheory.Closed A] (f : X ⟶ X') (g : X' ⟶ A ⟹ Y),
  CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A f)
      (CategoryTheory.MonoidalClosed.uncurry g)
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- `SubgroupClass S G` states `S` is a type of subsets `s ⊆ G` that are subgroups of `G`.  -/
SubgroupClass : (S : Type u_3) → (G : outParam (Type u_4)) → [DivInvMonoid G] → [SetLike S G] → Prop
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.not_mem_emptyc : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {k : α}, k ∉ ∅
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.eq_of_eqOn_top : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_7} [inst_1 : AddMonoid M] {f g : G →+ M}, Set.EqOn ⇑f ⇑g ↑⊤ → f = g
-- Mathlib.Algebra.Category.Grp.Basic
addEquivIsoAddGroupIso.eq_1 : ∀ {X Y : AddGrpCat},
  addEquivIsoAddGroupIso =
    { hom := TypeCat.ofHom fun e => e.toAddGrpIso, inv := TypeCat.ofHom fun i => i.addGroupIsoToAddEquiv,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Init.Data.Nat.ToString
Nat.repr_of_lt : ∀ {n : ℕ}, n < 10 → n.repr = String.singleton n.digitChar
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.leftUnitor_def : ∀ {R : Type u} [inst : CommSemiring R] (M : SemimoduleCat R),
  CategoryTheory.MonoidalCategoryStruct.leftUnitor M = SemimoduleCat.MonoidalCategory.leftUnitor M
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.smul_val : ∀ {d : ℤ} (n x y : ℤ), ↑n * { re := x, im := y } = { re := n * x, im := n * y }
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_inv_naturality_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y : C} (f : X ⟶ Y) (Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) (β_ Z Y).inv =
    CategoryTheory.CategoryStruct.comp (β_ Z X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_filterMap : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k fallback : α},
  (Std.DHashMap.filterMap f m).getKeyD k fallback =
    ((m.getKey? k).pfilter fun x_2 h' => (f x_2 (m.get x_2 ⋯)).isSome).getD fallback
-- Aesop.Tree.Data
Aesop.RappId.zero : Aesop.RappId
-- Mathlib.MeasureTheory.OuterMeasure.AE
MeasureTheory.ae_eq_set_compl_compl : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s t : Set α}, sᶜ =ᵐ[μ] tᶜ ↔ s =ᵐ[μ] t
-- Mathlib.GroupTheory.GroupAction.Embedding
Function.Embedding.vadd : {G : Type u_1} → {α : Type u_3} → {β : Type u_4} → [inst : AddGroup G] → [AddAction G β] → VAdd G (α ↪ β)
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.weights_nonneg : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] {M : Type u_9} {w : Convexity.StdSimplex R M} (i : M),
  0 ≤ w.weights i
-- Lean.Structure
Lean.StructureResolutionState.mk.inj : ∀ {resolutions resolutions_1 : Lean.PHashMap Lean.Name (Array Lean.Name)},
  { resolutions := resolutions } = { resolutions := resolutions_1 } → resolutions = resolutions_1
-- Mathlib.Analysis.Analytic.Constructions
/-- ZPowers of analytic functions (into a normed field over `𝕜`) are analytic away from the zeros.
 -/
AnalyticOnNhd.zpow : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {s : Set E} {n : ℤ}, AnalyticOnNhd 𝕜 f s → (∀ z ∈ s, f z ≠ 0) → AnalyticOnNhd 𝕜 (f ^ n) s
-- Mathlib.Order.CompleteLattice.Basic
Monotone.map_iInf_le : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [inst : CompleteLattice α] {s : ι → α} [inst_1 : CompleteLattice β]
  {f : α → β}, Monotone f → f (iInf s) ≤ ⨅ i, f (s i)
-- Mathlib.Tactic.GCongr.Core
/-- Assuming the lemma has conslusion `lhs ↔ rhs`, mark one of the implications
`lhs → rhs` or `rhs → lhs` as a `gcongr` lemma.  -/
_private.Mathlib.Tactic.GCongr.Core.0.Mathlib.Tactic.GCongr.addGCongrLemma.addIffGCongrLemma : Lean.Name →
  Lean.AttributeKind → ℕ → Bool → Bool → Lean.ConstantInfo → Array Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Unit
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Elimination stack. For every variable in `elimStack`. If `x` in `elimStack`, then `elimEqs[x]` is not `none`.
 -/
Lean.Meta.Grind.Arith.Linear.Struct.elimStack : Lean.Meta.Grind.Arith.Linear.Struct → List Lean.Grind.Linarith.Var
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.Simp.DischargeWrapper.custom.injEq : ∀ (ref : IO.Ref Lean.Elab.Term.State) (discharge : Lean.Meta.Simp.Discharge) (ref_1 : IO.Ref Lean.Elab.Term.State)
  (discharge_1 : Lean.Meta.Simp.Discharge),
  (Lean.Elab.Tactic.Simp.DischargeWrapper.custom ref discharge =
      Lean.Elab.Tactic.Simp.DischargeWrapper.custom ref_1 discharge_1) =
    (ref = ref_1 ∧ discharge = discharge_1)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomainRingHom.eq_1 : ∀ (R : Type u_3) {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N] (f : M →* N),
  MonoidAlgebra.mapDomainRingHom R f =
    { toFun := MonoidAlgebra.mapDomain ⇑f, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Group.TransferInstance
/-- Transfer `AddCommGroup` across an `Equiv`  -/
Equiv.addCommGroup : {α : Type u_2} → {β : Type u_3} → α ≃ β → [AddCommGroup β] → AddCommGroup α
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trStmts₁.match_1.eq_6 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (q : Turing.PartrecToTM2.Λ')
  (h_1 :
    (Q : Turing.PartrecToTM2.Λ') →
      (p : Turing.PartrecToTM2.Γ' → Bool) →
        (k₁ k₂ : Turing.PartrecToTM2.K') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.move p k₁ k₂ q → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (Q : Turing.PartrecToTM2.Λ') →
      (k : Turing.PartrecToTM2.K') →
        (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.push k s q → motive (Turing.PartrecToTM2.Λ'.push k s q))
  (h_3 :
    (Q : Turing.PartrecToTM2.Λ') →
      (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') →
        Q = Turing.PartrecToTM2.Λ'.read q → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (Q : Turing.PartrecToTM2.Λ') →
      (p : Turing.PartrecToTM2.Γ' → Bool) →
        (k : Turing.PartrecToTM2.K') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.clear p k q → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (Q q : Turing.PartrecToTM2.Λ') → Q = q.copy → motive q.copy)
  (h_6 : (Q q : Turing.PartrecToTM2.Λ') → Q = q.succ → motive q.succ)
  (h_7 : (Q q₁ q₂ : Turing.PartrecToTM2.Λ') → Q = q₁.pred q₂ → motive (q₁.pred q₂))
  (h_8 :
    (Q : Turing.PartrecToTM2.Λ') →
      (k : Turing.PartrecToTM2.Cont') → Q = Turing.PartrecToTM2.Λ'.ret k → motive (Turing.PartrecToTM2.Λ'.ret k)),
  (match q.succ with
    | Q@h:(Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) => h_1 Q p k₁ k₂ q h
    | Q@h:(Turing.PartrecToTM2.Λ'.push k s q) => h_2 Q k s q h
    | Q@h:(Turing.PartrecToTM2.Λ'.read q) => h_3 Q q h
    | Q@h:(Turing.PartrecToTM2.Λ'.clear p k q) => h_4 Q p k q h
    | Q@h:q.copy => h_5 Q q h
    | Q@h:q.succ => h_6 Q q h
    | Q@h:(q₁.pred q₂) => h_7 Q q₁ q₂ h
    | Q@h:(Turing.PartrecToTM2.Λ'.ret k) => h_8 Q k h) =
    h_6 q.succ q ⋯
-- Mathlib.AlgebraicGeometry.Restrict
/-- The restriction of a morphism `f : X ⟶ Y` to open sets on the source and target.  -/
AlgebraicGeometry.Scheme.Hom.resLE : {X Y : AlgebraicGeometry.Scheme} →
  (f : X.Hom Y) → (U : Y.Opens) → (V : X.Opens) → V ≤ (TopologicalSpace.Opens.map f.base).obj U → (↑V ⟶ ↑U)
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.opEquiv_symm_apply : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S : Subsemiring Rᵐᵒᵖ), (RelIso.symm Subsemiring.opEquiv) S = S.unop
-- Mathlib.Analysis.Analytic.Basic
FormalMultilinearSeries.partialSum.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : ContinuousConstSMul 𝕜 E]
  [inst_10 : ContinuousConstSMul 𝕜 F] (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) (x : E),
  p.partialSum n x = ∑ k ∈ Finset.range n, (p k) fun x_1 => x
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.instPowInt : {G : Type u_1} → [inst : Add G] → {a : G} → Pow (AddConstEquiv G G a a) ℤ
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- Eta-expanded form of `MeasureTheory.lintegral_indicator_one_le` -/
MeasureTheory.lintegral_indicator_fun_one_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α),
  ∫⁻ (a : α), s.indicator (fun x => 1) a ∂μ ≤ μ s
-- Mathlib.Algebra.Algebra.Opposite
AlgHom.toLinearMap_fromOpposite : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (hf : ∀ (x y : A), Commute (f x) (f y)),
  (f.fromOpposite hf).toLinearMap = f.toLinearMap ∘ₗ ↑(MulOpposite.opLinearEquiv R).symm
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.sup_pure : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → ∀ (x : α), (l ⊔ pure x).HasBasis p fun i => s i ∪ {x}
-- Mathlib.Data.Multiset.FinsetOps
Multiset.Nodup.ndunion : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) {t : Multiset α}, t.Nodup → (s.ndunion t).Nodup
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.prod_le_pow_card : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] [MulLeftMono α] (s : Multiset α) (n : α),
  (∀ x ∈ s, x ≤ n) → s.prod ≤ n ^ s.card
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.trans_apply : ∀ {α : Type u} {β : Type u_1} {γ : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] [inst_2 : UniformSpace γ]
  (h₁ : α ≃ᵤ β) (h₂ : β ≃ᵤ γ) (a : α), (h₁.trans h₂) a = h₂ (h₁ a)
-- Mathlib.Data.Int.Fib.Basic
Int.coe_fib_neg : ∀ (n : ℤ), ↑(Int.fib (-n)) = (-1) ^ (n + 1) * ↑(Int.fib n)
-- Mathlib.Order.Partition.Finpartition
Finpartition.toSubtype.eq_1 : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {s : α} (P : Finpartition s) {Pr : α → Prop}
  (Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)) (Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)) (Prbot : Pr ⊥)
  (hs : Pr s) (hP : ∀ p ∈ P.parts, Pr p),
  P.toSubtype Prsup Prinf Prbot hs hP =
    { parts := P.parts.preimage Subtype.val ⋯, supIndep := ⋯, sup_parts := ⋯, bot_notMem := ⋯ }
-- Aesop.Stats.Basic
Aesop.MonadStats.toMonadOptions : {m : Type → Type} → [self : Aesop.MonadStats m] → Lean.MonadOptions m
-- Mathlib.Data.Nat.Choose.Lucas
/-- For primes `p`, `choose n k` is congruent to the product of `choose (⌊n / p ^ i⌋ % p)
(⌊k / p ^ i⌋ % p)` over i < a, multiplied by `choose (⌊n / p ^ a⌋) (⌊k / p ^ a⌋)`, modulo `p`.  -/
Choose.choose_modEq_choose_mul_prod_range_choose : ∀ {n k p : ℕ} [Fact (Nat.Prime p)] (a : ℕ),
  ↑(n.choose k) ≡
    ↑((n / p ^ a).choose (k / p ^ a)) * ↑(∏ i ∈ Finset.range a, (n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.SolverExtension.getStateCoreImpl : {σ : Type} → Lean.Meta.Grind.SolverExtension σ → Lean.Meta.Grind.Goal → IO σ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ext_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp], (Std.ExtDTreeMap.Const.toList t₁).Perm (Std.ExtDTreeMap.Const.toList t₂) → t₁ = t₂
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.Scheme.isAffine_of_isLimit : ∀ {I : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} I] {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme}
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c)
  [∀ (i : I), AlgebraicGeometry.IsAffine (D.obj i)], AlgebraicGeometry.IsAffine c.pt
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.SimpleFunc.negPart.eq_1 : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : ↥(α →₁ₛ[μ] ℝ)),
  MeasureTheory.L1.SimpleFunc.negPart f = MeasureTheory.L1.SimpleFunc.posPart (-f)
-- Mathlib.LinearAlgebra.Dimension.RankNullity
/-- Given a family of `n` linearly independent vectors in a finite-dimensional space of
dimension `> n`, one may extend the family by another vector while retaining linear independence.  -/
exists_linearIndependent_snoc_of_lt_finrank : ∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [HasRankNullity.{u, u_1} R] [StrongRankCondition R] {n : ℕ} {v : Fin n → M},
  LinearIndependent R v → n < Module.finrank R M → ∃ x, LinearIndependent R (Fin.snoc v x)
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializationOptions.mk.injEq : ∀ (hasWidgets? : Option Bool) (logCfg? : Option Lean.Lsp.LogConfig) (hasWidgets?_1 : Option Bool)
  (logCfg?_1 : Option Lean.Lsp.LogConfig),
  ({ hasWidgets? := hasWidgets?, logCfg? := logCfg? } = { hasWidgets? := hasWidgets?_1, logCfg? := logCfg?_1 }) =
    (hasWidgets? = hasWidgets?_1 ∧ logCfg? = logCfg?_1)