mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Defs
NonAssocRing.mk : {α : Type u_1} →
  [toNonUnitalNonAssocRing : NonUnitalNonAssocRing α] →
    [toOne : One α] →
      (∀ (a : α), 1 * a = a) →
        (∀ (a : α), a * 1 = a) →
          [toNatCast : NatCast α] →
            autoParam (↑0 = 0) AddMonoidWithOne.natCast_zero._autoParam →
              autoParam (∀ (n : ℕ), ↑(n + 1) = ↑n + 1) AddMonoidWithOne.natCast_succ._autoParam →
                [toIntCast : IntCast α] →
                  autoParam (∀ (n : ℕ), IntCast.intCast ↑n = ↑n) AddGroupWithOne.intCast_ofNat._autoParam →
                    autoParam (∀ (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1))
                        AddGroupWithOne.intCast_negSucc._autoParam →
                      NonAssocRing α
-- Mathlib.Data.Option.NAry
Option.map_map₂_antidistrib : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → β → γ} {a : Option α} {b : Option β}
  {α' : Type u_5} {β' : Type u_6} {g : γ → δ} {f' : β' → α' → δ} {g₁ : β → β'} {g₂ : α → α'},
  (∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)) →
    Option.map g (Option.map₂ f a b) = Option.map₂ f' (Option.map g₁ b) (Option.map g₂ a)
-- Batteries.Data.MLList.Basic
/-- Concatenate two monadic lazy lists.  -/
MLList.append : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → MLList m α → (Unit → MLList m α) → MLList m α
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
/-- Möbius inversion for functions to a `CommGroupWithZero`, where the equalities only hold on
a well-behaved set.  -/
ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero : ∀ {R : Type u_1} [inst : CommGroupWithZero R] (s : Set ℕ),
  (∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) →
    ∀ {f g : ℕ → R},
      (∀ n > 0, f n ≠ 0) →
        (∀ n > 0, g n ≠ 0) →
          ((∀ n > 0, n ∈ s → ∏ i ∈ n.divisors, f i = g n) ↔
            ∀ n > 0, n ∈ s → ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ ArithmeticFunction.moebius x.1 = f n)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β),
  FreeMonoid.map f =
    { toFun := fun l => FreeMonoid.ofList (List.map f (FreeMonoid.toList l)), map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.Box.face.eq_1 : ∀ {n : ℕ} (I : BoxIntegral.Box (Fin (n + 1))) (i : Fin (n + 1)),
  I.face i = { lower := I.lower ∘ i.succAbove, upper := I.upper ∘ i.succAbove, lower_lt_upper := ⋯ }
-- Mathlib.AlgebraicGeometry.Birational.Birational
/-- `X` and `Y` are birational over `S` if there exists a partial isomorphism between them
that is compatible with the structure maps to `S`.  -/
AlgebraicGeometry.Scheme.BirationalOver : {S X Y : AlgebraicGeometry.Scheme} → (X ⟶ S) → (Y ⟶ S) → Prop
-- Mathlib.RingTheory.IdealFilter.Topology
/-- View an ideal of `A` as a subset of `WithIdealFilter F`.  -/
WithIdealFilter.idealSet : {A : Type u_1} → [inst : Ring A] → {F : IdealFilter A} → Ideal A → Set (WithIdealFilter F)
-- Mathlib.Data.Nat.Init
/-- Two natural numbers are equal if and only if they have the same divisors.  -/
Nat.dvd_left_iff_eq : ∀ {m n : ℕ}, (∀ (a : ℕ), a ∣ m ↔ a ∣ n) ↔ m = n
-- Init.Data.Array.Lemmas
Array.foldrM_empty : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] {f : α → β → m β} {init : β}
  {start stop : ℕ}, Array.foldrM f init #[] start stop = pure init
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.exists_isMinimal : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] (W : WeierstrassCurve K),
  ∃ C, WeierstrassCurve.IsMinimal R (C • W)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prodContinuousLinearEquiv_apply : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : Semiring 𝕜] [inst_3 : AddCommGroup α] [inst_4 : AddCommGroup β] [inst_5 : Module 𝕜 α] [inst_6 : Module 𝕜 β]
  (a : WithLp p (α × β)), (WithLp.prodContinuousLinearEquiv p 𝕜 α β) a = a.ofLp
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_end : ∀ (R : Type u) [inst : Ring R] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  [Module.Finite R M],
  ∃ n S d,
    (∀ (i : Fin n), IsSimpleModule R ↥(S i)) ∧
      (∀ (i : Fin n), NeZero (d i)) ∧
        Nonempty (Module.End R M ≃+* ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (Module.End R ↥(S i))))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_alter!_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {f : Option β → Option β} {hc : k ∈ Std.DTreeMap.Internal.Impl.Const.alter! k f t},
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.Const.alter! k f t) k hc =
    (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).get ⋯
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.congr_refl_refl : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N],
  TensorProduct.congr (LinearEquiv.refl R M) (LinearEquiv.refl R N) = LinearEquiv.refl R (TensorProduct R M N)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.pair.eq_1 : ∀ (x y : ZFSet.{u}), x.pair y = {{x}, {x, y}}
