mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- The oriented angle at `p₂` between the line segments to `p₁` and `p₃`, modulo `2 * π`. If
either of those points equals `p₂`, this is 0. See `EuclideanGeometry.angle` for the
corresponding unoriented angle definition.  -/
EuclideanGeometry.oangle : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [NormedAddTorsor V P] →
            [hd2 : Fact (Module.finrank ℝ V = 2)] → [Module.Oriented ℝ V (Fin 2)] → P → P → P → Real.Angle
-- Mathlib.Data.Rat.Cast.Order
NNRat.one_le_cast : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0}, 1 ≤ ↑p ↔ 1 ≤ p
-- Std.Data.DHashMap.Raw
/-- Transforms the hash map into an array of mappings in some order.  -/
Std.DHashMap.Raw.toArray : {α : Type u} → {β : α → Type v} → Std.DHashMap.Raw α β → Array ((a : α) × β a)
-- Init.Data.List.Count
List.countP_map : ∀ {α : Type u_2} {β : Type u_1} {p : β → Bool} {f : α → β} {l : List α},
  List.countP p (List.map f l) = List.countP (p ∘ f) l
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
/-- The homogeneous submodules form a graded ring. This instance is used by `DirectSum.commSemiring`
and `DirectSum.algebra`.  -/
MvPolynomial.IsHomogeneous.HomogeneousSubmodule.gcommSemiring : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R], SetLike.GradedMonoid (MvPolynomial.homogeneousSubmodule σ R)
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.isometryEquiv_comap_mkMetric : ∀ {X : Type u_2} {Y : Type u_3} [inst : EMetricSpace X] [inst_1 : EMetricSpace Y] (m : ENNReal → ENNReal) (f : X ≃ᵢ Y),
  (MeasureTheory.OuterMeasure.comap ⇑f) (MeasureTheory.OuterMeasure.mkMetric m) = MeasureTheory.OuterMeasure.mkMetric m
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.inversion_dist_center : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (c x : P), EuclideanGeometry.inversion c (dist x c) x = x
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- Any endomorphism of a fiber functor is an isomorphism.  -/
CategoryTheory.PreGaloisCategory.FibreFunctor.end_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (f : CategoryTheory.End F), CategoryTheory.IsIso f
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.inter_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {t₃ : Std.TreeSet.Raw α cmp},
  t₁.WF → t₂.WF → t₃.WF → t₂.Equiv t₃ → (t₁ ∩ t₂).Equiv (t₁ ∩ t₃)
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curry_obj_comp_flip : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  {D : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × B) D) (G : CategoryTheory.Functor D E),
  (CategoryTheory.Functor.curry.obj (F.comp G)).flip =
    (CategoryTheory.Functor.curry.obj F).flip.comp ((CategoryTheory.Functor.whiskeringRight C D E).obj G)
-- Mathlib.Topology.ClusterPt
MapClusterPt.tendsto_comp' : ∀ {X : Type u} [inst : TopologicalSpace X] {Y : Type v} {α : Type u_1} {F : Filter α} {u : α → X} {x : X}
  [inst_1 : TopologicalSpace Y] {f : X → Y} {y : Y},
  Filter.Tendsto f (nhds x ⊓ Filter.map u F) (nhds y) → MapClusterPt x F u → MapClusterPt y F (f ∘ u)
