mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Posterior
ProbabilityTheory.posterior_boolKernel_apply_true : ∀ {𝓧 : Type u_2} {m𝓧 : MeasurableSpace 𝓧} (μ ν : MeasureTheory.Measure 𝓧) [inst : MeasureTheory.IsFiniteMeasure μ]
  [inst_1 : MeasureTheory.IsFiniteMeasure ν] (π : MeasureTheory.Measure Bool)
  [inst_2 : MeasureTheory.IsFiniteMeasure π],
  ∀ᵐ (x : 𝓧) ∂π.bind ⇑(ProbabilityTheory.Kernel.boolKernel μ ν),
    ((ProbabilityTheory.posterior (ProbabilityTheory.Kernel.boolKernel μ ν) π) x) {true} =
      π {true} * ν.rnDeriv (π.bind ⇑(ProbabilityTheory.Kernel.boolKernel μ ν)) x
-- Mathlib.CategoryTheory.Monoidal.CommComon_
/-- The underlying object in the ambient monoidal category  -/
CategoryTheory.CommComon.X : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.CommComon C → C
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.ComposableArrows.isoMk₁.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 1}
  (left left_1 :
    F.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4 ≅ G.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4)
  (e_left : left = left_1)
  (right right_1 :
    F.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5 ≅ G.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5)
  (e_right : right = right_1)
  (w :
    CategoryTheory.CategoryStruct.comp
        (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5)
        right.hom =
      CategoryTheory.CategoryStruct.comp left.hom
        (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5)),
  CategoryTheory.ComposableArrows.isoMk₁ left right w = CategoryTheory.ComposableArrows.isoMk₁ left_1 right_1 ⋯
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.zero_comp : ∀ {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : TopologicalSpace β] [inst_1 : TopologicalSpace γ]
  [inst_2 : TopologicalSpace δ] [inst_3 : Zero δ] (g : CocompactMap β γ), CompactlySupportedContinuousMap.comp 0 g = 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
OrderDual.mulRightReflectLE : ∀ {α : Type u} [inst : LE α] [inst_1 : Mul α] [MulRightReflectLE α], MulRightReflectLE αᵒᵈ
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.setOfFloorPos.eq_1 : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι],
  IsProperLinearSet.setOfFloorPos✝ hs =
    {x |
      IsProperLinearSet.fract✝ hs x = IsProperLinearSet.base✝ hs ∧
        ∃ i, ↑i ∉ IsProperLinearSet.periods✝ hs ∧ 0 < IsProperLinearSet.floor✝ hs x i}
-- Mathlib.Order.Category.OmegaCompletePartialOrder
ωCPO.of.inj : ∀ {carrier : Type u} {str : OmegaCompletePartialOrder carrier} {carrier_1 : Type u}
  {str_1 : OmegaCompletePartialOrder carrier_1},
  { carrier := carrier, str := str } = { carrier := carrier_1, str := str_1 } → carrier = carrier_1 ∧ str ≍ str_1
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- `∏ x ∈ s, f x` is the product of `f x` as `x` ranges over the elements of the finite set `s`.

When the index type is a `Fintype`, the notation `∏ x, f x`, is a shorthand for
`∏ x ∈ Finset.univ, f x`.  -/
Finset.prod : {ι : Type u_1} → {M : Type u_3} → [CommMonoid M] → Finset ι → (ι → M) → M
-- Aesop.Rule.Name
_private.Aesop.Rule.Name.0.Aesop.RuleName.Json.phase : Aesop.RuleName.Json✝ → Aesop.PhaseName
-- Mathlib.Data.List.Rotate
List.IsRotated.cons_getLast_dropLast : ∀ {α : Type u} (L : List α) (hL : L ≠ []), L.getLast hL :: L.dropLast ~r L
-- Mathlib.Topology.Order.Monotone
MonotoneOn.tendsto_nhdsLT : ∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α},
  MonotoneOn f (Set.Iio x) →
    BddAbove (f '' Set.Iio x) → Filter.Tendsto f (nhdsWithin x (Set.Iio x)) (nhds (sSup (f '' Set.Iio x)))
