mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.CondDistrib
MeasureTheory.Integrable.condDistrib_ae : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F},
  AEMeasurable X μ →
    AEMeasurable Y μ →
      MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ) →
        ∀ᵐ (a : α) ∂μ, MeasureTheory.Integrable (fun ω => f (X a, ω)) ((ProbabilityTheory.condDistrib Y X μ) (X a))
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.dualEquiv_inverse : FinPartOrd.dualEquiv.inverse = FinPartOrd.dual
-- Lean.CoreM
/-- Includes a given task (such as from `wrapAsyncAsSnapshot`) in the overall snapshot tree for this
command's elaboration, making its result available to reporting and the language server. The
reporter will not know about this snapshot tree node until the main elaboration thread for this
command has finished so this function is not useful for incremental reporting within a longer
elaboration thread but only for tasks that outlive it such as background kernel checking or proof
elaboration.
 -/
Lean.Core.logSnapshotTask : Lean.Language.SnapshotTask Lean.Language.SnapshotTree → Lean.CoreM Unit
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toContinuousAddMonoidHom_add : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] [inst_8 : ContinuousAdd M₂]
  (f g : M₁ →SL[σ₁₂] M₂), ↑(f + g) = ↑f + ↑g
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift_fac_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Z)
  [hf : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] (g : Y ⟶ Z)
  (H :
    Set.range ⇑(CategoryTheory.ConcreteCategory.hom g.base) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base))
  {Z_1 : AlgebraicGeometry.PresheafedSpace C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.lift f g H)
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp g h
-- Lean.Data.Lsp.Diagnostics
/-- Unused or unnecessary code. Rendered as faded out eg for unused variables.  -/
Lean.Lsp.DiagnosticTag.unnecessary : Lean.Lsp.DiagnosticTag
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.Context : Type
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
HasMFDerivAt.mfderiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M}
  {f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)}, HasMFDerivAt% f x f' → mfderiv% f x = f'
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- `Matrix.invertibleOfFromBlocks₁₁Invertible` and `Matrix.fromBlocks₁₁Invertible` as an
equivalence.  -/
Matrix.invertibleEquivFromBlocks₁₁Invertible : {m : Type u_2} →
  {n : Type u_3} →
    {α : Type u_4} →
      [inst : Fintype m] →
        [inst_1 : Fintype n] →
          [inst_2 : DecidableEq m] →
            [inst_3 : DecidableEq n] →
              [inst_4 : CommRing α] →
                (A : Matrix m m α) →
                  (B : Matrix m n α) →
                    (C : Matrix n m α) →
                      (D : Matrix n n α) →
                        [inst_5 : Invertible A] → Invertible (Matrix.fromBlocks A B C D) ≃ Invertible (D - C * ⅟A * B)
-- Mathlib.GroupTheory.PGroup
isPGroup_iff_exponent_dvd_pow : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Finite G], IsPGroup p G ↔ ∃ n, Monoid.exponent G ∣ p ^ n
-- Mathlib.CategoryTheory.Sites.Coverage
/-- Given `S T : Presieve X`, we say that `S` factors through `T` if any morphism in `S`
factors through some morphism in `T`.

The lemma `Presieve.isSheafFor_of_factorsThru` gives a *sufficient* condition for a
presheaf to be a sheaf for a presieve `T`, in terms of `S.FactorsThru T`, provided
that the presheaf is a sheaf for `S`.
 -/
