mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.coeFn_inf : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f g : MeasureTheory.Filtration ι m},
  ↑(f ⊓ g) = ↑f ⊓ ↑g
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAtOfComplement.of_opens : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_7} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_11}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} [IsManifold I n M]
  (s : TopologicalSpace.Opens M) (y : ↥s), Manifold.IsImmersionAtOfComplement PUnit.{u_15 + 1} I I n Subtype.val y
-- Mathlib.CategoryTheory.Sites.Sheafification
/-- The sheafification of a presheaf `P`, as a functor.  -/
CategoryTheory.sheafification : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (D : Type u_1) →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          [CategoryTheory.HasWeakSheafify J D] →
            CategoryTheory.Functor (CategoryTheory.Functor Cᵒᵖ D) (CategoryTheory.Functor Cᵒᵖ D)
-- Aesop.EMap
Aesop.EMap.foldl : {σ : Type} → {α : Type u_1} → σ → (σ → Lean.Expr → α → σ) → Aesop.EMap α → σ
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Subtracting the first vector passed to `oangle` from the second vector negates the sign of
the angle.  -/
Orientation.oangle_sign_sub_left_eq_neg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), (o.oangle (y - x) y).sign = -(o.oangle x y).sign
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.eraseLeft.eq_1 : ∀ {n : ℕ} (c : OrderedFinpartition (n + 1)) (hc : Set.range (c.emb 0) = {0}),
  c.eraseLeft hc =
    { length := c.length - 1,
      partSize :=
        have this := ⋯;
        fun i => c.partSize (Fin.cast this i.succ),
      partSize_pos := ⋯,
      emb := fun i j =>
        have this := ⋯;
        (c.emb (Fin.cast this i.succ) j).pred ⋯,
      emb_strictMono := ⋯, parts_strictMono := ⋯, disjoint := ⋯, cover := ⋯ }
-- Mathlib.Data.PNat.Basic
PNat.dvd_antisymm : ∀ {m n : ℕ+}, m ∣ n → n ∣ m → m = n
-- Mathlib.Topology.Constructible
/-- [Stacks Tag 09YE](https://stacks.math.columbia.edu/tag/09YE) (Extracted from the proof) -/
IsRetrocompact.preimage_of_isClosedEmbedding : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y},
  Topology.IsClosedEmbedding f → IsCompact (Set.range f)ᶜ → IsRetrocompact s → IsRetrocompact (f ⁻¹' s)
-- Mathlib.Tactic.Linarith.Datatypes
Mathlib.Tactic.Linarith.PreprocessorBase.mk.inj : ∀ {name : autoParam Lean.Name Mathlib.Tactic.Linarith.PreprocessorBase.name._autoParam} {description : String}
  {name_1 : autoParam Lean.Name Mathlib.Tactic.Linarith.PreprocessorBase.name._autoParam} {description_1 : String},
  { name := name, description := description } = { name := name_1, description := description_1 } →
    name = name_1 ∧ description = description_1
-- Mathlib.Topology.Closure
Disjoint.closure_right : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, Disjoint s t → IsOpen s → Disjoint s (closure t)
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
ModuleCat.MonoidalCategory.tensor_ext : ∀ {R : Type u} [inst : CommRing R] {M₁ M₂ M₃ : ModuleCat R}
  {f g : CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂ ⟶ M₃},
  (∀ (m : ↑M₁) (n : ↑M₂), (ModuleCat.Hom.hom f) (m ⊗ₜ[R] n) = (ModuleCat.Hom.hom g) (m ⊗ₜ[R] n)) → f = g
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.map_id : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : NonUnitalSubring R),
  NonUnitalSubring.map (NonUnitalRingHom.id R) s = s
-- Mathlib.Topology.Path
Path.refl_symm : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a : X}, (Path.refl a).symm = Path.refl a
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- `f` has the derivative `f'` at the point `x`.

That is, `f x' = f x + (x' - x) • f' + o(x' - x)` where `x'` converges to `x`.
 -/
