mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit.eq_def : ∀ (e : Lean.Expr) (offset : ℕ) (fn : Lean.Expr → ℕ → Lean.Meta.Sym.Internal.AlphaShareBuilderM (Option Lean.Expr)),
  Lean.Meta.Sym.visit✝ e offset fn =
    match e with
    | Lean.Expr.lit a =>
      panicWithPosWithDecl "Lean.Meta.Sym.ReplaceS" "_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit" 35 67
        "unreachable code has been reached"
    | Lean.Expr.mvar mvarId =>
      panicWithPosWithDecl "Lean.Meta.Sym.ReplaceS" "_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit" 35 67
        "unreachable code has been reached"
    | Lean.Expr.bvar deBruijnIndex =>
      panicWithPosWithDecl "Lean.Meta.Sym.ReplaceS" "_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit" 35 67
        "unreachable code has been reached"
    | Lean.Expr.fvar fvarId =>
      panicWithPosWithDecl "Lean.Meta.Sym.ReplaceS" "_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit" 35 67
        "unreachable code has been reached"
    | Lean.Expr.const declName us =>
      panicWithPosWithDecl "Lean.Meta.Sym.ReplaceS" "_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit" 35 67
        "unreachable code has been reached"
    | Lean.Expr.sort u =>
      panicWithPosWithDecl "Lean.Meta.Sym.ReplaceS" "_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit" 35 67
        "unreachable code has been reached"
    | f.app a => do
      let __do_lift ← Lean.Meta.Sym.visitChild✝ f offset fn
      let __do_lift_1 ← Lean.Meta.Sym.visitChild✝ a offset fn
      e.updateAppS! __do_lift __do_lift_1
    | Lean.Expr.mdata data a => do
      let __do_lift ← Lean.Meta.Sym.visitChild✝ a offset fn
      e.updateMDataS! __do_lift
    | Lean.Expr.proj typeName idx a => do
      let __do_lift ← Lean.Meta.Sym.visitChild✝ a offset fn
      e.updateProjS! __do_lift
    | Lean.Expr.forallE binderName d b binderInfo => do
      let __do_lift ← Lean.Meta.Sym.visitChild✝ d offset fn
      let __do_lift_1 ← Lean.Meta.Sym.visitChild✝ b (offset + 1) fn
      e.updateForallS! __do_lift __do_lift_1
    | Lean.Expr.lam binderName d b binderInfo => do
      let __do_lift ← Lean.Meta.Sym.visitChild✝ d offset fn
      let __do_lift_1 ← Lean.Meta.Sym.visitChild✝ b (offset + 1) fn
      e.updateLambdaS! __do_lift __do_lift_1
    | Lean.Expr.letE declName t v b nondep => do
      let __do_lift ← Lean.Meta.Sym.visitChild✝ t offset fn
      let __do_lift_1 ← Lean.Meta.Sym.visitChild✝ v offset fn
      let __do_lift_2 ← Lean.Meta.Sym.visitChild✝ b (offset + 1) fn
      e.updateLetS! __do_lift __do_lift_1 __do_lift_2
