mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
MeasureTheory.Measure.addHaar_singleton_add_smul_div_singleton_add_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  [FiniteDimensional ℝ E] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {r : ℝ},
  r ≠ 0 → ∀ (x y : E) (s t : Set E), μ ({x} + r • s) / μ ({y} + r • t) = μ s / μ t
-- Lean.Elab.Deriving.Basic
Lean.Elab.DerivingClassView.cls : Lean.Elab.DerivingClassView → Lean.Term
-- Mathlib.RingTheory.Derivation.Basic
Derivation.map_one_eq_zero' : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
  (self : Derivation R A M), ↑self 1 = 0
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.ext_iff : ∀ {X : Type u_4} {d₁ d₂ : DiffeologicalSpace X}, d₁ = d₂ ↔ @Diffeology.IsPlot X d₁ = @Diffeology.IsPlot X d₂
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartAlgebra.Hom.instCoeFunForall : {R : Type u_1} →
  {A₁ : Type u_2} →
    {L₁ : Type u_3} →
      {A₂ : Type u_4} →
        {L₂ : Type u_5} →
          [inst : CommRing R] →
            [inst_1 : CommRing A₁] →
              [inst_2 : LieRing L₁] →
                [inst_3 : Module A₁ L₁] →
                  [inst_4 : LieRingModule L₁ A₁] →
                    [inst_5 : CommRing A₂] →
                      [inst_6 : LieRing L₂] →
                        [inst_7 : Module A₂ L₂] →
                          [inst_8 : LieRingModule L₂ A₂] →
                            [inst_9 : Algebra R A₁] →
                              [inst_10 : LieAlgebra R L₁] →
                                [inst_11 : Algebra R A₂] →
                                  [inst_12 : LieAlgebra R L₂] →
                                    {σ₁₂ : A₁ →ₐ[R] A₂} → CoeFun (LieRinehartAlgebra.Hom σ₁₂ L₁ L₂) fun x => L₁ → L₂
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.swap_swap_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Polynomial (Polynomial R)),
  Polynomial.Bivariate.swap (Polynomial.Bivariate.swap p) = p
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_obj_fst : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  (x : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback F G X).obj S).obj x).fst =
    S.fst.obj x
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Construct a morphism between whiskered lifts.  -/
CategoryTheory.Bicategory.LeftLift.whiskerHom : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          {s t : CategoryTheory.Bicategory.LeftLift f g} → (s ⟶ t) → {x : B} → (h : x ⟶ c) → s.whisker h ⟶ t.whisker h
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.instCoeWFWFInner : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → {t : Std.DTreeMap.Raw α β cmp} → Coe t.WF t.inner.WF
-- Lean.PrettyPrinter.Formatter
/-- Registers a formatter for a parser combinator.

`@[combinator_formatter c]` registers a declaration of type `Lean.PrettyPrinter.Formatter` for the
`Parser` declaration `c`. Note that, unlike with `@[formatter]`, this is not a node kind since
combinators usually do not introduce their own node kinds. The tagged declaration may optionally
accept parameters corresponding to (a prefix of) those of `c`, where `Parser` is replaced with
`Formatter` in the parameter types.
 -/
