mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.step_filterM.match_1.eq_1 : ∀ {β : Type u_1} {n : Type u_1 → Type u_2} {f : β → n (ULift.{u_1, 0} Bool)} [inst : MonadAttach n] (out : β)
  (motive : Subtype (MonadAttach.CanReturn (f out)) → Sort u_3) (hf : MonadAttach.CanReturn (f out) { down := false })
  (h_1 : (hf : MonadAttach.CanReturn (f out) { down := false }) → motive ⟨{ down := false }, hf⟩)
  (h_2 : (hf : MonadAttach.CanReturn (f out) { down := true }) → motive ⟨{ down := true }, hf⟩),
  (match ⟨{ down := false }, hf⟩ with
    | ⟨{ down := false }, hf⟩ => h_1 hf
    | ⟨{ down := true }, hf⟩ => h_2 hf) =
    h_1 hf
-- Init.GetElem
getElem_of_getElem? : ∀ {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} {e : elem}
  [inst : GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] {c : cont} {i : idx} [Decidable (dom c i)],
  c[i]? = some e → ∃ (h : dom c i), c[i] = e
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_eq_zero' : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] {s : Set α} {f : α → M},
  s.indicator f = 0 ↔ Disjoint (Function.support f) s
-- Lean.Meta.Tactic.Simp.Types
/-- Stores the "parent" term for the term being simplified.
If a simplification procedure result depends on this value,
then it is its responsibility to set `Result.cache := false`.

Motivation for this field:
Suppose we have a simplification procedure for normalizing arithmetic terms.
Then, given a term such as `t_1 + ... + t_n`, we don't want to apply the procedure
to every subterm `t_1 + ... + t_i` for `i < n` for performance issues. The procedure
can accomplish this by checking whether the parent term is also an arithmetical expression
and do nothing if it is. However, it should set `Result.cache := false` to ensure
we don't miss simplification opportunities. For example, consider the following:
```
example (x y : Nat) (h : y = 0) : id ((x + x) + y) = id (x + x) := by
  simp +arith only
  ...
```
If we don't set `Result.cache := false` for the first `x + x`, then we get
the resulting state:
```
... |- id (2*x + y) = id (x + x)
```
instead of
```
... |- id (2*x + y) = id (2*x)
```
as expected.

Remark: given an application `f a b c` the "parent" term for `f`, `a`, `b`, and `c`
is `f a b c`.
 -/
