mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.PreDefinition.PartialFixpoint.Induction
/-- Unfolds a PartialOrder relation between tuples of predicates into an array of quantified implications.

This function handles mutual recursion cases where we have a tuple of predicates being compared. For each predicate in the tuple it projects out the corresponding components from both sides of the relation and unfolds the partial order relation into quantified implications using `unfoldPredRel`

Parameters:
- `eqnInfo`: Equation information containing declaration names and fixpoint types for each predicate in the mutual block
- `body`: The partial order relation expression to unfold
- `reduceConclusion`: Optional parameter (defaults to false) that determines whether to perform weak head normalization on the conclusion

Returns:
An array of expressions, where each element represents the unfolded implication for the corresponding predicate in the mutual block.
 -/
_private.Lean.Elab.PreDefinition.PartialFixpoint.Induction.0.Lean.Elab.PartialFixpoint.unfoldPredRelMutual : Lean.Elab.PartialFixpoint.EqnInfo → Lean.Expr → optParam Bool false → Lean.MetaM (Array Lean.Expr)
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.orderBot : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} → {P : Type u_2} → [inst_1 : CommRing P] → [inst_2 : Algebra R P] → OrderBot (FractionalIdeal S P)
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.postcomposeComp_hom_app_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G H : CategoryTheory.Functor J C} (α : F ⟶ G) (β : G ⟶ H) (X : CategoryTheory.Limits.Cone F),
  ((CategoryTheory.Limits.Cone.postcomposeComp α β).hom.app X).hom = CategoryTheory.CategoryStruct.id X.pt
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.mul_compat_right : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] {a b c : FreeAlgebra.Pre R X},
  FreeAlgebra.Rel R X a b → FreeAlgebra.Rel R X (c * a) (c * b)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Orientation.rotationAux.congr_simp : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o o_1 : Orientation ℝ V (Fin 2)), o = o_1 → ∀ (θ θ_1 : Real.Angle), θ = θ_1 → o.rotationAux θ = o_1.rotationAux θ_1
-- Mathlib.Tactic.TacticAnalysis
/-- `TacticInfo` at the infotree node.  -/
Mathlib.TacticAnalysis.TacticNode.tacI : Mathlib.TacticAnalysis.TacticNode → Lean.Elab.TacticInfo
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.mul'.eq_2 : ∀ (k k_1 : ℤ) (v : Lean.Grind.Linarith.Var) (p_2 : Lean.Grind.Linarith.Poly),
  (Lean.Grind.Linarith.Poly.add k_1 v p_2).mul' k = Lean.Grind.Linarith.Poly.add (k * k_1) v (p_2.mul' k)
-- Mathlib.Tactic.Linarith.Oracle.FourierMotzkin
Mathlib.Tactic.Linarith.CompSource.brecOn.eq : ∀ {motive : Mathlib.Tactic.Linarith.CompSource → Sort u} (t : Mathlib.Tactic.Linarith.CompSource)
  (F_1 : (t : Mathlib.Tactic.Linarith.CompSource) → Mathlib.Tactic.Linarith.CompSource.below t → motive t),
  Mathlib.Tactic.Linarith.CompSource.brecOn t F_1 = F_1 t (Mathlib.Tactic.Linarith.CompSource.brecOn.go t F_1).2