Lean.PrettyPrinter.combinatorFormatterAttribute : Lean.ParserCompiler.CombinatorAttribute
-- Init.Data.UInt.Lemmas
UInt16.lt_or_le : ∀ (a b : UInt16), a < b ∨ b ≤ a
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Subalgebra.mk.congr_simp : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (toSubsemiring toSubsemiring_1 : Subsemiring A) (e_toSubsemiring : toSubsemiring = toSubsemiring_1)
  (algebraMap_mem' : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring.carrier),
  { toSubsemiring := toSubsemiring, algebraMap_mem' := algebraMap_mem' } =
    { toSubsemiring := toSubsemiring_1, algebraMap_mem' := ⋯ }
-- Mathlib.Algebra.Order.Hom.Monoid
map_nonpos : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Preorder α] [inst_2 : Zero α]
  [inst_3 : Preorder β] [inst_4 : Zero β] [OrderHomClass F α β] [ZeroHomClass F α β] (f : F) {a : α}, a ≤ 0 → f a ≤ 0
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing
SSet.Subcomplex.Pairing.inter : ∀ {X : SSet} {A : X.Subcomplex} (self : A.Pairing), self.I ∩ self.II = ∅
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.ofHom_apply : ∀ {X Y : Type u} (f : X → Y) (x : X), (CategoryTheory.ConcreteCategory.hom (TypeCat.ofHom f)) x = f x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_eq_none_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.maxKey? = none ↔ t.isEmpty = true
-- Mathlib.Data.Multiset.UnionInter
Multiset.inter_eq_zero_iff_disjoint : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s ∩ t = 0 ↔ Disjoint s t
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- A tensor product analogue of `mul_right_comm`.

Suppose we have a diagram of algebras `R → B ← S`,
and a `B`-module `M`, `S`-module `P`, `R`-module `Q`, then
```
(M ⊗ˢ P)      ⎛ M ⎞ ⊗ˢ P
 ⊗ᴿ       ≅ᴮ  ⎜ ⊗ᴿ⎟
 Q            ⎝ Q ⎠
```
 -/
TensorProduct.AlgebraTensorModule.rightComm : (R : Type uR) →
  (S : Type uS) →
    (B : Type uB) →
      (M : Type uM) →
        (P : Type uP) →
          (Q : Type uQ) →
            [inst : CommSemiring R] →
              [inst_1 : Semiring B] →
                [inst_2 : Algebra R B] →
                  [inst_3 : AddCommMonoid M] →
                    [inst_4 : Module R M] →
                      [inst_5 : Module B M] →
                        [inst_6 : IsScalarTower R B M] →
                          [inst_7 : AddCommMonoid P] →
                            [inst_8 : AddCommMonoid Q] →
                              [inst_9 : Module R Q] →
                                [inst_10 : CommSemiring S] →
                                  [inst_11 : Module S M] →
                                    [inst_12 : Module S P] →
                                      [inst_13 : Algebra S B] →
                                        [inst_14 : IsScalarTower S B M] →
                                          [inst_15 : SMulCommClass R S M] →
                                            [inst_16 : SMulCommClass S R M] →
                                              TensorProduct R (TensorProduct S M P) Q ≃ₗ[B]
                                                TensorProduct S (TensorProduct R M Q) P
-- Mathlib.GroupTheory.Congruence.Hom
AddCon.mapGen.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {c : AddCon M} (f : M → N),
  AddCon.mapGen f = addConGen (Relation.Map (⇑c) f f)
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.op_apply_apply : ∀ {α : Type u_7} {β : Type u_8} [inst : Add α] [inst_1 : Mul α] [inst_2 : Add β] [inst_3 : Mul β] (f : α ≃+* β)
  (a : αᵐᵒᵖ), (RingEquiv.op f) a = MulOpposite.op (f (MulOpposite.unop a))
-- Mathlib.CategoryTheory.Limits.Preserves.Grothendieck
Trans.trans.congr_simp : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {r : α → β → Sort u} {s : β → γ → Sort v} {t : α → γ → Sort w}
  [self : Trans r s t] {a : α} {b : β} {c : γ} (a_1 a_2 : r a b),
  a_1 = a_2 → ∀ (a_3 a_4 : s b c), a_3 = a_4 → Trans.trans a_1 a_3 = Trans.trans a_2 a_4
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Render the given rewrite results.  -/
Mathlib.Tactic.LibraryRewrite.renderRewrites : Lean.Expr →
  Array (Array Mathlib.Tactic.LibraryRewrite.RewriteInterface × Mathlib.Tactic.LibraryRewrite.Kind) →
    Lean.Lsp.Range → Lean.Server.FileWorker.EditableDocument → Bool → Lean.MetaM ProofWidgets.Html
-- Mathlib.Data.ZMod.Factorial
ZMod.cast_descFactorial : ∀ {n p : ℕ}, n ≤ p → ↑((p - 1).descFactorial n) = (-1) ^ n * ↑n.factorial
-- Mathlib.Algebra.Category.MonCat.Limits
/-- The forgetful functor from commutative monoids to monoids preserves all limits.

This means the underlying type of a limit can be computed as a limit in the category of monoids.  -/
CommMonCat.forget₂Mon_preservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ CommMonCat MonCat)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.all_of_get : ∀ {α : Type u} {p : α → Prop} {s : Stream'.Seq α}, (∀ (n : ℕ) (x : α), s.get? n = some x → p x) → ∀ x ∈ s, p x
-- Mathlib.FieldTheory.IsAlgClosed.Spectrum
/-- Every element `a` in a nontrivial finite-dimensional algebra `A`
over an algebraically closed field `𝕜` has non-empty spectrum.  -/
spectrum.nonempty_of_isAlgClosed_of_finiteDimensional : ∀ (𝕜 : Type u) {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [IsAlgClosed 𝕜] [Nontrivial A]
  [I : FiniteDimensional 𝕜 A] (a : A), (spectrum 𝕜 a).Nonempty
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.separableSpace_range_union_singleton : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x : MeasurableSpace α} [inst : TopologicalSpace β]
  [TopologicalSpace.PseudoMetrizableSpace β],
  MeasureTheory.StronglyMeasurable f → ∀ {b : β}, TopologicalSpace.SeparableSpace ↑(Set.range f ∪ {b})
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.notStrictValue : Lean.Parser.Parser
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_diff_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ \ t₂)[k]? = t₁[k]?
-- Mathlib.LinearAlgebra.Dimension.LinearMap
LinearMap.rank_zero : ∀ {K : Type u} {V : Type v} {V' : Type v'} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V'] [inst_4 : Module K V'] [Nontrivial K], LinearMap.rank 0 = 0
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.dirac_conv_dirac : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M] (x y : M),
  (MeasureTheory.Measure.dirac x).conv (MeasureTheory.Measure.dirac y) = MeasureTheory.Measure.dirac (x + y)
