mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Matroid.IndepAxioms
IndepMatroid.ofFinitaryCardAugment_E : ∀ {α : Type u_1} (E : Set α) (Indep : Set α → Prop) (indep_empty : Indep ∅)
  (indep_subset : ∀ ⦃I J : Set α⦄, Indep J → I ⊆ J → Indep I)
  (indep_aug :
    ∀ ⦃I J : Set α⦄, Indep I → I.Finite → Indep J → J.Finite → I.ncard < J.ncard → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I))
  (indep_compact : ∀ (I : Set α), (∀ J ⊆ I, J.Finite → Indep J) → Indep I)
  (subset_ground : ∀ (I : Set α), Indep I → I ⊆ E),
  (IndepMatroid.ofFinitaryCardAugment E Indep indep_empty indep_subset indep_aug indep_compact subset_ground).E = E
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.d_map_fourδ₄Toδ₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Category.{v_2, u_2} ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (f₃₄ : i₂ ⟶ i₄)
  (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.d_map_fourδ₄Toδ₃._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.d_map_fourδ₄Toδ₃._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.d_map_fourδ₄Toδ₃._auto_5),
  CategoryTheory.CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃)
      (X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (CategoryTheory.ComposableArrows.fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ hn₂ hn₃) =
    0
-- Mathlib.Algebra.Module.ZLattice.Summable
ZLattice.sum_piFinset_Icc_rpow_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {L : Submodule ℤ E} [inst_3 : DiscreteTopology ↥L] {ι : Type u_3} [inst_4 : Fintype ι] [inst_5 : DecidableEq ι]
  (b : Module.Basis ι ℤ ↥L) {d : ℕ},
  d = Fintype.card ι →
    ∀ (n : ℕ),
      ∀ r < -↑d,
        ∑ p ∈ Fintype.piFinset fun x => Finset.Icc (-↑n) ↑n, ‖∑ i, p i • b i‖ ^ r ≤
          2 * ↑d * 3 ^ (d - 1) * ZLattice.normBound b ^ r * ∑' (k : ℕ), ↑k ^ (↑d - 1 + r)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.eq_empty_iff_forall_not_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], m = ∅ ↔ ∀ (a : α), a ∉ m
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.aemeasurable : ∀ {α : Type u_1} {ε : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] [inst_2 : MeasurableSpace ε] [BorelSpace ε] [TopologicalSpace.PseudoMetrizableSpace ε]
  {f : α → ε}, MeasureTheory.Integrable f μ → AEMeasurable f μ
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.BoundedFormula.listEncode.match_1.eq_5 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) (x : ℕ)
  (φ : L.BoundedFormula α (x + 1)) (h_1 : (n : ℕ) → motive n FirstOrder.Language.BoundedFormula.falsum)
  (h_2 : (x : ℕ) → (t₁ t₂ : L.Term (α ⊕ Fin x)) → motive x (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (n l : ℕ) →
      (R : L.Relations l) → (ts : Fin l → L.Term (α ⊕ Fin n)) → motive n (FirstOrder.Language.BoundedFormula.rel R ts))
  (h_4 : (x : ℕ) → (φ₁ φ₂ : L.BoundedFormula α x) → motive x (φ₁.imp φ₂))
  (h_5 : (x : ℕ) → (φ : L.BoundedFormula α (x + 1)) → motive x φ.all),
  (match x, φ.all with
    | n, FirstOrder.Language.BoundedFormula.falsum => h_1 n
    | x, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 x t₁ t₂
    | n, FirstOrder.Language.BoundedFormula.rel R ts => h_3 n l R ts
    | x, φ₁.imp φ₂ => h_4 x φ₁ φ₂
    | x, φ.all => h_5 x φ) =
    h_5 x φ
-- Lean.Elab.DefView
Lean.Elab.instInhabitedDefViewElabHeaderData.default : Lean.Elab.DefViewElabHeaderData
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
/-- The morphism `mappingCone φ₁ ⟶ mappingCone φ₂` that is induced by a square that
is commutative up to homotopy.  -/
CochainComplex.mappingCone.mapOfHomotopy : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {K₁ L₁ K₂ L₂ : CochainComplex C ℤ} →
          {φ₁ : K₁ ⟶ L₁} →
            {φ₂ : K₂ ⟶ L₂} →
              {a : K₁ ⟶ K₂} →
                {b : L₁ ⟶ L₂} →
                  Homotopy (CategoryTheory.CategoryStruct.comp φ₁ b) (CategoryTheory.CategoryStruct.comp a φ₂) →
                    (CochainComplex.mappingCone φ₁ ⟶ CochainComplex.mappingCone φ₂)
-- Mathlib.Algebra.Field.Defs
/-- However `NNRat.cast` is defined, it must be equal to `a / b`.

Do not use this lemma directly. Use `NNRat.cast_def` instead.  -/
DivisionRing.nnratCast_def : ∀ {K : Type u_2} [self : DivisionRing K] (q : ℚ≥0), ↑q = ↑q.num / ↑q.den
-- Mathlib.RingTheory.LocalProperties.Exactness
LinearIndependent.of_isLocalized_maximal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5) [inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → CommSemiring (Rₚ P)]
  [inst_4 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Algebra R (Rₚ P)]
  [∀ (P : Ideal R) [inst_5 : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P]
  (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_6) [inst_6 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_7 : (P : Ideal R) → [inst_7 : P.IsMaximal] → Module R (Mₚ P)]
  [inst_8 : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)]
  [∀ (P : Ideal R) [inst_9 : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)]
  (f : (P : Ideal R) → [inst_10 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [∀ (P : Ideal R) [inst_10 : P.IsMaximal], IsLocalizedModule.AtPrime P (f P)] {ι : Type u_9} (v : ι → M),
  (∀ (P : Ideal R) [inst_11 : P.IsMaximal], LinearIndependent (Rₚ P) (⇑(f P) ∘ v)) → LinearIndependent R v
-- Mathlib.RingTheory.Localization.Defs
/-- Any localization of a commutative semiring without zero-divisors also has no zero-divisors.  -/
IsLocalization.noZeroDivisors : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] [NoZeroDivisors R], NoZeroDivisors S
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_X : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), (PowerSeries.coeff n) PowerSeries.X = if n = 1 then 1 else 0
-- Init.Data.Order.Ord
Std.OrientedCmp.not_isGE_of_gt : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α}, cmp a b = Ordering.gt → ¬(cmp b a).isGE = true
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_union_distrib_right : ∀ {α : Type u_1} [inst : DecidableEq α] (s t u : Finset α), s ∪ t ∪ u = s ∪ u ∪ (t ∪ u)
-- Mathlib.CategoryTheory.Localization.Monoidal.Braided
CategoryTheory.Localization.lift₂NatIso.eq_1 : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] (L₁ : CategoryTheory.Functor C₁ D₁)
  (L₂ : CategoryTheory.Functor C₂ D₂) (W₁ : CategoryTheory.MorphismProperty C₁)
  (W₂ : CategoryTheory.MorphismProperty C₂) [inst_5 : L₁.IsLocalization W₁] [inst_6 : L₂.IsLocalization W₂]
  [inst_7 : W₁.ContainsIdentities] [inst_8 : W₂.ContainsIdentities]
  (F₁ F₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E))
  (F₁' F₂' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E))
  [inst_9 : CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁']
  [inst_10 : CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'] (e : F₁ ≅ F₂),
  CategoryTheory.Localization.lift₂NatIso L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' e =
    { hom := CategoryTheory.Localization.lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' e.hom,
      inv := CategoryTheory.Localization.lift₂NatTrans L₁ L₂ W₁ W₂ F₂ F₁ F₂' F₁' e.inv, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }
-- Std.Time.Format.Modifier
/-- `Z`: Zone offset.
- `Z`, `ZZ`, `ZZZ`: output `±HHMMss` (no colon); parse `±HHMM[ss]`. Does **not** accept the literal `Z` character for UTC — use `ZZZZZ` or `XXX` for that.
- `ZZZZ`: outputs/parses localized GMT form (e.g., `GMT+08:00`).
- `ZZZZZ`: outputs `±HH:mm[:ss]` and uses `Z` for UTC (e.g., `Z`, `+01:30`).
 -/
Std.Time.Modifier.Z : Std.Time.OffsetZ → Std.Time.Modifier
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.map_truncatedSup : ∀ {α : Type u_1} {β : Type u_2} [inst : SemilatticeSup α] [inst_1 : SemilatticeSup β] [inst_2 : BoundedOrder β]
  [inst_3 : DecidableLE α] [inst_4 : OrderTop α] [inst_5 : DecidableLE β] (e : α ≃o β) (s : Finset α) (a : α),
  e (s.truncatedSup a) = (Finset.map e.toEmbedding s).truncatedSup (e a)
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.zero_toNat : Cardinal.toNat 0 = 0
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.one_subset : ∀ {α : Type u_2} [inst : One α] {s : Set α}, 1 ⊆ s ↔ 1 ∈ s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.ordered_keys_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp],
  List.Pairwise (fun a b => cmp a.1 b.1 = Ordering.lt) (Std.ExtDTreeMap.Const.toList t)
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the reverse direction of `upperSemicontinuousWithinAt_inv_iff`. -/
LowerSemicontinuousWithinAt.inv : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {s : Set α} {a : α} [inst_1 : PartialOrder β]
  [inst_2 : CommGroup β] [IsOrderedMonoid β], LowerSemicontinuousWithinAt f s a → UpperSemicontinuousWithinAt f⁻¹ s a
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.finSuccEquiv_X_zero : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ}, (MvPolynomial.finSuccEquiv R n) (MvPolynomial.X 0) = Polynomial.X
-- Mathlib.Algebra.Polynomial.Laurent
/-- Evaluation as an `R`-linear map.  -/
LaurentPolynomial.leval : (R : Type u_1) →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid S] → [inst_2 : Module R S] → [inst_3 : Monoid S] → Sˣ → LaurentPolynomial R →ₗ[R] S
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Justification.combine.sizeOf_spec : ∀ {s t : Lean.Omega.Constraint} {c : Lean.Omega.Coeffs} (j : Lean.Elab.Tactic.Omega.Justification s c)
  (k : Lean.Elab.Tactic.Omega.Justification t c),
  sizeOf (j.combine k) = 1 + sizeOf s + sizeOf t + sizeOf c + sizeOf j + sizeOf k
