mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
PresheafOfModules.sheafifyMap.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  {M₀ : PresheafOfModules R₀} {A : CategoryTheory.Sheaf J AddCommGrpCat} (φ : M₀.presheaf ⟶ A.obj)
  [inst_3 : CategoryTheory.Presheaf.IsLocallyInjective J φ] [inst_4 : CategoryTheory.Presheaf.IsLocallySurjective J φ]
  [inst_5 : J.WEqualsLocallyBijective AddCommGrpCat] {M₀' : PresheafOfModules R₀}
  {A' : CategoryTheory.Sheaf J AddCommGrpCat} (φ' : M₀'.presheaf ⟶ A'.obj)
  [inst_6 : CategoryTheory.Presheaf.IsLocallyInjective J φ'] [inst_7 : CategoryTheory.Presheaf.IsLocallySurjective J φ']
  (τ₀ τ₀_1 : M₀ ⟶ M₀') (e_τ₀ : τ₀ = τ₀_1) (τ τ_1 : A ⟶ A') (e_τ : τ = τ_1)
  (fac :
    CategoryTheory.CategoryStruct.comp ((PresheafOfModules.toPresheaf R₀).map τ₀) φ' =
      CategoryTheory.CategoryStruct.comp φ τ.hom),
  PresheafOfModules.sheafifyMap α φ φ' τ₀ τ fac = PresheafOfModules.sheafifyMap α φ φ' τ₀_1 τ_1 ⋯
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.monotone_map : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M →ₙ+ N}, Monotone (AddSubsemigroup.map f)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_fiberwise : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : CommMonoid M] [inst_1 : DecidableEq κ] [inst_2 : Fintype κ]
  (s : Finset ι) (g : ι → κ) (f : ι → M), ∏ j, ∏ i ∈ s with g i = j, f i = ∏ i ∈ s, f i
-- Mathlib.Algebra.Ring.Aut
RingAut.coe_pow : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R] (f : R ≃+* R) (n : ℕ), ⇑(f ^ n) = (⇑f)^[n]
-- Mathlib.NumberTheory.LegendreSymbol.Basic
/-- The Legendre symbol `legendreSym p a = 1` if there is a solution in `ℤ/pℤ`
of the equation `x^2 - a*y^2 = 0` with `x ≠ 0`.  -/
legendreSym.eq_one_of_sq_sub_mul_sq_eq_zero' : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {a : ℤ},
  ↑a ≠ 0 → ∀ {x y : ZMod p}, x ≠ 0 → x ^ 2 - ↑a * y ^ 2 = 0 → legendreSym p a = 1
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
Measurable.ennreal_tsum' : ∀ {α : Type u_1} {mα : MeasurableSpace α} {ι : Type u_5} [Countable ι] {f : ι → α → ENNReal},
  (∀ (i : ι), Measurable (f i)) → Measurable (∑' (i : ι), f i)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.PropAsSPredTautology.mk : ∀ {φ : Prop} {σs : outParam (List (Type u))} {P : outParam (Std.Do.SPred σs)},
  (φ ↔ ⊢ₛ P) → Std.Do.SPred.Tactic.PropAsSPredTautology φ P
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_le_of_le_one_left' : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : LE α] [MulRightMono α] {a b : α}, b ≤ 1 → b * a ≤ a
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
CFC.eq_zero_of_quasispectrum_eq_zero : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] (a : A),
  quasispectrum R a ⊆ {0} → autoParam (p a) CFC.eq_zero_of_quasispectrum_eq_zero._auto_1 → a = 0
-- Mathlib.Data.Nat.Choose.Sum
Finset.prod_antidiagonal_pow_choose_succ : ∀ {M : Type u_2} [inst : CommMonoid M] (f : ℕ → ℕ → M) (n : ℕ),
  ∏ ij ∈ Finset.HasAntidiagonal.antidiagonal (n + 1), f ij.1 ij.2 ^ (n + 1).choose ij.1 =
    (∏ ij ∈ Finset.HasAntidiagonal.antidiagonal n, f ij.1 (ij.2 + 1) ^ n.choose ij.1) *
      ∏ ij ∈ Finset.HasAntidiagonal.antidiagonal n, f (ij.1 + 1) ij.2 ^ n.choose ij.2