HasDerivAt : {𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {F : Type v} →
      [inst_1 : AddCommGroup F] →
        [inst_2 : Module 𝕜 F] → [inst_3 : TopologicalSpace F] → [ContinuousSMul 𝕜 F] → (𝕜 → F) → F → 𝕜 → Prop
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.Map.PreservesLE.le_iff : ∀ {α : Type u_1} {β : Type u_2} {inst : Std.PRange.UpwardEnumerable α} {inst_1 : Std.PRange.UpwardEnumerable β}
  {inst_2 : LE α} {inst_3 : LE β} {f : Std.PRange.UpwardEnumerable.Map α β} [self : f.PreservesLE] {a b : α},
  a ≤ b ↔ f.toFun a ≤ f.toFun b
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.isCycle_swap_mul_aux₂ : ∀ {α : Type u_4} [inst : DecidableEq α] (n : ℤ) {b x : α} {f : Equiv.Perm α},
  (Equiv.swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((Equiv.swap x (f x) * f) ^ i) (f x) = b
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.apply_iUnion_le : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {μ : MeasureTheory.FiniteMeasure Ω} {f : ℕ → Set Ω},
  (Summable fun n => μ (f n)) → μ (⋃ n, f n) ≤ ∑' (n : ℕ), μ (f n)
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.insertMany : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {ρ : Type u_1}
  [inst : ForIn Id ρ ((a : α) × β a)] {l : ρ} {t : Std.DTreeMap.Raw α β cmp}, t.WF → (t.insertMany l).WF
-- Mathlib.Logic.Basic
/-- **Alias** of `Decidable.not_imp_symm`. -/
Not.decidable_imp_symm : ∀ {a b : Prop} [Decidable a], (¬a → b) → ¬b → a
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.AtomicFact.eq.injEq : ∀ (lhs rhs : ℕ) (proof : Lean.Expr) (lhs_1 rhs_1 : ℕ) (proof_1 : Lean.Expr),
  (Mathlib.Tactic.Order.AtomicFact.eq lhs rhs proof = Mathlib.Tactic.Order.AtomicFact.eq lhs_1 rhs_1 proof_1) =
    (lhs = lhs_1 ∧ rhs = rhs_1 ∧ proof = proof_1)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.TriangleMorphism.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} (hom₁ hom₁_1 : T₁.obj₁ ⟶ T₂.obj₁) (e_hom₁ : hom₁ = hom₁_1)
  (hom₂ hom₂_1 : T₁.obj₂ ⟶ T₂.obj₂) (e_hom₂ : hom₂ = hom₂_1) (hom₃ hom₃_1 : T₁.obj₃ ⟶ T₂.obj₃) (e_hom₃ : hom₃ = hom₃_1)
  (comm₁ : CategoryTheory.CategoryStruct.comp T₁.mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ T₂.mor₁)
  (comm₂ : CategoryTheory.CategoryStruct.comp T₁.mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ T₂.mor₂)
  (comm₃ :
    CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map hom₁) =
      CategoryTheory.CategoryStruct.comp hom₃ T₂.mor₃),
  { hom₁ := hom₁, hom₂ := hom₂, hom₃ := hom₃, comm₁ := comm₁, comm₂ := comm₂, comm₃ := comm₃ } =
    { hom₁ := hom₁_1, hom₂ := hom₂_1, hom₃ := hom₃_1, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.mul_add_right_right : ∀ {R : Type u_1} [inst : CommRing R] {x y : R}, IsRelPrime x y → ∀ (z : R), IsRelPrime x (z * x + y)
-- Mathlib.Analysis.InnerProductSpace.Continuous
DenseRange.eq_zero_of_inner_left : ∀ {E : Type u_4} {ι : Type u_6} (𝕜 : Type u_7) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {x : E} {f : ι → E}, DenseRange f → (∀ (i : ι), inner 𝕜 x (f i) = 0) → x = 0
-- Mathlib.Data.Finset.Max
Finset.le_min' : ∀ {α : Type u_2} [inst : LinearOrder α] (s : Finset α) (H : s.Nonempty) (x : α), (∀ y ∈ s, x ≤ y) → x ≤ s.min' H
-- Std.Data.HashSet.Lemmas
Std.HashSet.get_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α} {h_mem : k ∈ m₁ \ m₂}, (m₁ \ m₂).get k h_mem = m₁.get k ⋯
-- Init.Data.List.SplitOn.Lemmas
List.splitOnPPrepend_cons_neg : ∀ {α : Type u_1} {p : α → Bool} {a : α} {l acc : List α},
  p a = false → List.splitOnPPrepend p (a :: l) acc = List.splitOnPPrepend p l (a :: acc)
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
/-- An infinitely smooth function `f : ℝ → ℝ` such that `f x = 0` for `x ≤ 0`,
`f x = 1` for `1 ≤ x`, and `0 < f x < 1` for `0 < x < 1`.  -/
Real.smoothTransition : ℝ → ℝ
-- Mathlib.Data.EReal.Operations
EReal.sub_lt_of_lt_add : ∀ {a b c : EReal}, a < b + c → a - c < b
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.symm_mk_one : ∀ {M : Type u_1} [inst : One M], DomMulAct.mk.symm 1 = 1
-- Mathlib.Tactic.DefEqTransformations
/-- Checks if the expression is of the form `S.mk x.1 ... x.n` with `n` nonzero
and `S.mk` a structure constructor and returns `x`.
Each projection `x.i` can be either a native projection or from a projection function.