-- Mathlib.Analysis.Normed.Group.SeparationQuotient
SeparationQuotient.liftNormedAddGroupHomEquiv_apply : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {N : Type u_3} [inst_1 : SeminormedAddCommGroup N]
  (f : { f // ∀ (x : M), ‖x‖ = 0 → f x = 0 }),
  SeparationQuotient.liftNormedAddGroupHomEquiv f = SeparationQuotient.liftNormedAddGroupHom ↑f ⋯
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.needDisambiguation : Lean.Name → String → Bool
-- Init.Data.UInt.Bitwise
USize.or_not_self : ∀ {a : USize}, a ||| ~~~a = -1
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.MapTarget.func : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {len : ℕ} → Std.Sat.AIG.RefVec.MapTarget aig len → (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0` and `+` is an additive left cancel monoid,if it
admits an injective map that preserves `0` and `+` to an additive left cancel monoid.  -/
Function.Injective.addCancelMonoid : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₁] →
      [inst_1 : Zero M₁] →
        [inst_2 : SMul ℕ M₁] →
          [inst_3 : AddCancelMonoid M₂] →
            (f : M₁ → M₂) →
              Function.Injective f →
                f 0 = 0 →
                  (∀ (x y : M₁), f (x + y) = f x + f y) → (∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) → AddCancelMonoid M₁
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.int_odd_mul_antiperiodic : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : NonAssocRing α] [inst_1 : InvolutiveNeg β],
  Function.Antiperiodic f c → ∀ (n : ℤ), Function.Antiperiodic f (↑n * (2 * c) + c)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.HasAddFundamentalDomain.ExistsIsAddFundamentalDomain : ∀ {G : Type u_6} {α : Type u_7} {inst : Zero G} {inst_1 : VAdd G α} {inst_2 : MeasurableSpace α}
  {ν : autoParam (MeasureTheory.Measure α) MeasureTheory.HasAddFundamentalDomain._auto_1}
  [self : MeasureTheory.HasAddFundamentalDomain G α ν], ∃ s, MeasureTheory.IsAddFundamentalDomain G s ν
-- Mathlib.Combinatorics.Matroid.Circuit
/-- A version of `Matroid.indep_iff_forall_subset_not_isCircuit` that has the ground-set
hypothesis as part of the equivalence, rather than a hypothesis.  -/
Matroid.indep_iff_forall_subset_not_isCircuit' : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I ↔ (∀ C ⊆ I, ¬M.IsCircuit C) ∧ I ⊆ M.E
-- Mathlib.Algebra.Group.Hom.Basic
ZeroHom.instAdd.eq_1 : ∀ {M : Type u_2} {N : Type u_3} [inst : Zero M] [inst_1 : AddZeroClass N],
  ZeroHom.instAdd = { add := fun f g => { toFun := fun m => f m + g m, map_zero' := ⋯ } }
-- Init.Prelude
/-- Converts a list of bytes into a `ByteArray`.
 -/
List.toByteArray : List UInt8 → ByteArray
-- Init.Data.String.PosRaw
String.Pos.Raw.zero_addChar_eq : ∀ (c : Char), 0 + c = { byteIdx := c.utf8Size }
-- Init.Data.List.Lemmas
List.getLast_append_right : ∀ {α : Type u_1} {l' l : List α} (h : l' ≠ []), (l ++ l').getLast ⋯ = l'.getLast h
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `hasStrictFDerivAt_sub_const_iff`. -/
HasStrictFDerivAt.sub_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} (c : F), HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun x => f x - c) f' x
-- Init.Data.Vector.Zip
Vector.getElem?_zip_eq_some : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {as : Vector α n} {bs : Vector β n} {z : α × β} {i : ℕ},
  (as.zip bs)[i]? = some z ↔ as[i]? = some z.1 ∧ bs[i]? = some z.2
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Another, more explicit, formulation of the universal property of a colimit cocone.
See also `homIso`.  -/
CategoryTheory.Limits.IsColimit.homIso' : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cocone F} →
            CategoryTheory.Limits.IsColimit t →
              (W : C) →
                ULift.{u₁, v₃} (t.pt ⟶ W) ≅
                  { p // ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (F.map f) (p j') = p j }
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.toMulEquiv : {R : Type u} →
  [inst : CommSemiring R] →
    {A : Type v} →
      {B : Type w} →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → (A ≃ₐc[R] B) → A ≃* B
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l → ∀ {h' : k' ∈ Std.ExtTreeMap.unitOfList l cmp}, (Std.ExtTreeMap.unitOfList l cmp).getKey k' h' = k
-- Mathlib.Algebra.Algebra.Unitization
Unitization.starMap_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] [inst_7 : NonUnitalSemiring B] [inst_8 : StarRing B] [inst_9 : Module R B]
  [inst_10 : SMulCommClass R B B] [inst_11 : IsScalarTower R B B] [inst_12 : StarModule R B] (φ : A →⋆ₙₐ[R] B)
  (x : Unitization R A), (Unitization.starMap φ) x = (algebraMap R (Unitization R B)) x.toProd.1 + ↑(φ x.toProd.2)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.toSubring_bot : ∀ (A : Type u_1) [inst : CommRing A] (R : Subring A), ⊥.toSubring = R
-- Mathlib.RingTheory.SimpleModule.Isotypic
LinearEquiv.isIsotypicOfType_iff : ∀ {R : Type u_2} {M : Type u} {N : Type u_3} {S : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup S] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R S]
  (e : M ≃ₗ[R] N), IsIsotypicOfType R M S ↔ IsIsotypicOfType R N S
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.idxOfAux.eq_def : ∀ {α : Type u} [inst : BEq α] (xs : Array α) (v : α) (i : ℕ),
  xs.idxOfAux v i = if h : i < xs.size then if (xs[i] == v) = true then some ⟨i, h⟩ else xs.idxOfAux v (i + 1) else none
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- The natural group hom from a subgroup of group `G` to `G`.  -/
Subgroup.subtype : {G : Type u_1} → [inst : Group G] → (H : Subgroup G) → ↥H →* G
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.isDenseEmbedding : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  IsDenseEmbedding ⇑h
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- Makes the identity isomorphism from a proof that two submonoids of a multiplicative
monoid are equal.  -/
MulEquiv.submonoidCongr : {M : Type u_1} → [inst : MulOneClass M] → {S T : Submonoid M} → S = T → ↥S ≃* ↥T
-- Lean.Meta.Basic
/-- When `zeta := true`, then `zetaHave := false` disables zeta reduction of `have` expressions.
 -/
Lean.Meta.Config.zetaHave : Lean.Meta.Config → Bool
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insertMin!.fun_cases_unfolding : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k)
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Prop),
  motive Std.DTreeMap.Internal.Impl.leaf
      (Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf) →
    (∀ (size : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β),
        motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r')
          (Std.DTreeMap.Internal.Impl.balanceL! k' v' (Std.DTreeMap.Internal.Impl.insertMin! k v l') r')) →
      ∀ (t : Std.DTreeMap.Internal.Impl α β), motive t (Std.DTreeMap.Internal.Impl.insertMin! k v t)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- If `P' : MorphismProperty C` is satisfied whenever `P` is, then also `P'.relative` is
satisfied whenever `P.relative` is.  -/
CategoryTheory.MorphismProperty.relative_monotone : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {P P' : CategoryTheory.MorphismProperty C},
  P ≤ P' → CategoryTheory.MorphismProperty.relative F P ≤ CategoryTheory.MorphismProperty.relative F P'
-- Mathlib.Data.PNat.Interval
PNat.map_subtype_embedding_Icc : ∀ (a b : ℕ+), Finset.map (Function.Embedding.subtype fun n => 0 < n) (Finset.Icc a b) = Finset.Icc ↑a ↑b
-- Mathlib.Analysis.Convex.SpecificFunctions.Basic
/-- **Bernoulli's inequality** for real exponents, non-strict version: for `0 ≤ p ≤ 1` and `-1 ≤ s`
we have `(1 + s) ^ p ≤ 1 + p * s`.  -/
rpow_one_add_le_one_add_mul_self : ∀ {s : ℝ}, -1 ≤ s → ∀ {p : ℝ}, 0 ≤ p → p ≤ 1 → (1 + s) ^ p ≤ 1 + p * s
-- Mathlib.Data.Finset.Sups
Finset.map_infs : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β]
  [inst_2 : SemilatticeInf α] [inst_3 : SemilatticeInf β] [inst_4 : FunLike F α β] [InfHomClass F α β] (f : F)
  (hf : Function.Injective ⇑f) (s t : Finset α),
  Finset.map { toFun := ⇑f, inj' := hf } (s ⊼ t) =
    Finset.map { toFun := ⇑f, inj' := hf } s ⊼ Finset.map { toFun := ⇑f, inj' := hf } t
-- Mathlib.Geometry.Manifold.Algebra.SMul
Diffeomorph.vadd_symm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G : Type u_8} [inst_7 : TopologicalSpace G] [inst_8 : ChartedSpace H G]
  {M : Type u_9} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H' M] [inst_11 : AddGroup G]
  [inst_12 : AddAction G M] {n : WithTop ℕ∞} [inst_13 : ContMDiffVAdd I I' n G M] (g : G) (x : M),
  (Diffeomorph.vadd I I' n g).symm x = -g +ᵥ x
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- The pseudofunctor from `Cat` to `Cat` defined with `WithInitial`.  -/
CategoryTheory.WithInitial.pseudofunctor : CategoryTheory.Pseudofunctor CategoryTheory.Cat CategoryTheory.Cat
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.bounded : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  (f : BoundedContinuousFunction α β), ∃ C, ∀ (x y : α), dist (f x) (f y) ≤ C
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instIsAddApplySetENNReal : ∀ {α : Type u_1}, IsAddApply (MeasureTheory.OuterMeasure α) (Set α) ENNReal
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.smul : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {𝕜 : Type u_8} [inst_1 : NormedAddCommGroup 𝕜] [inst_2 : SMulZeroClass 𝕜 β] [IsBoundedSMul 𝕜 β] (c : 𝕜) {f : α → β},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable (c • f) μ
-- Mathlib.Algebra.DualQuaternion
Quaternion.imK_snd_dualNumberEquiv : ∀ {R : Type u_1} [inst : CommRing R] (q : Quaternion (DualNumber R)),
  (TrivSqZeroExt.snd (Quaternion.dualNumberEquiv q)).imK = TrivSqZeroExt.snd q.imK
-- Mathlib.Algebra.Group.Basic
div_inv_eq_mul : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a b : α), a / b⁻¹ = a * b
-- Mathlib.RingTheory.LinearDisjoint
/-- If a basis of `A` is also `B`-linearly independent in the opposite ring,
then `A` and `B` are linearly disjoint.  -/
Subalgebra.LinearDisjoint.of_basis_left_op : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (A B : Subalgebra R S)
  {ι : Type u_1} (a : Module.Basis ι R ↥A),
  LinearIndependent (↥B.op) (MulOpposite.op ∘ ⇑A.val ∘ ⇑a) → A.LinearDisjoint B
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.sub_eval : ∀ (l₁ l₂ : Lean.Omega.LinearCombo) (v : Lean.Omega.Coeffs), (l₁ - l₂).eval v = l₁.eval v - l₂.eval v
-- Lean.Environment
/-- The level of information to save/load. Each level includes all previous ones.  -/
Lean.OLeanLevel : Type
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the lines determined by corresponding pairs of points in two angles are parallel, twice
those angles are equal.  -/
EuclideanGeometry.two_zsmul_oangle_of_parallel : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₄ p₅ p₆ : P},
  line[ℝ, p₁, p₂].Parallel line[ℝ, p₄, p₅] →
    line[ℝ, p₃, p₂].Parallel line[ℝ, p₆, p₅] →
      2 • EuclideanGeometry.oangle p₁ p₂ p₃ = 2 • EuclideanGeometry.oangle p₄ p₅ p₆
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.norm_indicatorConstLp : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E},
  p ≠ 0 → p ≠ ⊤ → ‖MeasureTheory.indicatorConstLp p hs hμs c‖ = ‖c‖ * μ.real s ^ (1 / p.toReal)
-- Mathlib.Geometry.Euclidean.Circumcenter
_private.Mathlib.Geometry.Euclidean.Circumcenter.0.Affine.Simplex.instFintypePointsWithCircumcenterIndex.match_5.splitter : (n : ℕ) →
  (motive : Affine.Simplex.PointsWithCircumcenterIndex n → Sort u_1) →
    (x : Affine.Simplex.PointsWithCircumcenterIndex n) →
      ((a : Fin (n + 1)) → motive (Affine.Simplex.PointsWithCircumcenterIndex.pointIndex a)) →
        (Unit → motive Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex) → motive x
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.instTypeNameInteractiveMessage.unsafe_1 : TypeName Lean.Widget.InteractiveMessage
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.instCountableFormula : ∀ {L : FirstOrder.Language} {α : Type u'} [Countable α] [Countable L.Symbols], Countable (L.Formula α)
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.Subobject.Classifier.hom`.

---

The unique morphism between classifiers mapping each others characteristic maps  -/
CategoryTheory.Classifier.hom : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (𝒞₁ 𝒞₂ : CategoryTheory.Subobject.Classifier C) → 𝒞₁.Ω ⟶ 𝒞₂.Ω
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.bound_zero : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}, ProbabilityTheory.Kernel.bound 0 = 0
-- Mathlib.Computability.RegularExpressions
RegularExpression.comp_def : ∀ {α : Type u_1} (P Q : RegularExpression α), P.comp Q = P * Q
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.opComm_symm_apply_apply : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (a : Aᵐᵒᵖ ≃ₐ[R] B) (a_1 : A),
  (AlgEquiv.opComm.symm a) a_1 = MulOpposite.op (a (MulOpposite.op a_1))
-- Mathlib.Data.PFunctor.Univariate.M
_private.Mathlib.Data.PFunctor.Univariate.M.0.PFunctor.M.isubtree.match_1.eq_1 : ∀ {F : PFunctor.{u_1, u_2}} (motive : PFunctor.Approx.Path F → F.M → Sort u_3) (x : F.M) (h_1 : (x : F.M) → motive [] x)
  (h_2 : (a : F.A) → (i : F.B a) → (ps : List F.Idx) → (x : F.M) → motive (⟨a, i⟩ :: ps) x),
  (match [], x with
    | [], x => h_1 x
    | ⟨a, i⟩ :: ps, x => h_2 a i ps x) =
    h_1 x
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
AlgebraicGeometry.instLocallyQuasiFiniteCompSchemeιQuasiFiniteLocus : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.LocallyOfFiniteType f],
  AlgebraicGeometry.LocallyQuasiFinite
    (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus f).ι f)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.Iter.step_filterMapWithPostcondition.match_1.splitter : {β γ : Type u_1} →
  {n : Type u_1 → Type u_2} →
    {f : β → Std.Iterators.PostconditionT n (Option γ)} →
      (out : β) →
        (motive : Subtype (f out).Property → Sort u_3) →
          (__do_lift : Subtype (f out).Property) →
            ((h' : (f out).Property none) → motive ⟨none, h'⟩) →
              ((out' : γ) → (h' : (f out).Property (some out')) → motive ⟨some out', h'⟩) → motive __do_lift
-- Mathlib.Analysis.Convex.Join
convexJoin_mono : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s₁ s₂ t₁ t₂ : Set E}, s₁ ⊆ s₂ → t₁ ⊆ t₂ → convexJoin 𝕜 s₁ t₁ ⊆ convexJoin 𝕜 s₂ t₂
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.functorFunctor_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : C ≌ D} (α : X ⟶ Y),
  (CategoryTheory.Equivalence.functorFunctor C D).map α = CategoryTheory.Equivalence.asNatTrans α
-- Mathlib.Combinatorics.Matroid.Basic
/-- There is an infinite base  -/
Matroid.RankInfinite.exists_infinite_isBase : ∀ {α : Type u_1} {M : Matroid α} [self : M.RankInfinite], ∃ B, M.IsBase B ∧ B.Infinite
-- Mathlib.NumberTheory.ModularForms.QExpansion
SlashInvariantFormClass.eq_cuspFunction : ∀ {k : ℤ} {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} (f : F)
  [SlashInvariantFormClass F Γ k] (τ : UpperHalfPlane),
  h ∈ Γ.strictPeriods → h ≠ 0 → UpperHalfPlane.cuspFunction h (⇑f) (Function.Periodic.qParam h ↑τ) = f τ
-- Mathlib.Topology.EMetricSpace.Diam
Metric.ediam_triple : ∀ {X : Type u_2} {x y z : X} [inst : PseudoEMetricSpace X],
  Metric.ediam {x, y, z} = max (max (edist x y) (edist x z)) (edist y z)
-- Mathlib.Data.Fin.Fin2
/-- `remapLeft f k : Fin2 (m + k) → Fin2 (n + k)` applies the function
`f : Fin2 m → Fin2 n` to inputs less than `m`, and leaves the right part
on the right (that is, `remapLeft f k (m + i) = n + i`).  -/
Fin2.remapLeft : {m n : ℕ} → (Fin2 m → Fin2 n) → (k : ℕ) → Fin2 (m + k) → Fin2 (n + k)
-- Mathlib.Data.Num.Basic
ZNum.instMul : Mul ZNum
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instFromJsonShowDocumentClientCapabilities : Lean.FromJson Lean.Lsp.ShowDocumentClientCapabilities
-- Mathlib.Algebra.Notation.Support
Function.notMem_mulSupport : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] {f : ι → M} {x : ι}, x ∉ Function.mulSupport f ↔ f x = 1
-- Mathlib.RingTheory.HopfAlgebra.Basic
/-- Isolates the antipode of a Hopf algebra, to allow API to be constructed before proving the
Hopf algebra axioms. See `HopfAlgebra` for documentation.  -/
HopfAlgebraStruct : (R : Type u) → (A : Type v) → [CommSemiring R] → [Semiring A] → Type (max u v)
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- The angle ∠ABB at a point is always `π / 2`.  -/
EuclideanGeometry.angle_self_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₀ p : P), EuclideanGeometry.angle p p₀ p₀ = Real.pi / 2
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.mapAlgEquiv.eq_1 : ∀ (R : Type u_1) {A : Type u_4} {B : Type u_5} (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : AddMonoid M] (e : A ≃ₐ[R] B),
  AddMonoidAlgebra.mapAlgEquiv R M e =
    { toFun := (↑↑(AddMonoidAlgebra.mapAlgHom M ↑e).toRingHom).toFun, invFun := ⇑(AddMonoidAlgebra.mapAlgHom M ↑e.symm),
      left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
-- Mathlib.Topology.Order.Priestley
PriestleySpace.priestley : ∀ {α : Type u_2} {inst : Preorder α} {inst_1 : TopologicalSpace α} [self : PriestleySpace α] {x y : α},
  ¬x ≤ y → ∃ U, IsClopen U ∧ IsUpperSet U ∧ x ∈ U ∧ y ∉ U
-- Init.Data.Nat.Lemmas
Nat.self_sub_mod : ∀ (n k : ℕ) [NeZero k], (n - k) % n = n - k
-- Mathlib.Combinatorics.SetFamily.Compression.UV
/-- Compressing a finset doesn't change its size.  -/
UV.card_compress : ∀ {α : Type u_1} [inst : DecidableEq α] {u v : Finset α},
  u.card = v.card → ∀ (a : Finset α), (UV.compress u v a).card = a.card
-- Mathlib.Tactic.FieldSimp
_private.Mathlib.Tactic.FieldSimp.0.Mathlib.Tactic.FieldSimp.qNF.mkDivProof.eq_def : ∀ {v : Lean.Level} {M : Q(Type v)} (iM : Q(CommGroupWithZero «$M»)) (l₁ l₂ : Mathlib.Tactic.FieldSimp.qNF M),
  Mathlib.Tactic.FieldSimp.qNF.mkDivProof iM l₁ l₂ =
    match l₁, l₂ with
    | [], l =>
      have a := l.toNF;
      q(⋯)
    | l, [] =>
      have a := l.toNF;
      q(⋯)
    | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ =>
      if k₁ > k₂ then
        have pf := Mathlib.Tactic.FieldSimp.qNF.mkDivProof iM t₁ (((a₂, x₂), k₂) :: t₂);
        q(⋯)
      else
        if k₁ = k₂ then
          have pf := Mathlib.Tactic.FieldSimp.qNF.mkDivProof iM t₁ t₂;
          q(⋯)
        else
          have pf := Mathlib.Tactic.FieldSimp.qNF.mkDivProof iM (((a₁, x₁), k₁) :: t₁) t₂;
          q(⋯)