mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- If the sign of the angle between three points is negative, the last two points are not equal.
 -/
EuclideanGeometry.right_ne_of_oangle_sign_eq_neg_one : ∀ {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}, (EuclideanGeometry.oangle p₁ p₂ p₃).sign = -1 → p₃ ≠ p₂
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
IsAbsoluteValue.abs_abv_sub_le_abv_sub : ∀ {S : Type u_5} [inst : CommRing S] [inst_1 : LinearOrder S] [IsStrictOrderedRing S] {R : Type u_6} [inst_3 : Ring R]
  (abv : R → S) [IsAbsoluteValue abv] (a b : R), |abv a - abv b| ≤ abv (a - b)
-- Mathlib.Order.Comparable
Relation.SymmGen.eq_1 : ∀ {α : Type u_1} (r : α → α → Prop) (a b : α), Relation.SymmGen r a b = (r a b ∨ r b a)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
mulLeftStrictMono_of_mulLeftReflectLE : ∀ (N : Type u_2) [inst : Mul N] [inst_1 : LinearOrder N] [MulLeftReflectLE N], MulLeftStrictMono N
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}, t.keys.isEmpty = t.isEmpty
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.mul_log_eq_log_iff : ∀ {x y z : ℝ}, 0 < x → 0 < z → (y * Real.log x = Real.log z ↔ x ^ y = z)
-- Mathlib.Data.String.Lemmas
_private.Mathlib.Data.String.Lemmas.0.String.IsPrefix.match_1.eq_1 : ∀ (motive : String → String → Sort u_1) (d1 d2 : String) (h_1 : (d1 d2 : String) → motive d1 d2),
  (match d1, d2 with
    | d1, d2 => h_1 d1 d2) =
    h_1 d1 d2
-- Mathlib.RingTheory.MvPolynomial.Tower
MvPolynomial.aeval_C_comp_left : ∀ {R : Type u_1} {A : Type u_2} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  {ι : Type u_5} (f : σ → A) (p : MvPolynomial σ R),
  (MvPolynomial.aeval (⇑MvPolynomial.C ∘ f)) p = MvPolynomial.C ((MvPolynomial.aeval f) p)
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_monotone : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Monotone (Submodule.span R)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.symmetricCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} →
      CategoryTheory.SymmetricCategory (PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat)))