-- Mathlib.Topology.Constructions.SumProd
/-- Postcomposing `f` with `Prod.fst` is continuous  -/
Continuous.fst : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y × Z}, Continuous f → Continuous fun x => (f x).1
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.presentationOfIsCokernelFree_relations : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {ι σ : Type u} {M : SheafOfModules R}
  (f : SheafOfModules.free ι ⟶ SheafOfModules.free σ) (g : SheafOfModules.free σ ⟶ M)
  (H : CategoryTheory.CategoryStruct.comp f g = 0)
  (H' : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ g H)),
  (SheafOfModules.presentationOfIsCokernelFree f g H H').relations = SheafOfModules.relationsOfIsCokernelFree f g H H'
-- Mathlib.Analysis.LocallyConvex.Barrelled
Seminorm.continuous_iSup : ∀ {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [BarrelledSpace 𝕜 E] (p : ι → Seminorm 𝕜 E),
  (∀ (i : ι), Continuous ⇑(p i)) → BddAbove (Set.range p) → Continuous (⨆ i, ⇑(p i))
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.buildTable.go.congr_simp : ∀ (pat : String.Slice) (table table_1 : Array ℕ) (e_table : table = table_1) (ht₀ : 0 < table.size)
  (ht : table.size ≤ pat.utf8ByteSize) (h : ∀ (i : ℕ) (hi : i < table.size), table[i] ≤ i),
  String.Slice.Pattern.ForwardSliceSearcher.buildTable.go✝ pat table ht₀ ht h =
    String.Slice.Pattern.ForwardSliceSearcher.buildTable.go✝ pat table_1 ⋯ ⋯ ⋯
-- Mathlib.Analysis.InnerProductSpace.JointEigenspace
/-- **Alias** of `LinearMap.IsSymmetric.directSum_isInternal_of_pairwise_commute`.

---

In finite dimensions, given a commuting family of symmetric linear operators, the inner
product space on which they act decomposes as an internal direct sum of joint eigenspaces.  -/
LinearMap.IsSymmetric.LinearMap.IsSymmetric.directSum_isInternal_of_pairwise_commute : ∀ {𝕜 : Type u_1} {E : Type u_2} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {T : n → Module.End 𝕜 E} [FiniteDimensional 𝕜 E] [inst_4 : DecidableEq (n → 𝕜)],
  (∀ (i : n), LinearMap.IsSymmetric (T i)) →
    Pairwise (Function.onFun Commute T) → DirectSum.IsInternal fun α => ⨅ j, (T j).eigenspace (α j)
-- Mathlib.CategoryTheory.Discrete.Basic
/-- The equivalence of categories `(J → C) ≌ (Discrete J ⥤ C)`.  -/
CategoryTheory.piEquivalenceFunctorDiscrete : (J : Type u₂) →
  (C : Type u₁) →
    [inst : CategoryTheory.Category.{v₁, u₁} C] → J → C ≌ CategoryTheory.Functor (CategoryTheory.Discrete J) C
-- Mathlib.Topology.EMetricSpace.Defs
edist_ofAdd : ∀ {X : Type u_1} [inst : EDist X] (a b : X), edist (Multiplicative.ofAdd a) (Multiplicative.ofAdd b) = edist a b
-- Mathlib.Order.Directed
directedOn_univ_iff : ∀ {α : Type u_1} {r : α → α → Prop}, DirectedOn r Set.univ ↔ IsDirected α r
-- Mathlib.Data.Nat.ModEq
Nat.odd_of_mod_four_eq_one : ∀ {n : ℕ}, n % 4 = 1 → n % 2 = 1
-- Mathlib.Probability.Independence.InfinitePi
MeasureTheory.Measure.infinitePi_map_eval_prod : ∀ {ι : Type u_1} {Ω : ι → Type u_4} {mΩ : (i : ι) → MeasurableSpace (Ω i)} {P : (i : ι) → MeasureTheory.Measure (Ω i)}
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (P i)] {i j : ι},
  i ≠ j → MeasureTheory.Measure.map (fun ω => (ω i, ω j)) (MeasureTheory.Measure.infinitePi P) = (P i).prod (P j)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Functor composition induces a functor on truncated cosimplicial objects.  -/
CategoryTheory.CosimplicialObject.Truncated.whiskering : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {n : ℕ} →
      (D : Type u_1) →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          CategoryTheory.Functor (CategoryTheory.Functor C D)
            (CategoryTheory.Functor (CategoryTheory.CosimplicialObject.Truncated C n)
              (CategoryTheory.CosimplicialObject.Truncated D n))
-- Mathlib.Data.QPF.Univariate.Basic
QPF.supp_eq : ∀ {F : Type u → Type u} [q : QPF F] {α : Type u} (x : F α),
  Functor.supp x = {u | ∀ (a : (QPF.P F).A) (f : (QPF.P F).B a → α), QPF.abs ⟨a, f⟩ = x → u ∈ f '' Set.univ}
-- Mathlib.RingTheory.Localization.BaseChange
/-- The `S`-isomorphism `S ⊗[R] Rᵣ ≃ₐ Sᵣ`.  -/
IsLocalization.Away.tensorEquiv : {R : Type u_7} →
  (S : Type u_8) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (r : R) →
            (A : Type u_9) →
              [inst_3 : CommSemiring A] →
                [inst_4 : Algebra R A] →
                  [IsLocalization.Away r A] → TensorProduct R S A ≃ₐ[S] Localization.Away ((algebraMap R S) r)
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.Karoubi.HomologicalComplex.comp_p_d_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {P Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) (n : ι) {Z : C}
  (h : Q.X.X n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f.f.f n) (CategoryTheory.CategoryStruct.comp (Q.p.f n) h) =
    CategoryTheory.CategoryStruct.comp (f.f.f n) h
-- Mathlib.Data.Sum.Order
Sum.Lex.noMinOrder_of_nonempty : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] [NoMinOrder α] [Nonempty α], NoMinOrder (α ⊕ₗ β)
-- Aesop.Tracing
Aesop.TraceOption.extraction : Aesop.TraceOption
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Int.Internal.Linear.Poly.denoteExpr' : Int.Internal.Linear.Poly → Lean.Meta.Grind.GoalM Lean.Expr
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.union_congr : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ m₃ m₄ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ ∪ m₂).Equiv (m₃ ∪ m₄)
-- Mathlib.RingTheory.WittVector.Truncated
/-- The uniqueness part of the universal property of `𝕎 R`.  -/
WittVector.lift_unique : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] {S : Type u_2} [inst_2 : Semiring S]
  {f : (k : ℕ) → S →+* TruncatedWittVector p k R}
  (f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁)
  (g : S →+* WittVector p R), (∀ (k : ℕ), (WittVector.truncate k).comp g = f k) → WittVector.lift f f_compat = g