-- Mathlib.Algebra.Torsor.Basic
Pi.vsub_def : ∀ {I : Type u} {fg : I → Type v} [inst : (i : I) → AddGroup (fg i)] {fp : I → Type w}
  [inst_1 : (i : I) → AddTorsor (fg i) (fp i)] (p q : (i : I) → fp i), p -ᵥ q = fun i => p i -ᵥ q i
-- Mathlib.LinearAlgebra.FreeProduct.Basic
_private.Mathlib.LinearAlgebra.FreeProduct.Basic.0.LinearAlgebra.FreeProduct.rel.match_1.eq_1 : ∀ (motive : Fin 2 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()) =
    h_1 ()
-- Lean.Message
Lean.MessageData.instCoeLevel : Coe Lean.Level Lean.MessageData
-- Mathlib.Order.Interval.Set.Infinite
/-- A nonempty preorder with no maximal element is infinite.  -/
NoMaxOrder.infinite : ∀ {α : Type u_1} [inst : Preorder α] [Nonempty α] [NoMaxOrder α], Infinite α
-- Mathlib.Topology.Order.Compact
/-- A continuous function is bounded above on a compact set.  -/
IsCompact.bddAbove_image : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIciTopology α] [Nonempty α] {f : β → α} {K : Set β}, IsCompact K → ContinuousOn f K → BddAbove (f '' K)
-- Mathlib.Data.Seq.Defs
Stream'.Seq.corec_eq : ∀ {α : Type u} {β : Type v} (f : β → Option (α × β)) (b : β),
  (Stream'.Seq.corec f b).destruct = Stream'.Seq.omap (Stream'.Seq.corec f) (f b)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula.0.WeierstrassCurve.Projective.toAffine_slope_of_ne : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  P 2 ≠ 0 →
    Q 2 ≠ 0 →
      P 0 * Q 2 ≠ Q 0 * P 2 →
        W.toAffine.slope (P 0 / P 2) (Q 0 / Q 2) (P 1 / P 2) (Q 1 / Q 2) =
          (P 1 * Q 2 - Q 1 * P 2) / (P 0 * Q 2 - Q 0 * P 2)
-- Init.Data.Float.Model.Unpacked.Pack.Lemmas
Float.Model.UnpackedFloat.packedZero.eq_1 : ∀ (spec : Float.Model.Format) (sign : Float.Model.UnpackedFloat.Sign),
  Float.Model.UnpackedFloat.packedZero spec sign = Float.Model.UnpackedFloat.packComponents spec sign 0 0
-- Init.Data.String.Lemmas.Order
String.Pos.startPos_lt_iff : ∀ {s : String} (p : s.Pos), s.startPos < p ↔ p ≠ s.startPos
-- Mathlib.Topology.Algebra.StarSubalgebra
/-- The `StarSubalgebra.inclusion` of a closed star subalgebra is a `IsClosedEmbedding`.  -/
StarSubalgebra.isClosedEmbedding_inclusion : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A] [inst_6 : StarModule R A]
  {S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂), IsClosed ↑S₁ → Topology.IsClosedEmbedding ⇑(StarSubalgebra.inclusion h)
-- Mathlib.RingTheory.Smooth.StandardSmooth
Algebra.IsStandardSmoothOfRelativeDimension.baseChange : ∀ (n : ℕ) {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_1)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [Algebra.IsStandardSmoothOfRelativeDimension n R S],
  Algebra.IsStandardSmoothOfRelativeDimension n T (TensorProduct R T S)
-- Lean.Parser.Term
Lean.Parser.Term.forInMacro'.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofTacticInfo.inj : ∀ {i i_1 : Lean.Elab.TacticInfo}, Lean.Elab.Info.ofTacticInfo i = Lean.Elab.Info.ofTacticInfo i_1 → i = i_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.Limits.HasPullback.comp_left_left_iff_of_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} {X' : C} (i : X' ⟶ X)
  [CategoryTheory.IsIso i],
  CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp i f) g ↔ CategoryTheory.Limits.HasPullback f g
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- The equivalence of `MulRingNorm R` and `AbsoluteValue R ℝ` when `R` is a nontrivial ring.  -/
MulRingNorm.mulRingNormEquivAbsoluteValue : {R : Type u_2} → [inst : Ring R] → [Nontrivial R] → MulRingNorm R ≃ AbsoluteValue R ℝ
-- Lean.Data.JsonRpc
Lean.JsonRpc.ResponseError.mk : {α : Type u} → Lean.JsonRpc.RequestID → Lean.JsonRpc.ErrorCode → String → Option α → Lean.JsonRpc.ResponseError α
-- Lean.Elab.Tactic.Omega.Core
/-- Wrapping for `Justification.tidy` when `tidy?` is nonempty.  -/
Lean.Elab.Tactic.Omega.Justification.tidy? : {s : Lean.Omega.Constraint} →
  {c : Lean.Omega.Coeffs} →
    Lean.Elab.Tactic.Omega.Justification s c →
      Option ((s' : Lean.Omega.Constraint) × (c' : Lean.Omega.Coeffs) × Lean.Elab.Tactic.Omega.Justification s' c')
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.TryThisInfo.mk.inj : ∀ {edit : Lean.Lsp.TextEdit} {codeActionTitle : String} {suggestion : Lean.Meta.Tactic.TryThis.Suggestion}
  {edit_1 : Lean.Lsp.TextEdit} {codeActionTitle_1 : String} {suggestion_1 : Lean.Meta.Tactic.TryThis.Suggestion},
  { edit := edit, codeActionTitle := codeActionTitle, suggestion := suggestion } =
      { edit := edit_1, codeActionTitle := codeActionTitle_1, suggestion := suggestion_1 } →
    edit = edit_1 ∧ codeActionTitle = codeActionTitle_1 ∧ suggestion = suggestion_1