-- Mathlib.CategoryTheory.Limits.ConeCategory
/-- `Functor.toStructuredArrow` can be expressed in terms of `Cone.toStructuredArrow`.  -/
CategoryTheory.Functor.toStructuredArrowIsoToStructuredArrow : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (G : CategoryTheory.Functor J K) →
              (X : C) →
                (F : CategoryTheory.Functor K C) →
                  (f : (Y : J) → X ⟶ F.obj (G.obj Y)) →
                    (h : ∀ {Y Z : J} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z) →
                      G.toStructuredArrow X F f ⋯ ≅
                        { pt := X, π := { app := f, naturality := ⋯ } }.toStructuredArrow.comp
                          (CategoryTheory.StructuredArrow.pre { pt := X, π := { app := f, naturality := ⋯ } }.pt G F)
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instZero.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Zero Y],
  LocallyConstant.instZero = { zero := LocallyConstant.const X 0 }
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
/-- `negAt` preserves `normAtPlace`.  -/
NumberField.mixedEmbedding.normAtPlace_negAt : ∀ {K : Type u_1} [inst : Field K] (s : Set { w // w.IsReal }) (x : NumberField.mixedEmbedding.mixedSpace K)
  (w : NumberField.InfinitePlace K),
  (NumberField.mixedEmbedding.normAtPlace w) ((NumberField.mixedEmbedding.negAt s) x) =
    (NumberField.mixedEmbedding.normAtPlace w) x
-- Mathlib.Probability.Kernel.Proper
/-- For two σ-algebras `𝓑 ≤ 𝓧` on a space `X`, a `𝓑, 𝓧`-kernel `π : X → Measure X` is proper if
`∫ x, g x * f x ∂(π x₀) = g x₀ * ∫ x, f x ∂(π x₀)` for all `x₀ : X`, `𝓧`-measurable function `f`
and `𝓑`-measurable function `g`.

By the standard machine, this is equivalent to having that, for all `B ∈ 𝓑`, `π` restricted to `B`
is the same as `π` times the indicator of `B`.

To avoid assuming `𝓑 ≤ 𝓧` in the definition, we replace `𝓑` by `𝓑 ⊓ 𝓧` in the restriction.  -/
ProbabilityTheory.Kernel.IsProper : {X : Type u_1} → {𝓑 𝓧 : MeasurableSpace X} → ProbabilityTheory.Kernel X X → Prop
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer reflection of a colimit along a natural isomorphism in the functor.  -/
CategoryTheory.Limits.reflectsColimit_of_natIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  {F G : CategoryTheory.Functor C D} (h : F ≅ G) [CategoryTheory.Limits.ReflectsColimit K F],
  CategoryTheory.Limits.ReflectsColimit K G
-- Mathlib.Combinatorics.Quiver.Schreier
Quiver.SchreierGraph.ofVertex.sizeOf_spec : ∀ {V : Type u_1} {M : Type u_2} [inst : SMul M V] {S : Type u_3} {_ι : S → M} [inst_1 : SizeOf V] [inst_2 : SizeOf M]
  [inst_3 : SizeOf S] (toVertex : V), sizeOf { toVertex := toVertex } = 1 + sizeOf toVertex
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- Construct an object of `Bimon C` from an object `X : C` and `BimonObj X` instance.  -/
CategoryTheory.Bimon.mk' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → (X : C) → [CategoryTheory.BimonObj X] → CategoryTheory.Bimon C
-- Mathlib.GroupTheory.Finiteness
AddMonoid.closure_finite_fg : ∀ {M : Type u_1} [inst : AddMonoid M] (s : Set M) [Finite ↑s], AddMonoid.FG ↥(AddSubmonoid.closure s)
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd : ∀ (R : Type u_1) [inst : CommRing R] {d n : ℕ},
  d ∈ n.properDivisors → (Polynomial.X ^ d - 1) * Polynomial.cyclotomic n R ∣ Polynomial.X ^ n - 1
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.biUnion_supp_eq_supp : ∀ {V : Type u} {G G' : SimpleGraph V},
  G ≤ G' → ∀ (c' : G'.ConnectedComponent), ⋃ c, ⋃ (_ : c.supp ⊆ c'.supp), c.supp = c'.supp
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.liftFSucc.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  (P : CategoryTheory.ProjectiveResolution Y) (Q : CategoryTheory.ProjectiveResolution Z) (n : ℕ)
  (g g_1 : P.complex.X n ⟶ Q.complex.X n) (e_g : g = g_1) (g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 1))
  (w :
    CategoryTheory.CategoryStruct.comp g' (Q.complex.d (n + 1) n) =
      CategoryTheory.CategoryStruct.comp (P.complex.d (n + 1) n) g),
  P.liftFSucc Q n g g' w = P.liftFSucc Q n g_1 g' ⋯
-- Std.Data.DHashMap.Internal.Model
/-- This is the general theorem to show that modification operations are correct.  -/
Std.DHashMap.Internal.toListModel_updateBucket : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α β}
      {g : List ((a : α) × β a) → List ((a : α) × β a)},
      (∀ {l : Std.DHashMap.Internal.AssocList α β}, (f l).toList.Perm (g l.toList)) →
        (∀ {l l' : List ((a : α) × β a)}, Std.Internal.List.DistinctKeys l → l.Perm l' → (g l).Perm (g l')) →
          (∀ {l l' : List ((a : α) × β a)}, Std.Internal.List.containsKey a l' = false → g (l ++ l') = g l ++ l') →
            (Std.DHashMap.Internal.toListModel (Std.DHashMap.Internal.updateBucket (↑m).buckets ⋯ a f)).Perm
              (g (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_atTop_one : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β} {f : α × β → ℚ → ℝ},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α), ∀ᵐ (t : β) ∂ν a, Filter.Tendsto (f (a, t)) Filter.atTop (nhds 1)
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.instOrderTop : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Min α] → [inst_1 : Top α] → [inst_2 : SemilatticeInf β] → [inst_3 : OrderTop β] → OrderTop (InfTopHom α β)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get!_diff_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], k ∈ t₂ → (t₁ \ t₂).get! k = default
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.TransitiveRelation.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (toJointlyMono₂ : CategoryTheory.JointlyMono₂ p₁ p₂) (c : CategoryTheory.Limits.PullbackCone p₂ p₁)
  (isLimit : CategoryTheory.Limits.IsLimit c) (t : c.pt ⟶ R)
  (transitivity₁ :
    autoParam (CategoryTheory.CategoryStruct.comp t p₁ = CategoryTheory.CategoryStruct.comp c.fst p₁)
      CategoryTheory.TransitiveRelation.transitivity₁._autoParam)
  (transitivity₂ :
    autoParam (CategoryTheory.CategoryStruct.comp t p₂ = CategoryTheory.CategoryStruct.comp c.snd p₂)
      CategoryTheory.TransitiveRelation.transitivity₂._autoParam)
  (toJointlyMono₂_1 : CategoryTheory.JointlyMono₂ p₁ p₂) (c_1 : CategoryTheory.Limits.PullbackCone p₂ p₁)
  (isLimit_1 : CategoryTheory.Limits.IsLimit c_1) (t_1 : c_1.pt ⟶ R)
  (transitivity₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp t_1 p₁ = CategoryTheory.CategoryStruct.comp c_1.fst p₁)
      CategoryTheory.TransitiveRelation.transitivity₁._autoParam)
  (transitivity₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp t_1 p₂ = CategoryTheory.CategoryStruct.comp c_1.snd p₂)
      CategoryTheory.TransitiveRelation.transitivity₂._autoParam),
  ({ toJointlyMono₂ := toJointlyMono₂, c := c, isLimit := isLimit, t := t, transitivity₁ := transitivity₁,
        transitivity₂ := transitivity₂ } =
      { toJointlyMono₂ := toJointlyMono₂_1, c := c_1, isLimit := isLimit_1, t := t_1, transitivity₁ := transitivity₁_1,
        transitivity₂ := transitivity₂_1 }) =
    (c = c_1 ∧ isLimit ≍ isLimit_1 ∧ t ≍ t_1)
-- Mathlib.LinearAlgebra.FreeModule.Finite.Matrix
Module.rank_linearMap : ∀ (R : Type u) (S : Type u') (M : Type v) (N : Type w) [inst : Ring R] [inst_1 : Ring S] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [Module.Free R M] [Module.Finite R M] [inst_6 : AddCommGroup N] [inst_7 : Module R N]
  [inst_8 : Module S N] [inst_9 : SMulCommClass R S N] [StrongRankCondition R] [StrongRankCondition S]
  [Module.Free S N],
  Module.rank S (M →ₗ[R] N) = Cardinal.lift.{w, v} (Module.rank R M) * Cardinal.lift.{v, w} (Module.rank S N)
-- Mathlib.Topology.Algebra.Module.Complement
ContinuousLinearMap.ofIsTopCompl_eq : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} {F : Type u_3} [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : TopologicalSpace F] [inst_6 : AddCommGroup F]
  [inst_7 : Module R F] [inst_8 : ContinuousAdd F] {p q : Submodule R E} (h : Submodule.IsTopCompl p q) {φ : ↥p →L[R] F}
  {ψ : ↥q →L[R] F} {χ : E →L[R] F},
  (∀ (u : ↥p), φ u = χ ↑u) → (∀ (u : ↥q), ψ u = χ ↑u) → ContinuousLinearMap.ofIsTopCompl h φ ψ = χ
-- Mathlib.LinearAlgebra.Finsupp.LSum
/-- An equivalence of domains induces a linear equivalence of finitely supported functions.

This is `Finsupp.domCongr` as a `LinearEquiv`.
See also `LinearMap.funCongrLeft` for the case of arbitrary functions.  -/
Finsupp.domLCongr : {M : Type u_2} →
  {R : Type u_5} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → {α₁ : Type u_9} → {α₂ : Type u_10} → α₁ ≃ α₂ → (α₁ →₀ M) ≃ₗ[R] α₂ →₀ M
-- Lean.Server.Completion.CompletionInfoSelection
_private.Lean.Server.Completion.CompletionInfoSelection.0.Lean.Server.Completion.filterDuplicateCompletionInfos.eq : Lean.Elab.CompletionInfo → Lean.Elab.CompletionInfo → Bool
-- Mathlib.Order.Filter.Pointwise
Filter.pure_one : ∀ {α : Type u_2} [inst : One α], pure 1 = 1
-- Init.Data.SInt.Basic
/-- Obtain the `BitVec` that contains the 2's complement representation of the `ISize`.
 -/
ISize.toBitVec : ISize → BitVec System.Platform.numBits
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.submoduleMap_apply_coe : ∀ {R : Type u_13} {R₂ : Type u_15} {M : Type u_16} {M₂ : Type u_17} [inst : Ring R] [inst_1 : Ring R₂]
  [inst_2 : SeminormedAddCommGroup M] [inst_3 : SeminormedAddCommGroup M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (p : Submodule R M)
  (e : M ≃ₛₗᵢ[σ₁₂] M₂) (c : ↥p), ↑((LinearIsometryEquiv.submoduleMap p e) c) = e ↑c
-- Init.Data.Order.FactoriesExtra
/-- The `BEq α` instance obtained from an `Ord α` instance is compatible with the `LE α` instance
instance if `Ord α` is compatible with it.
 -/
Std.instLawfulOrderBEq_ofOrd : ∀ {α : Type u} [inst : Ord α] [inst_1 : LE α] [Std.LawfulOrderOrd α], Std.LawfulOrderBEq α
-- Mathlib.NumberTheory.LSeries.ZMod
ZMod.LFunction.eq_1 : ∀ {N : ℕ} [inst : NeZero N] (Φ : ZMod N → ℂ) (s : ℂ),
  ZMod.LFunction Φ s = ↑N ^ (-s) * ∑ j, Φ j * HurwitzZeta.hurwitzZeta (ZMod.toAddCircle j) s
-- Init.Data.List.MinMaxIdx
List.minIdxOn?.congr_simp : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] {inst_1 : DecidableLE β} [inst_2 : DecidableLE β] (f f_1 : α → β),
  f = f_1 → ∀ (xs xs_1 : List α), xs = xs_1 → List.minIdxOn? f xs = List.minIdxOn? f_1 xs_1
-- Mathlib.Probability.Distributions.Gamma
/-- A Lebesgue Integral from -∞ to y can be expressed as the sum of one from -∞ to 0 and 0 to x  -/
lintegral_Iic_eq_lintegral_Iio_add_Icc : ∀ {y z : ℝ} (f : ℝ → ENNReal),
  z ≤ y → ∫⁻ (x : ℝ) in Set.Iic y, f x = (∫⁻ (x : ℝ) in Set.Iio z, f x) + ∫⁻ (x : ℝ) in Set.Icc z y, f x
-- Mathlib.Order.Sublocale
/-- The nuclei on a frame corresponds exactly to the sublocales on this frame.
The sublocales are ordered dually to the nuclei.  -/
nucleusIsoSublocale : {X : Type u_1} → [inst : Order.Frame X] → (Nucleus X)ᵒᵈ ≃o Sublocale X
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_sub_nhds_zero_iff : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {α : Type u_1} {l : Filter α}
  {x : G} {u : α → G}, Filter.Tendsto (fun x_1 => u x_1 - x) l (nhds 0) ↔ Filter.Tendsto u l (nhds x)
-- Mathlib.Algebra.Group.Units.Defs
/-- Units of a commutative monoid form a commutative group.  -/
Units.instCommGroupUnits : {α : Type u_1} → [inst : CommMonoid α] → CommGroup αˣ
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.add_antiperiod : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c₁ c₂ : α} [inst : AddSemigroup α] [inst_1 : Neg β],
  Function.Periodic f c₁ → Function.Antiperiodic f c₂ → Function.Antiperiodic f (c₁ + c₂)
