mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The 2-cycles `Z₂(G, A)` of `A : Rep k G`, defined as the kernel of the map
`(G² →₀ A) → (G →₀ A)` defined by `a·(g₁, g₂) ↦ ρ_A(g₁⁻¹)(a)·g₂ - a·g₁g₂ + a·g₁`.  -/
groupHomology.cycles₂ : {k G : Type u} → [inst : CommRing k] → [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → Submodule k (G × G →₀ ↑A)
-- Init.Data.Array.Zip
Array.zipWith_map_right : ∀ {α : Type u_1} {β : Type u_2} {β' : Type u_3} {γ : Type u_4} {as : Array α} {bs : Array β} {f : β → β'}
  {g : α → β' → γ}, Array.zipWith g as (Array.map f bs) = Array.zipWith (fun a b => g a (f b)) as bs
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.splits_charpoly : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [inst_3 : FiniteDimensional 𝕜 E], T.IsSymmetric → T.charpoly.Splits
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddZeroClassOfAddOpposite : {M : Type u_1} → [AddZeroClass Mᵃᵒᵖ] → AddZeroClass Mᵈᵃᵃ
-- Init.Data.SInt.Bitwise
ISize.ofBitVec_or : ∀ (a b : BitVec System.Platform.numBits), ISize.ofBitVec (a ||| b) = ISize.ofBitVec a ||| ISize.ofBitVec b
-- Init.Data.Int.DivMod.Basic
_private.Init.Data.Int.DivMod.Basic.0.Int.fdiv.match_1.splitter : (motive : ℤ → ℤ → Sort u_1) →
  (x x_1 : ℤ) →
    ((x : ℤ) → motive 0 x) →
      ((m n : ℕ) → (m = 0 → False) → motive (Int.ofNat m) (Int.ofNat n)) →
        ((m n : ℕ) → motive (Int.ofNat m.succ) (Int.negSucc n)) →
          ((a : ℕ) → motive (Int.negSucc a) 0) →
            ((m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n.succ)) →
              ((m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)) → motive x x_1
-- Mathlib.ModelTheory.Definability
/-- Finite existential quantifiers preserve definablity.  -/
Set.Definable.exists_of_finite : ∀ {M : Type w} {A : Set M} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u₁} {β : Type u_1} [Finite β]
  {S : Set (α ⊕ β → M)}, A.Definable L S → A.Definable L {v | ∃ u, Sum.elim v u ∈ S}
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- When a vector is in `Kᗮ`.  -/
Submodule.mem_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) (v : E), v ∈ Kᗮ ↔ ∀ u ∈ K, inner 𝕜 u v = 0
-- Mathlib.AlgebraicGeometry.Sites.EtalePoint
AlgebraicGeometry.Scheme.isConservative_pointSmallEtale : ∀ {ι : Type u_1} {S : AlgebraicGeometry.Scheme} {Ω : ι → Type u} [inst : (i : ι) → Field (Ω i)]
  [inst_1 : ∀ (i : ι), IsSepClosed (Ω i)] (s : (i : ι) → AlgebraicGeometry.Spec (CommRingCat.of (Ω i)) ⟶ S),
  ⋃ i, Set.range ⇑(s i) = Set.univ →
    (CategoryTheory.ObjectProperty.ofObj fun i =>
        AlgebraicGeometry.Scheme.pointSmallEtale (s i)).IsConservativeFamilyOfPoints
-- Mathlib.MeasureTheory.Function.LpSeminorm.Defs
/-- Real-valued `ℒp` seminorm, equal to `0` for `p = 0`, to `(∫ ‖f a‖^p ∂μ) ^ p⁻¹` for `0 < p < ∞`
and to `essSup ‖f‖ μ` for `p = ∞`.

This is well-defined only if `MemLp f p μ`. Otherwise, it equals `0`.  -/
MeasureTheory.lpNorm : {α : Type u_1} →
  {E : Type u_4} → {m0 : MeasurableSpace α} → [NormedAddCommGroup E] → (α → E) → ENNReal → MeasureTheory.Measure α → ℝ
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanced_balanceL! : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  l.Balanced →
    r.Balanced →
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size →
        (Std.DTreeMap.Internal.Impl.balanceL! k v l r).Balanced
