mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
_private.Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic.0.MeasureTheory.simpleFuncAux_eq_of_lt : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {f : α → β} {g : ℕ → α} {m : ℕ}
  [inst : MeasurableSingletonClass α], ∀ n > m, (MeasureTheory.simpleFuncAux✝ f g n) (g m) = f (g m)
-- Mathlib.Algebra.Group.Basic
inv_mul_eq_one : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a⁻¹ * b = 1 ↔ a = b
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- See also `iSupIndep_iff_linearIndependent_of_ne_zero`.  -/
LinearIndependent.iSupIndep_span_singleton : ∀ {ι : Type u'} {R : Type u_2} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M], LinearIndependent R v → iSupIndep fun i => R ∙ v i
-- Mathlib.Tactic.CasesM
/-- `casesm p` searches for the first hypothesis `h : type` where `type` matches the term `p`,
and splits the main goal by cases on `h`. Use holes in `p` to indicate arbitrary subexpressions,
for example `casesm _ ∧ _` will match any conjunction. `casesm p` fails if no hypothesis type
matches `p`.

* `casesm p_1, ..., p_n` searches for a hypothesis `h : type` where `type` matches one or more of
  the given patterns `p_1`, ... `p_n`, and splits the main goal by cases on `h`.
* `casesm* p` repeatedly performs case splits until no more hypothesis type matches `p`.
  This is a more efficient and compact version of `· repeat casesm p`.
  It is more efficient because the pattern is compiled once.
* `casesm! p` and `casesm!* p` skip a hypothesis if the main goal would be replaced with two or more
  subgoals.

Example:
```
example (h : a ∧ b ∨ c ∧ d) (h2 : e ∧ f) : True := by
  -- The following tactic destructs all conjunctions and disjunctions in the current context.
  casesm* _∨_, _∧_
  · clear ‹a› ‹b› ‹e› ‹f›; (fail_if_success clear ‹c›); trivial
  · clear ‹c› ‹d› ‹e› ‹f›; trivial
```
 -/
Mathlib.Tactic.casesM : Lean.ParserDescr
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vge_of_veq : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y : R}, x =ᵥ y → y ≤ᵥ x
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.Integrable.of_comp_snd : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  {f : β → E}, MeasureTheory.Integrable (fun x => f x.2) (μ.prod ν) → μ ≠ 0 → MeasureTheory.Integrable f ν
-- Mathlib.Analysis.Complex.Trigonometric
/-- The real hyperbolic sine function, defined as the real part of the complex hyperbolic sine  -/
Real.sinh : ℝ → ℝ
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddZero.eq_1 : ∀ {α : Type u_1} [inst : AddZero α],
  AddOpposite.instAddZero = { toZero := AddOpposite.instZero, toAdd := AddOpposite.instAdd }
-- Mathlib.Geometry.Euclidean.Altitude
/-- The inner product of an edge from `j` to `i` and the vector from the foot of `i` to `i`
is the square of the height.  -/
Affine.Simplex.inner_vsub_vsub_altitudeFoot_eq_height_sq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) [inst_4 : NeZero n] {i j : Fin (n + 1)},
  i ≠ j → inner ℝ (s.points i -ᵥ s.points j) (s.points i -ᵥ s.altitudeFoot i) = s.height i ^ 2
-- Batteries.Data.List.Scan
List.take_partialProds : ∀ {α : Type u_1} {i : ℕ} [inst : Mul α] [inst_1 : One α] {l : List α},
  List.take (i + 1) l.partialProds = (List.take i l).partialProds