-- Mathlib.Algebra.Group.Submonoid.Membership
AddSubmonoid.mem_sSup_of_mem : ∀ {M : Type u_1} [inst : AddZeroClass M] {S : Set (AddSubmonoid M)} {s : AddSubmonoid M},
  s ∈ S → ∀ {x : M}, x ∈ s → x ∈ sSup S
-- Mathlib.Data.Ordmap.Ordnode
/-- Auxiliary definition for `findIndex`.  -/
Ordnode.findIndexAux : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → α → Ordnode α → ℕ → Option ℕ
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.not_mem_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.isEmpty = true → a ∉ t
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
CategoryTheory.SmallObject.SuccStruct.ofCocone_map_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J] {j : J}
  {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.Limits.Cocone F) (i₁ i₂ : J) (hi : i₁ ≤ i₂)
  (hi₂ : i₂ < j) {Z : C} (h : (CategoryTheory.SmallObject.SuccStruct.ofCocone c).obj ⟨i₂, ⋯⟩ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.SmallObject.SuccStruct.ofCocone c).map (CategoryTheory.homOfLE hi)) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso c i₁ ⋯).hom
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE hi))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso c i₂ hi₂).inv h))
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
/-- If an integrable function has zero integral on all closed sets, then it is zero
almost everywhere.  -/
MeasureTheory.ae_eq_zero_of_forall_setIntegral_isClosed_eq_zero : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {β : Type u_3}
  [inst_3 : TopologicalSpace β] [inst_4 : MeasurableSpace β] [BorelSpace β] {μ : MeasureTheory.Measure β} {f : β → E},
  MeasureTheory.Integrable f μ → (∀ (s : Set β), IsClosed s → ∫ (x : β) in s, f x ∂μ = 0) → f =ᵐ[μ] 0