CategoryTheory.Presieve.FactorsThru : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → {X : C} → CategoryTheory.Presieve X → CategoryTheory.Presieve X → Prop
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.liftCycles_ιChainComplex_homologyπ_homology₀Iso_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) [inst_3 : CategoryTheory.CategoryWithHomology C]
  (x : X.obj (Opposite.op { len := 0 })) {Z : C} (h : (∐ fun x => R) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (HomologicalComplex.liftCycles (X.chainComplex R) (X.ιChainComplex x) 0
        SSet.liftCycles_ιChainComplex_homologyπ_homology₀Iso_hom._proof_1 ⋯)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ (X.chainComplex R) 0)
        (CategoryTheory.CategoryStruct.comp (X.homology₀Iso R).hom h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun x => R) (SSet.π₀.mk x)) h
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.noRepetition_singleton : ∀ {α : Type u} {a b : α}, NoRepetition✝ a [b]
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k : α}
  (contains_eq_false : (List.map Prod.fst l).contains k = false) {h' : k ∈ Std.DTreeMap.Raw.Const.insertMany t l},
  Std.DTreeMap.Raw.Const.get (Std.DTreeMap.Raw.Const.insertMany t l) k h' = Std.DTreeMap.Raw.Const.get t k ⋯
-- Mathlib.Algebra.Lie.Normalizer
/-- A Lie subalgebra `H` is an ideal of any Lie subalgebra `K` containing `H` and contained in the
normalizer of `H`.  -/
LieSubalgebra.exists_nested_lieIdeal_ofLe_normalizer : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {H K : LieSubalgebra R L} (h₁ : H ≤ K),
  K ≤ H.normalizer → ∃ I, LieIdeal.toLieSubalgebra R (↥K) I = LieSubalgebra.ofLe h₁
-- Init.Data.Array.OfFn
Array.ofFn_eq_empty_iff : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → α}, Array.ofFn f = #[] ↔ n = 0
-- Lean.MetavarContext
/-- The nesting depth of this metavariable. We do not want
unification subproblems to influence the results of parent
problems. The depth keeps track of this information and ensures
that unification subproblems cannot leak information out, by unifying
based on depth.
 -/
Lean.MetavarDecl.depth : Lean.MetavarDecl → ℕ
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
le_csSup : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α} {a : α}, BddAbove s → a ∈ s → a ≤ sSup s
-- Mathlib.Order.Disjoint
Codisjoint.left_le_of_le_inf_right : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderTop α] {a b c : α}, a ⊓ b ≤ c → Codisjoint b c → a ≤ c
-- Mathlib.RingTheory.HopfAlgebra.Quotient
HopfAlgebra.Quotient.antipode_comp_mkₐ : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : HopfAlgebraStruct R A] (I : Ideal A)
  [inst_3 : I.IsTwoSided] [inst_4 : Ideal.IsHopfIdeal R I],
  HopfAlgebraStruct.antipode R ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap =
    (Ideal.Quotient.mkₐ R I).toLinearMap ∘ₗ HopfAlgebraStruct.antipode R
-- Mathlib.Algebra.Star.MonoidHom
/-- A *star monoid equivalence* is an equivalence preserving multiplication and the star
operation.  -/
«term_≃⋆*_» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup
/-- The inclusion from a commutative monoid `M` to its Grothendieck group.

Note that this is only injective if `M` is cancellative.  -/
Algebra.GrothendieckGroup.of : {M : Type u_1} → [inst : CommMonoid M] → M →* Algebra.GrothendieckGroup M
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.mk.sizeOf_spec : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : SizeOf ι] [inst_6 : SizeOf R]
  [inst_7 : SizeOf M] [inst_8 : SizeOf N] (toLinearMap : M →ₗ[R] N →ₗ[R] R)
  [isPerfPair_toLinearMap : toLinearMap.IsPerfPair] (root : ι ↪ M) (coroot : ι ↪ N)
  (root_coroot_two : ∀ (i : ι), (toLinearMap (root i)) (coroot i) = 2) (reflectionPerm : ι → ι ≃ ι)
  (reflectionPerm_root : ∀ (i j : ι), root j - (toLinearMap (root j)) (coroot i) • root i = root ((reflectionPerm i) j))
  (reflectionPerm_coroot :
    ∀ (i j : ι), coroot j - (toLinearMap (root i)) (coroot j) • coroot i = coroot ((reflectionPerm i) j)),
  sizeOf
      { toLinearMap := toLinearMap, isPerfPair_toLinearMap := isPerfPair_toLinearMap, root := root, coroot := coroot,
        root_coroot_two := root_coroot_two, reflectionPerm := reflectionPerm,
        reflectionPerm_root := reflectionPerm_root, reflectionPerm_coroot := reflectionPerm_coroot } =
    1 + sizeOf toLinearMap + sizeOf isPerfPair_toLinearMap + sizeOf root + sizeOf coroot
