mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Independence.Kernel.Indep
/-- A family of sets is independent if the family of measurable space structures they generate is
independent. For a set `s`, the generated measurable space has measurable sets `∅, s, sᶜ, univ`.  -/
ProbabilityTheory.Kernel.iIndepSet : {α : Type u_1} →
  {Ω : Type u_2} →
    {ι : Type u_3} →
      {_mα : MeasurableSpace α} →
        {_mΩ : MeasurableSpace Ω} →
          (ι → Set Ω) →
            ProbabilityTheory.Kernel α Ω →
              autoParam (MeasureTheory.Measure α) ProbabilityTheory.Kernel.iIndepSet._auto_1 → Prop
-- Mathlib.Order.Bounds.Basic
isLeast_Ico : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a → IsLeast (Set.Ico b a) b
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- A version of `Finset.prod_map` and `Finset.prod_image`, but we do not assume that `f` is
injective. Rather, we assume that the image of `f` on `I` only overlaps where `g (f i) = 1`.
The conclusion is the same as in `prod_image`.  -/
Finset.prod_image_of_pairwise_eq_one : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : CommMonoid M] [inst_1 : DecidableEq ι] {f : κ → ι} {g : ι → M}
  {I : Finset κ}, ((↑I).Pairwise fun i j => f i = f j → g (f i) = 1) → ∏ s ∈ Finset.image f I, g s = ∏ i ∈ I, g (f i)
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.FunctorObjIndex.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} {f : (i : I) → A i ⟶ B i} {S X : C}
  {πX : X ⟶ S} [inst_1 : SizeOf C] [inst_2 : SizeOf I] (i : I) (t : A i ⟶ X) (b : B i ⟶ S)
  (w : CategoryTheory.CategoryStruct.comp t πX = CategoryTheory.CategoryStruct.comp (f i) b),
  sizeOf { i := i, t := t, b := b, w := w } = 1 + sizeOf i + sizeOf t + sizeOf b + sizeOf w
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- If `A` contains `B` and `B` contains `C`, then `A` contains `C`.  -/
SimpleGraph.IsContained.trans : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ},
  A.IsContained B → B.IsContained C → A.IsContained C
-- Std.Http.Protocol.H1.Error
Std.Http.Protocol.H1.instReprError.repr : Std.Http.Protocol.H1.Error → ℕ → Std.Format
-- Init.Data.List.MinMaxOn
List.minOn?_cons_eq_some_minOn : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {x : α} {xs : List α},
  List.minOn? f (x :: xs) = some (List.minOn f (x :: xs) ⋯)
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.mk'_eq_mk' : ∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [nN : N.Normal] {x y : G},
  (QuotientGroup.mk' N) x = (QuotientGroup.mk' N) y ↔ ∃ z ∈ N, x * z = y
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulOneClass α]
  [inst_3 : MulOneClass β] [inst_4 : SizeOf α] [inst_5 : SizeOf β] (toMonoidHom : α →* β)
  (monotone' : Monotone (↑toMonoidHom).toFun),
  sizeOf { toMonoidHom := toMonoidHom, monotone' := monotone' } = 1 + sizeOf toMonoidHom
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapSnd.eq_1 : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'}
  {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'}
  (β : F₂.comp R' ⟶ R.comp F) (α : L.comp F ⟶ F₁.comp L'),
  CategoryTheory.Comma.mapSnd β α =
    CategoryTheory.NatIso.ofComponents'
      (fun x => CategoryTheory.Iso.refl (((CategoryTheory.Comma.map β α).comp (CategoryTheory.Comma.snd R' L')).obj x))
      ⋯
-- Mathlib.Data.Quot
Quotient.out_eq : ∀ {α : Sort u_1} {s : Setoid α} (q : Quotient s), ⟦q.out⟧ = q
-- Lean.Parser.Term
Lean.Parser.Term.waitIfTypeMVar : Lean.Parser.Parser
-- Std.Async.System
/-- Gets information about the operating system.
 -/
Std.Async.System.OSInfo : Type
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.prehaar_self : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G]
  {K₀ : TopologicalSpace.PositiveCompacts G} {U : Set G},
  (interior U).Nonempty → MeasureTheory.Measure.haar.prehaar (↑K₀) U K₀.toCompacts = 1
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.adjoin.powerBasis.congr_simp : ∀ {K : Type u} [inst : Field K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {x : L} (hx : IsIntegral K x),
  IntermediateField.adjoin.powerBasis hx = IntermediateField.adjoin.powerBasis hx
-- Mathlib.Tactic.CancelDenoms.Core
/-- `findCompLemma e` arranges `e` in the form `lhs R rhs`, where `R ∈ {<, ≤, =, ≠}`, and returns
`lhs`, `rhs`, the `cancel_factors` lemma corresponding to `R`, and a Boolean indicating whether
`R` involves the order (i.e. `<` and `≤`) or not (i.e. `=` and `≠`).
In the case of `LT`, `LE`, `GE`, and `GT` an order on the type is needed, in the last case
it is not, the final component of the return value tracks this.
 -/
Mathlib.Tactic.CancelDenoms.findCompLemma : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Name × Bool))
-- Init.Data.Vector.Lemmas
Vector.allM_toList : ∀ {m : Type → Type u_1} {α : Type u_2} {n : ℕ} [inst : Monad m] [LawfulMonad m] {p : α → m Bool} {xs : Vector α n},
  List.allM p xs.toList = Vector.allM p xs
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Build the `apply at` discrimination tree?  -/
Mathlib.Tactic.ClickSuggestions.Choice.appAt : Mathlib.Tactic.ClickSuggestions.Choice → Bool
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherianRing_range : ∀ {R : Type u_1} [inst : Ring R] {S : Type u_2} [inst_1 : Ring S] (f : R →+* S) [IsNoetherianRing R],
  IsNoetherianRing ↥f.range