-- Lean.PrettyPrinter
Lean.PrettyPrinter.ppExpr : Lean.Expr → Lean.MetaM Std.Format
-- Mathlib.Data.Multiset.ZeroCons
Multiset.le_singleton : ∀ {α : Type u_1} {s : Multiset α} {a : α}, s ≤ {a} ↔ s = 0 ∨ s = {a}
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.instInhabited.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.Grp.instInhabited = { default := CategoryTheory.Grp.trivial C }
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_apply : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (i : n)
  (A : ↥(Subgroup.center (Matrix.SpecialLinearGroup n R))),
  (Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity' i) A = rootsOfUnity.mkOfPowEq (↑↑A i i) ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.instSmallOfLOfR : ∀ {J : CategoryTheory.Limits.MultispanShape} [Small.{t, w} J.L] [Small.{t, w'} J.R],
  Small.{t, max w' w} (CategoryTheory.Limits.WalkingMultispan J)
-- Mathlib.Data.Nat.ModEq
Nat.ModEq.add_left : ∀ {n a b : ℕ} (c : ℕ), a ≡ b [MOD n] → c + a ≡ c + b [MOD n]
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePresentation.aeval_val_equivMvPolynomial : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : StandardEtalePresentation R S) (p : Polynomial R),
  (MvPolynomial.aeval P.toPresentation.val) ((Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.C p)) =
    (Polynomial.aeval P.x) p