-- Mathlib.Algebra.Notation.Support
Function.support_subset_iff : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] {f : ι → M} {s : Set ι},
  Function.support f ⊆ s ↔ ∀ (x : ι), f x ≠ 0 → x ∈ s
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement_iff_existsUnique : ∀ {G : Type u_1} [inst : Group G] {S T : Set G}, Subgroup.IsComplement S T ↔ ∀ (g : G), ∃! x, ↑x.1 * ↑x.2 = g
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.isCutsatType : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.Data.List.Sigma
List.kextract_eq_dlookup_kerase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (l : List (Sigma β)),
  List.kextract a l = (List.dlookup a l, List.kerase a l)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.mul.eq_1 : ∀ (p : Int.Internal.Linear.Poly) (k : ℤ), p.mul k = if (k == 0) = true then Int.Internal.Linear.Poly.num 0 else p.mul' k
-- Init.Data.Vector.Erase
Vector.eraseIdx_set_eq : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {a : α} {h : i < n}, (xs.set i a h).eraseIdx i h = xs.eraseIdx i h
-- Mathlib.LinearAlgebra.TensorProduct.Associator
TensorProduct.tensorTensorTensorComm_trans_tensorTensorTensorComm : ∀ (R : Type u_1) [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R Q] [inst_8 : Module R P],
  TensorProduct.tensorTensorTensorComm R M N P Q ≪≫ₗ TensorProduct.tensorTensorTensorComm R M P N Q =
    LinearEquiv.refl R (TensorProduct R (TensorProduct R M N) (TensorProduct R P Q))