Lean.Meta.Simp.Context.parent? : Lean.Meta.Simp.Context → Option Lean.Expr
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.IsRegular.wf : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) [self : h.IsRegular], WellFounded h.AncestralRel
-- Mathlib.Algebra.Group.Submonoid.Basic
Submonoid.sup_eq_closure : ∀ {M : Type u_1} [inst : MulOneClass M] (N N' : Submonoid M), N ⊔ N' = Submonoid.closure (↑N ∪ ↑N')
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
/-- If `X` is a simplicial set, `£₀ X` is a coequalizer
of `X.δ 0 : X _⦋1⦌ → X _⦋0⦌` and `X.δ 1`.  -/
SSet.isColimitCoforkπ₀ : {X : SSet} → CategoryTheory.Limits.IsColimit SSet.coforkπ₀
-- Init.MetaTypes
/-- Configuration for the `lift_lets` tactic.
 -/
Lean.Meta.LiftLetsConfig : Type
-- Aesop.RulePattern
Aesop.RulePattern.boundPremises : Aesop.RulePattern → Array ℕ
-- Mathlib.GroupTheory.GroupAction.Hom
map_vadd : ∀ {F : Type u_8} {M : Type u_9} {X : Type u_10} {Y : Type u_11} [inst : VAdd M X] [inst_1 : VAdd M Y]
  [inst_2 : FunLike F X Y] [AddActionHomClass F M X Y] (f : F) (c : M) (x : X), f (c +ᵥ x) = c +ᵥ f x
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.weierstrassMod.eq_1 : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (f g : PowerSeries A)
  [inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A],
  f %ʷ g =
    if hg : (PowerSeries.map (IsLocalRing.residue A)) g ≠ 0 then PowerSeries.IsWeierstrassDivisorAt.mod ⋯ f else 0
-- Mathlib.RingTheory.MvPowerSeries.PiTopology
/-- The `IsUniformAddGroup` structure on `MvPowerSeries` of a `IsUniformAddGroup`  -/
MvPowerSeries.WithPiTopology.instIsUniformAddGroup : ∀ {σ : Type u_1} {R : Type u_2} [inst : UniformSpace R] [inst_1 : AddGroup R] [IsUniformAddGroup R],
  IsUniformAddGroup (MvPowerSeries σ R)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.coe_sub : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N : LieSubmodule R L M) (m m' : ↥N), ↑(m - m') = ↑m - ↑m'
-- Mathlib.Order.Cover
Bool.covBy_iff : ∀ {a b : Bool}, a ⋖ b ↔ a < b
-- Std.Time.Duration
/-- Creates a new `Duration` out of `Second.Offset`.
 -/
Std.Time.Duration.ofSeconds : Std.Time.Second.Offset → Std.Time.Duration
-- Mathlib.Topology.Inseparable
SeparationQuotient.tendsto_lift_nhds_mk : ∀ {X : Type u_1} {α : Type u_4} [inst : TopologicalSpace X] {x : X} {f : X → α}
  {hf : ∀ (x y : X), Inseparable x y → f x = f y} {l : Filter α},
  Filter.Tendsto (SeparationQuotient.lift f hf) (nhds (SeparationQuotient.mk x)) l ↔ Filter.Tendsto f (nhds x) l
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic valuation of `r : R` is less than 1 if and only if `v` divides the ideal `(r)`.  -/
IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R),
  (IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑r < 1 ↔ v.asIdeal ∣ Ideal.span {r}
-- Mathlib.RepresentationTheory.Homological.Resolution
/-- The differential from `Gⁿ⁺¹ →₀ k[G]` to `Gⁿ →₀ k[G]` in the bar resolution of `k` as a trivial
`k`-linear `G`-representation. It sends `(g₀, ..., gₙ)` to
`g₀·(g₁, ..., gₙ) + ∑ (-1)ʲ⁺¹·(g₀, ..., gⱼgⱼ₊₁, ..., gₙ) + (-1)ⁿ⁺¹·(g₀, ..., gₙ₋₁)` for
`j = 0, ..., n - 1`.  -/
Rep.barComplex.d : (k G : Type u) →
  [inst : CommRing k] → (n : ℕ) → [inst_1 : Group G] → Rep.free k G (Fin (n + 1) → G) ⟶ Rep.free k G (Fin n → G)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.all_eq_not_any_not : ∀ {m : Type u_1 → Type u_2} {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {p : β → Bool},
  Std.Iter.all p it = !Std.Iter.any (fun x => !p x) it
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.instRing : (M : Type u_2) →
  [inst : AddCommMonoid M] → {S : Type u_3} → [inst_1 : CommRing S] → [inst_2 : Module S M] → Ring (TensorAlgebra S M)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {he : t ≠ ∅}
  {km : α}, t.minKey he = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
cbiInf_id : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α}, BddBelow s → sInf s ≤ sInf ∅ → ⨅ i ∈ s, i = sInf s
-- Mathlib.Topology.Algebra.Monoid
/-- Construct a bundled additive semigroup homomorphism from a pointwise limit of additive
semigroup homomorphisms  -/
addHomOfTendsto : {α : Type u_2} →
  {M₁ : Type u_6} →
    {M₂ : Type u_7} →
      [inst : TopologicalSpace M₂] →
        [T2Space M₂] →
          [inst_2 : Add M₁] →
            [inst_3 : Add M₂] →
              [ContinuousAdd M₂] →
                {F : Type u_8} →
                  [inst_5 : FunLike F M₁ M₂] →
                    [AddHomClass F M₁ M₂] →
                      {l : Filter α} →
                        (f : M₁ → M₂) →
                          (g : α → F) → [l.NeBot] → Filter.Tendsto (fun a x => (g a) x) l (nhds f) → M₁ →ₙ+ M₂
-- Mathlib.Analysis.Normed.Algebra.Unitization
/-- Pull back the normed algebra structure from `𝕜 × (A →L[𝕜] A)` to `Unitization 𝕜 A` using the
algebra homomorphism `Unitization.splitMul 𝕜 A`.  -/
Unitization.instNormedAlgebra : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : IsScalarTower 𝕜 A A] →
            [inst_4 : SMulCommClass 𝕜 A A] → [inst_5 : RegularNormedAlgebra 𝕜 A] → NormedAlgebra 𝕜 (Unitization 𝕜 A)