-- Mathlib.Order.Filter.Lift
Filter.lift_lift'_same_le_lift' : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Set α → Set α → Set β},
  (f.lift fun s => f.lift' (g s)) ≤ f.lift' fun s => g s s
-- Mathlib.Tactic.Contrapose
/-- `contrapose` transforms the main goal into its contrapositive. If the goal has the form `⊢ P → Q`,
then `contrapose` turns it into `⊢ ¬ Q → ¬ P`. If the goal has the form `⊢ P ↔ Q`, then `contrapose`
turns it into `⊢ ¬ P ↔ ¬ Q`.

* `contrapose h` on a goal of the form `h : P ⊢ Q` turns the goal into `h : ¬ Q ⊢ ¬ P`. This is
  equivalent to `revert h; contrapose; intro h`.
* `contrapose h with new_h` uses the name `new_h` for the introduced hypothesis. This is equivalent
  to `revert h; contrapose; intro new_h`.
* `contrapose!`, `contrapose! h` and `contrapose! h with new_h` push negation deeper into the goal
  after contraposing (but before introducing the new hypothesis). See the `push Not` tactic for more
  details on the pushing algorithm.
* `contrapose! (config := cfg)` controls the options for negation pushing. All options for
  `Mathlib.Tactic.Push.Config` are supported:
  * `contrapose! +distrib` rewrites `¬ (p ∧ q)` into `¬ p ∨ ¬ q` instead of `p → ¬ q`.

Examples:
```lean4
variables (P Q R : Prop)

example (H : ¬ Q → ¬ P) : P → Q := by
  contrapose
  exact H

example (H : ¬ P ↔ ¬ Q) : P ↔ Q := by
  contrapose
  exact H

example (H : ¬ Q → ¬ P) (h : P) : Q := by
  contrapose h
  exact H h

example (H : ¬ R → P → ¬ Q) : (P ∧ Q) → R := by
  contrapose!
  exact H

example (H : ¬ R → ¬ P ∨ ¬ Q) : (P ∧ Q) → R := by
  contrapose! +distrib
  exact H
```
 -/
Mathlib.Tactic.Contrapose.contrapose! : Lean.ParserDescr
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.getLast?.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Init.Data.List.Nat.TakeDrop
List.zipWith_eq_zipWith_take_min : ∀ {α : Type u_1} {β : Type u_2} {α_1 : Type u_3} {f : α → β → α_1} {l₁ : List α} {l₂ : List β},
  List.zipWith f l₁ l₂ =
    List.zipWith f (List.take (min l₁.length l₂.length) l₁) (List.take (min l₁.length l₂.length) l₂)
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Algebra.TensorProduct.algEquivIncludeRange_symm_tmul : ∀ (R : Type u_1) (S : Type u_2) (T : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring T] [inst_4 : Algebra R T] (x : ↥Algebra.TensorProduct.includeLeft.range)
  (y : ↥Algebra.TensorProduct.includeRight.range),
  (Algebra.TensorProduct.algEquivIncludeRange R S T).symm (x ⊗ₜ[R] y) = ↑x * ↑y
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.rootSystem_root_apply : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [inst_4 : LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] (H : LieSubalgebra K L)
  [inst_6 : H.IsCartanSubalgebra] [inst_7 : LieModule.IsTriangularizable K (↥H) L] (α : ↥LieSubalgebra.root),
  (LieAlgebra.IsKilling.rootSystem H).root α = LieModule.Weight.toLinear K (↥H) L ↑α
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.Spec.nil : {m : Type u → Type u} → (self : MLList.Spec✝ m) → {α : Type u} → MLList.Spec.listM✝ self α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDocumentColorParams : Lean.ToJson Lean.Lsp.DocumentColorParams
-- Mathlib.Algebra.Tropical.Basic
Tropical.untrop_le_iff : ∀ {R : Type u} [inst : LE R] {x y : Tropical R}, Tropical.untrop x ≤ Tropical.untrop y ↔ x ≤ y
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instIsCancelMulZero : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M], IsCancelMulZero (Associates M)
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.cons_val' : ∀ {α : Type u} {m : ℕ} {n' : Type uₙ} (v : n' → α) (B : Fin m → n' → α) (i : Fin m.succ) (j : n'),
  Matrix.vecCons v B i j = Matrix.vecCons (v j) (fun i => B i j) i
-- Std.Time.Time.PlainTime
/-- Creates a `PlainTime` value from a total number of millisecond.
 -/
Std.Time.PlainTime.ofMilliseconds : Std.Time.Millisecond.Offset → Std.Time.PlainTime
-- Init.Control.Basic
«term_<&&>_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_X_pow_right : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R) (m n : ℕ),
  f.natDegree ≤ m → f.resultant (Polynomial.X ^ n) m n = (-1) ^ (m * n) * f.coeff 0 ^ n