-- Mathlib.Util.GetAllModules
/-- Like `getAllFiles`, but return an array of *module* names instead,
i.e. names of the form `Mathlib/Algebra/Algebra/Basic.lean`.
In addition, these names are sorted in a platform-independent order.  -/
getAllModulesSorted : Bool → String → IO (Array String)
-- Mathlib.Control.Bifunctor
Sum.lawfulBifunctor : LawfulBifunctor Sum
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.comap_normalClosure : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (s : Set N) (f : G ≃+ N),
  AddSubgroup.normalClosure (⇑f ⁻¹' s) = AddSubgroup.comap (↑f) (AddSubgroup.normalClosure s)
-- Std.Data.DHashMap.Lemmas
_private.Std.Data.DHashMap.Lemmas.0.Std.DHashMap.insert.eq_1 : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} (m : Std.DHashMap α β) (a : α) (b : β a),
  m.insert a b = { inner := ↑(Std.DHashMap.Internal.Raw₀.insert ⟨m.inner, ⋯⟩ a b), wf := ⋯ }
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.inclHomEquiv_apply_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) (Y : CategoryTheory.Limits.FormalCoproduct C)
  (f : (CategoryTheory.Limits.FormalCoproduct.incl C).obj X ⟶ Y),
  ((CategoryTheory.Limits.FormalCoproduct.inclHomEquiv X Y) f).snd = f.φ PUnit.unit
-- Lean.PrettyPrinter
/-- Pretty print a const expression using `delabConst` and generate terminfo.
This function avoids inserting `@` if the constant is for a function whose first
argument is implicit, which is what the default `toMessageData` for `Expr` does.
Panics if `e` is not a constant.
 -/