-- Mathlib.Data.List.Sigma
List.NodupKeys.sublist : ∀ {α : Type u} {β : α → Type v} {l₁ l₂ : List (Sigma β)}, l₁.Sublist l₂ → l₂.NodupKeys → l₁.NodupKeys
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivCommₐ_toRingEquiv : ∀ (R : Type u) {A : Type u_1} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (I J : Ideal A),
  (DoubleQuot.quotQuotEquivCommₐ R I J).toRingEquiv = DoubleQuot.quotQuotEquivComm I J
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.PosDef.prod : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] [inst_7 : PartialOrder P] [AddLeftMono P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P},
  Q₁.PosDef → Q₂.PosDef → (Q₁.prod Q₂).PosDef
-- Mathlib.Analysis.InnerProductSpace.OfNorm
_private.Mathlib.Analysis.InnerProductSpace.OfNorm.0.InnerProductSpaceable.real_prop : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [InnerProductSpaceable E] (r : ℝ), InnerProductSpaceable.innerProp'✝ E ↑r
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Complex.contDiff_sin : ∀ {n : WithTop ℕ∞}, ContDiff ℂ n Complex.sin
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSet.congr : ∀ {α : Type u_1} {m : MeasurableSpace α} {s t : Set α}, MeasurableSet s → s = t → MeasurableSet t
-- Mathlib.CategoryTheory.Sums.Products
/-- Composing the backward direction of `functorEquiv` with precomposition with `inl_ A A'`.
is naturally isomorphic to the first projection.  -/
CategoryTheory.Sum.functorEquivInverseCompWhiskeringLeftInlIso : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {A' : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] →
        {B : Type u} →
          [inst_2 : CategoryTheory.Category.{v, u} B] →
            (CategoryTheory.Sum.functorEquiv A A' B).inverse.comp
                ((CategoryTheory.Functor.whiskeringLeft A (A ⊕ A') B).obj (CategoryTheory.Sum.inl_ A A')) ≅
              CategoryTheory.Prod.fst (CategoryTheory.Functor A B) (CategoryTheory.Functor A' B)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_hom_inv_id'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ⟶ W) [inst_2 : CategoryTheory.IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) {Z_1 : C}
  (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj Z V ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom h (CategoryTheory.inv f))
        h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.CategoryStruct.id V))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom h (CategoryTheory.CategoryStruct.id V)) h_1)
-- Init.Grind.Util
/-- Gadget for marking `match`-expressions that should not be reduced by the `grind` simplifier, but the discriminants should be normalized.
We use it when adding instances of `match`-equations to prevent them from being simplified to true.

Remark: it must not be marked as `[reducible]`. Otherwise, `simp` will reduce
```
simpMatchDiscrsOnly (match 0 with | 0 => true | _ => false) = true
```
using `eq_self`.
 -/
Lean.Grind.simpMatchDiscrsOnly : {α : Sort u} → α → α
-- Mathlib.Algebra.GroupWithZero.Action.End
/-- Compose a `MulDistribMulAction` with a `MonoidHom`, with action `f r' • m`.
See note [reducible non-instances].  -/
MulDistribMulAction.compHom : {M : Type u_1} →
  {N : Type u_2} →
    (A : Type u_3) →
      [inst : Monoid A] →
        [inst_1 : Monoid M] → [MulDistribMulAction M A] → [inst_3 : Monoid N] → (N →* M) → MulDistribMulAction N A
-- Batteries.Data.List.Basic
/-- Fold a list from right to left as with `foldr`, but the combining function
also receives each element's index added to an optional parameter `start`
(i.e. the numbers that `f` takes as its first argument will be greater than or equal to `start` and
less than `start + l.length`).
 -/
List.foldrIdx : {α : Type u} → {β : Type v} → (ℕ → α → β → β) → β → List α → optParam ℕ 0 → β
-- Mathlib.Data.Sym.Card
Sym.card_sym_fin_eq_multichoose : ∀ (n k : ℕ), Fintype.card (Sym (Fin n) k) = n.multichoose k
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.evalMonoidHom_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : MulOneClass Y] (x : X)
  (x_1 : LocallyConstant X Y), (LocallyConstant.evalMonoidHom x) x_1 = x_1 x