-- Mathlib.Analysis.Distribution.Support
Filter.HasBasis.notMem_dsupport : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_6} {V : Type u_10} [inst : FunLike F α β] [inst_1 : TopologicalSpace α]
  [inst_2 : Zero β] [inst_3 : Zero V] {f : F → V} {ι : Sort u_11} {p : ι → Prop} {s : ι → Set α} {x : α},
  (nhds x).HasBasis p s → (x ∉ Distribution.dsupport f ↔ ∃ i, p i ∧ Distribution.IsVanishingOn f (s i))
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.tryCatch_Option : ∀ {α : Type} {x : Option α} {h : PUnit.{1} → Option α}
  (Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{1} Std.Do.PostShape.pure)),
  ⦃(Std.Do.wp x).apply (Q.1, fun e => (Std.Do.wp (h e)).apply Q, Q.2.2)⦄ MonadExceptOf.tryCatch x h ⦃Q⦄
-- Mathlib.Algebra.Polynomial.Identities
_private.Mathlib.Algebra.Polynomial.Identities.0.Polynomial.polyBinomAux1 : {R : Type u} →
  [inst : CommRing R] →
    (x y : R) → (e : ℕ) → (a : R) → { k // a * (x + y) ^ e = a * (x ^ e + ↑e * x ^ (e - 1) * y + k * y ^ 2) }
-- Mathlib.MeasureTheory.Function.UnifTight
MeasureTheory.UnifTight.eventually_cofinite_indicator : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup β] {f : ι → α → β} {p : ENNReal},
  MeasureTheory.UnifTight f p μ →
    ∀ {ε : ENNReal},
      ε ≠ 0 → ∀ᶠ (s : Set α) in μ.cofinite.smallSets, ∀ (i : ι), MeasureTheory.eLpNorm (s.indicator (f i)) p μ ≤ ε
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.functorialFactorizationData_Z_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  {X Y : CategoryTheory.Arrow C} (φ : X ⟶ Y),
  (CategoryTheory.SmallObject.functorialFactorizationData I κ).Z.map φ = CategoryTheory.SmallObject.objMap I κ φ
-- Mathlib.Algebra.Group.Basic
inv_bijective : ∀ {G : Type u_3} [inst : InvolutiveInv G], Function.Bijective Inv.inv
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_ric_eq_toArray_rco : ∀ {n : ℕ}, (*...=n).toArray = (0...n + 1).toArray
-- Mathlib.Algebra.Group.Hom.Defs
/-- `M →+ N` is the type of functions `M → N` that preserve the `AddZero` structure.

`AddMonoidHom` is also used for group homomorphisms.

When possible, instead of parametrizing results over `(f : M →+ N)`,
you should parametrize over `(F : Type*) [AddMonoidHomClass F M N] (f : F)`.

When you extend this structure, make sure to extend `AddMonoidHomClass`.


[Wikidata Q868169](https://www.wikidata.org/wiki/Q868169) -/
AddMonoidHom : (M : Type u_10) → (N : Type u_11) → [AddZero M] → [AddZero N] → Type (max u_10 u_11)
-- Mathlib.Algebra.Order.Monovary
antivaryOn_inv₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : Semifield β] [inst_4 : LinearOrder β] [IsStrictOrderedRing β] {s : Set ι} {f : ι → α} {g : ι → β},
  (∀ i ∈ s, 0 < f i) → (∀ i ∈ s, 0 < g i) → (AntivaryOn f⁻¹ g⁻¹ s ↔ AntivaryOn f g s)