-- Lean.Elab.Coinductive
/-- Main entry point for elaborating mutual coinductive predicates. This function is called after
generating a flat inductive and adding it to the environment.

We look at corresponding existential form of the flat inductive (see `Meta.MkIffOfInductiveProp`),
use it to populate `PreDefinition`s that correspond to the predicates, and then we call
the `PartialFixpoint` machinery to register them as (co)inductive predicates.

Finally, we generate constructors for each of the predicates, that correspond to the constructors
that were given by the user.
 -/
Lean.Elab.Command.elabCoinductive : Array Lean.Elab.Command.CoinductiveElabData → Lean.Elab.TermElabM Unit
-- Init.PropLemmas
exists_or : ∀ {α : Sort u_1} {p q : α → Prop}, (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ ∃ x, q x
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_eq_iSup_nat' : ∀ {f : ℕ → ENNReal} {N : ℕ → ℕ},
  Filter.Tendsto N Filter.atTop Filter.atTop → ∑' (i : ℕ), f i = ⨆ i, ∑ a ∈ Finset.range (N i), f a
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.instCoeTCQuotient.eq_1 : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M), c.instCoeTCQuotient = { coe := AddCon.toQuotient }
-- Lean.Parser.Do
Lean.Parser.Term.doMatchAlts.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.dec.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (n : ℕ) (check persistent : Bool) (objs? : Option ℕ)
  (k : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_17),
  sizeOf (Lean.Compiler.LCNF.Code.dec fvarId n check persistent objs? k h) =
    1 + sizeOf fvarId + sizeOf n + sizeOf check + sizeOf persistent + sizeOf objs? + sizeOf k + sizeOf h
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
/-- An n-ary version of `Set.add_mem_add`.  -/
Set.list_sum_mem_list_sum : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] (t : List ι) (f : ι → Set α) (g : ι → α),
  (∀ i ∈ t, g i ∈ f i) → (List.map g t).sum ∈ (List.map f t).sum
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {Wₗ Wᵣ : CategoryTheory.MorphismProperty C}
  {c c' apex : C} {l : apex ⟶ c} {r : apex ⟶ c'} {wl : Wₗ l} {wr : Wᵣ r} {apex_1 : C} {l_1 : apex_1 ⟶ c}
  {r_1 : apex_1 ⟶ c'} {wl_1 : Wₗ l_1} {wr_1 : Wᵣ r_1},
  { apex := apex, l := l, r := r, wl := wl, wr := wr } =
      { apex := apex_1, l := l_1, r := r_1, wl := wl_1, wr := wr_1 } →
    apex = apex_1 ∧ l ≍ l_1 ∧ r ≍ r_1
-- Init.Data.Rat.Lemmas
Rat.abs_of_nonpos : ∀ {x : ℚ}, x ≤ 0 → x.abs = -x
-- Mathlib.Topology.Algebra.GroupWithZero
/-- **Alias** of the forward direction of `tendsto_div_nhds_one_iff_eq₀`.

---

If `f → a` and `g → b` along a nontrivial filter, valued in a Hausdorff
`GroupWithZero` with continuous multiplication and `ContinuousInv₀`, and `b ≠ 0`,
then `f / g → 1` if and only if `a = b`.  -/
eq_of_tendsto_div_nhds_one₀ : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  [ContinuousMul G₀] {f g : α → G₀} {l : Filter α} [l.NeBot] [T2Space G₀] {a b : G₀},
  Filter.Tendsto f l (nhds a) →
    Filter.Tendsto g l (nhds b) → b ≠ 0 → Filter.Tendsto (fun x => f x / g x) l (nhds 1) → a = b
-- Mathlib.Algebra.Order.GroupWithZero.Basic
lt_div_comm₀ : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < a → 0 < c → (a < b / c ↔ c < b / a)
-- Mathlib.Analysis.Complex.Norm
Complex.cauSeqRe.eq_1 : ∀ (f : CauSeq ℂ fun x => ‖x‖), Complex.cauSeqRe f = ⟨fun n => (↑f n).re, ⋯⟩
-- Init.Data.Float.Model.Float
Float.Model.instNeg : Neg Float.Model
-- Lean.Expr
Lean.Expr.proj.inj : ∀ {typeName : Lean.Name} {idx : ℕ} {struct : Lean.Expr} {typeName_1 : Lean.Name} {idx_1 : ℕ} {struct_1 : Lean.Expr},
  Lean.Expr.proj typeName idx struct = Lean.Expr.proj typeName_1 idx_1 struct_1 →
    typeName = typeName_1 ∧ idx = idx_1 ∧ struct = struct_1
-- Mathlib.Data.ENNReal.Inv
ENNReal.exists_nat_mul_gt : ∀ {a b : ENNReal}, a ≠ 0 → b ≠ ⊤ → ∃ n, b < ↑n * a
-- Mathlib.Order.Closure
ClosureOperator.instFunLike : (α : Type u_1) → [inst : Preorder α] → FunLike (ClosureOperator α) α α
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.forget₂_map_pushforward_obj_val_map : ∀ {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}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) {U V : Cᵒᵖ} (f : U ⟶ V)
  (M : SheafOfModules R),
  (CategoryTheory.forget₂ (ModuleCat ↑(S.obj.obj U)) Ab).map (((SheafOfModules.pushforward φ).obj M).val.map f) =
    M.val.presheaf.map (F.map f.unop).op