-- Mathlib.Data.Complex.Basic
Complex.zero_im : Complex.im 0 = 0
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.faithful_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat} (c : C),
  (CategoryTheory.Grothendieck.ι F c).Faithful
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_eq_some_getKey! : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {a : α}, a ∈ t → t.getKey? a = some (t.getKey! a)
-- Mathlib.Algebra.Order.Group.Synonym
toDual_one : ∀ {α : Type u_1} [inst : One α], OrderDual.toDual 1 = 1
-- Mathlib.Topology.Category.CompHaus.Basic
CompHaus.epi_iff_surjective : ∀ {X Y : CompHaus} (f : X ⟶ Y), CategoryTheory.Epi f ↔ Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Topology.ContinuousOn
continuousOn_prod_of_discrete_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [DiscreteTopology β] {f : α × β → γ} {s : Set (α × β)},
  ContinuousOn f s ↔ ∀ (b : β), ContinuousOn (fun x => f (x, b)) {a | (a, b) ∈ s}
-- Mathlib.Combinatorics.Additive.Dissociation
Finset.mulSpan.eq_1 : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : DecidableEq α] [inst_2 : Fintype α] (s : Finset α),
  s.mulSpan = Finset.image (fun ε => ∏ a ∈ s, a ^ ε a) (Fintype.piFinset fun _a => {-1, 0, 1})
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.right_inv : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} (self : ρ.Equiv σ),
  Function.RightInverse self.invFun (↑self).toFun
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.minKey?_alter_eq_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β},
  (Std.DTreeMap.Const.alter t k f).minKey? = some k ↔
    (f (Std.DTreeMap.Const.get? t k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.mul : {α : Type u} →
  [inst : Lean.Grind.Semiring α] →
    Lean.Grind.Ring.OfSemiring.Q α → Lean.Grind.Ring.OfSemiring.Q α → Lean.Grind.Ring.OfSemiring.Q α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.whiskerleft_id : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆} {A'' : Type u₇} {B'' : Type u₈}
  {C'' : Type u₉} [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  [inst_6 : CategoryTheory.Category.{v₇, u₇} A''] [inst_7 : CategoryTheory.Category.{v₈, u₈} B'']
  [inst_8 : CategoryTheory.Category.{v₉, u₉} C''] {F'' : CategoryTheory.Functor A'' B''}
  {G'' : CategoryTheory.Functor C'' B''} {ψ : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  {φ : CategoryTheory.Limits.CatCospanTransform F' G' F'' G''},
  CategoryTheory.Limits.CatCospanTransformMorphism.whiskerLeft ψ (CategoryTheory.CategoryStruct.id φ) =
    CategoryTheory.CategoryStruct.id (ψ.comp φ)
-- Init.Data.Array.Find
_private.Init.Data.Array.Find.0.Array.finIdxOf?.eq_1 : ∀ {α : Type u} [inst : BEq α] (xs : Array α) (v : α), xs.finIdxOf? v = xs.idxOfAux v 0
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.instAddCommGroupAsModule : (R : Type u_5) → [inst : CommRing R] → (M : CommRing.Pic R) → AddCommGroup M.AsModule
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.instHasInitial : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Limits.HasInitial (CategoryTheory.Mon C)
-- Aesop.RuleTac.Basic
Aesop.RuleApplication.mk.inj : ∀ {goals : Array Aesop.Subgoal} {postState : Lean.Meta.SavedState} {scriptSteps? : Option (Array Aesop.Script.LazyStep)}
  {successProbability? : Option Aesop.Percent} {goals_1 : Array Aesop.Subgoal} {postState_1 : Lean.Meta.SavedState}
  {scriptSteps?_1 : Option (Array Aesop.Script.LazyStep)} {successProbability?_1 : Option Aesop.Percent},
  { goals := goals, postState := postState, scriptSteps? := scriptSteps?, successProbability? := successProbability? } =
      { goals := goals_1, postState := postState_1, scriptSteps? := scriptSteps?_1,
        successProbability? := successProbability?_1 } →
    goals = goals_1 ∧
      postState = postState_1 ∧ scriptSteps? = scriptSteps?_1 ∧ successProbability? = successProbability?_1
-- Mathlib.Algebra.Homology.Embedding.Boundary
ComplexShape.Embedding.boundaryGE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {i' : ι'} {j : ι},
  c'.Rel i' (e.f j) → (∀ (i : ι), e.f i ≠ i') → e.BoundaryGE j
-- Mathlib.Data.Set.Operations
Set.prod_eq : ∀ {α : Type u} {β : Type v} (s : Set α) (t : Set β), s ×ˢ t = Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t
-- Mathlib.Data.Finsupp.Single
Finsupp.unique_single_eq_iff : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a a' : α} {b : M} [Unique α] {b' : M},
  ((fun₀ | a => b) = fun₀ | a' => b') ↔ b = b'
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
_private.Mathlib.Combinatorics.SimpleGraph.Triangle.Counting.0.SimpleGraph.good_vertices_triangle_card : ∀ {α : Type u_1} (G : SimpleGraph α) [inst : DecidableRel G.Adj] {ε : ℝ} {s t u : Finset α} [inst_1 : DecidableEq α],
  2 * ε ≤ ↑(G.edgeDensity s t) →
    2 * ε ≤ ↑(G.edgeDensity s u) →
      2 * ε ≤ ↑(G.edgeDensity t u) →
        G.IsUniform ε t u →
          ∀ x ∈ s \ (SimpleGraph.badVertices✝ G ε s t ∪ SimpleGraph.badVertices✝ G ε s u),
            ε ^ 3 * ↑t.card * ↑u.card ≤
              ↑(Finset.image (fun x_1 => (x, x_1))
                    ({x ∈ {y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y} |
                      match x with
                      | (y, z) => G.Adj y z})).card
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.unop_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : S.RightHomologyData), h.unop.i = h.p.unop
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instDecidableLEOpposite : {α : Type u_1} → {i : LE α} → [id : DecidableLE α] → DecidableLE α
-- Mathlib.Algebra.Category.ModuleCat.Images
ModuleCat.imageIsoRange_hom_subtype_apply : ∀ {R : Type u} [inst : Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : ↑(CategoryTheory.Limits.image f)),
  ↑((CategoryTheory.ConcreteCategory.hom (ModuleCat.imageIsoRange f).hom) x) =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.image.ι f)) x