-- Mathlib.Algebra.Lie.Nilpotent
LieIdeal.lcs_succ : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I : LieIdeal R L)
  (M : Type u_3) [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] (k : ℕ),
  I.lcs M (k + 1) = ⁅I, I.lcs M k⁆
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sUnion_add : ∀ {α : Type u_2} [inst : Add α] (S : Set (Set α)) (t : Set α), ⋃₀ S + t = ⋃ s ∈ S, s + t
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Splitting.rightHom_comp_splitting : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : Group N] [inst_1 : Group E] [inst_2 : Group G]
  {S : GroupExtension N E G} (s : S.Splitting), S.rightHom.comp ↑s = MonoidHom.id G
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k a fallback : α} {v : β},
      (t.insert k v).getKeyD a fallback = if cmp k a = Ordering.eq then k else t.getKeyD a fallback
-- Mathlib.CategoryTheory.Iso
CategoryTheory.asIso'_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : Y ⟶ X) [inst_1 : CategoryTheory.IsIso f],
  (CategoryTheory.asIso' f).inv = f
-- Mathlib.Data.DFinsupp.Order
DFinsupp.instSemilatticeInf : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → Zero (α i)] → [(i : ι) → SemilatticeInf (α i)] → SemilatticeInf (Π₀ (i : ι), α i)
-- Mathlib.CategoryTheory.Sites.Pullback
/-- The constructed pullback of sheaves is isomorphic to the abstract one.  -/
CategoryTheory.Functor.sheafPullbackConstruction.sheafPullbackIso : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {D : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} D] →
        (G : CategoryTheory.Functor C D) →
          (A : Type u₁) →
            [inst_2 : CategoryTheory.Category.{v₁, u₁} A] →
              (J : CategoryTheory.GrothendieckTopology C) →
                (K : CategoryTheory.GrothendieckTopology D) →
                  [inst_3 : G.IsContinuous J K] →
                    [inst_4 : ∀ (F : CategoryTheory.Functor Cᵒᵖ A), G.op.HasLeftKanExtension F] →
                      [inst_5 : CategoryTheory.HasWeakSheafify K A] →
                        G.sheafPullback A J K ≅ CategoryTheory.Functor.sheafPullbackConstruction.sheafPullback G A J K