-- Mathlib.NumberTheory.Real.GoldenRatio
Real.goldenConj.eq_1 : Real.goldenConj = (1 - √5) / 2
-- Mathlib.CategoryTheory.WithTerminal.Lemmas
CategoryTheory.WithInitial.instIsFilteredOfIsFilteredOrEmpty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.IsFilteredOrEmpty C],
  CategoryTheory.IsFiltered (CategoryTheory.WithInitial C)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.postcompose₂_obj_right_map : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H)
  (G : CategoryTheory.Functor H D')
  (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D H).obj L))
  {X_1 Y : D} (f : X_1 ⟶ Y),
  ((CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).obj X).right.map f = G.map (X.right.map f)
-- Mathlib.Analysis.Normed.Module.Bases
GeneralSchauderBasis.ext_iff : ∀ {β : Type u_3} {𝕜 : Type u_4} {X : Type u_5} {inst : NontriviallyNormedField 𝕜} {inst_1 : NormedAddCommGroup X}
  {inst_2 : NormedSpace 𝕜 X} {L : SummationFilter β} {x y : GeneralSchauderBasis β 𝕜 X L},
  x = y ↔ ↑x = ↑y ∧ x.coord = y.coord
-- Mathlib.CategoryTheory.Join.Basic
_private.Mathlib.CategoryTheory.Join.Basic.0.CategoryTheory.Join.id.match_1.splitter : {C : Type u_3} →
  [inst : CategoryTheory.Category.{u_1, u_3} C] →
    {D : Type u_4} →
      [inst_1 : CategoryTheory.Category.{u_2, u_4} D] →
        (motive : CategoryTheory.Join C D → Sort u_5) →
          (x : CategoryTheory.Join C D) →
            ((x : C) → motive (CategoryTheory.Join.left x)) →
              ((x : D) → motive (CategoryTheory.Join.right x)) → motive x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isSome_getKey?_iff_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  (t.getKey? a).isSome = true ↔ a ∈ t
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.beth_ofNat_eq_lift : ∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo],
  Cardinal.beth (OfNat.ofNat n) = Cardinal.lift.{v, u} c ↔ Cardinal.beth (OfNat.ofNat n) = c