-- Mathlib.Geometry.Euclidean.Incenter
/-- The incenter is equidistant to any two of its touchpoints.  -/
Affine.Simplex.dist_incenter_eq_dist_incenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i₁ i₂ : Fin (n + 1)),
  dist s.incenter (s.touchpoint ∅ i₁) = dist s.incenter (s.touchpoint ∅ i₂)
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMap.attachBound_apply_coe : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (f : C(X, ℝ)) (x : X), ↑(f.attachBound x) = f x
-- Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated
CategoryTheory.Pretriangulated.Opposite.mem_distinguishedTriangles_iff' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle Cᵒᵖ),
  T ∈ CategoryTheory.Pretriangulated.Opposite.distinguishedTriangles C ↔
    ∃ T',
      ∃ (_ : T' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
        Nonempty (T ≅ (CategoryTheory.Pretriangulated.triangleOpEquivalence C).functor.obj (Opposite.op T'))
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.fold_push : ∀ {α : Type u} {β : α → Type v} {l : Std.DHashMap.Raw α β} {acc : Array ((a : α) × β a)},
  Std.DHashMap.Raw.fold (fun acc k v => acc.push ⟨k, v⟩) acc l =
    acc ++ (Std.DHashMap.Internal.toListModel l.buckets).toArray
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.insert : ℤ → Lean.Grind.Linarith.Var → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly
-- Mathlib.RingTheory.Localization.Basic
Localization.mk_natCast : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (m : ℕ), Localization.mk (↑m) 1 = ↑m
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_ofList : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List (α × β)} {k : α}, k ∈ Std.ExtHashMap.ofList l ↔ (List.map Prod.fst l).contains k = true
-- Mathlib.Order.BooleanAlgebra.Set
Set.insert_sdiff_of_notMem : ∀ {α : Type u_1} {t : Set α} {a : α} (s : Set α), a ∉ t → insert a s \ t = insert a (s \ t)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.forIn_toList : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type x → Type x'} [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {γ : Type x} {it : Std.Iter β}
  {init : γ} {f : β → γ → m (ForInStep γ)}, forIn it.toList init f = forIn it init f
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.ConfigWithKey.mk : Lean.Meta.Config → UInt64 → Lean.Meta.ConfigWithKey
-- Mathlib.Data.String.Basic
String.ltb.eq_1 : ∀ (s₁ s₂ : String.Legacy.Iterator),
  String.ltb s₁ s₂ =
    if s₂.hasNext = true then
      if s₁.hasNext = true then if s₁.curr = s₂.curr then String.ltb s₁.next s₂.next else decide (s₁.curr < s₂.curr)
      else true
    else false
-- Mathlib.Order.Category.Lat
Lat.mk : (carrier : Type u_1) → [str : Lattice carrier] → Lat
-- Init.Data.Float.Float
Float.ofModel.sizeOf_spec : ∀ (toModel : Float.Model), sizeOf { toModel := toModel } = 1 + sizeOf toModel
-- Mathlib.Topology.ContinuousMap.Star
ContinuousMap.compStarAlgHom'_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (𝕜 : Type u_4)
  [inst_2 : CommSemiring 𝕜] (A : Type u_5) [inst_3 : TopologicalSpace A] [inst_4 : Semiring A]
  [inst_5 : IsTopologicalSemiring A] [inst_6 : Star A] [inst_7 : ContinuousStar A] [inst_8 : Algebra 𝕜 A] (f : C(X, Y))
  (g : C(Y, A)), (ContinuousMap.compStarAlgHom' 𝕜 A f) g = g.comp f
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.up_mk : ∀ {α : Type u_2} [inst : Add α] [inst_1 : IsRightCancelAdd α] [inst_2 : One α] (i j : α),
  i + 1 = j → (ComplexShape.up α).Rel i j
-- Mathlib.NumberTheory.Height.MvPolynomial
Height.max_mulHeightBound_zero_one_eq_one : ∀ (K : Type u_4) [inst : Field K] (ι : Type u_5) (ι' : Type u_6) [inst_1 : Height.AdmissibleAbsValues K],
  max (Height.mulHeightBound 0) 1 = 1
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingCoeff_eq_zero_iff : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R},
  m.leadingCoeff f = 0 ↔ f = 0
-- Mathlib.Algebra.Group.Defs
mul_left_injective : ∀ {G : Type u_1} [inst : Mul G] [IsRightCancelMul G] (a : G), Function.Injective fun x => x * a
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.reindex_symm : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} (eₘ : m ≃ l) (eₙ : n ≃ o),
  (Matrix.reindex eₘ eₙ).symm = Matrix.reindex eₘ.symm eₙ.symm
-- Init.Data.SInt.Lemmas
Int16.div_one : ∀ {a : Int16}, a / 1 = a
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.RepresentableBy.uniqueUpToIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor Cᵒᵖ (Type v)} {Y Y' : C}
  (e : F.RepresentableBy Y) (e' : F.RepresentableBy Y'),
  (e.uniqueUpToIso e').inv =
    CategoryTheory.Yoneda.fullyFaithful.preimage
      (CategoryTheory.NatIso.ofComponents
          (fun Z =>
            { hom := TypeCat.ofHom (⇑e'.homEquiv.symm ∘ ⇑e.homEquiv),
              inv := TypeCat.ofHom (⇑e.homEquiv.symm ∘ ⇑e'.homEquiv), hom_inv_id := ⋯, inv_hom_id := ⋯ })
          ⋯).inv
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingCoeff_leadingTerm : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (f : MvPolynomial σ R),
  m.leadingCoeff (m.leadingTerm f) = m.leadingCoeff f
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.isUnit_dblZ_of_Y_ne : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} {P Q : Fin 3 → F},
  W.Equation P → W.Equation Q → P 2 ≠ 0 → Q 2 ≠ 0 → P 0 * Q 2 = Q 0 * P 2 → P 1 * Q 2 ≠ Q 1 * P 2 → IsUnit (W.dblZ P)
-- Init.Core
/-- `Antisymm r` says that `r` is antisymmetric, that is, `r a b → r b a → a = b`.  -/
Std.Antisymm : {α : Sort u} → (α → α → Prop) → Prop
-- Mathlib.Data.Finset.Defs
Finset.subset_iff : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, s₁ ⊆ s₂ ↔ ∀ ⦃x : α⦄, x ∈ s₁ → x ∈ s₂
-- Mathlib.RingTheory.Valuation.Integral
Valuation.Integers.isIntegral_iff_v_le_one : ∀ {R : Type u} {Γ₀ : Type v} [inst : CommRing R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O R], v.Integers O → ∀ {x : R}, IsIntegral O x ↔ v x ≤ 1
-- Mathlib.RingTheory.Ideal.Over
Ideal.Quotient.algEquivOfEqMap_apply : ∀ {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  [inst_3 : Algebra A B] [inst_4 : Algebra A C] {P : Ideal B} {Q : Ideal C} (p : Ideal A) [inst_5 : Q.LiesOver p]
  [inst_6 : P.LiesOver p] {E : Type u_7} [inst_7 : EquivLike E B C] [inst_8 : AlgEquivClass E A B C] (σ : E)
  (h : Q = Ideal.map σ P) (x : B),
  (Ideal.Quotient.algEquivOfEqMap p σ h) ((Ideal.Quotient.mk P) x) = (Ideal.Quotient.mk Q) (σ x)
-- Mathlib.Data.Fin.VecNotation
Matrix.empty_vecAppend : ∀ {α : Type u} {n : ℕ} (v : Fin n → α), Matrix.vecAppend ⋯ ![] v = v
-- Mathlib.Order.Lattice.Nat
Nat.iInf_lt_succ : ∀ {α : Type u_1} [inst : CompleteLattice α] (u : ℕ → α) (n : ℕ),
  ⨅ k, ⨅ (_ : k < n + 1), u k = (⨅ k, ⨅ (_ : k < n), u k) ⊓ u n
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.instIsSMulApplySet : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {R : Type u_4} [inst_2 : Semiring R] [inst_3 : DistribMulAction R M] [inst_4 : ContinuousConstSMul R M],
  IsSMulApply R (MeasureTheory.VectorMeasure α M) (Set α) M
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ArgSpec.many : Lean.Name → Lean.Expr → Lean.Doc.ArgSpec✝
-- Mathlib.Algebra.Ring.Parity
Nat.not_even_bit1 : ∀ (n : ℕ), ¬Even (2 * n + 1)
-- Lean.Compiler.IR.Basic
Lean.IR.Decl.getInfo : Lean.IR.Decl → Lean.IR.DeclInfo
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.isoOpEquiv_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (A B : Cᵒᵖ) (f : A ≅ B),
  (CategoryTheory.isoOpEquiv A B) f = f.unop
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isLimitOfCoconeUnopOfCone_lift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) {c : CategoryTheory.Limits.Cone F}
  (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeUnopOfCone c)) (s : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.isLimitOfCoconeUnopOfCone F hc).lift s =
    (hc.desc (CategoryTheory.Limits.coconeUnopOfCone s)).op
-- Lean.Meta.Tactic.Grind.Core
/-- Removes `root` parents from the congruence table.
This is an auxiliary function performed while merging equivalence classes.
 -/
_private.Lean.Meta.Tactic.Grind.Core.0.Lean.Meta.Grind.removeParents : Lean.Expr → Lean.Meta.Grind.GoalM Lean.Meta.Grind.ParentSet
-- Mathlib.Order.SupIndep
/-- A variant of `iSupIndep_comp_coe_iff_supIndep` for `Fintype`s.  -/
iSupIndep_iff_supIndep_univ : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] [inst_1 : Fintype ι] {f : ι → α},
  iSupIndep f ↔ Finset.univ.SupIndep f
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
Std.Tactic.BVDecide.LRAT.Internal.Limplies.trans : ∀ {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [inst : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] [inst_2 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ3]
  (f1 : σ1) (f2 : σ2) (f3 : σ3),
  Std.Tactic.BVDecide.LRAT.Internal.Limplies α f1 f2 →
    Std.Tactic.BVDecide.LRAT.Internal.Limplies α f2 f3 → Std.Tactic.BVDecide.LRAT.Internal.Limplies α f1 f3
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_empty_univ : ∀ {α : Type u_4} [inst : Fintype α] [IsEmpty α] {β : α → Type u_5} {m : (α : α) → MeasurableSpace (β α)}
  (μ : (a : α) → MeasureTheory.Measure (β a)), (MeasureTheory.Measure.pi μ) Set.univ = 1
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.add : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [ContinuousAdd E] [ContinuousSMul 𝕜 E] {f₁ f₂ : α → E} {g : α → F}
  {l : Filter α}, f₁ =o[𝕜; l] g → f₂ =o[𝕜; l] g → (f₁ + f₂) =o[𝕜; l] g
-- Mathlib.CategoryTheory.Subfunctor.Finite
CategoryTheory.PresheafIsGeneratedBy.of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {ι : Type w'}
  {X : ι → Cᵒᵖ} {x : (i : ι) → F.obj (X i)},
  CategoryTheory.PresheafIsGeneratedBy F x →
    ∀ {F' : CategoryTheory.Functor Cᵒᵖ (Type w)} (f : F ⟶ F') [CategoryTheory.Epi f],
      CategoryTheory.PresheafIsGeneratedBy F' fun i => (CategoryTheory.ConcreteCategory.hom (f.app (X i))) (x i)
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
CategoryTheory.Abelian.Ext.covariant_sequence_exact₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (X : C) {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {n₀ : ℕ}
  (x₃ : CategoryTheory.Abelian.Ext X S.X₃ n₀) {n₁ : ℕ} (hn₁ : n₀ + 1 = n₁),
  x₃.comp hS.extClass hn₁ = 0 → ∃ x₂, x₂.comp (CategoryTheory.Abelian.Ext.mk₀ S.g) ⋯ = x₃
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_le_size_insertIfNew : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k : α} {v : β k}, (↑m).size ≤ (↑(m.insertIfNew k v)).size
-- Mathlib.Geometry.Manifold.Immersion
/-- Every `ModelWithCorners 𝕜 E H` is an immersion when viewed as a map `H → E`.  -/
ModelWithCorners.isImmersionOfComplement : ∀ {𝕜 : 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} {n : ℕ},
  Manifold.IsImmersionOfComplement PUnit.{u_15 + 1} I (modelWithCornersSelf 𝕜 E) ↑n ↑I
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.zero.eq_1 : ∀ {M : Type u_1} [inst : Add M] [inst_1 : Zero M] (c : AddCon M), c.zero = { zero := Quotient.mk'' 0 }
-- Mathlib.Data.Set.Function
Function.invFunOn_apply_mem : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {a : α} [inst : Nonempty α],
  a ∈ s → Function.invFunOn f s (f a) ∈ s
-- Mathlib.SetTheory.ZFC.Ordinal
/-- **Alias** of the forward direction of `ZFSet.isTransitive_iff_mem_trans`. -/
ZFSet.IsTransitive.mem_trans : ∀ {z : ZFSet.{u}}, z.IsTransitive → ∀ {x y : ZFSet.{u}}, x ∈ y → y ∈ z → x ∈ z
-- Mathlib.Data.Fintype.Defs
Finset.mem_univ : ∀ {α : Type u_1} [inst : Fintype α] (x : α), x ∈ Finset.univ
-- Mathlib.RingTheory.RingHom.Integral
RingHom.isIntegral_respectsIso : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral
-- Init.Data.SInt.Lemmas
Int32.neg_add : ∀ {a b : Int32}, -(a + b) = -a - b
-- Mathlib.Algebra.Group.Units.Hom
MonoidHom.isLocalHom_comp : ∀ {R : Type u_2} {S : Type u_3} {T : Type u_4} [inst : Monoid R] [inst_1 : Monoid S] [inst_2 : Monoid T] (g : S →* T)
  (f : R →* S) [IsLocalHom g] [IsLocalHom f], IsLocalHom (g.comp f)
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.mk.injEq : ∀ {M : Type u_10} {N : Type u_11} [inst : Add M] [inst_1 : Add N] (toFun : M → N)
  (map_add' : ∀ (x y : M), toFun (x + y) = toFun x + toFun y) (toFun_1 : M → N)
  (map_add'_1 : ∀ (x y : M), toFun_1 (x + y) = toFun_1 x + toFun_1 y),
  ({ toFun := toFun, map_add' := map_add' } = { toFun := toFun_1, map_add' := map_add'_1 }) = (toFun = toFun_1)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.IsBasis'.eRk_eq_eRk : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis' I X → M.eRk I = M.eRk X
-- Init.Data.Vector.Count
Vector.count_append : ∀ {α : Type u_1} [inst : BEq α] {n m : ℕ} {a : α} {xs : Vector α n} {ys : Vector α m},
  Vector.count a (xs ++ ys) = Vector.count a xs + Vector.count a ys
-- Mathlib.Topology.Algebra.Nonarchimedean.Bases
/-- For each set `B` in the submodule basis on `A`, there is another basis element `B'` such
that the set-theoretic product `B' * B'` is in `B`.  -/
SubmodulesRingBasis.mul : ∀ {ι : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {B : ι → Submodule R A}, SubmodulesRingBasis B → ∀ (i : ι), ∃ j, ↑(B j) * ↑(B j) ⊆ ↑(B i)
-- Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
_private.Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ.0.WeierstrassCurve.exists_variableChange_of_char_ne_two_or_three : ∀ {F : Type u_1} [inst : Field F] [IsSepClosed F] (E E' : WeierstrassCurve F) [inst_2 : E.IsElliptic]
  [inst_3 : E'.IsElliptic] {p : ℕ} [CharP F p], p ≠ 2 → p ≠ 3 → E.j = E'.j → ∃ C, C • E = E'
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.AbsolutelyContinuous.compProd_of_compProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β} [MeasureTheory.SFinite ν] [ProbabilityTheory.IsSFiniteKernel η],
  μ.AbsolutelyContinuous ν →
    (μ.compProd κ).AbsolutelyContinuous (μ.compProd η) → (μ.compProd κ).AbsolutelyContinuous (ν.compProd η)
-- Lean.Meta.Basic
/-- See `isDefEq`.  -/
Lean.Meta.isExprDefEq : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.lt_endPos_iff : ∀ {s : String.Slice} (p : s.Pos), p < s.endPos ↔ p ≠ s.endPos
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- **Alias** of `SimpleGraph.Colorable.isEmpty`.

---

**Alias** of the forward direction of `SimpleGraph.colorable_zero_iff`. -/
SimpleGraph.isEmpty_of_colorable_zero : ∀ {V : Type u} {G : SimpleGraph V}, G.Colorable 0 → IsEmpty V
-- Init.Data.List.Find
List.findSome?_replicate_of_pos : ∀ {n : ℕ} {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {a : α},
  0 < n → List.findSome? f (List.replicate n a) = f a
-- Mathlib.Data.Semiquot
/-- Extract the value from an `IsPure` semiquotient.  -/
Semiquot.get : {α : Type u_1} → (q : Semiquot α) → q.IsPure → α
-- Mathlib.Order.InitialSeg
PrincipalSeg.mk.sizeOf_spec : ∀ {α : Type u_4} {β : Type u_5} {r : α → α → Prop} {s : β → β → Prop} [inst : SizeOf α] [inst_1 : SizeOf β]
  [inst_2 : (a a_1 : α) → SizeOf (r a a_1)] [inst_3 : (a a_1 : β) → SizeOf (s a a_1)] (toRelEmbedding : r ↪r s)
  (top : β) (mem_range_iff_rel' : ∀ (b : β), b ∈ Set.range ⇑toRelEmbedding ↔ s b top),
  sizeOf { toRelEmbedding := toRelEmbedding, top := top, mem_range_iff_rel' := mem_range_iff_rel' } =
    1 + sizeOf toRelEmbedding + sizeOf top
-- Mathlib.RingTheory.PicardGroup
/-- The class group of a domain is isomorphic to the Picard group.  -/
ClassGroup.equivPic : (R : Type u_5) → [inst : CommRing R] → [inst_1 : IsDomain R] → ClassGroup R ≃* CommRing.Pic R
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k a : α} {v : β k}
  {h₁ : Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.insertIfNew! k v t) = true},
  (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).getKey a h₁ =
    if h₂ : compare k a = Ordering.eq ∧ k ∉ t then k else t.getKey a ⋯
-- Mathlib.CategoryTheory.Monoidal.Limits.Colimits
/-- The external tensor product of colimit cocones for functors `F₁ : J₁ ⥤ C`
and `F₂ : J₂ ⥤ C` is a colimit cocone when `PreservesColimit₂ F₁ F₂ (curriedTensor C)`
holds.  -/
CategoryTheory.Limits.IsColimit.tensor₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {J₁ : Type u_3} →
        {J₂ : Type u_4} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} J₁] →
            [inst_3 : CategoryTheory.Category.{v_4, u_4} J₂] →
              {F₁ : CategoryTheory.Functor J₁ C} →
                {F₂ : CategoryTheory.Functor J₂ C} →
                  {c₁ : CategoryTheory.Limits.Cocone F₁} →
                    {c₂ : CategoryTheory.Limits.Cocone F₂} →
                      [CategoryTheory.Limits.PreservesColimit₂ F₁ F₂
                            (CategoryTheory.MonoidalCategory.curriedTensor C)] →
                        CategoryTheory.Limits.IsColimit c₁ →
                          CategoryTheory.Limits.IsColimit c₂ → CategoryTheory.Limits.IsColimit (c₁.tensor₂ c₂)
-- Mathlib.RepresentationTheory.Intertwining
Representation.Equiv.mk'.congr_simp : ∀ {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} (toIntertwiningMap toIntertwiningMap_1 : ρ.IntertwiningMap σ)
  (e_toIntertwiningMap : toIntertwiningMap = toIntertwiningMap_1) (invFun invFun_1 : W → V)
  (e_invFun : invFun = invFun_1) (left_inv : Function.LeftInverse invFun toIntertwiningMap.toFun)
  (right_inv : Function.RightInverse invFun toIntertwiningMap.toFun),
  { toIntertwiningMap := toIntertwiningMap, invFun := invFun, left_inv := left_inv, right_inv := right_inv } =
    { toIntertwiningMap := toIntertwiningMap_1, invFun := invFun_1, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Topology.Algebra.Module.IsWeak
/-- Scalar multiplication in `E` is continuous when `E` is equipped with a `LinearMap.IsWeak`
topology.  -/
LinearMap.IsWeak.continuousSMul : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [hB : B.IsWeak] [ContinuousSMul 𝕜 𝕜], ContinuousSMul 𝕜 E
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α} (k_beq : (k == k') = true) {v : β k},
      List.Pairwise (fun a b => (a.fst == b.fst) = false) l → ⟨k, v⟩ ∈ l → (m.insertMany l).get? k' = some (cast ⋯ v)