-- Mathlib.Data.Nat.Prime.Defs
Nat.prime_def_lt : ∀ {p : ℕ}, Nat.Prime p ↔ 2 ≤ p ∧ ∀ m < p, m ∣ p → m = 1
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.norm_mk_le : ∀ {α : Type u_1} {L₁ : List (α × Bool)} [inst : DecidableEq α], (FreeAddGroup.mk L₁).norm ≤ L₁.length
-- Mathlib.Topology.Bornology.BoundedOperation
SeminormedAddCommGroup.lipschitzWith_sub : ∀ {R : Type u_1} [inst : SeminormedAddCommGroup R], LipschitzWith 2 fun p => p.1 - p.2
-- Mathlib.Algebra.Module.FinitePresentation
Module.FinitePresentation.out : ∀ {R : Type u_1} {M : Type u_2} {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M}
  [self : Module.FinitePresentation R M],
  ∃ s, Submodule.span R ↑s = ⊤ ∧ (Finsupp.linearCombination R Subtype.val).ker.FG
-- Mathlib.Data.List.Cycle
List.nextOr_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {xs : List α} {x d : α}, d ∈ xs → xs.nextOr x d ∈ xs
-- Mathlib.Order.SuccPred.Basic
Order.succ_eq_iff_isMax : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] {a : α}, Order.succ a = a ↔ IsMax a
-- Mathlib.Order.LiminfLimsup
/-- If `f : α → α` is a morphism of complete lattices, then the liminf of its iterates of any
`a : α` is a fixed point.  -/
CompleteLatticeHom.apply_liminf_iterate : ∀ {α : Type u_1} [inst : CompleteLattice α] (f : CompleteLatticeHom α α) (a : α),
  f (Filter.liminf (fun n => (⇑f)^[n] a) Filter.atTop) = Filter.liminf (fun n => (⇑f)^[n] a) Filter.atTop
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor_map_fiber : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat)
  {X Y : CategoryTheory.Grothendieck (F.comp CategoryTheory.Cat.asSmallFunctor)} (f : X ⟶ Y),
  ((CategoryTheory.Grothendieck.compAsSmallFunctorEquivalenceFunctor F).map f).fiber =
    CategoryTheory.AsSmall.down.map f.fiber
-- Mathlib.Order.SymmDiff
symmDiff_isCommutative : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α], Std.Commutative fun x1 x2 => symmDiff x1 x2
-- Mathlib.Analysis.Convex.Basic
convex_Ioo : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_5 : Module 𝕜 β] [PosSMulStrictMono 𝕜 β] (r s : β),
  Convex 𝕜 (Set.Ioo r s)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.mem_closed_of_isRelational : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] [L.IsRelational] (s : Set M),
  s ∈ (FirstOrder.Language.Substructure.closure L).closed
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsNonloopAt.vertex_mem : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} {G : Graph α β}, G.IsNonloopAt e x → x ∈ G.vertexSet
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- Fundamental theorem of calculus: if `f : ℝ → E` is integrable on `a..b` and `f x` has a finite
limit `c` almost surely as `x` tends to `b` from the right or from the left, then the right
(resp., left) derivative of `u ↦ ∫ x in a..u, f x` at `b` equals `c`.  -/
intervalIntegral.derivWithin_integral_of_tendsto_ae_right : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E}
  {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    ∀ {s t : Set ℝ} [intervalIntegral.FTCFilter b (nhdsWithin b s) (nhdsWithin b t)],
      StronglyMeasurableAtFilter f (nhdsWithin b t) MeasureTheory.volume →
        Filter.Tendsto f (nhdsWithin b t ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c) →
          autoParam (UniqueDiffWithinAt ℝ s b) intervalIntegral.derivWithin_integral_of_tendsto_ae_right._auto_1 →
            derivWithin (fun u => ∫ (x : ℝ) in a..u, f x) s b = c
-- Mathlib.GroupTheory.Coset.Basic
rightCoset_eq_iff : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {x y : α},
  MulOpposite.op x • ↑s = MulOpposite.op y • ↑s ↔ y * x⁻¹ ∈ s
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.factorₐ_evalₐ_one : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (x : AdicCompletion I R),
  (Ideal.Quotient.factor ⋯) ((AdicCompletion.evalₐ I 1) x) = (AdicCompletion.evalOneₐ I) x
-- Mathlib.Analysis.InnerProductSpace.LinearMap
/-- `innerSL` is an isometry. Note that the associated `LinearIsometry` is defined in
`InnerProductSpace.Dual` as `toDualMap`.  -/
innerSL_apply_norm : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), ‖(innerSL 𝕜) x‖ = ‖x‖
-- Mathlib.Topology.Bornology.Absorbs
Absorbs.mono_left : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s₁ s₂ t : Set α},
  Absorbs M s₁ t → s₁ ⊆ s₂ → Absorbs M s₂ t
