mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapPairLeft_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (Fₗ : CategoryTheory.Functor C E) (Fᵣ : CategoryTheory.Functor D E')
  (X : C),
  (CategoryTheory.Join.mapPairLeft Fₗ Fᵣ).inv.app X =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left (Fₗ.obj X))
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.instIsMulCommutative : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], IsMulCommutative (CategoryTheory.CatCenter C)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.toLp.eq_1 : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : α → E) (h_mem_ℒp : MeasureTheory.MemLp f p μ),
  MeasureTheory.MemLp.toLp f h_mem_ℒp = ⟨MeasureTheory.AEEqFun.mk f ⋯, ⋯⟩
-- Mathlib.Algebra.Group.Basic
add_right_iterate_apply_zero : ∀ {M : Type u_4} [inst : AddMonoid M] {n : ℕ} (a : M), (fun x => x + a)^[n] 0 = n • a
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.val_smul : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A] {𝒜 : ι → σ} (x : Submonoid A)
  {α : Type u_4} [inst_2 : SMul α A] [inst_3 : IsScalarTower α A A] [inst_4 : SMulMemClass σ α A] (n : α)
  (y : HomogeneousLocalization 𝒜 x), (n • y).val = n • y.val
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.terminal_isIso_from : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] {A : C} (f : ⊤_ C ⟶ A), CategoryTheory.IsIso f
-- Lean.CoreM
/-- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`.
Also checks for cancellation, so that recursive elaboration functions
(inferType, whnf, isDefEq, …) respond promptly to interrupt requests.  -/
Lean.Core.withIncRecDepth : {m : Type → Type u_1} → {α : Type} → [Monad m] → [MonadControlT Lean.CoreM m] → m α → m α
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrixAlgEquiv_transpose_apply' : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) (f : M₁ →ₗ[R] M₁) (j : n),
  ((LinearMap.toMatrixAlgEquiv v₁) f).transpose j = ⇑(v₁.repr (f (v₁ j)))
-- Mathlib.Order.UpperLower.Principal
UpperSet.Ici_iSup₂ : ∀ {α : Type u_1} {ι : Sort u_3} {κ : ι → Sort u_4} [inst : CompleteLattice α] (f : (i : ι) → κ i → α),
  UpperSet.Ici (⨆ i, ⨆ j, f i j) = ⨆ i, ⨆ j, UpperSet.Ici (f i j)
-- Mathlib.GroupTheory.Perm.MaximalSubgroups
Equiv.Perm.ofSubtype_mem_stabilizer : ∀ {α : Type u_2} {s : Set α} [inst : DecidablePred fun x => x ∈ s] (g : Equiv.Perm ↑s),
  Equiv.Perm.ofSubtype g ∈ MulAction.stabilizer (Equiv.Perm α) s
-- Init.Data.Int.Bitwise.Lemmas
Int.neg_shiftLeft : ∀ (a : ℤ) (n : ℕ), (-a) <<< n = -a <<< n
-- Lean.Elab.Calc
Lean.Elab.Term.CalcStepView.mk.inj : ∀ {ref : Lean.Syntax} {term proof : Lean.Term} {ref_1 : Lean.Syntax} {term_1 proof_1 : Lean.Term},
  { ref := ref, term := term, proof := proof } = { ref := ref_1, term := term_1, proof := proof_1 } →
    ref = ref_1 ∧ term = term_1 ∧ proof = proof_1
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.Away.awayToAwayLeft_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {P : Type u_3}
  [inst_3 : CommSemiring P] (x : R) [inst_4 : IsLocalization.Away x S] (y : R) [inst_5 : Algebra R P]
  [inst_6 : IsLocalization.Away (y * x) P] (a : R),
  (IsLocalization.Away.awayToAwayLeft x y) ((algebraMap R S) a) = (algebraMap R P) a
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_insertMany_list : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α},
  (m.insertMany l)[k]? =
    (List.findSomeRev?
          (fun x_2 =>
            match x_2 with
            | (a, b) => if (a == k) = true then some b else none)
          l).or
      m[k]?
-- Std.Data.Internal.List.Associative
Std.Internal.List.le_maxKey!_of_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α}, Std.Internal.List.containsKey k l = true → (compare k (Std.Internal.List.maxKey! l)).isLE = true
-- Mathlib.Data.Nat.Basic
Nat.dvd_sub_self_right : ∀ {n m : ℕ}, n ∣ m - n ↔ n ∣ m ∨ m ≤ n
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
/-- If `x` is a transcendence basis of `A/R`, then it is empty if and only if
`A/R` is algebraic.  -/
IsTranscendenceBasis.isEmpty_iff_isAlgebraic : ∀ {ι : Type u} {R : Type u_1} {A : Type w} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Nontrivial R], IsTranscendenceBasis R x → (IsEmpty ι ↔ Algebra.IsAlgebraic R A)
-- Mathlib.Data.Num.Bitwise
NzsNum.bit.injEq : ∀ (a : Bool) (a_1 : NzsNum) (a_2 : Bool) (a_3 : NzsNum), (NzsNum.bit a a_1 = NzsNum.bit a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.mem_mk : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {S : NonUnitalSubsemiring R} {x : R}
  (h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier), x ∈ { toNonUnitalSubsemiring := S, neg_mem' := h } ↔ x ∈ S
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_insertIfNew_le_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (cmp ((t.insertIfNew k v).minKey ⋯) k).isLE = true
-- Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory
/-- The type of morphisms in the semi-simplex category are order embeddings.
This type is made irreducible: use `SemiSimplexCategory.homEquiv` to make
the conversion.  -/
SemiSimplexCategory.Hom : SemiSimplexCategory → SemiSimplexCategory → Type
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- Functional equation for the odd Hurwitz zeta function.  -/
HurwitzZeta.completedHurwitzZetaOdd_one_sub : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.completedHurwitzZetaOdd a (1 - s) = HurwitzZeta.completedSinZeta a s
-- Mathlib.CategoryTheory.Limits.Types.Colimits
/-- (internal implementation) the fact that the proposed colimit cocone is the colimit  -/
CategoryTheory.Limits.Types.colimitCoconeIsColimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J (Type u)) →
      [inst_1 : Small.{u, max u v} F.ColimitType] →
        CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Types.colimitCocone F)
-- Mathlib.Geometry.Convex.Cone.Face.Basic
PointedCone.IsFaceOf.sum_mem_iff_mem : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {C F : PointedCone R M} {ι : Type u_4} [inst_5 : Fintype ι]
  {f : ι → M}, F.IsFaceOf C → (∀ (i : ι), f i ∈ C) → (∑ i, f i ∈ F ↔ ∀ (i : ι), f i ∈ F)
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.of_pow : ∀ {α : Type u_2} {f : Equiv.Perm α} [inst : DecidableEq α] [inst_1 : Fintype α] {n : ℕ},
  (f ^ n).IsCycle → f.support ⊆ (f ^ n).support → f.IsCycle
-- Mathlib.Tactic.Linarith.Verification
/-- Typesafe conversion of `n : ℕ` to `Q($α)`.  -/
Qq.ofNatQ : {u : Lean.Level} →
  (α :
      have u := u;
      Q(Type u)) →
    Q(Semiring «$α») → ℕ → Q(«$α»)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Φ_neg : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ), W.Φ (-n) = W.Φ n
-- Mathlib.Data.Finsupp.Basic
Finsupp.embDomain_inr : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Zero γ] (b : β →₀ γ),
  Finsupp.embDomain Function.Embedding.inr b = Finsupp.sumElim 0 b
-- Mathlib.FieldTheory.Finite.GaloisField
FiniteField.nonempty_algHom_of_finrank_dvd : ∀ {F : Type u_3} {K : Type u_4} {L : Type u_5} [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K]
  [inst_3 : Field L] [inst_4 : Algebra F L] [Finite L], Module.finrank F K ∣ Module.finrank F L → Nonempty (K →ₐ[F] L)
-- Init.Data.Array.MapIdx
Array.size_mapFinIdx : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β}, (xs.mapFinIdx f).size = xs.size
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.toArray_filterMap : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w}
  {f : (a : α) → β a → Option (γ a)} (h : t.WF),
  (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl.toArray =
    Array.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toArray
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
ContinuousWithinAt.clm_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {G : Type u_4} [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {X : Type u_5}
  [inst_7 : TopologicalSpace X] {g : X → F →L[𝕜] G} {f : X → E →L[𝕜] F} {s : Set X} {x : X},
  ContinuousWithinAt g s x → ContinuousWithinAt f s x → ContinuousWithinAt (fun x => g x ∘SL f x) s x
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.size_toArray : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.Rxi.HasSize α] [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxi.IsAlwaysFinite α]
  [Std.Rxi.LawfulHasSize α], r.toArray.size = r.size
-- Mathlib.Topology.MetricSpace.Thickening
Metric.hasBasis_nhdsSet_cthickening : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {K : Set α},
  IsCompact K → (nhdsSet K).HasBasis (fun δ => 0 < δ) fun δ => Metric.cthickening δ K
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
/-- One can get `f'' v w` as the limit of `h ^ (-2)` times the alternate sum of the values of `f`
along the vertices of a quadrilateral with sides `h v` and `h w` based at `x`.
In a setting where `f` is not guaranteed to be continuous at `f`, we can still
get this if we use a quadrilateral based at `h v + h w`.  -/
Convex.isLittleO_alternate_sum_square : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {s : Set E},
  Convex ℝ s →
    ∀ {f : E → F} {f' : E → E →L[ℝ] F} {f'' : E →L[ℝ] E →L[ℝ] F},
      (∀ x ∈ interior s, HasFDerivAt f (f' x) x) →
        ∀ {x : E},
          x ∈ s →
            HasFDerivWithinAt f' f'' (interior s) x →
              ∀ {v w : E},
                x + 4 • v ∈ interior s →
                  x + 4 • w ∈ interior s →
                    (fun h =>
                        f (x + h • (2 • v + 2 • w)) + f (x + h • (v + w)) - f (x + h • (2 • v + w)) -
                            f (x + h • (v + 2 • w)) -
                          h ^ 2 • (f'' v) w) =o[nhdsWithin 0 (Set.Ioi 0)]
                      fun h => h ^ 2
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.List.filterMapM.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Std.Data.String.ToInt
_private.Std.Data.String.ToInt.0.String.Slice.isInt.match_1.eq_1 : ∀ (motive : Option String.Slice → Sort u_1) (rest : String.Slice) (h_1 : (rest : String.Slice) → motive (some rest))
  (h_2 : Unit → motive none),
  (match some rest with
    | some rest => h_1 rest
    | none => h_2 ()) =
    h_1 rest
-- Mathlib.Computability.RegularExpressions
RegularExpression.map.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), RegularExpression.map f RegularExpression.epsilon = 1
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The first projection `(homotopyCofiber φ).X i ⟶ F.X j` when `c.Rel i j`.  -/
HomologicalComplex.homotopyCofiber.fstX : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {F G : HomologicalComplex C c} →
            (φ : F ⟶ G) →
              [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
                [inst_3 : DecidableRel c.Rel] →
                  (i j : ι) → c.Rel i j → (HomologicalComplex.homotopyCofiber.X φ i ⟶ F.X j)
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
/-- If `G : C ⥤ H` admits a left Kan extension along a functor `L : C ⥤ D` and `H` has colimits of
shape `C` and `D`, then the colimit of `G` is isomorphic to the colimit of a canonical functor
`Grothendieck (CostructuredArrow.functor L) ⥤ H` induced by `L` and `G`.  -/
CategoryTheory.Functor.colimitIsoColimitGrothendieck : {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] →
        (L : CategoryTheory.Functor C D) →
          {H : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} H] →
              (G : CategoryTheory.Functor C H) →
                [inst_3 : L.HasPointwiseLeftKanExtension G] →
                  [inst_4 : CategoryTheory.Limits.HasColimitsOfShape D H] →
                    [inst_5 : CategoryTheory.Limits.HasColimitsOfShape C H] →
                      CategoryTheory.Limits.colimit G ≅
                        CategoryTheory.Limits.colimit ((CategoryTheory.CostructuredArrow.grothendieckProj L).comp G)
-- Mathlib.CategoryTheory.Comma.CardinalArrow
CategoryTheory.small_of_small_arrow : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [Small.{w, max u v} (CategoryTheory.Arrow C)], Small.{w, u} C
-- Init.Data.Array.BasicAux
List.toArray_eq_toArray_eq : ∀ {α : Type u_1} {as bs : List α}, (as.toArray = bs.toArray) = (as = bs)
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- **Alias** of `MonoidHom.pi_injective`. -/
MonoidHom.injective_pi : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → MulOneClass (f i)] {γ : Type w} [Nonempty I] [inst_2 : MulOneClass γ]
  (g : (i : I) → γ →* f i), (∀ (i : I), Function.Injective ⇑(g i)) → Function.Injective ⇑(MonoidHom.pi g)
-- Init.Data.Order.Lemmas
Std.lt_of_le_of_lt : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] [Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2]
  [Std.LawfulOrderLT α] {a b c : α}, a ≤ b → b < c → a < c
-- Mathlib.Algebra.Group.Commute.Basic
AddCommute.addConj : ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, AddCommute a b → ∀ (h : G), AddCommute (h + a + -h) (h + b + -h)
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.coeff_zero : ∀ {σ : Type u_1} {τ : Type u_4} {S : Type u_5} [inst : CommRing S] {a : σ → MvPowerSeries τ S},
  MvPowerSeries.HasSubst a → ∀ (d : τ →₀ ℕ), {s | (MvPowerSeries.coeff d) (a s) ≠ 0}.Finite
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.Pattern.mk : {A : Type u_1} →
  {G : Type u_2} →
    [inst : Inhabited A] →
      (config : G → A) →
        (support : Finset G) → (∀ g ∉ support, config g = default) → SymbolicDynamics.FullShift.Pattern A G
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_apply_ne : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] (d : n → α) {i j : n},
  i ≠ j → Matrix.diagonal d i j = 0
-- Mathlib.RingTheory.RootsOfUnity.EnoughRootsOfUnity
HasEnoughRootsOfUnity.mk : ∀ {M : Type u_1} [inst : CommMonoid M] {n : ℕ},
  (∃ m, IsPrimitiveRoot m n) → IsCyclic ↥(rootsOfUnity n M) → HasEnoughRootsOfUnity M n
-- Lean.Data.FuzzyMatching
Lean.FuzzyMatching.CharRole.separator.sizeOf_spec : sizeOf Lean.FuzzyMatching.CharRole.separator = 1
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.toSucc_surjectivity : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_3 : CategoryTheory.Limits.HasPushouts C]
  [inst_4 : CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)]
  {X Y : C} (f : X ⟶ Y),
  W f →
    ∀ (g : X ⟶ Z),
      ∃ g',
        CategoryTheory.CategoryStruct.comp f g' =
          CategoryTheory.CategoryStruct.comp g (CategoryTheory.OrthogonalReflection.toSucc W Z)
-- Lean.Linter.TacticTypeCheck
/-- A linter that runs `Meta.check _ .implicit` on every tactic goal.  -/
_private.Lean.Linter.TacticTypeCheck.0.Lean.Linter.tacticCheckInstances : Lean.Linter
-- Mathlib.Tactic.Linter.DocString
_private.Mathlib.Tactic.Linter.DocString.0.Mathlib.Linter.getDeclModifiers.match_1.eq_1 : ∀ (motive : Lean.Syntax → Sort u_1) (info : Lean.SourceInfo) (kind : Lean.SyntaxNodeKind) (args : Array Lean.Syntax)
  (h_1 :
    (s : Lean.Syntax) →
      (info : Lean.SourceInfo) →
        (kind : Lean.SyntaxNodeKind) →
          (args : Array Lean.Syntax) → s = Lean.Syntax.node info kind args → motive (Lean.Syntax.node info kind args))
  (h_2 : (x : Lean.Syntax) → motive x),
  (match Lean.Syntax.node info kind args with
    | s@h:(Lean.Syntax.node info kind args) => h_1 s info kind args h
    | x => h_2 x) =
    h_1 (Lean.Syntax.node info kind args) info kind args ⋯
-- Std.Internal.Do.Order.Basic
Lean.Order.le_meet : ∀ {α : Type u} [inst : Lean.Order.CompleteLattice α] (x y z : α),
  Lean.Order.PartialOrder.rel x y →
    Lean.Order.PartialOrder.rel x z → Lean.Order.PartialOrder.rel x (Lean.Order.meet y z)
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.unop.eq_1 : ∀ {M : Type u_2} [inst : AddZeroClass M] (x : AddSubmonoid Mᵃᵒᵖ),
  x.unop = { carrier := AddOpposite.op ⁻¹' ↑x, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.Geometry.RingedSpace.Basic
AlgebraicGeometry.RingedSpace.basicOpen_of_isUnit : ∀ (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
  {f : ↑(X.presheaf.obj (Opposite.op U))}, IsUnit f → X.basicOpen f = U
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.ofTwoCocycle.mk.inj : ∀ {R : Type u_5} {L : Type u_6} {M : Type u_7} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L}
  {inst_3 : AddCommGroup M} {inst_4 : Module R M} {inst_5 : LieRingModule L M} {inst_6 : LieModule R L M}
  {c : ↥(LieModule.Cohomology.twoCocycle R L M)} {carrier carrier_1 : L × M},
  { carrier := carrier } = { carrier := carrier_1 } → carrier = carrier_1
-- Mathlib.Topology.MetricSpace.ProperSpace.Lemmas
isProperMap_nndist : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [ProperSpace α] (x : α), IsProperMap (nndist x)
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarSubalgebra.instIsTopologicalRing : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : TopologicalSpace A] [inst_2 : NonUnitalRing A]
  [inst_3 : Module R A] [inst_4 : Star A] [IsTopologicalRing A] (s : NonUnitalStarSubalgebra R A), IsTopologicalRing ↥s
-- Mathlib.Order.Category.Lat
Lat.instCoeSortType : CoeSort Lat (Type u_1)
-- Mathlib.Tactic.GCongr.Core
/-- The number of arguments that `declName` takes when applying it.  -/
Mathlib.Tactic.GCongr.GCongrLemma.numHyps : Mathlib.Tactic.GCongr.GCongrLemma → ℕ
-- Mathlib.Topology.UniformSpace.Closeds
UniformContinuous.prod_closeds : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : UniformSpace α] [inst_1 : UniformSpace β]
  [inst_2 : UniformSpace γ] {f : α → TopologicalSpace.Closeds β} {g : α → TopologicalSpace.Closeds γ},
  UniformContinuous f → UniformContinuous g → UniformContinuous fun x => f x ×ˢ g x
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfLEArgs.isLE_compare : ∀ {α : Type u} (self : Std.Packages.LinearPreorderOfLEArgs α),
  let this := self.le;
  let this_1 := self.decidableLE;
  let this_2 := self.ord;
  ∀ (a b : α), (compare a b).isLE = true ↔ a ≤ b
-- Mathlib.Topology.Algebra.Valued.NormedValued
Valuation.norm_nonneg : ∀ {L : Type u_1} [inst : Field L] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation L Γ₀)
  [hv : v.RankOne] (x : L), 0 ≤ v.norm x
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.mul_sUnion : ∀ {α : Type u_2} [inst : Mul α] (s : Set α) (T : Set (Set α)), s * ⋃₀ T = ⋃ t ∈ T, s * t
-- Init.Data.Option.Lemmas
Option.any_merge : ∀ {α : Type u_1} {p : α → Bool} {f : α → α → α},
  (∀ (a b : α), p (f a b) = (p a || p b)) →
    ∀ {o o' : Option α}, Option.any p (Option.merge f o o') = (Option.any p o || Option.any p o')
-- Lean.Elab.DefView
Lean.Elab.DefView.value : Lean.Elab.DefView → Lean.Syntax
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.Context.mk.injEq : ∀ (config config_1 : Lean.Try.Config), ({ config := config } = { config := config_1 }) = (config = config_1)
-- Mathlib.Computability.Reduce
oneOneReducible_refl : ∀ {α : Type u_1} [inst : Primcodable α] (p : α → Prop), p ≤₁ p
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.extendCone_obj_π_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cone (F.comp G)) (d : D),
  (CategoryTheory.Functor.Initial.extendCone.obj c).π.app d =
    CategoryTheory.CategoryStruct.comp (c.π.app (CategoryTheory.Functor.Initial.lift F d))
      (G.map (CategoryTheory.Functor.Initial.homToLift F d))
-- Lean.Meta.Tactic.Grind.Theorems
/-- A `TheoremsArray α` is a collection of `Theorems α`.
The array is scanned linear during theorem activation.
This avoids the need for efficiently merging the `Theorems α` data structure.
 -/
Lean.Meta.Grind.TheoremsArray : Type → Type
-- Mathlib.Data.PNat.Factors
PrimeMultiset.prod_smul : ∀ (d : ℕ) (u : PrimeMultiset), (d • u).prod = u.prod ^ d
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The pre-`0`-hypercover defined by a single morphism.  -/
CategoryTheory.PreZeroHypercover.singleton : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {S T : C} → (S ⟶ T) → CategoryTheory.PreZeroHypercover T
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.isClosedEmbedding_mk_symm : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsClosedEmbedding ⇑DomMulAct.mk.symm
-- Mathlib.Topology.Neighborhoods
eventually_eventuallyEq_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {x : X} {f g : X → α},
  (∀ᶠ (y : X) in nhds x, f =ᶠ[nhds y] g) ↔ f =ᶠ[nhds x] g
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.union! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] {t₁ : Std.DTreeMap.Internal.Impl α β},
  t₁.WF → ∀ {t₂ : Std.DTreeMap.Internal.Impl α β}, t₂.WF → (t₁.union! t₂).WF
-- Mathlib.CategoryTheory.Category.Cat.Terminal
/-- Any `T : Cat.{u, u}` with a unique object and discrete homs is isomorphic to `⊤_ Cat.{u, u}.`  -/
CategoryTheory.Cat.terminalIsoOfUniqueOfIsDiscrete : {T : Type u} →
  [inst : CategoryTheory.Category.{v, u} T] →
    [Unique T] → [CategoryTheory.IsDiscrete T] → ⊤_ CategoryTheory.Cat ≅ CategoryTheory.Cat.of T
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.fullyFaihtfulForget₂ToAddMonCat.eq_1 : AddGrpCat.fullyFaihtfulForget₂ToAddMonCat =
  { preimage := fun {X Y} f => AddGrpCat.ofHom (AddMonCat.Hom.hom f),
    map_preimage := @AddGrpCat.fullyFaihtfulForget₂ToAddMonCat._proof_1,
    preimage_map := @AddGrpCat.fullyFaihtfulForget₂ToAddMonCat._proof_2 }
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.ones_length : ∀ (n : ℕ), (Composition.ones n).length = n
-- Mathlib.Combinatorics.Matroid.Map
Matroid.mapEmbedding.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (M : Matroid α) (f : α ↪ β), M.mapEmbedding f = M.map ⇑f ⋯
-- Mathlib.Combinatorics.Colex
Finset.sum_toFinset_bitIndices_two_pow : ∀ (n : ℕ), ∑ i ∈ n.bitIndices.toFinset, 2 ^ i = n
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CanonArgKey.mk : Lean.Expr → ℕ → Lean.Expr → Lean.Meta.Grind.CanonArgKey