-- Init.Core
DoResultPR.return.injEq : ∀ {α β σ : Type u} (a : β) (a_1 : σ) (a_2 : β) (a_3 : σ),
  (DoResultPR.return a a_1 = DoResultPR.return a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.Topology.Constructions
Topology.IsOpenEmbedding.piMap : ∀ {ι : Type u_5} {A : ι → Type u_6} {B : ι → Type u_7} [T : (i : ι) → TopologicalSpace (A i)]
  [inst : (i : ι) → TopologicalSpace (B i)] [Finite ι] {f : (i : ι) → A i → B i},
  (∀ (i : ι), Topology.IsOpenEmbedding (f i)) → Topology.IsOpenEmbedding (Pi.map f)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.fold_push_apply : ∀ {α : Type u} {β : α → Type v} {γ : Type w} {l : Std.DHashMap.Raw α β} {acc : Array γ} (f : (a : α) → β a → γ),
  Std.DHashMap.Raw.fold (fun acc k v => acc.push (f k v)) acc l =
    acc ++ Array.map (fun p => f p.fst p.snd) (Std.DHashMap.Internal.toListModel l.buckets).toArray
-- Mathlib.RingTheory.Valuation.Discrete.Basic
/-- If two elements of `K₀` are uniformizers, then they are associated.  -/
Valuation.associated_of_isUniformizer : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {K : Type u_2} [inst_1 : Field K] {v : Valuation K Γ}
  [hv : v.IsRankOneDiscrete] {π₁ π₂ : ↥v.valuationSubring}, v.IsUniformizer ↑π₁ → v.IsUniformizer ↑π₂ → Associated π₁ π₂
-- Mathlib.Control.Monad.Writer
instMonadWriterAdapterWriterTOfMonad : {ω : Type u} → {m : Type u → Type u_1} → [Monad m] → MonadWriterAdapter ω (WriterT ω m)
-- Mathlib.Data.Finsupp.Single
Finsupp.card_support_le_one' : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] [Nonempty α] {f : α →₀ M}, f.support.card ≤ 1 ↔ ∃ a b, f = fun₀ | a => b
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.constantCoeff_eq : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R], ⇑MvPolynomial.constantCoeff = MvPolynomial.coeff 0
-- Lean.Data.Lsp.Internal
/-- Start line of the range of this location.  -/
Lean.Lsp.RefInfo.Location.startPosLine : Lean.Lsp.RefInfo.Location → ℕ
-- Std.Internal.UV.System
Std.Internal.UV.System.RUsage.inBlock : Std.Internal.UV.System.RUsage → UInt64
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.bot : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {f : α → E} {g : α → F}, f =o[𝕜; ⊥] g
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforwardNatTrans_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} {T : CategoryTheory.Sheaf J RingCat} {S : CategoryTheory.Sheaf K RingCat}
  [inst_2 : G.IsContinuous J K] (φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S),
  SheafOfModules.pushforwardNatTrans φ (CategoryTheory.CategoryStruct.id G) = (SheafOfModules.pushforwardCongr ⋯).hom
-- Mathlib.Geometry.Euclidean.Projection
EuclideanGeometry.reflection_apply : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] (p : P),
  (EuclideanGeometry.reflection s) p =
    s.direction.reflection (p -ᵥ ↑(Classical.arbitrary ↥s)) +ᵥ ↑(Classical.arbitrary ↥s)
-- Lean.Server.RequestCancellation
Lean.Server.RequestCancellationToken.mk.inj : ∀ {cancelledByCancelRequest cancelledByEdit : IO.CancelToken}
  {requestCancellationPromise editCancellationPromise : IO.Promise Unit}
  {cancelledByCancelRequest_1 cancelledByEdit_1 : IO.CancelToken}
  {requestCancellationPromise_1 editCancellationPromise_1 : IO.Promise Unit},
  { cancelledByCancelRequest := cancelledByCancelRequest, cancelledByEdit := cancelledByEdit,
        requestCancellationPromise := requestCancellationPromise, editCancellationPromise := editCancellationPromise } =
      { cancelledByCancelRequest := cancelledByCancelRequest_1, cancelledByEdit := cancelledByEdit_1,
        requestCancellationPromise := requestCancellationPromise_1,
        editCancellationPromise := editCancellationPromise_1 } →
    cancelledByCancelRequest = cancelledByCancelRequest_1 ∧
      cancelledByEdit = cancelledByEdit_1 ∧
        requestCancellationPromise = requestCancellationPromise_1 ∧ editCancellationPromise = editCancellationPromise_1
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.coe_orderAddMonoidHom_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] (f : α →+*o β) (a : α), ↑f a = f a
-- Mathlib.Data.Finset.Sups
Finset.infs_sups_subset_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DistribLattice α] (s t u : Finset α), (t ⊻ u) ⊼ s ⊆ t ⊼ s ⊻ u ⊼ s
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalStarRing.hom_ext : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonUnitalNonAssocSemiring (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [inst_6 : (i : ι) → StarRing (G i)]
  [inst_7 : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)] [inst_8 : Nonempty ι] (P : Type u_7)
  [inst_9 : NonUnitalNonAssocSemiring P] [inst_10 : StarRing P] {g₁ g₂ : DirectLimit G f →⋆ₙ+* P},
  (∀ (i : ι), g₁.comp (DirectLimit.NonUnitalStarRing.of G f i) = g₂.comp (DirectLimit.NonUnitalStarRing.of G f i)) →
    g₁ = g₂
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.relNorm_smul : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S] {G : Type u_4}
  [inst_11 : Group G] [inst_12 : MulSemiringAction G S] [SMulCommClass G R S] (g : G) (I : Ideal S),
  (Ideal.relNorm R) (g • I) = (Ideal.relNorm R) I
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1.congr_simp : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] {T T_1 : Set α → E →L[ℝ] F} (e_T : T = T_1) {C C_1 : ℝ} (e_C : C = C_1)
  (hT : MeasureTheory.DominatedFinMeasAdditive μ T C), MeasureTheory.L1.setToL1 hT = MeasureTheory.L1.setToL1 ⋯
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
/-- Given measures `μ` and `ν`, if `s` is a measure mutually singular to `ν` and `f` is a
measurable function such that `μ = s + fν`, then `f = μ.rnDeriv ν`.