`tryWhnfR` controls whether to try applying `whnfR` to arguments when none of them
are obviously projections.

Once an obviously correct projection is found, relies on the structure eta rule in `isDefEq`.  -/
Mathlib.Tactic.etaStruct? : Lean.Expr → optParam Bool true → Lean.MetaM (Option Lean.Expr)
-- Mathlib.GroupTheory.ArchimedeanDensely
/-- Any locally finite linear group is mul-archimedean.  -/
MulArchimedean.of_locallyFiniteOrder : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [LocallyFiniteOrder G],
  MulArchimedean G
-- Mathlib.NumberTheory.PythagoreanTriples
PythagoreanTriple.isPrimitiveClassified_of_coprime : ∀ {x y z : ℤ} (h : PythagoreanTriple x y z), x.gcd y = 1 → h.IsPrimitiveClassified
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.ConstructibleSetData.map_id : ∀ {R : Type u_1} [inst : CommSemiring R] (s : PrimeSpectrum.ConstructibleSetData R),
  PrimeSpectrum.ConstructibleSetData.map (RingHom.id R) s = s
-- Lean.Meta.Sym.Arith.Poly
/-- Monomial factor applied to polynomial `p₂`.  -/
Lean.Grind.CommRing.SPolResult.m₂ : Lean.Grind.CommRing.SPolResult → Lean.Grind.CommRing.Mon
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
LinearMap.linearEquivOfInjective.congr_simp : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {V₂ : Type v'}
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [inst_5 : FiniteDimensional K V] [inst_6 : FiniteDimensional K V₂]
  (f f_1 : V →ₗ[K] V₂) (e_f : f = f_1) (hf : Function.Injective ⇑f) (hdim : Module.finrank K V = Module.finrank K V₂),
  f.linearEquivOfInjective hf hdim = f_1.linearEquivOfInjective ⋯ hdim
-- Mathlib.Algebra.Group.Hom.Defs
instInhabitedAddMonoidHom.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZeroClass N],
  instInhabitedAddMonoidHom = { default := 0 }
-- Init.Data.Option.Lemmas
Option.get_dite : ∀ {β : Type u_1} {p : Prop} {x : Decidable p} (b : p → β) (w : (if h : p then some (b h) else none).isSome = true),
  (if h : p then some (b h) else none).get w = b ⋯
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (X₂ : C₂)
  (L : (Φ.LeftResolution X₂)ᵒᵖ),
  (CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor Φ X₂).obj L = (Opposite.unop L).op
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.IsSelfAdjoint.eq_1 : ∀ {R : Type u_1} {n : Type u_11} [inst : CommRing R] [inst_1 : Fintype n] (J A₁ : Matrix n n R),
  J.IsSelfAdjoint A₁ = J.IsAdjointPair J A₁ A₁
-- Mathlib.Data.Finset.Insert
Finset.insert_inj_on : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), Set.InjOn (fun a => insert a s) (↑s)ᶜ
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.mk.injEq : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_3} [inst : Semiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] {ρ : Representation A G W} (toSubmodule : Submodule A W)
  (apply_mem_toSubmodule : ∀ (g : G) ⦃v : W⦄, v ∈ toSubmodule → (ρ g) v ∈ toSubmodule) (toSubmodule_1 : Submodule A W)
  (apply_mem_toSubmodule_1 : ∀ (g : G) ⦃v : W⦄, v ∈ toSubmodule_1 → (ρ g) v ∈ toSubmodule_1),
  ({ toSubmodule := toSubmodule, apply_mem_toSubmodule := apply_mem_toSubmodule } =
      { toSubmodule := toSubmodule_1, apply_mem_toSubmodule := apply_mem_toSubmodule_1 }) =
    (toSubmodule = toSubmodule_1)