Lean.MessageData.ofConst : Lean.Expr → Lean.MessageData
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix'_comp : ∀ {R : Type u_1} [inst : CommSemiring R] {l : Type u_3} {m : Type u_4} {n : Type u_5} [inst_1 : DecidableEq n]
  [inst_2 : Fintype n] [inst_3 : Fintype l] [inst_4 : DecidableEq l] (f : (n → R) →ₗ[R] m → R)
  (g : (l → R) →ₗ[R] n → R), LinearMap.toMatrix' (f ∘ₗ g) = LinearMap.toMatrix' f * LinearMap.toMatrix' g
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring
HomogeneousSubsemiring.mk.congr_simp : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : AddMonoid ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_4 : DecidableEq ι] [inst_5 : GradedRing 𝒜]
  (toSubsemiring toSubsemiring_1 : Subsemiring A) (e_toSubsemiring : toSubsemiring = toSubsemiring_1)
  (is_homogeneous' : DirectSum.SetLike.IsHomogeneous 𝒜 toSubsemiring),
  { toSubsemiring := toSubsemiring, is_homogeneous' := is_homogeneous' } =
    { toSubsemiring := toSubsemiring_1, is_homogeneous' := ⋯ }
-- Std.Data.ExtHashMap.Basic
/-- Creates a new empty hash map. The optional parameter `capacity` can be supplied to presize the
map so that it can hold the given number of mappings without reallocating. It is also possible to
use the empty collection notations `∅` and `{}` to create an empty hash map with the default
capacity.
 -/
Std.ExtHashMap.emptyWithCapacity : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → optParam ℕ 8 → Std.ExtHashMap α β
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ωScottContinuous.apply : ∀ {α : Type u_2} {β : α → Type u_6} [inst : (x : α) → OmegaCompletePartialOrder (β x)] (x : α),
  OmegaCompletePartialOrder.ωScottContinuous fun f => f x
-- Lean.DocString.Add
/-- Parses and elaborates a Verso module docstring.
 -/
Lean.versoModDocString : Lean.DeclarationRange →
  Lean.TSyntax `Lean.Doc.Parser.document →
    Lean.Elab.TermElabM (Lean.VersoModuleDocs.Snippet × Array Lean.Doc.DeferredCheck)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_eq_get_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {a : α} {h' : a ∈ t}, t.getKey a h' = (t.getKey? a).get ⋯
-- Std.Data.DHashMap.Basic
/-- Inserts multiple keys with the value `()` into the hash map by iterating over the given collection
and calling `insertIfNew`. If the same key appears multiple times, the first occurrence takes
precedence.

This is mainly useful to implement `HashSet.insertMany`, so if you are considering using this,
`HashSet` or `HashSet.Raw` might be a better fit for you.
 -/
Std.DHashMap.Const.insertManyIfNewUnit : {α : Type u} →
  {x : BEq α} →
    {x_1 : Hashable α} →
      {ρ : Type w} → [ForIn Id ρ α] → (Std.DHashMap α fun x => Unit) → ρ → Std.DHashMap α fun x => Unit
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.Away.eventually_smul_mem : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ} [GradedRing 𝒜] {f : A}
  {m : ι},
  f ∈ 𝒜 m →
    ∀ (z : HomogeneousLocalization.Away 𝒜 f),
      ∀ᶠ (n : ℕ) in Filter.atTop,
        f ^ n • HomogeneousLocalization.val z ∈ ⇑(algebraMap A (Localization (Submonoid.powers f))) '' ↑(𝒜 (n • m))
-- Mathlib.Analysis.LocallyConvex.Polar
/-- **Alias** of `StrongDual.polarSubmodule_eq_setOfPred`. -/
StrongDual.polarSubmodule_eq_setOf : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] {E : Type u_5} [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] {S : Type u_6} [inst_4 : SetLike S E]
  [inst_5 : SMulMemClass S 𝕜 E] (m : S), ↑(StrongDual.polarSubmodule 𝕜 m) = {y | ∀ x ∈ m, y x = 0}
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.equiv_of_beq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [LawfulBEq α],
  m₁.WF → m₂.WF → (m₁ == m₂) = true → m₁.Equiv m₂
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
IsAddUnit.sum_iff : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : AddCommMonoid M] {f : ι → M},
  IsAddUnit (∑ a ∈ s, f a) ↔ ∀ a ∈ s, IsAddUnit (f a)
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.leftDualIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X₁ X₂ Y : C}
  (p₁ : CategoryTheory.ExactPairing X₁ Y) (p₂ : CategoryTheory.ExactPairing X₂ Y),
  CategoryTheory.leftDualIso p₁ p₂ =
    { hom := ᘁCategoryTheory.CategoryStruct.id Y, inv := ᘁCategoryTheory.CategoryStruct.id Y, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.comp_τ₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : S₁ ⟶ S₂) (φ₂₃ : S₂ ⟶ S₃) {Z : C} (h : S₃.X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp φ₁₂ φ₂₃).τ₁ h =
    CategoryTheory.CategoryStruct.comp φ₁₂.τ₁ (CategoryTheory.CategoryStruct.comp φ₂₃.τ₁ h)
-- Mathlib.Order.Filter.Defs
/-- A function `f` is eventually less than or equal to a function `g` at a filter `l`.  -/
Filter.EventuallyLE : {α : Type u_1} → {β : Type u_2} → [LE β] → Filter α → (α → β) → (α → β) → Prop
-- Lean.ExtraModUses
Lean.instHashableExtraModUse.hash : Lean.ExtraModUse → UInt64
-- Mathlib.Topology.Algebra.OpenSubgroup
/-- Reinterpret an `OpenAddSubgroup` as an `AddSubgroup`.  -/
OpenAddSubgroup.toAddSubgroup : {G : Type u_1} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → OpenAddSubgroup G → AddSubgroup G
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.not_step_singleton : ∀ {α : Type u} {L : List (α × Bool)} {p : α × Bool}, ¬FreeAddGroup.Red.Step [p] L
-- Mathlib.Topology.Algebra.Module.Basic
continuousSMul_induced : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : SMul R M₁] [inst_1 : SMul R M₂] [u : TopologicalSpace R]
  {t : TopologicalSpace M₂} [ContinuousSMul R M₂] {F : Type u_6} [inst_3 : FunLike F M₁ M₂]
  [MulActionHomClass F R M₁ M₂] (f : F), ContinuousSMul R M₁
-- Batteries.Data.Fin.Lemmas
Fin.isNone_findSome?_iff : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Option α}, (Fin.findSome? f).isNone = true ↔ ∀ (i : Fin n), (f i).isNone = true
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.ext_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {e₁ e₂ : α ≃ᵐ β},
  e₁ = e₂ ↔ ⇑e₁ = ⇑e₂
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
/-- Characterization of desirable equivalence relations on M-types  -/
MvQPF.IsPrecongr : {n : ℕ} →
  {F : TypeVec.{u} (n + 1) → Type u} →
    [q : MvQPF F] → {α : TypeVec.{u} n} → ((MvQPF.P F).M α → (MvQPF.P F).M α → Prop) → Prop
-- Init.Prelude
/-- The number of distinct values representable by `USize`, that is, `2^System.Platform.numBits`.  -/
USize.size : ℕ
-- Mathlib.Topology.Separation.Regular
instT3SpaceForall : ∀ {ι : Type u_3} {X : ι → Type u_4} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), T3Space (X i)],
  T3Space ((i : ι) → X i)
-- Mathlib.Data.Finset.NAry
Finset.image₂_singleton : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] {f : α → β → γ} {a : α} {b : β},
  Finset.image₂ f {a} {b} = {f a b}
-- Mathlib.LinearAlgebra.RootSystem.Reduced
RootPairing.pairingIn_neg_two_neg_two_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_5)
  (i j : ι) [Finite ι] [CharZero R] [IsDomain R] [Module.IsTorsionFree R M] [inst_9 : CommRing S]
  [inst_10 : Algebra S R] [FaithfulSMul S R] [inst_12 : P.IsValuedIn S],
  P.pairingIn S i j = -2 ∧ P.pairingIn S j i = -2 ↔ P.root i = -P.root j
-- Mathlib.Analysis.Analytic.Inverse
_private.Mathlib.Analysis.Analytic.Inverse.0.FormalMultilinearSeries.leftInv.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (n : ℕ) → motive n.succ.succ),
  (match 1 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | n.succ.succ => h_3 n) =
    h_2 ()
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prev_le : ∀ {s : String.Slice} {p : s.Pos} {h : p ≠ s.startPos}, p.prev h ≤ p
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.of_subsingleton_codomain : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε' : Type u_8} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddMonoid ε'] [Subsingleton ε'] {f : α → ε'}, MeasureTheory.Integrable f μ
-- Init.Data.UInt.Bitwise
UInt64.toBitVec_shiftLeft : ∀ (a b : UInt64), (a <<< b).toBitVec = a.toBitVec <<< (b.toBitVec % 64)
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Real.differentiableOn_rpow_const : ∀ (p : ℝ), DifferentiableOn ℝ (fun x => x ^ p) {0}ᶜ
-- Init.Data.Slice.Array.Lemmas
Array.size_mkSlice_rci : ∀ {α : Type u_1} {xs : Array α} {lo : ℕ}, Std.Slice.size (Std.Rci.Sliceable.mkSlice xs lo...*) = xs.size - lo
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.algEquivOfAlgEquiv_apply : ∀ {A : Type u_4} [inst : CommSemiring A] {R : Type u_5} [inst_1 : CommSemiring R] [inst_2 : Algebra A R]
  {M : Submonoid R} (S : Type u_6) [inst_3 : CommSemiring S] [inst_4 : Algebra A S] [inst_5 : Algebra R S]
  [inst_6 : IsScalarTower A R S] [inst_7 : IsLocalization M S] {P : Type u_7} [inst_8 : CommSemiring P]
  [inst_9 : Algebra A P] {T : Submonoid P} (Q : Type u_8) [inst_10 : CommSemiring Q] [inst_11 : Algebra A Q]
  [inst_12 : Algebra P Q] [inst_13 : IsScalarTower A P Q] [inst_14 : IsLocalization T Q] (h : R ≃ₐ[A] P)
  (H : Submonoid.map h M = T) (a : S), (IsLocalization.algEquivOfAlgEquiv S Q h H) a = (IsLocalization.map Q ↑h ⋯) a
-- Mathlib.FieldTheory.KummerExtension
autEquivRootsOfUnity.eq_1 : ∀ {K : Type u} [inst : Field K] {n : ℕ} (hζ : (primitiveRoots n K).Nonempty) {a : K}
  (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) (L : Type u_1) [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] [inst_4 : NeZero n],
  autEquivRootsOfUnity hζ H L =
    (adjoinRootXPowSubCEquiv hζ H ⋯).symm.autCongr.trans (autAdjoinRootXPowSubCEquiv hζ H).symm
-- Mathlib.Geometry.Euclidean.Angle.Incenter
/-- An excenter lying on the external angle bisector from a vertex is the excenter opposite
another vertex.  -/
Affine.Triangle.eq_excenter_singleton_of_oangle_eq_add_pi : ∀ {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)]
  {t : Affine.Triangle ℝ P} {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        ∀ {signs : Finset (Fin 3)},
          EuclideanGeometry.oangle (t.points i₂) (t.points i₁) (Affine.Simplex.excenter t signs) =
              EuclideanGeometry.oangle (Affine.Simplex.excenter t signs) (t.points i₁) (t.points i₃) + ↑Real.pi →
            Affine.Simplex.excenter t signs = Affine.Simplex.excenter t {i₂} ∨
              Affine.Simplex.excenter t signs = Affine.Simplex.excenter t {i₃}
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.inv_toFun : ∀ (E : Type u_6) [inst : CommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalGroup E] (a : E),
  (ContinuousMonoidHom.inv E) a = a⁻¹
-- Mathlib.Data.Multiset.Bind
Multiset.mem_sigma : ∀ {α : Type u_1} {σ : α → Type u_4} {s : Multiset α} {t : (a : α) → Multiset (σ a)} {p : (a : α) × σ a},
  p ∈ s.sigma t ↔ p.fst ∈ s ∧ p.snd ∈ t p.fst
-- Mathlib.Tactic.Ring.Common
/-- The expression `e` (the sum of monomials) is equal to another monomial
(with nonzero leading coefficient).  -/
Mathlib.Tactic.Ring.Common.Overlap.nonzero : {u : Lean.Level} →
  {α : Q(Type u)} →
    {bt : Q(«$α») → Type} →
      {sα : Q(CommSemiring «$α»)} →
        {e : Q(«$α»)} →
          Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExProd bt sα) e →
            Mathlib.Tactic.Ring.Common.Overlap bt sα e
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.iUnion_neg_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {s : Set β}, ⋃ g, -g +ᵥ s = ⋃ g, g +ᵥ s
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicClosure_eq_closure : ∀ (𝕜 : Type u_1) {V : Type u_2} {P : Type u_5} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] [inst_5 : MetricSpace P]
  [inst_6 : NormedAddTorsor V P] (s : Set P), intrinsicClosure 𝕜 s = closure s
-- Mathlib.Analysis.InnerProductSpace.SingularValues
LinearMap.singularValues_eq_zero_iff_le_finrank_range : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) {n : ℕ}, T.singularValues n = 0 ↔ Module.finrank 𝕜 ↥T.range ≤ n
-- Aesop.Index.DiscrTreeConfig
Aesop.getUnify : {α : Type} → Lean.Meta.DiscrTree α → Lean.Expr → Lean.MetaM (Array α)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.IterM.step_filterWithPostcondition.match_1.eq_1 : ∀ {β : Type u_1} {n : Type u_1 → Type u_2} {f : β → Std.Iterators.PostconditionT n (ULift.{u_1, 0} Bool)} (out : β)
  (motive : Subtype (f out).Property → Sort u_3) (h' : (f out).Property { down := false })
  (h_1 : (h' : (f out).Property { down := false }) → motive ⟨{ down := false }, h'⟩)
  (h_2 : (h' : (f out).Property { down := true }) → motive ⟨{ down := true }, h'⟩),
  (match ⟨{ down := false }, h'⟩ with
    | ⟨{ down := false }, h'⟩ => h_1 h'
    | ⟨{ down := true }, h'⟩ => h_2 h') =
    h_1 h'
-- Aesop.Tracing
Aesop.withConstAesopTraceNode : {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 → m Lean.MessageData → m α → optParam Bool true → m α
-- Mathlib.MeasureTheory.Measure.Haar.Disintegration
/-- Given a surjective linear map `L`, it is equivalent to require a property almost everywhere
in the source or the target spaces of `L`, with respect to additive Haar measures there.  -/
MeasureTheory.ae_comp_linearMap_mem_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : MeasurableSpace E] [BorelSpace E] [inst_5 : NormedSpace 𝕜 E]
  [inst_6 : NormedAddCommGroup F] [inst_7 : MeasurableSpace F] [BorelSpace F] [inst_9 : NormedSpace 𝕜 F] (L : E →ₗ[𝕜] F)
  (μ : MeasureTheory.Measure E) (ν : MeasureTheory.Measure F) [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure]
  [LocallyCompactSpace E],
  Function.Surjective ⇑L → ∀ {s : Set F}, MeasurableSet s → ((∀ᵐ (x : E) ∂μ, L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s)
-- Mathlib.Order.Filter.SmallSets
Filter.smallSets.eq_1 : ∀ {α : Type u_1} (l : Filter α), l.smallSets = l.lift' Set.powerset
-- Mathlib.Topology.MetricSpace.DilationEquiv
DilationEquiv.mk.sizeOf_spec : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] [inst_2 : SizeOf X]
  [inst_3 : SizeOf Y] (toEquiv : X ≃ Y)
  (edist_eq' : ∃ r, r ≠ 0 ∧ ∀ (x y : X), edist (toEquiv.toFun x) (toEquiv.toFun y) = ↑r * edist x y),
  sizeOf { toEquiv := toEquiv, edist_eq' := edist_eq' } = 1 + sizeOf toEquiv + sizeOf edist_eq'
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Seed.baseEmbedding.eq_1 : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] (seed : HahnEmbedding.Seed K M R),
  seed.baseEmbedding =
    { domain := seed.baseDomain,
      toFun :=
        ↑(toLexLinearEquiv K (HahnSeries (FiniteArchimedeanClass M) R)) ∘ₗ
          HahnSeries.ofFinsuppLinearMap K ∘ₗ ↑(finsuppLequivDFinsupp K).symm ∘ₗ seed.hahnCoeff }
-- Mathlib.Algebra.Lie.Prod
LieHom.prod_ext_iff : ∀ (R : Type u_1) (L₁ : Type u_2) (L₂ : Type u_3) {L : Type u_4} [inst : CommRing R] [inst_1 : LieRing L₁]
  [inst_2 : LieAlgebra R L₁] [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] [inst_5 : LieRing L]
  [inst_6 : LieAlgebra R L] {f g : L₁ × L₂ →ₗ⁅R⁆ L},
  f = g ↔
    f.comp (LieHom.inl R L₁ L₂) = g.comp (LieHom.inl R L₁ L₂) ∧
      f.comp (LieHom.inr R L₁ L₂) = g.comp (LieHom.inr R L₁ L₂)
-- Init.Data.Vector.Range
/-- Replace `zipIdx` with a starting index with `zipIdx` starting from 0,
followed by a `map` increasing the indices.  -/
Vector.zipIdx_eq_map_add : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ},
  xs.zipIdx i =
    Vector.map
      (fun x =>
        match x with
        | (a, j) => (a, i + j))
      xs.zipIdx
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- If every element belongs to at least `n` Finsets, then the sum of their sizes is at least `n`
times how many they are.  -/
Finset.le_sum_card_inter : ∀ {α : Type u_2} [inst : DecidableEq α] {s : Finset α} {B : Finset (Finset α)} {n : ℕ},
  (∀ a ∈ s, n ≤ {b ∈ B | a ∈ b}.card) → s.card * n ≤ ∑ t ∈ B, (s ∩ t).card
-- Mathlib.RingTheory.Ideal.MonicSpan
Polynomial.exists_monic_span_sup_map_eq : ∀ (R : Type u_1) [inst : CommRing R] (p : Ideal (Polynomial R)),
  (Ideal.comap Polynomial.C p).IsMaximal →
    p ≠ Ideal.map Polynomial.C (Ideal.comap Polynomial.C p) →
      ∃ f, f.Monic ∧ p = Ideal.map Polynomial.C (Ideal.comap Polynomial.C p) ⊔ Ideal.span {f}
-- Mathlib.Topology.Connected.Clopen
ConnectedComponents.instInhabited : {α : Type u} → [inst : TopologicalSpace α] → [Inhabited α] → Inhabited (ConnectedComponents α)
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.mapEdgeSet_apply : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G ≃g G') (e : ↑G.edgeSet),
  f.mapEdgeSet e = SimpleGraph.Hom.mapEdgeSet (RelIso.toRelEmbedding f).toRelHom e