-- Init.Data.SInt.Lemmas
Int8.ofIntTruncate_bitVecToInt : ∀ (n : BitVec 8), Int8.ofIntClamp n.toInt = Int8.ofBitVec n
-- Mathlib.CategoryTheory.Sites.Localization
CategoryTheory.Sieve.W_shrinkFunctor_ι_of_mem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.LocallySmall.{w, v_1, u_1} C] {X : C},
  ∀ S ∈ J X, J.W (CategoryTheory.Sieve.shrinkFunctor.{w, v_1, u_1} S).ι
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp},
  t₁.Equiv t₂ → ∀ (f : (a : α) → β a → γ a), (Std.DTreeMap.map f t₁).Equiv (Std.DTreeMap.map f t₂)
-- Mathlib.Data.PFun
/-- Another induction lemma for `b ∈ f.fix a` which allows one to prove a predicate `P` holds for
`a` given that `f a` inherits `P` from `a` and `P` holds for preimages of `b`.
 -/
PFun.fixInduction' : {α : Type u_1} →
  {β : Type u_2} →
    {C : α → Sort u_7} →
      {f : α →. β ⊕ α} →
        {b : β} →
          {a : α} →
            b ∈ f.fix a →
              ((a_final : α) → Sum.inl b ∈ f a_final → C a_final) →
                ((a₀ a₁ : α) → b ∈ f.fix a₁ → Sum.inr a₁ ∈ f a₀ → C a₁ → C a₀) → C a
-- Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
/-- The circle-valued characters of a finite abelian group are the same as its complex-valued
characters.  -/
AddChar.circleEquivComplex : {α : Type u_1} → [inst : AddCommGroup α] → [Finite α] → AddChar α Circle ≃+ AddChar α ℂ
-- Mathlib.NumberTheory.RamificationInertia.Galois
/-- The `inertiaDegIn` is equal to any ramification index over the same ideal.  -/
Ideal.inertiaDegIn_eq_inertiaDeg : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (p : Ideal A)
  (P : Ideal B) [hPp : P.IsPrime] [hp : P.LiesOver p] (G : Type u_3) [inst_3 : Group G] [Finite G]
  [inst_5 : MulSemiringAction G B] [IsGaloisGroup G A B], p.inertiaDegIn B = P.inertiaDeg A
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn_bot_le_iff : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrderBot ι] [WellFoundedLT ι]
  {u : ι → Ω → β} {s : Set β} {i n : ι} {ω : Ω},
  (∃ j ≤ n, u j ω ∈ s) → (MeasureTheory.hittingBtwn u s ⊥ n ω ≤ i ↔ ∃ j ≤ i, u j ω ∈ s)
-- Init.Data.Function
Function.HasLeftInverse.injective : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.HasLeftInverse f → Function.Injective f
-- Mathlib.Topology.Category.Profinite.Product
Profinite.IndexFunctor.eq_of_forall_π_app_eq : ∀ {ι : Type u} {X : ι → Type} [inst : (i : ι) → TopologicalSpace (X i)] {C : Set ((i : ι) → X i)} (a b : ↑C),
  (∀ (J : Finset ι),
      (Profinite.IndexFunctor.π_app C fun x => x ∈ J) a = (Profinite.IndexFunctor.π_app C fun x => x ∈ J) b) →
    a = b
-- Lean.Declaration
Lean.ConstantVal.name : Lean.ConstantVal → Lean.Name
-- Mathlib.Order.BooleanAlgebra.Basic
compl_sdiff : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], (x \ y)ᶜ = x ⇨ y
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_set_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {a : α} {b : β}, a • {b} = {a • b}
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
neg_add_le_iff_le_add : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c : α}, -b + a ≤ c ↔ a ≤ b + c
-- Mathlib.Algebra.Star.BigOperators
star_sum : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : StarAddMonoid R] {α : Type u_2} (s : Finset α) (f : α → R),
  star (∑ x ∈ s, f x) = ∑ x ∈ s, star (f x)