-- Mathlib.LinearAlgebra.Ray
/-- Negating a ray twice produces the original ray.  -/
Module.Ray.instInvolutiveNeg : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        {M : Type u_2} → [inst_3 : AddCommGroup M] → [inst_4 : Module R M] → InvolutiveNeg (Module.Ray R M)
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The center of a ring `R` is the set of elements that commute with everything in `R`  -/
Subring.center : (R : Type u) → [inst : NonAssocRing R] → Subring R
-- Mathlib.Topology.NhdsWithin
map_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] (f : α → β) (a : α) (s : Set α),
  Filter.map f (nhdsWithin a s) = ⨅ t ∈ {t | a ∈ t ∧ IsOpen t}, Filter.principal (f '' (t ∩ s))
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.ShiftSequence.leftComp_isoZero : ∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} A]
  {F : CategoryTheory.Functor C A} {π : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D A} (e : π.comp H ≅ F)
  (M : Type u_4) [inst_3 : AddMonoid M] [inst_4 : CategoryTheory.HasShift C M] [inst_5 : CategoryTheory.HasShift D M]
  [inst_6 : π.CommShift M] [inst_7 : H.ShiftSequence M],
  CategoryTheory.Functor.ShiftSequence.isoZero = π.isoWhiskerLeft (H.isoShiftZero M) ≪≫ e
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.minKeyD.match_1.eq_3 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3) (size : ℕ) (k : α)
  (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r r_1 : Std.DTreeMap.Internal.Impl α β) (fallback : α)
  (h_1 : (fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : α) → motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β k_2) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r →
                      (r_2 : Std.DTreeMap.Internal.Impl α β) →
                        (fallback : α) →
                          motive
                            (Std.DTreeMap.Internal.Impl.inner size k v
                              (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r) r_2)
                            fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1,
      fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_1 r)) r_2,
      fallback => h_3 size k v l size_2 k_2 v_2 l_1 r h r_2 fallback) =
    h_3 size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) size_1 k_1 v_1 l r ⋯ r_1 fallback
-- Mathlib.Analysis.InnerProductSpace.Dual
_private.Mathlib.Analysis.InnerProductSpace.Dual.0.InnerProductSpace.«term_†_1» : Lean.TrailingParserDescr
-- Mathlib.Data.Finset.Sum
Finset.toRight_map_sumComm : ∀ {α : Type u_1} {β : Type u_2} {u : Finset (α ⊕ β)}, (Finset.map (Equiv.sumComm α β).toEmbedding u).toRight = u.toLeft
-- Mathlib.Dynamics.BirkhoffSum.Average
birkhoffAverage_congr_ring' : ∀ (R : Type u_1) {α : Type u_2} {M : Type u_3} [inst : DivisionSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (S : Type u_4) [inst_3 : DivisionSemiring S] [inst_4 : Module S M],
  birkhoffAverage R = birkhoffAverage S