-- Mathlib.MeasureTheory.PiSystem
isPiSystem_image_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Set α), IsPiSystem (Set.Iio '' s)
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.refl.eq_1 : ∀ (α : Type u_2) [inst : Preorder α] [inst_1 : Add α],
  OrderAddMonoidIso.refl α = { toAddEquiv := AddEquiv.refl α, map_le_map_iff' := ⋯ }
-- Init.Internal.Order.Basic
Lean.Order.prod_sup_is_sup : ∀ {α : Sort u} {β : Sort v} [inst : Lean.Order.CompleteLattice α] [inst_1 : Lean.Order.CompleteLattice β]
  (c : α ×' β → Prop), Lean.Order.is_sup c (Lean.Order.prod_sup c)
-- Mathlib.MeasureTheory.Group.Convolution
MeasureTheory.Measure.add_conv : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M] (μ ν ρ : MeasureTheory.Measure M)
  [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] [MeasureTheory.SFinite ρ], (μ + ν).conv ρ = μ.conv ρ + ν.conv ρ
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.linearEquivTuple_apply : ∀ {R : Type u_1} (a b : R) [inst : Semiring R] (z : QuadraticAlgebra R a b),
  (QuadraticAlgebra.linearEquivTuple a b) z = ![z.re, z.im]
-- Lean.Elab.InfoTree.Types
Lean.Elab.ErrorNameInfo.errorName : Lean.Elab.ErrorNameInfo → Lean.Name
-- Mathlib.LinearAlgebra.Projectivization.Action
DistribMulAction.toModuleEnd.congr_simp : ∀ (R : Type u_1) {S : Type u_3} (M : Type u_4) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass S R M],
  DistribMulAction.toModuleEnd R M = DistribMulAction.toModuleEnd R M