-- Init.Data.Float.Model.Unpacked.Round
/-- Suppose given a real number `x : ℝ` with binary expansion
`x = ± x₀.x₁x₂x₃…`. Truncating the expansion at some point gives an
approximation of `x` as a floating-point number `y`. We can then ask how `y`
is related to `x`. If `y` is exactly `x`, then we say that we are exact.
Otherwise we are inexact, and `y` is slightly smaller than `x`, but `x` is also
smaller than `y + 1ulp`. Together with the information that we are inexact,
we store the information of where `x` is located relative to `y + ½ulp`. This
is sufficient information for rounding `y` according to the various IEEE rounding
rules.
 -/
Float.Model.UnpackedFloat.Accuracy : Type
-- Mathlib.RingTheory.PowerSeries.Inverse
PowerSeries.mul_invOfUnit : ∀ {R : Type u_1} [inst : Ring R] (φ : PowerSeries R) (u : Rˣ), PowerSeries.constantCoeff φ = ↑u → φ * φ.invOfUnit u = 1
-- Mathlib.CategoryTheory.Galois.EssSurj
_private.Mathlib.CategoryTheory.Galois.EssSurj.0.CategoryTheory.PreGaloisCategory.coconeQuotientDiagDesc_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.GaloisCategory C] [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F]
  {V U : OpenSubgroup (CategoryTheory.Aut F)} (h : (↑U).Normal) {A : C}
  (u :
    (CategoryTheory.PreGaloisCategory.functorToAction F).obj A ≅
      Action.FintypeCat.ofMulAction (CategoryTheory.Aut F) (FintypeCat.of (CategoryTheory.Aut F ⧸ ↑U)))
  (hUinV : U ≤ V)
  (s :
    CategoryTheory.Limits.Cocone
      ((CategoryTheory.PreGaloisCategory.quotientDiag✝ V h u).comp
        (CategoryTheory.PreGaloisCategory.functorToAction F))),
  (CategoryTheory.PreGaloisCategory.coconeQuotientDiagDesc✝ h u hUinV s).hom =
    FintypeCat.homMk
      (Quotient.lift
        (fun σ =>
          (CategoryTheory.ConcreteCategory.hom
              (CategoryTheory.CategoryStruct.comp u.inv
                  (s.ι.app (CategoryTheory.SingleObj.star (↥↑V ⧸ (↑U).subgroupOf ↑V)))).hom)
            ⟦σ⟧)
        ⋯)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblXYZ_Y : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R), W'.dblXYZ P 1 = W'.dblY P
-- Lean.Level
_private.Lean.Level.0.Lean.Level.updateMax!Impl : Lean.Level → Lean.Level → Lean.Level → Lean.Level
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesLE_succ : ∀ (n : ℕ), (n + 1).primesLE = if Nat.Prime (n + 1) then insert (n + 1) n.primesLE else n.primesLE
-- Mathlib.CategoryTheory.MorphismProperty.FunctorCategory
CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape.functorCategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {K : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} K] [W.IsStableUnderLimitsOfShape K] (J : Type u'')
  [inst_3 : CategoryTheory.Category.{v'', u''} J] [CategoryTheory.Limits.HasLimitsOfShape K C],
  (W.functorCategory J).IsStableUnderLimitsOfShape K
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintKind.type : Lean.Elab.InlayHintKind
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.pow_iff : ∀ {β : Type u_3} [Finite β] {f : Equiv.Perm β}, f.IsCycle → ∀ {n : ℕ}, (f ^ n).IsCycle ↔ n.Coprime (orderOf f)
-- Std.Time.Zoned.Database.TZdb
Std.Time.Database.TZdb.TZSpec.zoneId.sizeOf_spec : ∀ (id : String), sizeOf (Std.Time.Database.TZdb.TZSpec.zoneId id) = 1 + sizeOf id
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.FiniteSpanningSetsIn.spanning : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {C : Set (Set α)}
  (self : μ.FiniteSpanningSetsIn C), ⋃ i, self.set i = Set.univ