This theorem provides the uniqueness of the `rnDeriv` in the Lebesgue decomposition
theorem, while `MeasureTheory.Measure.eq_singularPart` provides the uniqueness of the
`singularPart`. Here, the uniqueness is given in terms of the functions, while the uniqueness in
terms of the functions is given in `eq_withDensity_rnDeriv`.  -/
MeasureTheory.Measure.eq_rnDeriv : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite ν]
  {s : MeasureTheory.Measure α} {f : α → ENNReal},
  Measurable f → s.MutuallySingular ν → μ = s + ν.withDensity f → f =ᵐ[ν] μ.rnDeriv ν
-- Lean.Parser.Do
Lean.Parser.Term.doIfCond.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.FieldTheory.Separable
Polynomial.unique_separable_of_irreducible : ∀ {F : Type u} [inst : Field F] (p : ℕ) [HF : CharP F p] {f : Polynomial F},
  Irreducible f →
    0 < p →
      ∀ (n₁ : ℕ) (g₁ : Polynomial F),
        g₁.Separable →
          (Polynomial.expand F (p ^ n₁)) g₁ = f →
            ∀ (n₂ : ℕ) (g₂ : Polynomial F), g₂.Separable → (Polynomial.expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂
-- Mathlib.LinearAlgebra.Goursat
Submodule.goursatFst_toAddSubgroup : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {L : Submodule R (M × N)},
  L.goursatFst.toAddSubgroup = L.toAddSubgroup.goursatFst
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.inducedMap_zero : ∀ (α : Type u_2) (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α],
  ConditionallyCompleteLinearOrderedField.inducedMap α β 0 = 0
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instZero : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    (ρ : Representation A G V) → (σ : Representation A G W) → Zero (ρ.IntertwiningMap σ)
-- Mathlib.Algebra.Order.Interval.Set.Instances
/-- like `coe_nonneg`, but with the inequality in `Icc (0:R) 1`.  -/
Set.Icc.nonneg : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {t : ↑(Set.Icc 0 1)}, 0 ≤ t
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.instInhabitedΛ' : {Γ : Type u_1} → {Λ : Type u_2} → {σ : Type u_3} → [Inhabited Λ] → Inhabited (Turing.TM1to1.Λ' Γ Λ σ)
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.nz_of_isRat : ∀ {A : Type u_1} {e : A} {n : ℤ} {d : ℕ} [inst : Ring A] [inst_1 : LinearOrder A] [IsStrictOrderedRing A],
  Mathlib.Meta.NormNum.IsRat e n d → decide (n < 0) = true → e ≠ 0
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.commRingNorm : Lean.Meta.Grind.Arith.Cutsat.EqCnstr →
  Lean.Meta.Grind.Arith.CommRing.RingExpr → Lean.Grind.CommRing.Poly → Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkInductiveAux₁.congr_simp : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : ChainComplex V ℕ} (e : P ⟶ Q) (zero zero_1 : P.X 0 ⟶ Q.X 1) (e_zero : zero = zero_1)
  (one one_1 : P.X 1 ⟶ Q.X 2) (e_one : one = one_1)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1))
  (succ succ_1 :
    (n : ℕ) →
      (p :
          (f : P.X n ⟶ Q.X (n + 1)) ×'
            (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f +
                  CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) →
        (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst +
              CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))),
  succ = succ_1 →
    ∀ (n : ℕ), Homotopy.mkInductiveAux₁ e zero one comm_one succ n = Homotopy.mkInductiveAux₁ e zero_1 one_1 ⋯ succ_1 n