-- Mathlib.MeasureTheory.Group.AEStabilizer
MulAction.aestabilizer_empty : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {x : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : MeasureTheory.SMulInvariantMeasure G α μ], MulAction.aestabilizer G μ ∅ = ⊤
-- Mathlib.Data.Fin.Rev
Fin.cast_rev : ∀ {n m : ℕ} (i : Fin n) (h : n = m), Fin.cast h i.rev = (Fin.cast h i).rev
-- Mathlib.Data.List.Sort
/-- If `l` is already `List.Pairwise` with respect to `r`, then `insertionSort` does not change
it.  -/
List.Pairwise.insertionSort_eq : ∀ {α : Type u_1} {r : α → α → Prop} [inst : DecidableRel r] {l : List α}, List.Pairwise r l → List.insertionSort r l = l
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
/-- Formula for `ζ 1`. Note that mathematically `ζ 1` is undefined, but our construction ascribes
this particular value to it.  -/
riemannZeta_one : riemannZeta 1 = (↑Real.eulerMascheroniConstant - Complex.log (4 * ↑Real.pi)) / 2
-- Mathlib.Data.FP.Basic
FP.RMode.NE.sizeOf_spec : sizeOf FP.RMode.NE = 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF → m₂.WF → ∀ {k : α} {fallback : β}, k ∉ m₁ → Std.DTreeMap.Raw.Const.getD (m₁ ∩ m₂) k fallback = fallback
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
/-- `f : X ⟶ Y` is left homotopic to itself relative to any cylinder.  -/
HomotopicalAlgebra.Cylinder.LeftHomotopy.refl : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        (P : HomotopicalAlgebra.Cylinder X) → (f : X ⟶ Y) → P.LeftHomotopy f f
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
CategoryTheory.Bicategory.instIsIsoHomLeftZigzagHom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (η : CategoryTheory.CategoryStruct.id a ≅ CategoryTheory.CategoryStruct.comp f g)
  (ε : CategoryTheory.CategoryStruct.comp g f ≅ CategoryTheory.CategoryStruct.id b),
  CategoryTheory.IsIso (CategoryTheory.Bicategory.leftZigzag η.hom ε.hom)