-- Mathlib.AlgebraicGeometry.Sites.Proetale
/-- The pro-étale topology on the small pro-étale site.  -/
AlgebraicGeometry.Scheme.ProEt.topology : (S : AlgebraicGeometry.Scheme) → CategoryTheory.GrothendieckTopology S.ProEt
-- Lean.Elab.DefView
Lean.Elab.DefKind.abbrev : Lean.Elab.DefKind
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.of_algEquiv : ∀ {F : Type u_1} {E : Type u_3} [inst : Field F] [inst_1 : Field E] {E' : Type u_4} [inst_2 : Field E']
  [inst_3 : Algebra F E'] [inst_4 : Algebra F E] [IsGalois F E] (f : E ≃ₐ[F] E'), IsGalois F E'
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.withSimpDiagnostics : Lean.Elab.Tactic.TacticM Lean.Meta.Simp.Diagnostics → Lean.Elab.Tactic.TacticM Unit
-- Lean.Meta.DiscrTree.Basic
Lean.Meta.DiscrTree.insertKeyValue : {α : Type} → [BEq α] → Lean.Meta.DiscrTree α → Array Lean.Meta.DiscrTree.Key → α → Lean.Meta.DiscrTree α
-- Init.Data.Range.Polymorphic.Nat
Std.PRange.instInfinitelyUpwardEnumerableNat : Std.PRange.InfinitelyUpwardEnumerable ℕ
-- Mathlib.Logic.Denumerable
/-- The lift of a denumerable type is denumerable.  -/
Denumerable.ulift : {α : Type u_1} → [Denumerable α] → Denumerable (ULift.{u_3, u_1} α)
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cocone.equivStructuredArrow_inverse : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C),
  (CategoryTheory.Limits.Cocone.equivStructuredArrow F).inverse = CategoryTheory.Limits.Cocone.fromStructuredArrow F
-- Mathlib.Order.UpperLower.Closure
lowerClosure_eq_bot_iff : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, lowerClosure s = ⊥ ↔ s = ∅
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- The unipotent upper triangular matrix
```
(1 r)
(0 1)
```
as an isomorphism.
 -/