-- Mathlib.ModelTheory.Skolem
/-- A language consisting of Skolem functions for another language.
Called `skolem₁` because it is the first step in building a Skolemization of a language.  -/
FirstOrder.Language.skolem₁ : FirstOrder.Language → FirstOrder.Language
-- Mathlib.NumberTheory.Bernoulli
bernoulli'_def : ∀ (n : ℕ), bernoulli' n = 1 - ∑ k ∈ Finset.range n, ↑(n.choose k) / (↑n - ↑k + 1) * bernoulli' k
-- Mathlib.Probability.Kernel.Proper
/-- Auxiliary lemma for `IsProper.lintegral_mul` and
`IsProper.setLIntegral_eq_indicator_mul_lintegral`.  -/
_private.Mathlib.Probability.Kernel.Proper.0.ProbabilityTheory.Kernel.IsProper.lintegral_indicator_mul : ∀ {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : ProbabilityTheory.Kernel X X} {B : Set X} {f : X → ENNReal} {x₀ : X},
  π.IsProper →
    𝓑 ≤ 𝓧 →
      Measurable f →
        MeasurableSet B → ∫⁻ (x : X), B.indicator 1 x * f x ∂π x₀ = B.indicator 1 x₀ * ∫⁻ (x : X), f x ∂π x₀
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.derivedLitsInvariant_confirmRupHint : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_assignments_size : f.assignments.size = n)
  (rupHints : Array ℕ) (i : Fin rupHints.size)
  (acc :
    Array Std.Tactic.BVDecide.LRAT.Internal.Assignment ×
      Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool),
  (∃ (hsize : acc.1.size = n), f.DerivedLitsInvariant f_assignments_size acc.1 hsize acc.2.1) →
    have rupHint_res := Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint f.clauses acc rupHints[i];
    ∃ (hsize : rupHint_res.1.size = n), f.DerivedLitsInvariant f_assignments_size rupHint_res.1 hsize rupHint_res.2.1
-- Init.Data.Format.Basic
Std.Format.nest.injEq : ∀ (indent : ℤ) (f : Std.Format) (indent_1 : ℤ) (f_1 : Std.Format),
  (Std.Format.nest indent f = Std.Format.nest indent_1 f_1) = (indent = indent_1 ∧ f = f_1)
-- Mathlib.Order.Atoms
IsAtom.ne_bot : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : OrderBot α] {a : α}, IsAtom a → a ≠ ⊥
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
isAddIndecomposable_id_univ : ∀ {M : Type u_2} [inst : AddMonoid M] [Subsingleton (AddUnits M)] {x : M},
  x ≠ 0 → (IsAddIndecomposable id Set.univ x ↔ AddIrreducible x)
-- Mathlib.LinearAlgebra.Matrix.Rank
Matrix.lift_cRank_submatrix : ∀ {m : Type um} {m₀ : Type um₀} {n₀ : Type un₀} {R : Type uR} {n : Type un} [inst : Semiring R] (A : Matrix m n R)
  (em : m₀ ≃ m) (en : n₀ ≃ n),
  Cardinal.lift.{um, max uR um₀} (A.submatrix ⇑em ⇑en).cRank = Cardinal.lift.{um₀, max uR um} A.cRank
-- Mathlib.Logic.Basic
/-- **Alias** of `Bool.beq_eq_decide_eq`. -/
beq_eq_decide : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] [inst_2 : DecidableEq α] (a b : α), (a == b) = decide (a = b)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α} (h : t.WF),
  (Std.TreeMap.Raw.filterMap f t).getKey? k = (t.getKey? k).pfilter fun x h' => (f x t[x]).isSome
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- Pointwise monoids (`Set`, `Finset`, `Filter`) have derived pointwise actions of the form
`SMul α β → SMul α (Set β)`. When `α` is `ℕ` or `ℤ`, this action conflicts with the
nat or int action coming from `Set β` being a `Monoid` or `DivInvMonoid`. For example,
`2 • {a, b}` can both be `{2 • a, 2 • b}` (pointwise action, pointwise repeated addition,
`Set.smulSet`) and `{a + a, a + b, b + a, b + b}` (nat or int action, repeated pointwise
addition, `Set.NSMul`).

Because the pointwise action can easily be spelled out in such cases, we give higher priority to the
nat and int actions.
 -/