-- Mathlib.Combinatorics.Graph.Basic
/-- Every graph on just one vertex is a bouquet on that vertex.  -/
Graph.eq_bouquet_of_subsingleton : ∀ {α : Type u_1} {β : Type u_2} {v : α} {G : Graph α β},
  v ∈ G.vertexSet → G.vertexSet.Subsingleton → G = Graph.bouquet v G.edgeSet
-- Mathlib.RingTheory.Ideal.Operations
Ideal.span_singleton_mul_right_injective : ∀ {R : Type u} [inst : CommSemiring R] [IsDomain R] {x : R}, x ≠ 0 → Function.Injective fun x_1 => Ideal.span {x} * x_1
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.smul_snd : ∀ {p : ENNReal} {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : AddCommGroup α]
  [inst_2 : AddCommGroup β] (x : WithLp p (α × β)) (c : 𝕜) [inst_3 : Module 𝕜 α] [inst_4 : Module 𝕜 β],
  (c • x).snd = c • x.snd
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.isValidEq.eq_1 : ∀ (k : ℤ), (Int.Internal.Linear.Poly.num k).isValidEq = (k == 0)
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.Subtype.instUnion : {α : Type u_1} → [inst : MeasurableSpace α] → Union (Subtype MeasurableSet)
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.image_eq_isOpen_inter_range : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace X],
  Topology.IsInducing f → ∀ {s : Set X}, IsOpen s → ∃ c, IsOpen c ∧ f '' s = c ∩ Set.range f
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.dec.sizeOf_spec : ∀ (x : Lean.IR.VarId) (n : ℕ) (c persistent : Bool) (b : Lean.IR.FnBody),
  sizeOf (Lean.IR.FnBody.dec x n c persistent b) = 1 + sizeOf x + sizeOf n + sizeOf c + sizeOf persistent + sizeOf b
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.leftInvSeq_concat : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (ω : List B) (i : B),
  cs.leftInvSeq (ω.concat i) = (cs.leftInvSeq ω).concat (cs.wordProd ω * cs.simple i * (cs.wordProd ω)⁻¹)
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mergeAll?.match_1.eq_2 : ∀ (motive : Option (Lean.TSyntax `tactic) → Sort u_1) (x : Option (Lean.TSyntax `tactic))
  (h_1 : (tac' : Lean.TSyntax `tactic) → motive (some tac')) (h_2 : (x : Option (Lean.TSyntax `tactic)) → motive x),
  (∀ (tac' : Lean.TSyntax `tactic), x = some tac' → False) →
    (match x with
      | some tac' => h_1 tac'
      | x => h_2 x) =
      h_2 x
-- Mathlib.Algebra.Group.Finsupp
/-- A finitely supported function can be built by adding up `single a b` for increasing `a`.

The lemma `induction_on_max` swaps the argument order in the sum.  -/
Finsupp.induction_on_max₂ : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] [inst_1 : LinearOrder ι] {motive : (ι →₀ M) → Prop}
  (f : ι →₀ M),
  motive 0 →
    (∀ (a : ι) (b : M) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → motive f → motive (f + fun₀ | a => b)) →
      motive f
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
/-- `ConjRootClass K L` is the quotient of `L` by the relation `IsConjRoot K`.  -/
ConjRootClass : (K : Type u_1) → (L : Type u_2) → [inst : Field K] → [inst_1 : Field L] → [Algebra K L] → Type u_2
-- Mathlib.LinearAlgebra.DirectSum.Finite
Module.Finite.instDirectSum : ∀ {R : Type u_1} {ι : Type u_2} [inst : Semiring R] [Finite ι] (M : ι → Type u_3)
  [inst_2 : (i : ι) → AddCommMonoid (M i)] [inst_3 : (i : ι) → Module R (M i)] [∀ (i : ι), Module.Finite R (M i)],
  Module.Finite R (DirectSum ι fun i => M i)
-- Mathlib.NumberTheory.Harmonic.GammaDeriv
Complex.hasDerivAt_Gammaℝ_one : HasDerivAt Complex.Gammaℝ (-(↑Real.eulerMascheroniConstant + Complex.log (4 * ↑Real.pi)) / 2) 1
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
_private.Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks.0.CategoryTheory.Limits.cospanOp.match_1.eq_1 : ∀ (motive : CategoryTheory.Limits.WalkingCospan → Sort u_1) (h_1 : Unit → motive none)
  (h_2 : Unit → motive (some CategoryTheory.Limits.WalkingPair.left))
  (h_3 : Unit → motive (some CategoryTheory.Limits.WalkingPair.right)),
  (match none with
    | none => h_1 ()
    | some CategoryTheory.Limits.WalkingPair.left => h_2 ()
    | some CategoryTheory.Limits.WalkingPair.right => h_3 ()) =
    h_1 ()
-- Mathlib.Topology.Algebra.Group.Basic
neg_mem_nhds_zero : ∀ (G : Type w) [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {S : Set G},
  S ∈ nhds 0 → -S ∈ nhds 0
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.toAdditiveBialgEquiv.eq_1 : ∀ (R : Type u_1) (A : Type u_3) (M : Type u_8) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  [inst_3 : Monoid M],
  MonoidAlgebra.toAdditiveBialgEquiv R A M = BialgEquiv.ofAlgEquiv (MonoidAlgebra.toAdditiveAlgEquiv R A M) ⋯ ⋯
-- Mathlib.Probability.Martingale.Upcrossing
_private.Mathlib.Probability.Martingale.Upcrossing.0.MeasureTheory.upperCrossingTime.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.injOn_ofDigits : ∀ {b : ℕ}, 1 < b → ∀ (l : ℕ), Set.InjOn (Nat.ofDigits b) {L | L.length = l ∧ ∀ x ∈ L, x < b}
-- Mathlib.Order.Category.LinOrd
LinOrd.ofHom_apply : ∀ {X Y : Type u} [inst : LinearOrder X] [inst_1 : LinearOrder Y] (f : X →o Y) (x : X),
  (CategoryTheory.ConcreteCategory.hom (LinOrd.ofHom f)) x = f x
-- Mathlib.Order.Filter.IsBounded
Filter.IsBoundedUnder.inf : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeInf α] {f : Filter β} {u v : β → α},
  Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f u →
    Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f v → Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f fun a => u a ⊓ v a
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.inclusion_apply : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] {S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂)
  (a : ↥S₁), (StarSubalgebra.inclusion h) a = Subtype.map id h a