-- Mathlib.SetTheory.Ordinal.Notation
/-- Notation for 1  -/
ONote.instOne : One ONote
-- Mathlib.Order.Interval.Set.Monotone
strictAntiOn_Iic_of_succ_lt : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : Preorder β] {ψ : α → β} [inst_2 : SuccOrder α]
  [IsSuccArchimedean α] {n : α}, (∀ m < n, ψ (Order.succ m) < ψ m) → StrictAntiOn ψ (Set.Iic n)
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.saturation_induction : ∀ {M : Type u_1} [inst : MulOneClass M] {s : Submonoid M} {p : (x : M) → x ∈ s.saturation → Prop},
  (∀ (x : M) (hx : x ∈ s), p x ⋯) →
    (∀ (x y : M) (hx : x ∈ s.saturation) (hy : y ∈ s.saturation), p x hx → p y hy → p (x * y) ⋯) →
      (∀ (x y : M) (hxy : x * y ∈ s.saturation), p (x * y) hxy → p x ⋯ ∧ p y ⋯) →
        ∀ {x : M} (hx : x ∈ s.saturation), p x hx
-- Mathlib.Analysis.Calculus.FDeriv.Const
fderivWithin_fun_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {s : Set E} (c : F), fderivWithin 𝕜 (fun x => c) s = 0
-- Mathlib.Algebra.Module.LinearMap.Polynomial
Matrix.toMvPolynomial_mul : ∀ {m : Type u_1} {n : Type u_2} {o : Type u_3} {R : Type u_4} [inst : Fintype n] [inst_1 : Fintype o]
  [inst_2 : CommSemiring R] (M : Matrix m n R) (N : Matrix n o R) (i : m),
  (M * N).toMvPolynomial i = (MvPolynomial.bind₁ N.toMvPolynomial) (M.toMvPolynomial i)
-- Mathlib.Tactic.TacticAnalysis
/-- Read a configuration from a declaration of the right type.  -/
Mathlib.TacticAnalysis.Entry.import : Mathlib.TacticAnalysis.Entry → Lean.ImportM Mathlib.TacticAnalysis.Pass
-- Init.Tactics
/-- `first | tac | ...` runs each `tac` until one succeeds, or else fails.  -/
Lean.Parser.Tactic.first : Lean.ParserDescr
-- Lean.Data.NameTrie
Lean.NamePart.str.injEq : ∀ (s s_1 : String), (Lean.NamePart.str s = Lean.NamePart.str s_1) = (s = s_1)
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.Expanded.const.inj : ∀ {c c_1 : Lean.Term},
  Mathlib.Tactic.LinearCombinationPrime.Expanded.const c = Mathlib.Tactic.LinearCombinationPrime.Expanded.const c_1 →
    c = c_1
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Finset.inf'_id_eq_csInf : ∀ {α : Type u_2} [inst : ConditionallyCompleteLattice α] (s : Finset α) (hs : s.Nonempty), s.inf' hs id = sInf ↑s
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} {M N : Bimod A B} {f g : M ⟶ N}, f = g ↔ f.hom = g.hom
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.coe_singleton : ∀ {ι : Type u_7} {𝕜 : Type u_8} [inst : Unique ι] [inst_1 : RCLike 𝕜], ⇑(OrthonormalBasis.singleton ι 𝕜) = 1
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.functoriality_full : ∀ {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)
  (G : CategoryTheory.Functor C D) [G.Full] [G.Faithful], (CategoryTheory.Limits.Cocone.functoriality F G).Full
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
/-- A function is interval integrable with respect to a given measure `μ` on `a..b` if and
only if it is integrable on `uIoc a b` with respect to `μ`. This is an equivalent
definition of `IntervalIntegrable`.  -/
intervalIntegrable_iff : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] [TopologicalSpace.PseudoMetrizableSpace ε]
  {f : ℝ → ε} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
  IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.uIoc a b) μ
-- Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Mathlib.Tactic.Monoidal.instMkEqOfNaturalityMonoidalM : Mathlib.Tactic.BicategoryLike.MkEqOfNaturality Mathlib.Tactic.Monoidal.MonoidalM
-- Mathlib.Topology.Category.CompHausLike.Basic
/-- A constructor for objects of the category `CompHausLike P`,
taking a type, and bundling the compact Hausdorff topology
found by typeclass inference.  -/
CompHausLike.of : (P : TopCat → Prop) →
  (X : Type u) →
    [inst : TopologicalSpace X] → [CompactSpace X] → [T2Space X] → [CompHausLike.HasProp P X] → CompHausLike P
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.declName : Lean.Elab.PreDefinition → Lean.Name
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.forget₂AddCommGroup_preservesLimits : ∀ {R : Type u} [inst : Ring R],
  CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)
-- Mathlib.Topology.Constructions.SumProd
/-- `Prod.snd` maps neighborhood of `x : X × Y` within the section `Prod.fst ⁻¹' {x.1}`
to `𝓝 x.2`.  -/
map_snd_nhdsWithin : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X × Y),
  Filter.map Prod.snd (nhdsWithin x (Prod.fst ⁻¹' {x.1})) = nhds x.2
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
NormedSpace.toModule.hcongr_5 : ∀ (𝕜 𝕜' : Type u_6),
  𝕜 = 𝕜' →
    ∀ (E E' : Type u_7),
      E = E' →
        ∀ (inst : NormedField 𝕜) (inst' : NormedField 𝕜'),
          inst ≍ inst' →
            ∀ (inst_1 : SeminormedAddCommGroup E) (inst'_1 : SeminormedAddCommGroup E'),
              inst_1 ≍ inst'_1 →
                ∀ (self : NormedSpace 𝕜 E) (self' : NormedSpace 𝕜' E'), self ≍ self' → self.toModule ≍ self'.toModule
-- Lean.Parser.Do
Lean.Parser.Term.doSeqItem.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Homology.DifferentialObject
ComplexShape.up'.congr_simp : ∀ {α : Type u_2} [inst : Add α] [inst_1 : IsRightCancelAdd α] (a a_1 : α),
  a = a_1 → ComplexShape.up' a = ComplexShape.up' a_1
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.toCycles_i_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) {Z : C}
  (h_1 : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.toCycles f g fg h n)
      (CategoryTheory.CategoryStruct.comp (X.iCycles f g n) h_1) =
    CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) h_1
-- Mathlib.CategoryTheory.Limits.Preorder
Preorder.coneOfLowerBound_pt : ∀ {C : Type u} [inst : Preorder C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v, u'} J]
  (F : CategoryTheory.Functor J C) {x : C} (h : x ∈ lowerBounds (Set.range F.obj)),
  (Preorder.coneOfLowerBound F h).pt = x
-- Mathlib.Order.PiLex
Pi.lt_toLex_update_self_iff : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] {x : (i : ι) → β i} {i : ι} {a : β i}
  [inst_1 : (i : ι) → PartialOrder (β i)] [WellFoundedLT ι], toLex x < toLex (Function.update x i a) ↔ x i < a
-- Mathlib.RingTheory.Localization.Module
IsLocalizedModule.map_surjective_iff_localizedModuleMap_surjective : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {M' : Type u_4} {N' : Type u_5} [inst : CommSemiring R] {S : Submonoid R}
  [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  [inst_5 : AddCommMonoid M'] [inst_6 : Module R M'] [inst_7 : AddCommMonoid N'] [inst_8 : Module R N']
  (g₁ : M →ₗ[R] M') (g₂ : N →ₗ[R] N') [inst_9 : IsLocalizedModule S g₁] [inst_10 : IsLocalizedModule S g₂]
  {l : M →ₗ[R] N},
  Function.Surjective ⇑((IsLocalizedModule.map S g₁ g₂) l) ↔ Function.Surjective ⇑((LocalizedModule.map S) l)
-- Mathlib.Algebra.Category.ModuleCat.Products
ModuleCat.lof_coprodIsoDirectSum_inv : ∀ {R : Type u} [inst : Ring R] {ι : Type v} (Z : ι → ModuleCat R) [inst_1 : DecidableEq ι]
  [inst_2 : CategoryTheory.Limits.HasCoproduct Z] (i : ι),
  CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (DirectSum.lof R ι (fun i => ↑(Z i)) i))
      (ModuleCat.coprodIsoDirectSum Z).inv =
    CategoryTheory.Limits.Sigma.ι Z i
-- Mathlib.Order.Disjoint
Disjoint.right_lt_sup_of_left_ne_bot : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b → a ≠ ⊥ → b < a ⊔ b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.find?_toArray_eq_none_iff_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF → ∀ {k : α}, Array.find? (fun x => x.1 == k) (Std.DHashMap.Raw.Const.toArray ↑m) = none ↔ m.contains k = false
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.map_neg_atBot : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G],
  Filter.map Neg.neg Filter.atBot = Filter.atTop
-- Mathlib.Analysis.Convex.Segment
segment_eq_Icc : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y : 𝕜},
  x ≤ y → segment 𝕜 x y = Set.Icc x y
-- Mathlib.CategoryTheory.Abelian.Preradical.Basic
/-- A preradical on an abelian category `C` is a monomorphism in `C ⥤ C` with codomain `𝟭 C`.  -/
CategoryTheory.Abelian.Preradical : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Init.Data.Option.Lemmas
Option.isSome_apply_of_isSome_bind : ∀ {α : Type u_1} {β : Type u_2} {x : Option α} {f : α → Option β} (h : (x.bind f).isSome = true),
  (f (x.get ⋯)).isSome = true
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.NullSingletonClass.measure_singleton : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [self : MeasureTheory.NullSingletonClass μ]
  (x : α), μ {x} = 0
-- Init.Data.Vector.Algebra
Vector.hmul_add : ∀ {β : Type u_1} {γ : Type u_2} {α : Type u_3} {n : ℕ} [inst : Add β] [inst_1 : Add γ] [inst_2 : HMul α β γ],
  (∀ (c : α) (x y : β), c * (x + y) = c * x + c * y) → ∀ (c : α) (xs ys : Vector β n), c * (xs + ys) = c * xs + c * ys
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.contains_alter : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  m.WF → (m.alter k f).contains k' = if (k == k') = true then (f m[k]?).isSome else m.contains k'
-- Mathlib.Algebra.Group.Subgroup.Actions
/-- The action by a subgroup is the action by the underlying group.  -/
Subgroup.instMulAction : {G : Type u_1} → {α : Type u_2} → [inst : Group G] → [MulAction G α] → {S : Subgroup G} → MulAction (↥S) α
-- Mathlib.Geometry.Convex.ConvexSpace.Module
Convexity.instIsModuleConvexSpaceForall : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {ι : Type u_6}
  {M : ι → Type u_7} [inst_3 : (i : ι) → AddCommMonoid (M i)] [inst_4 : (i : ι) → Module R (M i)]
  [inst_5 : (i : ι) → Convexity.ConvexSpace R (M i)] [∀ (i : ι), Convexity.IsModuleConvexSpace R (M i)],
  Convexity.IsModuleConvexSpace R ((i : ι) → M i)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.insertManyIfNewUnit_nil : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp},
  Std.DTreeMap.Raw.Const.insertManyIfNewUnit t [] = t
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₂_app_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 2}
  (app₀ : f.obj' 0 _proof_245✝ ⟶ g.obj' 0 _proof_245✝) (app₁ : f.obj' 1 _proof_246✝ ⟶ g.obj' 1 _proof_246✝)
  (app₂ : f.obj' 2 _proof_247✝ ⟶ g.obj' 2 _proof_247✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_246✝))
      _auto_251✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_247✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_247✝))
      _auto_253✝),
  (CategoryTheory.ComposableArrows.homMk₂ app₀ app₁ app₂ w₀ w₁).app 0 = app₀
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.δFromOpcycles.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ : ℤ)
  (hn₁ : n₀ + 1 = n₁), X.δFromOpcycles f₁ f₂ f₃ n₀ n₁ hn₁ = X.descOpcycles f₂ f₃ (n₀ - 1) n₀ ⋯ (X.δ f₁ f₂ n₀ n₁ hn₁) ⋯