-- Mathlib.Topology.ContinuousMap.Units
ContinuousMap.val_addUnitsLift_apply_apply : ∀ {X : Type u_1} {M : Type u_2} [inst : TopologicalSpace X] [inst_1 : AddMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : ContinuousAdd M] (f : C(X, AddUnits M)) (x : X), ↑(ContinuousMap.addUnitsLift f) x = ↑(f x)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.updateCell.induct : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α)
  (f : Std.DTreeMap.Internal.Cell α β (compare k) → Std.DTreeMap.Internal.Cell α β (compare k))
  (motive : (l : Std.DTreeMap.Internal.Impl α β) → l.Balanced → Prop),
  (∀ (hl : Std.DTreeMap.Internal.Impl.leaf.Balanced),
      (f Std.DTreeMap.Internal.Cell.empty).inner = none → motive Std.DTreeMap.Internal.Impl.leaf hl) →
    (∀ (hl : Std.DTreeMap.Internal.Impl.leaf.Balanced) (k' : α) (v' : β k'),
        (f Std.DTreeMap.Internal.Cell.empty).inner = some ⟨k', v'⟩ → motive Std.DTreeMap.Internal.Impl.leaf hl) →
      (∀ (sz : ℕ) (ky : α) (y : β ky) (l r : Std.DTreeMap.Internal.Impl α β)
          (hl : (Std.DTreeMap.Internal.Impl.inner sz ky y l r).Balanced),
          compare k ky = Ordering.lt →
            ∀ (newL : Std.DTreeMap.Internal.Impl α β) (h₁ : newL.Balanced) (h₂ : l.size - 1 ≤ newL.size)
              (h₃ : newL.size ≤ l.size + 1),
              Std.DTreeMap.Internal.Impl.updateCell k f l ⋯ =
                  { impl := newL, balanced_impl := h₁, lb_le_size_impl := h₂, size_impl_le_ub := h₃ } →
                motive l ⋯ → motive (Std.DTreeMap.Internal.Impl.inner sz ky y l r) hl) →
        (∀ (sz : ℕ) (ky : α) (y : β ky) (l r : Std.DTreeMap.Internal.Impl α β)
            (hl : (Std.DTreeMap.Internal.Impl.inner sz ky y l r).Balanced) (h : compare k ky = Ordering.eq),
            (f (Std.DTreeMap.Internal.Cell.ofEq ky y ⋯)).inner = none →
              motive (Std.DTreeMap.Internal.Impl.inner sz ky y l r) hl) →
          (∀ (sz : ℕ) (ky : α) (y : β ky) (l r : Std.DTreeMap.Internal.Impl α β)
              (hl : (Std.DTreeMap.Internal.Impl.inner sz ky y l r).Balanced) (h : compare k ky = Ordering.eq) (k' : α)
              (v' : β k'),
              (f (Std.DTreeMap.Internal.Cell.ofEq ky y ⋯)).inner = some ⟨k', v'⟩ →
                motive (Std.DTreeMap.Internal.Impl.inner sz ky y l r) hl) →
            (∀ (sz : ℕ) (ky : α) (y : β ky) (l r : Std.DTreeMap.Internal.Impl α β)
                (hl : (Std.DTreeMap.Internal.Impl.inner sz ky y l r).Balanced),
                compare k ky = Ordering.gt →
                  ∀ (newL : Std.DTreeMap.Internal.Impl α β) (h₁ : newL.Balanced) (h₂ : r.size - 1 ≤ newL.size)
                    (h₃ : newL.size ≤ r.size + 1),
                    Std.DTreeMap.Internal.Impl.updateCell k f r ⋯ =
                        { impl := newL, balanced_impl := h₁, lb_le_size_impl := h₂, size_impl_le_ub := h₃ } →
                      motive r ⋯ → motive (Std.DTreeMap.Internal.Impl.inner sz ky y l r) hl) →
              ∀ (l : Std.DTreeMap.Internal.Impl α β) (hl : l.Balanced), motive l hl
-- Init.Data.BitVec.Lemmas
BitVec.concat_xor_concat : ∀ {w : ℕ} (x y : BitVec w) (a b : Bool), x.concat a ^^^ y.concat b = (x ^^^ y).concat (a ^^ b)
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.coimIsoIm_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Arrow C),
  CategoryTheory.Abelian.coimIsoIm.hom.app X = CategoryTheory.Abelian.coimageImageComparison X.hom
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β}, (m.insert k v).contains a = (k == a || m.contains a)
-- Mathlib.Algebra.Order.Field.Power
abs_zpow : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a : α) (p : ℤ), |a ^ p| = |a| ^ p
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.Weight.instLinearMapClass : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [LieModule.LinearWeights R L M], LinearMapClass (LieModule.Weight R L M) R L R
-- Mathlib.RingTheory.ZMod.UnitsCyclic
ZMod.isCyclic_units_two : IsCyclic (ZMod 2)ˣ
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁.Hom S₂) (g : S₂.Hom S₃),
  (f.comp g).f₃ = CategoryTheory.CategoryStruct.comp f.f₃ g.f₃