-- Mathlib.Algebra.Tropical.BigOperators
/-- Note we cannot use `i ∈ s` instead of `i : s` here
as it is simply not true on conditionally complete lattices!  -/
Finset.untrop_sum : ∀ {R : Type u_1} {S : Type u_2} [inst : ConditionallyCompleteLinearOrder R] (s : Finset S)
  (f : S → Tropical (WithTop R)), Tropical.untrop (∑ i ∈ s, f i) = ⨅ i, Tropical.untrop (f ↑i)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctorCore.map₂_whisker_right : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryPseudofunctorCore B C) {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
  self.map₂ (CategoryTheory.Bicategory.whiskerRight η h) =
    CategoryTheory.CategoryStruct.comp (self.mapComp f h).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.map₂ η) (self.map h))
        (self.mapComp g h).inv)
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Graph.in₁₂_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b : β} {c : γ},
  (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₂ c) ↔ ∃ a, (a, b, c) ∈ t
-- Mathlib.MeasureTheory.Function.SimpleFunc
/-- A simple function is measurable  -/
MeasureTheory.SimpleFunc.measurable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  (f : MeasureTheory.SimpleFunc α β), Measurable ⇑f
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- All the moments of a real Gaussian distribution are finite. That is, the identity is in Lp for
all finite `p`.  -/
ProbabilityTheory.memLp_id_gaussianReal' : ∀ {μ : ℝ} {v : NNReal} (p : ENNReal), p ≠ ⊤ → MeasureTheory.MemLp id p (ProbabilityTheory.gaussianReal μ v)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.map_comap_eq : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R →+* S) (t : Subsemiring S),
  Subsemiring.map f (Subsemiring.comap f t) = t ⊓ f.rangeS
-- Mathlib.Algebra.Homology.Homotopy
/-- A constructor for a `Homotopy e 0`, for `e` a chain map between `ℕ`-indexed cochain complexes,
working by induction.

You need to provide the components of the homotopy in degrees 0 and 1,
show that these satisfy the homotopy condition,
and then give a construction of each component,
and the fact that it satisfies the homotopy condition,
using as an inductive hypothesis the data and homotopy condition for the previous two components.
 -/