-- Mathlib.Data.Finset.Card
/-- Given a bijection from a finite set `s` to a finite set `t`, the cardinalities of `s` and `t`
are equal.

The difference with `Finset.card_bij` is that the bijection is specified with an inverse, rather
than as a surjective injection.

The difference with `Finset.card_nbij'` is that the bijection and its inverse are allowed to use
membership of the domains, rather than being non-dependent functions.  -/
Finset.card_bij' : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (i : (a : α) → a ∈ s → β) (j : (a : β) → a ∈ t → α)
  (hi : ∀ (a : α) (ha : a ∈ s), i a ha ∈ t) (hj : ∀ (a : β) (ha : a ∈ t), j a ha ∈ s),
  (∀ (a : α) (ha : a ∈ s), j (i a ha) ⋯ = a) → (∀ (a : β) (ha : a ∈ t), i (j a ha) ⋯ = a) → s.card = t.card
-- Mathlib.Order.BooleanAlgebra.Defs
/-- `⊥` is the least element  -/
BooleanAlgebra.bot_le : ∀ {α : Type u} [self : BooleanAlgebra α] (a : α), ⊥ ≤ a
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS_even : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (m : ℤ),
  preNormEDS b c d (2 * m) =
    preNormEDS b c d (m - 1) ^ 2 * preNormEDS b c d m * preNormEDS b c d (m + 2) -
      preNormEDS b c d (m - 2) * preNormEDS b c d m * preNormEDS b c d (m + 1) ^ 2
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.BoundedFormula.restrictFreeVar.match_1.splitter : {L : FirstOrder.Language} →
  {α : Type u_3} →
    {β : Type u_5} →
      [inst : DecidableEq α] →
        (motive : (x : ℕ) → (x_1 : L.BoundedFormula α x) → (↥x_1.freeVarFinset → β) → Sort u_4) →
          (x : ℕ) →
            (x_1 : L.BoundedFormula α x) →
              (x_2 : ↥x_1.freeVarFinset → β) →
                ((_n : ℕ) →
                    (_f : ↥FirstOrder.Language.BoundedFormula.falsum.freeVarFinset → β) →
                      motive _n FirstOrder.Language.BoundedFormula.falsum _f) →
                  ((_n : ℕ) →
                      (t₁ t₂ : L.Term (α ⊕ Fin _n)) →
                        (f : ↥(FirstOrder.Language.BoundedFormula.equal t₁ t₂).freeVarFinset → β) →
                          motive _n (FirstOrder.Language.BoundedFormula.equal t₁ t₂) f) →
                    ((_n l : ℕ) →
                        (R : L.Relations l) →
                          (ts : Fin l → L.Term (α ⊕ Fin _n)) →
                            (f : ↥(FirstOrder.Language.BoundedFormula.rel R ts).freeVarFinset → β) →
                              motive _n (FirstOrder.Language.BoundedFormula.rel R ts) f) →
                      ((_n : ℕ) →
                          (φ₁ φ₂ : L.BoundedFormula α _n) →
                            (f : ↥(φ₁.imp φ₂).freeVarFinset → β) → motive _n (φ₁.imp φ₂) f) →
                        ((_n : ℕ) →
                            (φ : L.BoundedFormula α (_n + 1)) → (f : ↥φ.all.freeVarFinset → β) → motive _n φ.all f) →
                          motive x x_1 x_2
-- Lean.Meta.SynthInstance
_private.Lean.Meta.SynthInstance.0.Lean.Meta.PreprocessKind.mvarsNoOutputParams.sizeOf_spec : sizeOf Lean.Meta.PreprocessKind.mvarsNoOutputParams✝ = 1