-- Std.Do.WP.Monad
_private.Std.Do.WP.Monad.0.ExceptT.run_bind.match_1.splitter : {ε α : Type u_1} →
  (motive : Except ε α → Sort u_2) →
    (x : Except ε α) → ((x : α) → motive (Except.ok x)) → ((e : ε) → motive (Except.error e)) → motive x
-- Init.GrindInstances.Ring.Nat
Lean.Grind.instOrderedRingNat : Lean.Grind.OrderedRing ℕ
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instCancelMonoid.eq_1 : ∀ {α : Type u_1} [inst : CancelMonoid α],
  Colex.instCancelMonoid = { toLeftCancelMonoid := Colex.instLeftCancelMonoid, toIsRightCancelMul := ⋯ }
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iter.toList.eq_1 : ∀ {α β : Type w} [inst : Std.Iterator α Id β] (it : Std.Iter β), it.toList = it.toIterM.toList.run
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.toSemiring_of : ∀ {ι : Type u_1} [inst : DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] [inst_4 : Semiring R] (f : (i : ι) → A i →+ R)
  (hone : (f 0) GradedMonoid.GOne.one = 1)
  (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj) (i : ι)
  (x : A i), (DirectSum.toSemiring f hone hmul) ((DirectSum.of A i) x) = (f i) x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_eq_false_iff_exists_contains_eq_true : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → (t.isEmpty = false ↔ ∃ a, t.contains a = true)
-- Mathlib.LinearAlgebra.Orientation
Orientation.map_refl : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (ι : Type u_4),
  Orientation.map ι (LinearEquiv.refl R M) = Equiv.refl (Orientation R M ι)
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpIndL1.congr_simp : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m m0 : MeasurableSpace α}
  (hm : m ≤ m0) (μ : MeasureTheory.Measure α) (s s_1 : Set α),
  s = s_1 →
    ∀ [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)] (x x_1 : G),
      x = x_1 → MeasureTheory.condExpIndL1 hm μ s x = MeasureTheory.condExpIndL1 hm μ s_1 x_1
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.InjectiveResolution.isoRightDerivedToHomotopyCategoryObj_inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] {X Y : C} (f : X ⟶ Y) (I : CategoryTheory.InjectiveResolution X)
  (J : CategoryTheory.InjectiveResolution Y) (φ : I.cocomplex ⟶ J.cocomplex),
  CategoryTheory.CategoryStruct.comp (I.ι.f 0) (φ.f 0) = CategoryTheory.CategoryStruct.comp f (J.ι.f 0) →
    ∀ (F : CategoryTheory.Functor C D) [inst_5 : F.Additive] {Z : HomotopyCategory D (ComplexShape.up ℕ)}
      (h : F.rightDerivedToHomotopyCategory.obj Y ⟶ Z),
      CategoryTheory.CategoryStruct.comp (I.isoRightDerivedToHomotopyCategoryObj F).inv
          (CategoryTheory.CategoryStruct.comp (F.rightDerivedToHomotopyCategory.map f) h) =
        CategoryTheory.CategoryStruct.comp
          ((HomotopyCategory.quotient D (ComplexShape.up ℕ)).map ((F.mapHomologicalComplex (ComplexShape.up ℕ)).map φ))
          (CategoryTheory.CategoryStruct.comp (J.isoRightDerivedToHomotopyCategoryObj F).inv h)
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.coprodMonad_η_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  (x : C), (CategoryTheory.coprodMonad X).η.app x = CategoryTheory.Limits.coprod.inr
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.CG.map : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N : Type u_2} [inst_1 : L.Structure N]
  (f : L.Hom M N) {s : L.Substructure M}, s.CG → (FirstOrder.Language.Substructure.map f s).CG
-- Mathlib.Data.Multiset.Powerset
/-- **Alias** of the forward direction of `Multiset.nodup_powerset`. -/
Multiset.Nodup.ofPowerset : ∀ {α : Type u_1} {s : Multiset α}, s.powerset.Nodup → s.Nodup
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- The `v`-adic absolute value is nonarchimedean  -/
NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R], IsNonarchimedean ⇑(NumberField.HeightOneSpectrum.adicAbv K v)
-- Init.Data.Nat.Basic
Nat.zero_sub_one : 0 - 1 = 0