-- Mathlib.Algebra.Polynomial.Degree.Support
Polynomial.nonempty_support_iff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.support.Nonempty ↔ p ≠ 0
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.laverage_lt_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  ∫⁻ (x : α), f x ∂μ ≠ ⊤ → ⨍⁻ (x : α), f x ∂μ < ⊤
-- Mathlib.Algebra.GCDMonoid.Basic
normalize_eq_zero : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] {x : α}, normalize x = 0 ↔ x = 0
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
Finpartition.IsEquipartition.card_interedges_sparsePairs_le' : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : DecidableEq α] {A : Finset α} {P : Finpartition A} {G : SimpleGraph α} [inst_4 : DecidableRel G.Adj]
  {ε : 𝕜},
  P.IsEquipartition →
    0 ≤ ε →
      ↑((P.sparsePairs G ε).biUnion fun x =>
              match x with
              | (U, V) => G.interedges U V).card ≤
        ε * (↑A.card + ↑P.parts.card) ^ 2
-- Init.Grind.Order
Lean.Grind.Order.le_eq_true_of_lt : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] {a b : α}, a < b → (a ≤ b) = True
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.smul_lt_const : ∀ {α : Type u_1} {K : Type u_2} {t s : K} [inst : Ring K] [inst_1 : PartialOrder K] [IsOrderedRing K]
  [inst_3 : AddCommGroup α] [inst_4 : PartialOrder α] [IsOrderedAddMonoid α] [inst_6 : Module K α]
  [IsStrictOrderedModule K α], t < s → ∀ {a : α}, 0 < a → t • a < s • a
-- Mathlib.NumberTheory.ModularForms.CongruenceSubgroups
/-- For any `g ∈ GL(2, ℚ)` and `M ≠ 0`, there exists `N` such that `g Γ(N) g⁻¹ ≤ Γ(M)`.  -/
CongruenceSubgroup.exists_Gamma_le_conj' : ∀ (g : GL (Fin 2) ℚ) (M : ℕ) [NeZero M],
  ∃ N,
    N ≠ 0 ∧
      ConjAct.toConjAct ((Matrix.GeneralLinearGroup.map (Rat.castHom ℝ)) g) •
          Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma N) ≤
        Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma M)
-- Mathlib.CategoryTheory.Filtered.Final
/-- The inclusion of the initial object is initial.  -/
CategoryTheory.Functor.initial_const_initial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsCofiltered C] [inst_3 : CategoryTheory.Limits.HasInitial D],
  ((CategoryTheory.Functor.const C).obj (⊥_ D)).Initial
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.Nonempty.eq_1 : ∀ (u : ZFSet.{u}), u.Nonempty = (↑u).Nonempty
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_pow : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (a : MvPolynomial σ R) (n : ℕ),
  (a ^ n).totalDegree ≤ n * a.totalDegree
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instSemilatticeInfOpenAddSubgroup : {G : Type u_1} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → SemilatticeInf (OpenAddSubgroup G)
-- Init.Data.List.Lemmas
/-- See also `eq_append_cons_of_mem`, which proves a stronger version
in which the initial list must not contain the element.
 -/
List.append_of_mem : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ l → ∃ s t, l = s ++ a :: t
-- Mathlib.Order.Interval.Set.Image
directedOn_ge_Icc : ∀ {α : Type u_1} [inst : Preorder α] (a b : α), DirectedOn (fun x1 x2 => x1 ≥ x2) (Set.Icc a b)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
/-- Grade involution, inverting the sign of each basis vector.  -/
CliffordAlgebra.involute : {R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] → {Q : QuadraticForm R M} → CliffordAlgebra Q →ₐ[R] CliffordAlgebra Q
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.mem_orbit_self : ∀ {M : Type u_1} {α : Type u_3} [inst : Monoid M] [inst_1 : MulAction M α] (a : α), a ∈ MulAction.orbit M a
-- Mathlib.Order.Heyting.Hom
/-- The proposition that a bi-Heyting homomorphism preserves the difference operation.  -/
BiheytingHom.map_sdiff' : ∀ {α : Type u_6} {β : Type u_7} [inst : BiheytingAlgebra α] [inst_1 : BiheytingAlgebra β] (self : BiheytingHom α β)
  (a b : α), self.toFun (a \ b) = self.toFun a \ self.toFun b