-- Mathlib.LinearAlgebra.FreeProduct.Basic
LinearAlgebra.FreeProduct.ringCon.eq_1 : ∀ {I : Type u} [inst : DecidableEq I] (R : Type v) [inst_1 : CommSemiring R] (A : I → Type w)
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)],
  LinearAlgebra.FreeProduct.ringCon R A = ringConGen (LinearAlgebra.FreeProduct.rel R A)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.instCoeCharParserFn : Coe Char Lean.Parser.ParserFn
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.isLeast_opNNNorm : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→L[𝕜] F),
  IsLeast {C | ∀ (m : ι → E), ‖f m‖₊ ≤ C * ∏ i, ‖m i‖₊} ‖f‖₊
-- Mathlib.MeasureTheory.Function.Jacobian
/-- Let `f` be a function which is sufficiently close (in the Lipschitz sense) to a given linear
map `A`. Then it expands the volume of any set by at least `m` for any `m < det A`.  -/
MeasureTheory.mul_le_addHaar_image_of_lt_det : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (A : E →L[ℝ] E)
  {m : NNReal},
  ↑m < ENNReal.ofReal |A.det| →
    ∀ᶠ (δ : NNReal) in nhdsWithin 0 (Set.Ioi 0),
      ∀ (s : Set E) (f : E → E), ApproximatesLinearOn f A s δ → ↑m * μ s ≤ μ (f '' s)
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_of_inj : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    Module.Flat R ↥A ∨ Module.Flat R ↥B → Function.Injective ⇑(algebraMap R S) → Module.rank R ↥(A ⊓ B) = 1
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- The good products span `LocallyConstant C ℤ` if and only all the products do.  -/
Profinite.NobelingProof.GoodProducts.span_iff_products : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [WellFoundedLT I],
  ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval C)) ↔
    ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.Products.eval C))
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
/-- the extra degeneracy  -/
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject.Augmented C} →
      X.ExtraDegeneracy → (n : ℕ) → X.left.obj (Opposite.op { len := n }) ⟶ X.left.obj (Opposite.op { len := n + 1 })
-- Init.Data.Array.Lemmas
/-- Variant of `all_push` with a side condition on `stop`.  -/
Array.all_push' : ∀ {α : Type u_1} {stop : ℕ} {xs : Array α} {a : α} {p : α → Bool},
  stop = xs.size + 1 → (xs.push a).all p 0 stop = (xs.all p && p a)
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.F₄_diag : ∀ (i : Fin 4), CartanMatrix.F₄ i i = 2
-- Mathlib.Data.Fin.Tuple.Basic
Fin.find?_eq_some_find_of_isSome : ∀ {n : ℕ} {p : Fin n → Bool} (h : (Fin.find? p).isSome = true), Fin.find? p = some (Fin.find (fun x => p x = true) ⋯)
-- Mathlib.RingTheory.FractionalIdeal.Norm
FractionalIdeal.absNorm_eq_zero_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Module.Free ℤ R]
  [inst_3 : Module.Finite ℤ R] {K : Type u_2} [inst_4 : CommRing K] [inst_5 : Algebra R K] [inst_6 : IsFractionRing R K]
  [IsDomain K] {I : FractionalIdeal (nonZeroDivisors R) K}, FractionalIdeal.absNorm I = 0 ↔ I = 0
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.castLE_rfl : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} (h : n ≤ n) (φ : L.BoundedFormula α n),
  FirstOrder.Language.BoundedFormula.castLE h φ = φ
-- Mathlib.Probability.Kernel.IonescuTulcea.Maps
/-- Identifying `{a + 1}` with `Ioc a (a + 1)`, as a measurable equiv on dependent functions.  -/
MeasurableEquiv.piSingleton : {X : ℕ → Type u_1} →
  [inst : (n : ℕ) → MeasurableSpace (X n)] → (a : ℕ) → X (a + 1) ≃ᵐ ((i : ↥(Finset.Ioc a (a + 1))) → X ↑i)
-- Init.Data.Array.Monadic
Array.foldrM_filterMap : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} {γ : Type u_1} {start : ℕ} [inst : Monad m] [LawfulMonad m]
  {f : α → Option β} {g : β → γ → m γ} {xs : Array α} {init : γ} {w : start = (Array.filterMap f xs).size},
  Array.foldrM g init (Array.filterMap f xs) start =
    Array.foldrM
      (fun x y =>
        match f x with
        | some b => g b y
        | none => pure y)
      init xs