-- Mathlib.Analysis.Complex.SummableUniformlyOn
SummableLocallyUniformlyOn.differentiableOn : ∀ {ι : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E]
  {f : ι → ℂ → E} {s : Set ℂ},
  IsOpen s →
    SummableLocallyUniformlyOn f s →
      (∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r) → DifferentiableOn ℂ (fun z => ∑' (n : ι), f n z) s
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.linearIsometryBoundedOfCompact_of_compact_toEquiv : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] {𝕜 : Type u_4} [inst_3 : NormedRing 𝕜] [inst_4 : Module 𝕜 E]
  [inst_5 : IsBoundedSMul 𝕜 E],
  (ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜).toEquiv = ContinuousMap.equivBoundedOfCompact α E
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.PairingCore.WeakRankFunction.mk.injEq : ∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} {α : Type v} [inst : PartialOrder α] (rank : h.ι → α)
  (lt : ∀ {x y : h.ι}, h.AncestralRel x y → h.dim x = h.dim y → rank x < rank y) (rank_1 : h.ι → α)
  (lt_1 : ∀ {x y : h.ι}, h.AncestralRel x y → h.dim x = h.dim y → rank_1 x < rank_1 y),
  ({ rank := rank, lt := lt } = { rank := rank_1, lt := lt_1 }) = (rank = rank_1)
-- Init.Data.Nat.Bitwise.Lemmas
Nat.shiftLeft_add_eq_or_of_lt : ∀ {i b : ℕ}, b < 2 ^ i → ∀ (a : ℕ), a <<< i + b = a <<< i ||| b
-- Mathlib.Topology.Order.LeftRightNhds
/-- If `a > 1`, then open intervals `(a / ε, aε)`, `1 < ε ≤ a`,
form a basis of neighborhoods of `a`.

This upper bound for `ε` guarantees that all elements of these intervals are greater than one.  -/
nhds_basis_Ioo_one_lt_of_one_lt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CommGroup α] [inst_2 : LinearOrder α] [IsOrderedMonoid α]
  [OrderTopology α] [NoMaxOrder α] {a : α},
  1 < a → (nhds a).HasBasis (fun ε => 1 < ε ∧ ε ≤ a) fun ε => Set.Ioo (a / ε) (a * ε)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeGroupBasis.injective : ∀ {ι : Type u_1} {G : Type u_3} [inst : Group G] (b : FreeGroupBasis ι G), Function.Injective ⇑b
-- Mathlib.MeasureTheory.Integral.Lebesgue.Map
/-- Generalization of `lintegral_comp` to ae-measurable functions.  -/
MeasureTheory.lintegral_comp' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {f : β → ENNReal} {g : α → β},
  AEMeasurable f (MeasureTheory.Measure.map g μ) →
    AEMeasurable g μ → MeasureTheory.lintegral μ (f ∘ g) = ∫⁻ (a : β), f a ∂MeasureTheory.Measure.map g μ