Homotopy.mkCoinductive : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Preadditive V] →
      {P Q : CochainComplex V ℕ} →
        (e : P ⟶ Q) →
          (zero : P.X 1 ⟶ Q.X 0) →
            e.f 0 = CategoryTheory.CategoryStruct.comp (P.d 0 1) zero →
              (one : P.X 2 ⟶ Q.X 1) →
                e.f 1 =
                    CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) +
                      CategoryTheory.CategoryStruct.comp (P.d 1 2) one →
                  ((n : ℕ) →
                      (p :
                          (f : P.X (n + 1) ⟶ Q.X n) ×'
                            (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
                              e.f (n + 1) =
                                CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) +
                                  CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') →
                        (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
                          e.f (n + 2) =
                            CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) +
                              CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'') →
                    Homotopy e 0
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedBilinearMap.smul_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] [inst_5 : SeminormedAddCommGroup G]
  [inst_6 : Module 𝕜 G] {f : E × F → G},
  IsBoundedBilinearMap 𝕜 f → ∀ (c : 𝕜) (x : E) (y : F), f (x, c • y) = c • f (x, y)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.continuous_snd : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β],
  Continuous WithLp.snd
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.brecOn_4.eq : ∀ {motive_1 : Lean.Elab.Term.Do.Code → Sort u}
  {motive_2 : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u}
  {motive_3 : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u}
  {motive_4 : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u}
  {motive_5 : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u}
  {motive_6 : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code → Sort u}
  {motive_7 : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code → Sort u}
  (t : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code))
  (F_1 : (t : Lean.Elab.Term.Do.Code) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_1 t → motive_2 t)
  (F_3 : (t : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_2 t → motive_3 t)
  (F_4 : (t : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) → Lean.Elab.Term.Do.Code.below_4 t → motive_5 t)
  (F_6 : (t : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code.below_5 t → motive_6 t)
  (F_7 : (t : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Lean.Elab.Term.Do.Code.below_6 t → motive_7 t),
  Lean.Elab.Term.Do.Code.brecOn_4 t F_1 F_2 F_3 F_4 F_5 F_6 F_7 =
    F_5 t (Lean.Elab.Term.Do.Code.brecOn_4.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7).2
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.mono_map'_of_injective : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.MonoCoprod C] {I : Type u_2}
  {J : Type u_3} (X : I → C) (ι : J → I),
  Function.Injective ι →
    ∀ [inst_2 : CategoryTheory.Limits.HasCoproduct (X ∘ ι)] [inst_3 : CategoryTheory.Limits.HasCoproduct X]
      [CategoryTheory.Limits.HasCoproduct fun k => X ↑k],
      CategoryTheory.Mono (CategoryTheory.Limits.Sigma.map' ι fun j => CategoryTheory.CategoryStruct.id ((X ∘ ι) j))
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.MeasureSpace.toMeasurableSpace : {α : Type u_6} → [self : MeasureTheory.MeasureSpace α] → MeasurableSpace α
-- Init.Data.SInt.Basic
instPowInt32Nat : Pow Int32 ℕ
-- Mathlib.Data.FunLike.Group
/-- Coercion as an additive monoid homomorphism.  -/
FunLike.coeAddMonoidHom : (F : Type u_1) →
  (α : Type u_2) →
    (β : Type u_3) →
      [inst : FunLike F α β] →
        [inst_1 : AddZero F] → [inst_2 : AddZeroClass β] → [IsZeroApply F α β] → [IsAddApply F α β] → F →+ α → β
-- Mathlib.Data.Finset.Preimage
Finset.image_eq_iff_eq_preimage : ∀ {α : Type u} {β : Type v} [inst : DecidableEq β] {s : Finset α} {t : Finset β} {f : α → β}
  (hf : Function.Bijective f), Finset.image f s = t ↔ s = t.preimage f ⋯
-- Mathlib.Order.Category.BddOrd
BddOrd.dualEquiv_inverse : BddOrd.dualEquiv.inverse = BddOrd.dual
-- Mathlib.Topology.Constructions
continuous_ofDual : ∀ {X : Type u} [inst : TopologicalSpace X], Continuous ⇑OrderDual.ofDual
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.ext_iff : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat}
  {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {φ : S ⟶ F.op.comp R}
  {x y : M.Derivation φ},
  x = y ↔
    @PresheafOfModules.Derivation.d C inst D inst_1 S F R M φ x =
      @PresheafOfModules.Derivation.d C inst D inst_1 S F R M φ y
-- Mathlib.CategoryTheory.RegularCategory.Basic
CategoryTheory.Regular.hasCoequalizer_of_isKernelPair : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.Regular C] {X Y Z : C} {f : X ⟶ Y}
  {g₁ g₂ : Z ⟶ X}, CategoryTheory.IsKernelPair f g₁ g₂ → CategoryTheory.Limits.HasCoequalizer g₁ g₂
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.inv_sub_inv_eq_inv : ∀ {p q r : ℝ}, p.HolderTriple q r → r⁻¹ - q⁻¹ = p⁻¹
-- Lean.DocString.Parser
Lean.Doc.Parser.instInhabitedInlineCtxt.default : Lean.Doc.Parser.InlineCtxt
-- Lean.Meta.Sym.AlphaShareCommon
Lean.Meta.Sym.AlphaShareCommon.State.mk.injEq : ∀ (set set_1 : Lean.PHashSet Lean.Meta.Sym.AlphaKey), ({ set := set } = { set := set_1 }) = (set = set_1)
-- Init.Data.Slice.Array.Lemmas
Array.start_mkSlice_roc : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  (Std.Roc.Sliceable.mkSlice xs lo<...=hi).start = min (lo + 1) (min (hi + 1) xs.size)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.Type₁.mk.injEq : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) (d : ℕ)
  (hd : x.dim = d + 1) (index : Fin (d + 1)) (isIndex : SSet.prodStdSimplex.pairingCore.IsIndex x hd index.succ)
  (x_1 : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) (d_1 : ℕ) (hd_1 : x_1.dim = d_1 + 1)
  (index_1 : Fin (d_1 + 1)) (isIndex_1 : SSet.prodStdSimplex.pairingCore.IsIndex x_1 hd_1 index_1.succ),
  ({ x := x, d := d, hd := hd, index := index, isIndex := isIndex } =
      { x := x_1, d := d_1, hd := hd_1, index := index_1, isIndex := isIndex_1 }) =
    (x = x_1 ∧ d = d_1 ∧ index ≍ index_1)
-- Mathlib.Order.BooleanAlgebra.Set
Set.union_eq_compl_compl_inter_compl : ∀ {α : Type u_1} (s t : Set α), s ∪ t = (sᶜ ∩ tᶜ)ᶜ
-- Mathlib.Algebra.Star.StarAlgHom
/-- By definition, a non-unital ⋆-algebra homomorphism preserves the `star` operation.  -/
NonUnitalStarAlgHom.map_star' : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] (self : A →⋆ₙₐ[R] B) (a : A),
  self.toFun (star a) = star (self.toFun a)
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_empty : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α}, s \ ∅ = s
-- Mathlib.GroupTheory.GroupAction.Basic
MulEquiv.subgroupCongr.congr_simp : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} (h : H = K), MulEquiv.subgroupCongr h = MulEquiv.subgroupCongr h
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.hasCokernel_comp_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y Z : C}
  (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Limits.HasCokernel f] [CategoryTheory.IsIso g],
  CategoryTheory.Limits.HasCokernel (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_mul : ∀ {R : Type u} [inst : Semiring R] (a b : Polynomial R), (a * b).toFinsupp = a.toFinsupp * b.toFinsupp
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.entryAtIdxD.eq_2 : ∀ {α : Type u} {β : α → Type v} (x : ℕ) (x_1 : (a : α) × β a) (size : ℕ) (k : α) (v : β k)
  (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v l r).entryAtIdxD x x_1 =
    match compare x l.size with
    | Ordering.lt => l.entryAtIdxD x x_1
    | Ordering.eq => ⟨k, v⟩
    | Ordering.gt => r.entryAtIdxD (x - l.size - 1) x_1
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.variableChange_b₈ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (C : WeierstrassCurve.VariableChange R),
  (C • W).b₈ = ↑C.u⁻¹ ^ 8 * (W.b₈ + 3 * C.r * W.b₆ + 3 * C.r ^ 2 * W.b₄ + C.r ^ 3 * W.b₂ + 3 * C.r ^ 4)