-- Mathlib.CategoryTheory.Functor.CurryingThree
/-- Uncurrying functors in three variables gives a fully faithful functor.  -/
CategoryTheory.Functor.fullyFaithfulUncurry₃ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_4} →
      {E : Type u_9} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃] →
              [inst_3 : CategoryTheory.Category.{v_9, u_9} E] → CategoryTheory.Functor.uncurry₃.FullyFaithful
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
ModelWithCorners.interior.eq_def : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} (M : Type u_4)
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M], ModelWithCorners.interior M = {x | I.IsInteriorPoint x}
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CategoryTheory.eqToIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (p : X = Y),
  CategoryTheory.eqToIso p =
    { hom := CategoryTheory.eqToHom p, inv := CategoryTheory.eqToHom ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Init.Data.Order.PackageFactories
Std.LinearOrderPackage.toMin : {α : Type u} → [self : Std.LinearOrderPackage α] → Min α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.size_ofList_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List ((a : α) × β a)},
  (Std.DTreeMap.Raw.ofList l cmp).inner.size ≤ l.length
-- Mathlib.CategoryTheory.Bicategory.Yoneda
/-- Left component of the associator as a 2-isomorphism in `Cat`.  -/
CategoryTheory.Bicategory.associatorNatIsoLeftCat : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    (a : B) →
      {b c d : B} →
        (g : b ⟶ c) →
          (h : c ⟶ d) →
            CategoryTheory.CategoryStruct.comp ((CategoryTheory.Bicategory.postcomposingCat a b c).obj g)
                ((CategoryTheory.Bicategory.postcomposingCat a c d).obj h) ≅
              (CategoryTheory.Bicategory.postcomposingCat a b d).obj (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.range_cotangentToQuotientSquare : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R),
  I.cotangentToQuotientSquare.range = Submodule.restrictScalars R I.cotangentIdeal