-- Std.Data.Iterators.Lemmas.Producers.Array
Array.toListRev_iterFromIdx : ∀ {β : Type w} {array : Array β} {pos : ℕ}, (array.iterFromIdx pos).toListRev = (List.drop pos array.toList).reverse
-- Mathlib.Algebra.Group.Basic
add_zsmul_add : ∀ {G : Type u_3} [inst : AddGroup G] (a b : G) (n : ℤ), n • (a + b) + a = a + n • (b + a)
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.coeff_mapAddEquiv`. -/
MonoidAlgebra.mapRangeAddEquiv_apply : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Mul M] (e : R ≃+ S)
  (x : MonoidAlgebra R M) (m : M), ((MonoidAlgebra.mapAddEquiv M e) x).coeff m = e (x.coeff m)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroMorphisms C}
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData}
  {left : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁.left h₂.left}
  {right : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁.right h₂.right}
  {left_1 : CategoryTheory.ShortComplex.LeftHomologyMapData φ h₁.left h₂.left}
  {right_1 : CategoryTheory.ShortComplex.RightHomologyMapData φ h₁.right h₂.right},
  { left := left, right := right } = { left := left_1, right := right_1 } → left = left_1 ∧ right = right_1
-- Aesop.Tracing
Aesop.withAesopTraceNode : {m : Type → Type} →
  {ε : Type} →
    [Monad m] →
      [Lean.MonadTrace m] →
        [MonadLiftT BaseIO m] →
          [Lean.MonadRef m] →
            [Lean.AddMessageContext m] →
              [Lean.MonadOptions m] →
                [Lean.MonadAlwaysExcept ε m] →
                  {α : Type} →
                    [Lean.ExceptToTraceResult ε α] →
                      Aesop.TraceOption → (Except ε α → m Lean.MessageData) → m α → optParam Bool true → m α
-- Mathlib.Data.Stream.Init
Stream'.get_tail : ∀ {α : Type u} {n : ℕ} {s : Stream' α}, s.tail.get n = s.get (n + 1)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.SelectM.State.suggestions : Lean.Meta.Grind.SelectM.State✝ → Array Lean.Meta.Tactic.TryThis.Suggestion
-- Mathlib.NumberTheory.FLT.Three
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution'.b : {K : Type u_1} →
  [inst : Field K] →
    {ζ : K} → {hζ : IsPrimitiveRoot ζ 3} → FermatLastTheoremForThreeGen.Solution'✝ hζ → NumberField.RingOfIntegers K
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_of_tmod_eq_zero : ∀ {a b : ℤ}, b.tmod a = 0 → a ∣ b
-- Mathlib.Data.Finset.Preimage
Equiv.restrictPreimageFinset_apply_coe : ∀ {α : Type u} {β : Type v} (e : α ≃ β) (s : Finset β) (a : ↥(s.preimage ⇑e ⋯)),
  ↑((e.restrictPreimageFinset s) a) = e ↑a
-- Mathlib.Analysis.MeanInequalitiesPow
Real.rpow_add_le_add_rpow : ∀ {p a b : ℝ}, 0 ≤ a → 0 ≤ b → 0 ≤ p → p ≤ 1 → (a + b) ^ p ≤ a ^ p + b ^ p
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
_private.Mathlib.CategoryTheory.Sites.Descent.Precoverage.0.CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve.fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S}
  {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S} {i : ι} {Z : C} {q : Z ⟶ X i}
  (hq :
    (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve✝ f f' i).arrows (CategoryTheory.Over.homMk q ⋯)),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve.hom✝ hq)
      (f' (CategoryTheory.Pseudofunctor.DescentData.full_pullFunctor.sieve.idx✝ hq)) =
    CategoryTheory.CategoryStruct.comp q (f i)
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_mul_right_nhdsGT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [inst_2 : PartialOrder H] [IsOrderedMonoid H]
  [ContinuousMul H] {c a : H},
  Filter.map (fun x => x * c) (nhdsWithin a (Set.Ioi a)) = nhdsWithin (a * c) (Set.Ioi (a * c))
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singleton_zero : ∀ {α : Type u_2} [inst : Zero α], {0} = 0
-- Init.Data.String.Bootstrap
String.Internal.nextWhile : String → (Char → Bool) → String.Pos.Raw → String.Pos.Raw
-- Mathlib.Topology.Algebra.InfiniteSum.Module
/-- Automorphization of a function into an `R`-`Module` distributes, that is, commutes with the
`R`-scalar multiplication.  -/
QuotientAddGroup.automorphize_smul_left : ∀ {M : Type u_11} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M] [T2Space M] {R : Type u_12}
  [inst_3 : DivisionRing R] [inst_4 : Module R M] [ContinuousConstSMul R M] {G : Type u_13} [inst_6 : AddGroup G]
  {Γ : AddSubgroup G} (f : G → M) (g : G ⧸ Γ → R),
  QuotientAddGroup.automorphize (g ∘ Quotient.mk' • f) = g • QuotientAddGroup.automorphize f
-- Mathlib.RingTheory.LocalRing.RingHom.Basic
isLocalHom_id : ∀ (R : Type u_4) [inst : Semiring R], IsLocalHom (RingHom.id R)
-- Std.Http.Server.Config
/-- Maximum number of bytes consumed while parsing request start-lines (default: 8192 bytes).
 -/
Std.Http.Config.maxStartLineLength : Std.Http.Config → ℕ
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
/-- See also `pow_left_strictMonoOn₀`.  -/
pow_left_strictMono : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftStrictMono M] [MulRightStrictMono M] {n : ℕ},
  n ≠ 0 → StrictMono fun x => x ^ n
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.copyBase.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) (g : ↥X → ↥Y) (h : ⇑f = g),
  f.copyBase g h =
    { base := TopCat.ofHom { toFun := g, continuous_toFun := ⋯ },
      c := CategoryTheory.CategoryStruct.comp f.c (TopCat.Presheaf.pushforwardEq ⋯ X.presheaf).hom, prop := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.id_tensorHom_id : ∀ {C : Type u} {X Y : CategoryTheory.FreeMonoidalCategory C},
  CategoryTheory.FreeMonoidalCategory.HomEquiv
    ((CategoryTheory.FreeMonoidalCategory.Hom.id X).tensor (CategoryTheory.FreeMonoidalCategory.Hom.id Y))
    (CategoryTheory.FreeMonoidalCategory.Hom.id (X.tensor Y))
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.WeakLimitCone.mk.injEq : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J C} (cone : CategoryTheory.Limits.Cone F)
  (isWeakLimit : CategoryTheory.Limits.IsWeakLimit cone) (cone_1 : CategoryTheory.Limits.Cone F)
  (isWeakLimit_1 : CategoryTheory.Limits.IsWeakLimit cone_1),
  ({ cone := cone, isWeakLimit := isWeakLimit } = { cone := cone_1, isWeakLimit := isWeakLimit_1 }) =
    (cone = cone_1 ∧ isWeakLimit ≍ isWeakLimit_1)
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.instIsProbabilityMeasureElemRealVolume : MeasureTheory.IsProbabilityMeasure MeasureTheory.volume
-- Mathlib.MeasureTheory.Function.JacobianOneDim
/-- Integrability in the change of variable formula for differentiable functions: if a real
function `f` is monotone and differentiable on a measurable set `s`, then a function
`g : ℝ → F` is integrable on `f '' s` if and only if `f' x • g ∘ f` is integrable on `s` .  -/
MeasureTheory.integrableOn_image_iff_integrableOn_deriv_smul_of_monotoneOn : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {s : Set ℝ} {f f' : ℝ → ℝ},
  MeasurableSet s →
    (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) →
      MonotoneOn f s →
        ∀ (g : ℝ → F),
          MeasureTheory.IntegrableOn g (f '' s) MeasureTheory.volume ↔
            MeasureTheory.IntegrableOn (fun x => f' x • g (f x)) s MeasureTheory.volume