LibraryNote.pointwise_nat_action : Batteries.Util.LibraryNote
-- Mathlib.Algebra.Group.Defs
IsDedekindFiniteAddMonoid.of_exists_add_self_eq_zero : ∀ (M : Type u_2) [inst : AddMonoid M], (∀ (x y : M), x + y = 0 → ∃ z, z + x = 0) → IsDedekindFiniteAddMonoid M
-- Mathlib.Algebra.Group.Pi.Basic
Pi.commMagma : {I : Type u} → {f : I → Type v₁} → [(i : I) → CommMagma (f i)] → CommMagma ((i : I) → f i)
-- Std.Data.ExtDHashMap.Lemmas
_private.Std.Data.ExtDHashMap.Lemmas.0.Std.ExtDHashMap.insertIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m : Std.ExtDHashMap α β) (a : α) (b : β a),
  m.insertIfNew a b = Std.ExtDHashMap.lift (fun m => Std.ExtDHashMap.mk (m.insertIfNew a b)) ⋯ m
-- Aesop.Tree.Data
Aesop.RappId.mk.inj : ∀ {toNat toNat_1 : ℕ}, { toNat := toNat } = { toNat := toNat_1 } → toNat = toNat_1
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.mono_lie_right : ∀ {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 N' : LieSubmodule R L M} [inst_5 : LieAlgebra R L]
  (I : LieIdeal R L), N ≤ N' → ⁅I, N⁆ ≤ ⁅I, N'⁆
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.valueGroup.mk_mul : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : CommGroupWithZero B] (f : A →*₀ B) {r₁ s₁ r₂ s₂ : A}
  {hr₁ : f r₁ ≠ 0} {hs₁ : f s₁ ≠ 0} {hr₂ : f r₂ ≠ 0} {hs₂ : f s₂ ≠ 0},
  MonoidWithZeroHom.valueGroup.mk f r₁ s₁ hr₁ hs₁ * MonoidWithZeroHom.valueGroup.mk f r₂ s₂ hr₂ hs₂ =
    MonoidWithZeroHom.valueGroup.mk f (r₁ * r₂) (s₁ * s₂) ⋯ ⋯