-- Lean.LocalContext
Lean.LocalContext.findDecl? : {β : Type u_1} → Lean.LocalContext → (Lean.LocalDecl → Option β) → Option β
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
_private.Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite.0.CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.generator : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type v} →
      [inst_1 : CategoryTheory.SmallCategory D] →
        CategoryTheory.Functor D Cᵒᵖ →
          [inst_2 : CategoryTheory.Abelian C] → [CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] → Cᵒᵖ
-- Mathlib.SetTheory.Lists
Lists'.mem_of_subset' : ∀ {α : Type u_1} {a : Lists α} {l₁ l₂ : Lists' α true}, l₁ ⊆ l₂ → a ∈ l₁.toList → a ∈ l₂
-- Mathlib.RingTheory.Perfection
ModP.preVal_eq_zero : ∀ {K : Type u₁} [inst : Field K] {v : Valuation K NNReal} {O : Type u₂} [inst_1 : CommRing O] [inst_2 : Algebra O K],
  v.Integers O → ∀ {p : ℕ} {x : ModP O p}, ModP.preVal K v O p x = 0 ↔ x = 0
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₂_ρ_map_inv_sub_map_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G} (f : ↥(groupCohomology.cocycles₂ A))
  (g : G), (A.ρ g) (f (g⁻¹, g)) - f (g, g⁻¹) = f (1, 1) - f (g, 1)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- The image of the `plusPart` of `A` by `negAt` have all the same volume as `plusPart A`.  -/