-- Mathlib.CategoryTheory.Abelian.SerreClass.Basic
CategoryTheory.ObjectProperty.instIsSerreClassIsZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  CategoryTheory.ObjectProperty.IsSerreClass CategoryTheory.Limits.IsZero
-- Mathlib.Data.Nat.Log
Nat.log.go.fun_cases_unfolding : ∀ (n : ℕ) (motive : ℕ → ℕ → ℕ × ℕ → Prop),
  (∀ (x : ℕ), motive x 0 (n, 0)) →
    (∀ (b fuel : ℕ), n < b → motive b fuel.succ (n, 0)) →
      (∀ (b fuel : ℕ),
          ¬n < b → ∀ (q e : ℕ), Nat.log.go n (b * b) fuel = (q, e) → q < b → motive b fuel.succ (q, 2 * e)) →
        (∀ (b fuel : ℕ),
            ¬n < b → ∀ (q e : ℕ), Nat.log.go n (b * b) fuel = (q, e) → ¬q < b → motive b fuel.succ (q / b, 2 * e + 1)) →
          ∀ (a a_1 : ℕ), motive a a_1 (Nat.log.go n a a_1)
-- Std.Do.Triple.SpecLemmas
_private.Std.Do.Triple.SpecLemmas.0.List.forIn'_cons.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.done b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_1 b
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.nilpotencyClass_prod`.

---

The nilpotency class of a product is the max of the nilpotency classes of the factors.  -/
nilpotencyClass_prod : ∀ {G₁ : Type u_2} {G₂ : Type u_3} [inst : Group G₁] [inst_1 : Group G₂] [Group.IsNilpotent G₁] [Group.IsNilpotent G₂],
  Group.nilpotencyClass (G₁ × G₂) = max (Group.nilpotencyClass G₁) (Group.nilpotencyClass G₂)
-- Mathlib.Order.Preorder.Chain
IsChain.image_relEmbedding : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α},
  IsChain r s → ∀ (φ : r ↪r r'), IsChain r' (⇑φ '' s)
-- Mathlib.LinearAlgebra.RootSystem.Basic
_private.Mathlib.LinearAlgebra.RootSystem.Basic.0.RootPairing.exist_eq_reflection_of_mapsTo : ∀ {ι : 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] (p : M →ₗ[R] N →ₗ[R] R) (root : ι ↪ M)
  (coroot : ι ↪ N) (i j : ι),
  (∀ (i : ι), Set.MapsTo (⇑(Module.preReflection (root i) (p.flip (coroot i)))) (Set.range ⇑root) (Set.range ⇑root)) →
    ∃ k, root k = (Module.preReflection (root i) (p.flip (coroot i))) (root j)
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.iterationFunctorObjObjRightIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ]
  (f : CategoryTheory.Arrow C) (j : κ.ord.ToType),
  CategoryTheory.SmallObject.iterationFunctorObjObjRightIso I κ f j =
    CategoryTheory.asIso
        ((CategoryTheory.SmallObject.transfiniteCompositionOfShapeιIterationAppRight I κ f).incl.app j) ≪≫
      (CategoryTheory.SmallObject.iterationObjRightIso I κ f).symm
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
/-- The canonical isomorphism relating `(Cospan f g).op` and `Span f.op g.op`  -/
CategoryTheory.Limits.opCospan : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          (CategoryTheory.Limits.cospan f g).op ≅
            CategoryTheory.Limits.walkingCospanOpEquiv.functor.comp (CategoryTheory.Limits.span f.op g.op)
-- Mathlib.Data.WSeq.Relation
_private.Mathlib.Data.WSeq.Relation.0.Stream'.WSeq.destruct_join.aux.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option (Stream'.WSeq α × Stream'.WSeq (Stream'.WSeq α)) → Sort u_2) (s : Stream'.WSeq α)
  (S : Stream'.WSeq (Stream'.WSeq α)) (h_1 : Unit → motive none)
  (h_2 : (s : Stream'.WSeq α) → (S : Stream'.WSeq (Stream'.WSeq α)) → motive (some (s, S))),
  (match some (s, S) with
    | none => h_1 ()
    | some (s, S) => h_2 s S) =
    h_2 s S
-- Mathlib.Algebra.Homology.AlternatingConst
HomologicalComplex.alternatingConst_X : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (A : C) {φ ψ : A ⟶ A} (hOdd : CategoryTheory.CategoryStruct.comp φ ψ = 0)
  (hEven : CategoryTheory.CategoryStruct.comp ψ φ = 0) {c : ComplexShape ℕ} [inst_2 : DecidableRel c.Rel]
  (hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)) (n : ℕ), (HomologicalComplex.alternatingConst A hOdd hEven hc).X n = A
-- Mathlib.Logic.Equiv.Basic
Equiv.eq_or_eq_of_swap_apply_ne_self : ∀ {α : Sort u_1} [inst : DecidableEq α] {a b x : α}, (Equiv.swap a b) x ≠ x → x = a ∨ x = b
-- Mathlib.Order.Filter.IndicatorFunction
Filter.EventuallyEq.mulIndicator : ∀ {α : Type u_1} {β : Type u_2} [inst : One β] {l : Filter α} {f g : α → β} {s : Set α},
  f =ᶠ[l] g → s.mulIndicator f =ᶠ[l] s.mulIndicator g
-- Mathlib.AlgebraicTopology.DoldKan.Homotopies
/-- In degree `0`, the null homotopic map `Hσ` is zero.  -/
AlgebraicTopology.DoldKan.Hσ_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q : ℕ), (AlgebraicTopology.DoldKan.Hσ q).f 0 = 0
-- Init.Data.Range.Polymorphic.IntLemmas
Int.map_add_toList_roo : ∀ {m n k : ℤ}, List.map (fun x => x + k) (m<...n).toList = ((m + k)<...n + k).toList
-- Mathlib.LinearAlgebra.TensorProduct.Map
TensorProduct.range_map : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} {P : Type u_9} {Q : Type u_10}
  [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 P] [inst_8 : Module R Q] (f : M →ₗ[R] P)
  (g : N →ₗ[R] Q), (TensorProduct.map f g).range = Submodule.map₂ (TensorProduct.mk R P Q) f.range g.range
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.braiding_inv_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y}
  (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t)
  {Z : C} (h : (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.left } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).inv
      (CategoryTheory.CategoryStruct.comp s.fst h) =
    CategoryTheory.CategoryStruct.comp t.snd h
-- Lean.Parser.Term
Lean.Parser.Term.sort.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
/-- A version of the **Borel-Cantelli lemma**: if `pᵢ` is a sequence of predicates such that
`∑' i, μ {x | pᵢ x}` is finite, then the measure of `x` such that `pᵢ x` holds frequently as `i → ∞`
(or equivalently, `pᵢ x` holds for infinitely many `i`) is equal to zero.  -/
MeasureTheory.measure_setOfPred_frequently_eq_zero : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  {p : ℕ → α → Prop}, ∑' (i : ℕ), μ {x | p i x} ≠ ⊤ → μ {x | ∃ᶠ (n : ℕ) in Filter.atTop, p n x} = 0
-- Mathlib.Analysis.Convex.Between
Sbtw.left_mem_affineSpan : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {x y z : P}, Sbtw R x y z → x ∈ line[R, z, y]
-- Mathlib.Analysis.Normed.Operator.Banach
ContinuousLinearMap.coe_linearMap_equivRange : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜'] {σ : 𝕜 →+* 𝕜'}
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {F : Type u_4}
  [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜' F] {σ' : 𝕜' →+* 𝕜} [inst_6 : RingHomInvPair σ σ']
  [inst_7 : RingHomIsometric σ] [inst_8 : RingHomIsometric σ'] [inst_9 : CompleteSpace F] [inst_10 : CompleteSpace E]
  [inst_11 : RingHomInvPair σ' σ] {f : E →SL[σ] F} (hinj : Function.Injective ⇑f) (hclo : IsClosed (Set.range ⇑f)),
  ↑(ContinuousLinearMap.equivRange hinj hclo) = f.rangeRestrict
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.relNorm_singleton : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S] (r : S),
  (Ideal.relNorm R) (Ideal.span {r}) = Ideal.span {(Algebra.intNorm R S) r}