-- Mathlib.Order.Interval.Set.Basic
/-- If `a < b`, then `(b, +∞) ⊂ (a, +∞)`. In preorders, this is just an implication. If you need
the equivalence in linear orders, use `Ioi_ssubset_Ioi_iff`.  -/
Set.Ioi_ssubset_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a → Set.Ioi a ⊂ Set.Ioi b
-- Mathlib.MeasureTheory.Measure.Map
MeasureTheory.Measure.map_zero : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β),
  MeasureTheory.Measure.map f 0 = 0
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.intCast_dvd_intCast : ∀ {d : ℤ} (a b : ℤ), ↑a ∣ ↑b ↔ a ∣ b
-- Mathlib.Computability.Ackermann
one_lt_ack_succ_left : ∀ (m n : ℕ), 1 < ack (m + 1) n
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- Kan lifts on `g` along `f` are unique up to isomorphism.  -/
CategoryTheory.Bicategory.RightLift.IsKan.uniqueUpToIso : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} → {g : c ⟶ a} → {s t : CategoryTheory.Bicategory.RightLift f g} → s.IsKan → t.IsKan → (s ≅ t)
-- Mathlib.Topology.Covering.Quotient
IsAddQuotientCoveringMap.isCancelVAdd : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : AddGroup G] [inst_3 : AddAction G E], IsAddQuotientCoveringMap f G → IsCancelVAdd G E
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.le_maxKeyD_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t → ∀ {fallback : α}, (cmp k (t.maxKeyD fallback)).isLE = true
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Limits.pullbackConeEquivBinaryFan_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : Y ⟶ X} {g : Z ⟶ X},
  CategoryTheory.Limits.pullbackConeEquivBinaryFan.counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun X_1 =>
        CategoryTheory.Limits.BinaryFan.ext
          (CategoryTheory.Over.isoMk
            (CategoryTheory.Iso.refl
              (({
                            obj := fun c =>
                              CategoryTheory.Limits.PullbackCone.mk (CategoryTheory.Over.Hom.left c.fst)
                                (CategoryTheory.Over.Hom.left c.snd) ⋯,
                            map := fun {c₁ c₂} a => { hom := CategoryTheory.Over.Hom.left a.hom, w := ⋯ }, map_id := ⋯,
                            map_comp := ⋯ }.comp
                        {
                          obj := fun c =>
                            CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.Over.homMk c.fst ⋯)
                              (CategoryTheory.Over.homMk c.snd ⋯),
                          map := fun {c₁ c₂} a => { hom := CategoryTheory.Over.homMk a.hom ⋯, w := ⋯ }, map_id := ⋯,
                          map_comp := ⋯ }).obj
                    X_1).pt.left)
            ⋯)
          ⋯ ⋯)
      ⋯
-- Mathlib.Order.SuccPred.Limit
/-- Recursion principle on a well-founded partial `PredOrder`.  -/
PredOrder.prelimitRecOn : {α : Type u_1} →
  (b : α) →
    {motive : α → Sort u_2} →
      [inst : PartialOrder α] →
        [inst_1 : PredOrder α] →
          [WellFoundedGT α] →
            ((a : α) → ¬IsMin a → motive a → motive (Order.pred a)) →
              ((a : α) → Order.IsPredPrelimit a → ((b : α) → a < b → motive b) → motive a) → motive b