NumberField.mixedEmbedding.volume_negAt_plusPart : ∀ {K : Type u_1} [inst : Field K] {s : Set { w // w.IsReal }} {A : Set (NumberField.mixedEmbedding.mixedSpace K)}
  [inst_1 : NumberField K],
  MeasurableSet A →
    MeasureTheory.volume (⇑(NumberField.mixedEmbedding.negAt s) '' NumberField.mixedEmbedding.plusPart A) =
      MeasureTheory.volume (NumberField.mixedEmbedding.plusPart A)
-- Mathlib.Logic.Function.Defs
Function.swap_comp_prod : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_3} (f : ι → α) (g : ι → β),
  Prod.swap ∘ Function.prod f g = Function.prod g f
-- Mathlib.Data.Finset.Defs
Finset.mem_coe : ∀ {α : Type u_1} {a : α} {s : Finset α}, a ∈ ↑s ↔ a ∈ s
-- Lean.SubExpr
Lean.SubExpr.Pos.pushAppFn : Lean.SubExpr.Pos → Lean.SubExpr.Pos
-- Mathlib.Algebra.Group.Pi.Basic
Pi.involutiveNeg.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → InvolutiveNeg (f i)],
  Pi.involutiveNeg = { toNeg := Pi.instNeg, neg_neg := ⋯ }
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.pow : Lean.Grind.CommRing.Poly → ℕ → Lean.Grind.CommRing.Poly
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod_sum : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {ι : Type u_4} {ι' : Type u_5}
  [Countable ι'] (m : ι → MeasureTheory.Measure α) (m' : ι' → MeasureTheory.Measure β)
  [∀ (n : ι'), MeasureTheory.SFinite (m' n)],
  (MeasureTheory.Measure.sum m).prod (MeasureTheory.Measure.sum m') =
    MeasureTheory.Measure.sum fun p => (m p.1).prod (m' p.2)
-- Std.Http.Data.Chunk
Std.Http.Chunk.mk.sizeOf_spec : ∀ (data : ByteArray) (extensions : Array (Std.Http.Chunk.ExtensionName × Option Std.Http.Chunk.ExtensionValue)),
  sizeOf { data := data, extensions := extensions } = 1 + sizeOf data + sizeOf extensions
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffWithinAt.congr_of_mem : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f f₁ : E → F} {x : E} {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f s x → (∀ y ∈ s, f₁ y = f y) → x ∈ s → ContDiffWithinAt 𝕜 n f₁ s x
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
isIntegral_algebraMap_iff : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Ring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B] {x : A},
  Function.Injective ⇑(algebraMap A B) → (IsIntegral R ((algebraMap A B) x) ↔ IsIntegral R x)
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.simplex_fst_le_castSucc_iff : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} (x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N) {d : ℕ}
  (hd : x.dim = d) (i : Fin (d + 1)),
  (x.cast hd).simplex.1 i ≤ k.castSucc ↔ i < SSet.prodStdSimplex.pairingCore.min x hd
-- Mathlib.Algebra.Ring.CentroidHom
Module.toCentroidHom_apply_toFun : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] {R : Type u_6} [inst_1 : CommSemiring R] [inst_2 : Module R α]
  [inst_3 : SMulCommClass R α α] [inst_4 : IsScalarTower R α α] (x : R) (a : α), (Module.toCentroidHom x) a = x • a
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.comp_hom_c_app' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : AlgebraicGeometry.SheafedSpace C} (α : X ⟶ Y)
  (β : Y ⟶ Z) (U : TopologicalSpace.Opens ↑↑Z.toPresheafedSpace),
  (CategoryTheory.CategoryStruct.comp α β).hom.c.app (Opposite.op U) =
    CategoryTheory.CategoryStruct.comp (β.hom.c.app (Opposite.op U))
      (α.hom.c.app (Opposite.op ((TopologicalSpace.Opens.map β.hom.base).obj U)))
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.IsOrtho.map : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (f : E →ₗᵢ[𝕜] F)
  {U V : Submodule 𝕜 E}, U ⟂ V → Submodule.map (↑f) U ⟂ Submodule.map (↑f) V
-- Mathlib.Order.Sublattice
Sublattice.map_bot : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β), Sublattice.map f ⊥ = ⊥
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_modifyKey_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Inhabited α] {k : α} {f : β k → β k}
  (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey! k (Std.Internal.List.modifyKey k f l) =
      if Std.Internal.List.containsKey k l = true then k else default
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsNonloop.removeLoops_isNonloop : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsNonloop e → M.removeLoops.IsNonloop e
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.UsedSimps.contains : Lean.Meta.Simp.UsedSimps → Lean.Meta.Origin → Bool
-- Mathlib.Analysis.Calculus.Gradient.Basic
inner_gradientWithin_left : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {x y : F} {s : Set F},
  inner 𝕜 (gradientWithin f s x) y = (fderivWithin 𝕜 f s x) y
-- Mathlib.Geometry.Manifold.Riemannian.Basic
norm_tangentSpace_vectorSpace : ∀ {F : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {x : F}
  {v : TangentSpace (modelWithCornersSelf ℝ F) x}, ‖v‖ = ‖v‖
-- Mathlib.CategoryTheory.Sums.Associator
/-- Further characterizing the composition of the associator and the left inclusion.  -/
CategoryTheory.sum.inlCompInlCompAssociator : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u₃) →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (CategoryTheory.Sum.inl_ C D).comp
                ((CategoryTheory.Sum.inl_ (C ⊕ D) E).comp (CategoryTheory.sum.associator C D E)) ≅
              CategoryTheory.Sum.inl_ C (D ⊕ E)
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- **Alias** of `dimH_orthogonalProjectionOnto_le`.

---

The Hausdorff dimension of the orthogonal projection of a set `s` onto a subspace `K`
is less than or equal to the Hausdorff dimension of `s`.
 -/
dimH_orthogonalProjection_le : ∀ {𝕜 : Type u_6} {E : Type u_7} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection] (s : Set E), dimH (⇑K.orthogonalProjectionOnto '' s) ≤ dimH s
-- Init.Data.Nat.Lemmas
Nat.zero_shiftRight : ∀ (n : ℕ), 0 >>> n = 0
-- Mathlib.Analysis.Normed.Group.Basic
/-- Extension for the `positivity` tactic: additive norms are always nonnegative, and positive
on non-zero inputs.  -/
Mathlib.Meta.Positivity.evalAddNorm : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- Every zero object is isomorphic to *the* zero object.  -/
CategoryTheory.Limits.IsZero.isoZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] → {X : C} → CategoryTheory.Limits.IsZero X → (X ≅ 0)
-- Mathlib.Data.Ordmap.Invariants
Ordnode.insert.eq_1 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] (x : α), Ordnode.insert x Ordnode.nil = Ordnode.singleton x
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.not_isSimplyLaced_G₂ : ¬CartanMatrix.G₂.IsSimplyLaced
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.SieveStruct.fac_assoc : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {X : C} {data : F.OneHypercoverDenseData J₀ J X} {X₀ : C₀}
  {f : F.obj X₀ ⟶ X} {Y₀ : C₀} {g : Y₀ ⟶ X₀} (self : data.SieveStruct f g) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.q (CategoryTheory.CategoryStruct.comp (data.f self.i₀) h) =
    CategoryTheory.CategoryStruct.comp (F.map g) (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.length_eq_four : ∀ {α : Type u_1} {v : FreeMonoid α},
  v.length = 4 ↔ ∃ a b c d, v = FreeMonoid.of a * FreeMonoid.of b * FreeMonoid.of c * FreeMonoid.of d
-- Lean.ReducibilityAttrs
Lean.instBEqReducibilityStatus.beq : Lean.ReducibilityStatus → Lean.ReducibilityStatus → Bool
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_ofList_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List (α × β)} {k : α} [inst_2 : Inhabited β],
  (List.map Prod.fst l).contains k = false → (Std.TreeMap.Raw.ofList l cmp)[k]! = default
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.congr'_apply_left : ∀ {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [inst : Group N₁] [inst_1 : Group G₁]
  [inst_2 : Group N₂] [inst_3 : Group G₂] {φ₁ : G₁ →* MulAut N₁} (fn : N₁ ≃* N₂) (fg : G₁ ≃* G₂) (x : N₁ ⋊[φ₁] G₁),
  ((SemidirectProduct.congr' fn fg) x).left = fn x.left
-- Mathlib.Order.Booleanisation
Booleanisation.instPartialOrder : {α : Type u_1} → [GeneralizedBooleanAlgebra α] → PartialOrder (Booleanisation α)
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.ofπ.congr_simp : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (π π_1 : (relations.G →₀ A) →ₗ[A] M) (e_π : π = π_1)
  (hπ : ∀ (r : relations.R), π (relations.relation r) = 0),
  Module.Relations.Solution.ofπ π hπ = Module.Relations.Solution.ofπ π_1 ⋯
-- Mathlib.RingTheory.AdicCompletion.Completeness
MvPowerSeries.instIsAdicCompleteSpanRangeXOfFinite : ∀ {R : Type u_1} [inst : CommRing R] {σ : Type u_3} [Finite σ],
  IsAdicComplete (Ideal.span (Set.range MvPowerSeries.X)) (MvPowerSeries σ R)