-- Mathlib.RingTheory.Ideal.Pointwise
Ideal.mem_inv_pointwise_smul_iff : ∀ {M : Type u_1} {R : Type u_3} [inst : Group M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {a : M}
  {S : Ideal R} {x : R}, x ∈ a⁻¹ • S ↔ a • x ∈ S
-- Mathlib.Order.WithBot
WithBot.monotone_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : WithBot α → β},
  Monotone f ↔ (Monotone fun a => f ↑a) ∧ ∀ (x : α), f ⊥ ≤ f ↑x
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.functorialityEquivalence_unitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor J C) (e : C ≌ D),
  (CategoryTheory.Limits.Cone.functorialityEquivalence F e).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun c =>
        CategoryTheory.Limits.Cone.ext
          (e.unitIso.app ((CategoryTheory.Functor.id (CategoryTheory.Limits.Cone F)).obj c).1) ⋯)
      ⋯
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_const_add : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {x : 𝕜} {s : Set 𝕜} {f : 𝕜 → F},
  0 < n → ∀ (c : F), iteratedDerivWithin n (fun z => c + f z) s x = iteratedDerivWithin n f s x
-- Mathlib.Tactic.CancelDenoms.Core
Mathlib.Tactic.CancelDenoms.sub_subst : ∀ {α : Type u_1} [inst : Ring α] {n e1 e2 t1 t2 : α}, n * e1 = t1 → n * e2 = t2 → n * (e1 - e2) = t1 - t2
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
/-- The isomorphism `(K.restriction e).homology j ≅ K.homology j'` when `e.f j = j'`,
the predecessors `i` and `i'` of `j` and `j'` satisfy `e.f i = i'`,
and the successors `k` and `k'` of `j` and `j'` satisfy `e.f k = k'`  -/
HomologicalComplex.restrictionHomologyIso : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : e.IsRelIff] →
                    (i j k : ι) →
                      c.prev j = i →
                        c.next j = k →
                          {i' j' k' : ι'} →
                            e.f i = i' →
                              e.f j = j' →
                                e.f k = k' →
                                  c'.prev j' = i' →
                                    c'.next j' = k' →
                                      [inst_3 : K.HasHomology j'] →
                                        [inst_4 : (K.restriction e).HasHomology j] →
                                          (K.restriction e).homology j ≅ K.homology j'
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_erase_eq_div : ∀ {ι : Type u_1} {G : Type u_3} {s : Finset ι} [inst : CommGroup G] [inst_1 : DecidableEq ι] {f : ι → G} {a : ι},
  a ∈ s → ∏ x ∈ s.erase a, f x = (∏ x ∈ s, f x) / f a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.field : Lean.Lsp.CompletionItemKind
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
_private.Mathlib.Algebra.Homology.Embedding.ExtendHomotopy.0.Homotopy.extend.homAux.match_1.eq_1 : ∀ {ι : Type u_1} (motive : Option ι → Option ι → Sort u_2) (x : Option ι) (h_1 : (x : Option ι) → motive none x)
  (h_2 : (x : Option ι) → motive x none) (h_3 : (i j : ι) → motive (some i) (some j)),
  (match none, x with
    | none, x => h_1 x
    | x, none => h_2 x
    | some i, some j => h_3 i j) =
    h_1 x
-- Mathlib.SetTheory.Cardinal.ENat
/-- **Alias** of the reverse direction of `Cardinal.ofENat_lt_ofENat`. -/
Cardinal.ofENat_lt_ofENat_of_lt : ∀ {m n : ℕ∞}, m < n → ↑m < ↑n
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_obj_obj₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (j : C),
  ((t.triangleLTLTGELT a b h).obj j).obj₁ = (t.truncLT a).obj j
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- Two simplices with the same points have the same circumcenter.  -/
Affine.Simplex.circumcenter_eq_of_range_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} {s₁ s₂ : Affine.Simplex ℝ P n},
  Set.range s₁.points = Set.range s₂.points → s₁.circumcenter = s₂.circumcenter
-- Mathlib.Order.Hom.Basic
/-- Note that this goal could also be stated `(Codisjoint on f) a b`  -/
Codisjoint.map_orderIso : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderTop α] [inst_2 : SemilatticeSup β]
  [inst_3 : OrderTop β] {a b : α} (f : α ≃o β), Codisjoint a b → Codisjoint (f a) (f b)
-- Mathlib.CategoryTheory.Limits.Creates
/-- If `F` creates limits of shape `J` and `F ≅ G`, then `G` creates limits of shape `J`.  -/
CategoryTheory.createsLimitsOfShapeOfNatIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : Type w} →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            {F G : CategoryTheory.Functor C D} →
              (F ≅ G) → [CategoryTheory.CreatesLimitsOfShape J F] → CategoryTheory.CreatesLimitsOfShape J G