-- Mathlib.CategoryTheory.Equivalence.Symmetry
/-- An "unopped" version of the equivalence `inverseFunctorObj'`.  -/
CategoryTheory.Equivalence.inverseFunctorObj' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (e : C ≌ D) → Opposite.unop ((CategoryTheory.Equivalence.inverseFunctor C D).obj e) ≅ e.inverse
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.braiding_inv_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y : CategoryTheory.Dial C),
  (X.braiding Y).inv.F =
    CategoryTheory.Limits.prod.lift
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)
-- Init.Data.Iterators.Basic
/-- Match pattern for the `done` case. See also `IterStep.done`.
 -/
Std.PlausibleIterStep.done : {α : Type u} →
  {β : Type w} →
    {IsPlausibleStep : Std.IterStep α β → Prop} →
      IsPlausibleStep Std.IterStep.done → Std.PlausibleIterStep IsPlausibleStep
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
LinearOrderedCommGroupWithZero.mk : {α : Type u_3} →
  [toLinearOrderedCommMonoidWithZero : LinearOrderedCommMonoidWithZero α] →
    [toInv : Inv α] →
      [toDiv : Div α] →
        [toZPow : ZPow α] →
          autoParam (∀ (a b : α), a / b = a * b⁻¹) DivInvMonoid.div_eq_mul_inv._autoParam →
            autoParam (∀ (a : α), a ^ 0 = 1) DivInvMonoid.zpow_zero'._autoParam →
              autoParam (∀ (n : ℕ) (a : α), a ^ ↑n.succ = a ^ ↑n * a) DivInvMonoid.zpow_succ'._autoParam →
                autoParam (∀ (n : ℕ) (a : α), a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹) DivInvMonoid.zpow_neg'._autoParam →
                  [toNontrivial : Nontrivial α] →
                    0⁻¹ = 0 → (∀ (a : α), a ≠ 0 → a * a⁻¹ = 1) → LinearOrderedCommGroupWithZero α