CategoryTheory.Biprod.unipotentUpper : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] → {X₁ X₂ : C} → (X₁ ⟶ X₂) → (X₁ ⊞ X₂ ≅ X₁ ⊞ X₂)
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.step_intermediateZip.match_3.splitter : {α₁ β₁ : Type u_1} →
  [inst : Std.Iterator α₁ Id β₁] →
    (motive : Option { out // ∃ it, it.toIterM.IsPlausibleOutput out } → Sort u_2) →
      (memo : Option { out // ∃ it, it.toIterM.IsPlausibleOutput out }) →
        (Unit → motive none) →
          ((out₁ : { out // ∃ it, it.toIterM.IsPlausibleOutput out }) → motive (some out₁)) → motive memo
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C) (D : Type uD)
  [inst_1 : CategoryTheory.Category.{uD', uD} D],
  (CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.unitIso W D).hom = CategoryTheory.eqToHom ⋯
-- Init.Data.String.Slice
String.Slice.SplitInclusiveIterator : {σ : String.Slice → Type} →
  {ρ : Type} → (pat : ρ) → String.Slice → [String.Slice.Pattern.ToForwardSearcher pat σ] → Type
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsUpperSet.mk : ∀ {α : Type u_4} [t : TopologicalSpace α] [inst : Preorder α], t = Topology.upperSet α → Topology.IsUpperSet α
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_eq_bot : ∀ {α : Type u} [inst : Semiring α] {s : Set α}, Ideal.span s = ⊥ ↔ ∀ x ∈ s, x = 0
-- Mathlib.FieldTheory.Galois.GaloisClosure
/-- The type of intermediate fields of `K/k` that are finite and Galois over `k`  -/
FiniteGaloisIntermediateField : (k : Type u_1) → (K : Type u_2) → [inst : Field k] → [inst_1 : Field K] → [Algebra k K] → Type u_2
-- Mathlib.MeasureTheory.SpecificCodomains.Pi
MeasureTheory.MemLp.fst : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {p : ENNReal} {E : Type u_2} {F : Type u_3}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {f : X → E × F},
  MeasureTheory.MemLp f p μ → MeasureTheory.MemLp (fun x => (f x).1) p μ
-- Mathlib.Analysis.Convex.Jensen
StrictConvexOn.map_sum_lt_iff_of_nonneg : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConvexOn 𝕜 s f →
    (∀ i ∈ t, 0 ≤ w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) →
          (f (∑ i ∈ t, w i • p i) < ∑ i ∈ t, w i • f (p i) ↔ ∃ j ∈ t, ∃ k ∈ t, w j ≠ 0 ∧ w k ≠ 0 ∧ p j ≠ p k)
-- Mathlib.Algebra.Group.Defs
SubNegZeroMonoid.neg_zero : ∀ {G : Type u_2} [self : SubNegZeroMonoid G], -0 = 0
-- Init.Data.Order.Lemmas
Std.total_of_not_rel_swap_imp_rel : ∀ {α : Sort u_1} {r : α → α → Prop}, (∀ {a b : α}, ¬r a b → r b a) → Std.Total r
-- Std.Do.WP.Sound
_private.Std.Do.WP.Sound.0.Std.Do.instWPSoundExceptTExceptPureOfLawfulMonad.match_5.eq_2 : ∀ {ε α : Type u_1} {P : α → Prop}
  (motive :
    (r : Except ε α) →
      (match r with
        | Except.ok a => P a
        | Except.error a => True) →
        Sort u_2)
  (e : ε)
  (x :
    match Except.error e with
    | Except.ok a => P a
    | Except.error a => True)
  (h_1 :
    (a : α) →
      (hp :
          match Except.ok a with
          | Except.ok a => P a
          | Except.error a => True) →
        motive (Except.ok a) hp)
  (h_2 :
    (e : ε) →
      (x :
          match Except.error e with
          | Except.ok a => P a
          | Except.error a => True) →
        motive (Except.error e) x),
  (match Except.error e, x with
    | Except.ok a, hp => h_1 a hp
    | Except.error e, x => h_2 e x) =
    h_2 e x
-- Lean.Data.Iterators.Producers.PersistentHashMap
Lean.PersistentHashMap.Zipper.consCollision.injEq : ∀ {α : Type u} {β : Type v} (keys : Subarray α) (vals : Subarray β) (a : Std.Slice.size keys = Std.Slice.size vals)
  (a_1 : Lean.PersistentHashMap.Zipper α β) (keys_1 : Subarray α) (vals_1 : Subarray β)
  (a_2 : Std.Slice.size keys_1 = Std.Slice.size vals_1) (a_3 : Lean.PersistentHashMap.Zipper α β),
  (Lean.PersistentHashMap.Zipper.consCollision keys vals a a_1 =
      Lean.PersistentHashMap.Zipper.consCollision keys_1 vals_1 a_2 a_3) =
    (keys = keys_1 ∧ vals = vals_1 ∧ a_1 = a_3)
-- Mathlib.Data.Set.Function
Set.SurjOn.subset_range : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β}, Set.SurjOn f s t → t ⊆ Set.range f
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Set.measurable_restrict₂ : ∀ {δ : Type u_4} {X : δ → Type u_6} [inst : (a : δ) → MeasurableSpace (X a)] {s t : Set δ} (hst : s ⊆ t),
  Measurable (Set.domRestrict₂ hst)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_eq_getD_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {fallback : α},
  t.minKeyD fallback = t.keysArray.getD 0 fallback
-- Mathlib.Algebra.Group.Center
AddSemigroup.mem_center_iff : ∀ {M : Type u_1} [inst : AddSemigroup M] {z : M}, z ∈ Set.addCenter M ↔ ∀ (g : M), g + z = z + g
-- Init.Data.List.Nat.Range
List.map_zipIdx : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α} {k : ℕ},
  List.map (Prod.map f id) (l.zipIdx k) = (List.map f l).zipIdx k
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_eq_none : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, a ∉ t → t.getKey? a = none
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableAt_of_isInvertible_mfderiv : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M},
  (mfderiv% f x).IsInvertible → MDiffAt f x