-- Mathlib.Topology.Category.Born
/-- Construct a bundled `Born` from a `Bornology`.  -/
Born.of : (carrier : Type u_1) → [str : Bornology carrier] → Born
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trNormal_run : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} {k : K} (s : Turing.TM2to1.StAct K Γ σ k)
  (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2to1.trNormal (Turing.TM2to1.stRun s q) = Turing.TM1.Stmt.goto fun x x_1 => Turing.TM2to1.Λ'.go k s q
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
/-- **Alias** of `OpenPartialHomeomorph.replacePartialEquiv_eq_self`. -/
OpenPartialHomeomorph.replaceEquiv_eq_self : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (e' : PartialEquiv X Y) (h : e.toPartialEquiv = e'), e.replacePartialEquiv e' h = e
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.combine_mul_k' : ℕ → ℤ → ℤ → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Int.Internal.Linear.Poly
-- Mathlib.Data.EReal.Basic
EReal.one_mul : ∀ (x : EReal), 1 * x = x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.insert.eq_1 : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (l : Std.ExtTreeMap α β cmp) (a : α)
  (b : β), l.insert a b = { inner := l.inner.insert a b }
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DeclarationParams.mk.injEq : ∀ (toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams),
  ({ toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 }) =
    (toTextDocumentPositionParams = toTextDocumentPositionParams_1)
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.toLp_multisetSum : ∀ (p : ENNReal) (V : Type u_4) [inst : AddCommGroup V] (s : Multiset V),
  WithLp.toLp p s.sum = (Multiset.map (WithLp.toLp p) s).sum
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.algebraMap_left_injective : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {S : Type u_3} [inst_1 : CommRing R]
  (v : Valuation R Γ₀) [inst_2 : Semiring S] [inst_3 : Algebra R S],
  Function.Injective ⇑(algebraMap R S) → Function.Injective ⇑(algebraMap (WithVal v) S)
-- Mathlib.Topology.Order
continuous_inf_dom_left : ∀ {α : Type u} {β : Type v} {f : α → β} {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β},
  Continuous f → Continuous f
-- Mathlib.Algebra.Category.ModuleCat.Limits
/-- If `J` is `u`-small, the category of `R`-modules has limits of shape `J`.  -/
ModuleCat.hasLimitsOfShape : ∀ {R : Type u} [inst : Ring R] {J : Type v} [inst_1 : CategoryTheory.Category.{t, v} J] [Small.{w, v} J],
  CategoryTheory.Limits.HasLimitsOfShape J (ModuleCat R)
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
/-- Given the data of a basic constructible set `s = V(g₁, ..., gₙ) \ V(f)`, return `g`.  -/
PrimeSpectrum.BasicConstructibleSetData.g : {R : Type u_1} → (self : PrimeSpectrum.BasicConstructibleSetData R) → Fin self.n → R
-- Mathlib.Analysis.Complex.Basic
Complex.uniformContinuous_re : UniformContinuous Complex.re
-- Init.Data.UInt.Lemmas
UInt64.toUInt8_mod_of_dvd : ∀ (a b : UInt64), b.toNat ∣ 256 → (a % b).toUInt8 = a.toUInt8 % b.toUInt8
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicAt.div : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} {f g : 𝕜 → 𝕜'}, MeromorphicAt f x → MeromorphicAt g x → MeromorphicAt (f / g) x
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.foldRev.eq_2 : ∀ {α : Type u} (x : α) (n : ℕ) (f : (i : ℕ) → i < n.succ → α → α),
  n.succ.foldRev f x = n.foldRev (fun i h => f i ⋯) (f n ⋯ x)
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.ReflectsLimitOfIsCosplitPair.mk : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D},
  (∀ {A B : C} (f g : A ⟶ B) [F.IsCosplitPair f g],
      CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.parallelPair f g) F) →
    CategoryTheory.Comonad.ReflectsLimitOfIsCosplitPair F
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.of_mul_inv_t : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} (a : ↥A),
  HNNExtension.of ↑a * HNNExtension.t⁻¹ = HNNExtension.t⁻¹ * HNNExtension.of ↑(φ a)
-- Init.Data.Ord.Basic
Ordering.isGT_gt : Ordering.gt.isGT = true