-- Batteries.Data.List.Lemmas
List.idxOfNth_cons : ∀ {α : Type u_1} {xs : List α} {x : α} {n : ℕ} [inst : BEq α] {a : α},
  List.idxOfNth x (a :: xs) n =
    if n = 0 then if (a == x) = true then 0 else List.idxOfNth x xs 0 + 1
    else if (a == x) = true then List.idxOfNth x xs (n - 1) + 1 else List.idxOfNth x xs n + 1
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomotopyEquiv.trans_homotopyHomInvId : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (e : S₁.HomotopyEquiv S₂) (e' : S₂.HomotopyEquiv S₃),
  (e.trans e').homotopyHomInvId =
    (CategoryTheory.ShortComplex.Homotopy.ofEq ⋯).trans
      (((e'.homotopyHomInvId.compRight e.inv).compLeft e.hom).trans
        ((CategoryTheory.ShortComplex.Homotopy.ofEq ⋯).trans e.homotopyHomInvId))
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.widePullbackShapeUnop_obj : ∀ (J : Type w) (X : (CategoryTheory.Limits.WidePullbackShape J)ᵒᵖ),
  (CategoryTheory.Limits.widePullbackShapeUnop J).obj X = Opposite.unop X
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.map_comp : ∀ {V : Type u} {W : Type v} {G : SimpleGraph V} {G' : SimpleGraph W} {U : Type u_2} {G'' : SimpleGraph U}
  (H : G.Subgraph) (f : G →g G') (g : G' →g G''),
  SimpleGraph.Subgraph.map (g.comp f) H = SimpleGraph.Subgraph.map g (SimpleGraph.Subgraph.map f H)
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
CategoryTheory.Functor.IsCocartesian.map_self : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsCocartesian f φ],
  CategoryTheory.Functor.IsCocartesian.map p f φ φ = CategoryTheory.CategoryStruct.id b
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_inv_app_op_zero : CategoryTheory.Limits.walkingParallelPairOpEquiv.counitIso.inv.app
    (Opposite.op CategoryTheory.Limits.WalkingParallelPair.zero) =
  CategoryTheory.CategoryStruct.id (Opposite.op CategoryTheory.Limits.WalkingParallelPair.zero)
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.piecewise'_apply_right : ∀ {X : Type u_1} {Z : Type u_3} [inst : TopologicalSpace X] {C₀ C₁ C₂ : Set X} (h₀ : C₀ ⊆ C₁ ∪ C₂) (h₁ : IsClosed C₁)
  (h₂ : IsClosed C₂) (f₁ : LocallyConstant (↑C₁) Z) (f₂ : LocallyConstant (↑C₂) Z)
  [inst_1 : DecidablePred fun x => x ∈ C₁] (hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩) (x : ↑C₀)
  (hx : ↑x ∈ C₂), (LocallyConstant.piecewise' h₀ h₁ h₂ f₁ f₂ hf) x = f₂ ⟨↑x, hx⟩
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.instSemiring : {R : Type u_1} →
  {M : Type u_4} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Semiring (Module.End R M)
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_neg_nhdsGT_neg : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddCommGroup H] [inst_2 : PartialOrder H] [IsOrderedAddMonoid H]
  [ContinuousNeg H] {a : H}, Filter.Tendsto Neg.neg (nhdsWithin (-a) (Set.Ioi (-a))) (nhdsWithin a (Set.Iio a))
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.asIsoHomologyπ.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) [inst_2 : S.HasHomology], S.asIsoHomologyπ hf = S.asIsoHomologyπ hf
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.varFinsetLeft.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_4} {β : Type u_3} (motive : L.Term (α ⊕ β) → Sort u_5) (i : α)
  (h_1 : (i : α) → motive (FirstOrder.Language.var (Sum.inl i)))
  (h_2 : (_i : β) → motive (FirstOrder.Language.var (Sum.inr _i)))
  (h_3 : (l : ℕ) → (_f : L.Functions l) → (ts : Fin l → L.Term (α ⊕ β)) → motive (FirstOrder.Language.func _f ts)),
  (match FirstOrder.Language.var (Sum.inl i) with
    | FirstOrder.Language.var (Sum.inl i) => h_1 i
    | FirstOrder.Language.var (Sum.inr _i) => h_2 _i
    | FirstOrder.Language.func _f ts => h_3 l _f ts) =
    h_1 i
-- Mathlib.RingTheory.Congruence.BigOperators
RingCon.coe_finsuppSum : ∀ {ι : Type u_1} {β : Type u_2} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : Mul M] [inst_2 : Zero β]
  (c : RingCon M) (h : ι → β → M) (f : ι →₀ β), ↑(f.sum h) = f.sum fun i b => ↑(h i b)
-- Mathlib.LinearAlgebra.Orientation
/-- If the index type has cardinality equal to the finite dimension, composing an alternating
map with the same linear equiv on each argument gives the negation of that orientation if and
only if the determinant is negative.  -/
Orientation.map_eq_neg_iff_det_neg : ∀ {R : Type u_1} [inst : Field R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {ι : Type u_3} [inst_5 : Fintype ι] (x : Orientation R M ι)
  (f : M ≃ₗ[R] M), Fintype.card ι = Module.finrank R M → ((Orientation.map ι f) x = -x ↔ LinearMap.det ↑f < 0)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (W : C)
  {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) {Z_1 : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj W Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft W g) h)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_presheaf_map_top : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens),
  CategoryTheory.CategoryStruct.comp U.toSpecΓ
      (AlgebraicGeometry.Spec.map (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) =
    CategoryTheory.CategoryStruct.comp U.ι X.toSpecΓ
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_insertList_le : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l toInsert : List ((a : α) × β a)},
  (Std.Internal.List.insertList l toInsert).length ≤ l.length + toInsert.length
-- Mathlib.Algebra.Order.Group.Abs
/-- `|a - b| ≤ n` if `0 ≤ a ≤ n` and `0 ≤ b ≤ n`.  -/
abs_sub_le_of_nonneg_of_le : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b n : G},
  0 ≤ a → a ≤ n → 0 ≤ b → b ≤ n → |a - b| ≤ n