mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
FiberBundle.writtenInExtChartAt_trivializationAt_symm : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E] {x : Bundle.TotalSpace F E}
  {y : EB × F},
  y ∈ (extChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) x).target →
    writtenInExtChartAt (IB.prod (modelWithCornersSelf 𝕜 F)) (IB.prod (modelWithCornersSelf 𝕜 F))
        (↑(trivializationAt F E x.proj) x) (↑(trivializationAt F E x.proj).symm) y =
      y
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.comp_coconePointsIsoOfNatIso_inv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {s : CategoryTheory.Limits.Cocone F} {t : CategoryTheory.Limits.Cocone G}
  (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) (w : F ≅ G) (j : J),
  CategoryTheory.CategoryStruct.comp (t.ι.app j) (P.coconePointsIsoOfNatIso Q w).inv =
    CategoryTheory.CategoryStruct.comp (w.inv.app j) (s.ι.app j)
-- Mathlib.Tactic.Order.CollectFacts
Mathlib.Tactic.Order.instInhabitedAtomicFact.default : Mathlib.Tactic.Order.AtomicFact
-- Mathlib.Dynamics.FixedPoints.Defs
Function.fixedPoints.decidable : {α : Type u_1} → [DecidableEq α] → (f : α → α) → (x : α) → Decidable (x ∈ Function.fixedPoints f)
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Summable.sigma : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [IsUniformAddGroup α]
  [CompleteSpace α] {γ : β → Type u_4} {f : (b : β) × γ b → α}, Summable f → Summable fun b => ∑' (c : γ b), f ⟨b, c⟩
-- Init.System.IO
/-- The number of additional nanoseconds.  -/
IO.FS.SystemTime.nsec : IO.FS.SystemTime → UInt32
-- Mathlib.Topology.Order.LeftRightLim
Monotone.rightLim_le_leftLim : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {f : α → β},
  Monotone f → ∀ {x y : α}, x < y → Function.rightLim f x ≤ Function.leftLim f y
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.coe_equivMapOfInjective_apply : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H : Subgroup G) (f : G →* N)
  (hf : Function.Injective ⇑f) (h : ↥H), ↑((H.equivMapOfInjective f hf) h) = f ↑h
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.coe_top : ∀ {R : Type u} [inst : NonAssocSemiring R], ↑⊤ = Set.univ
-- Mathlib.Data.ENNReal.Operations
/-- This is a special case of `WithTop.sub_top` in the `ENNReal` namespace  -/
ENNReal.sub_top : ∀ {a : ENNReal}, a - ⊤ = 0
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.insertMany_nil : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp}, t.insertMany [] = t
-- Mathlib.LinearAlgebra.Dimension.RankNullity
/-- Given a nonzero vector in a finite-dimensional space of dimension `> 1`, one may find another
vector linearly independent of the first one.  -/
exists_linearIndependent_pair_of_one_lt_finrank : ∀ {R : Type u_1} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [HasRankNullity.{u, u_1} R] [StrongRankCondition R] [IsDomain R] [Module.IsTorsionFree R M],
  1 < Module.finrank R M → ∀ {x : M}, x ≠ 0 → ∃ y, LinearIndependent R ![x, y]
-- Lean.Elab.Tactic.Rewrite
Lean.Elab.Tactic.evalRewriteSeq : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.DirectSum.Basic
DirectSum.coe_of_apply : ∀ {ι : Type v} {M : Type u_1} {S : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike S M]
  [inst_3 : AddSubmonoidClass S M] {A : ι → S} (i j : ι) (x : ↥(A i)),
  ↑(((DirectSum.of (fun i => ↥(A i)) i) x) j) = ↑(if i = j then x else 0)
-- Mathlib.Topology.Algebra.Group.Pointwise
IsClosed.mul_right_of_isCompact : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {s t : Set G},
  IsClosed t → IsCompact s → IsClosed (t * s)
-- Mathlib.Order.RelClasses
/-- Construct a partial order from an `isStrictOrder` relation.

See note [reducible non-instances].  -/
partialOrderOfSO : {α : Type u} → (r : α → α → Prop) → [IsStrictOrder α r] → PartialOrder α
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Composition of graph embeddings.  -/
SimpleGraph.Embedding.comp : {V : Type u_1} →
  {W : Type u_2} →
    {X : Type u_3} → {G : SimpleGraph V} → {G' : SimpleGraph W} → {G'' : SimpleGraph X} → G' ↪g G'' → G ↪g G' → G ↪g G''
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.Path.interval.congr_simp : ∀ {X : SSet} {n : ℕ} (f f_1 : X.Path n),
  f = f_1 → ∀ (j j_1 : ℕ) (e_j : j = j_1) (l : ℕ) (h : j + l ≤ n), f.interval j l h = f_1.interval j_1 l ⋯
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Limits.biproduct.reindex_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {β γ : Type}
  [inst_2 : Finite β] (ε : β ≃ γ) (f : γ → C) [inst_3 : CategoryTheory.Limits.HasBiproduct f]
  [inst_4 : CategoryTheory.Limits.HasBiproduct (f ∘ ⇑ε)],
  (CategoryTheory.Limits.biproduct.reindex ε f).inv =
    CategoryTheory.Limits.biproduct.lift fun b => CategoryTheory.Limits.biproduct.π f (ε b)
-- Std.Data.TreeSet.Raw.Basic
/-- Tries to retrieve the smallest element that is less than the given element,
returning `fallback` if no such element exists.
 -/
Std.TreeSet.Raw.getLTD : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → α → α → α
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mul.go.induct_unfolding : ∀ (motive : ℕ → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Prop),
  (∀ (m₁ m₂ : Lean.Grind.CommRing.Mon), motive 0 m₁ m₂ (m₁.concat m₂)) →
    (∀ (fuel : ℕ) (m₁ : Lean.Grind.CommRing.Mon), motive fuel.succ m₁ Lean.Grind.CommRing.Mon.unit m₁) →
      (∀ (fuel : ℕ) (m₂ : Lean.Grind.CommRing.Mon),
          (m₂ = Lean.Grind.CommRing.Mon.unit → False) → motive fuel.succ Lean.Grind.CommRing.Mon.unit m₂ m₂) →
        (∀ (fuel : ℕ) (pw₁ : Lean.Grind.CommRing.Power) (m₁ : Lean.Grind.CommRing.Mon) (pw₂ : Lean.Grind.CommRing.Power)
            (m₂ : Lean.Grind.CommRing.Mon),
            pw₁.varLt pw₂ = true →
              motive fuel m₁ (Lean.Grind.CommRing.Mon.mult pw₂ m₂)
                  (Lean.Grind.CommRing.Mon.mul.go fuel m₁ (Lean.Grind.CommRing.Mon.mult pw₂ m₂)) →
                motive fuel.succ (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)
                  (Lean.Grind.CommRing.Mon.mult pw₁
                    (Lean.Grind.CommRing.Mon.mul.go fuel m₁ (Lean.Grind.CommRing.Mon.mult pw₂ m₂)))) →
          (∀ (fuel : ℕ) (pw₁ : Lean.Grind.CommRing.Power) (m₁ : Lean.Grind.CommRing.Mon)
              (pw₂ : Lean.Grind.CommRing.Power) (m₂ : Lean.Grind.CommRing.Mon),
              pw₁.varLt pw₂ = false →
                pw₂.varLt pw₁ = true →
                  motive fuel (Lean.Grind.CommRing.Mon.mult pw₁ m₁) m₂
                      (Lean.Grind.CommRing.Mon.mul.go fuel (Lean.Grind.CommRing.Mon.mult pw₁ m₁) m₂) →
                    motive fuel.succ (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)
                      (Lean.Grind.CommRing.Mon.mult pw₂
                        (Lean.Grind.CommRing.Mon.mul.go fuel (Lean.Grind.CommRing.Mon.mult pw₁ m₁) m₂))) →
            (∀ (fuel : ℕ) (pw₁ : Lean.Grind.CommRing.Power) (m₁ : Lean.Grind.CommRing.Mon)
                (pw₂ : Lean.Grind.CommRing.Power) (m₂ : Lean.Grind.CommRing.Mon),
                pw₁.varLt pw₂ = false →
                  pw₂.varLt pw₁ = false →
                    motive fuel m₁ m₂ (Lean.Grind.CommRing.Mon.mul.go fuel m₁ m₂) →
                      motive fuel.succ (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)
                        (Lean.Grind.CommRing.Mon.mult { x := pw₁.x, k := pw₁.k + pw₂.k }
                          (Lean.Grind.CommRing.Mon.mul.go fuel m₁ m₂))) →
              ∀ (fuel : ℕ) (m₁ m₂ : Lean.Grind.CommRing.Mon),
                motive fuel m₁ m₂ (Lean.Grind.CommRing.Mon.mul.go fuel m₁ m₂)
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- Construct an adjunction from the data of a `CoreHomEquivUnitCounit`, i.e. a hom set
equivalence, unit and counit natural transformations together with proofs of the equalities
`homEquiv_unit` and `homEquiv_counit` relating them to each other.
 -/
CategoryTheory.Adjunction.mk' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} → CategoryTheory.Adjunction.CoreHomEquivUnitCounit F G → (F ⊣ G)
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.instHasLimitsOfSizeOver : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C)
  [CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₁, u₁} C],
  CategoryTheory.Limits.HasLimitsOfSize.{w, w', v₁, max u₁ v₁} (CategoryTheory.Over X)
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.evalIntExprCore : Lean.Expr → Lean.MetaM ℤ
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.le_span_singleton_iff : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Submodule R M}
  {v₀ : M}, s ≤ R ∙ v₀ ↔ ∀ v ∈ s, ∃ r, r • v₀ = v
-- Mathlib.CategoryTheory.Limits.Types.Colimits
/-- If `F : J ⥤ Type u`, then the data of a "type-theoretic" cocone of `F`
with a point in `Type u` is the same as the data of a cocone (in a categorical sense).  -/
CategoryTheory.Functor.coconeTypesEquiv : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J (Type u)) → F.CoconeTypes ≃ CategoryTheory.Limits.Cocone F
-- Mathlib.Order.UpperLower.Basic
IsUpperSet.top_notMem : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [inst_1 : OrderTop α], IsUpperSet s → (⊤ ∉ s ↔ s = ∅)
-- Mathlib.Data.Sym.Sym2
Sym2.other_mem' : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {z : Sym2 α} (h : a ∈ z), Sym2.Mem.other' h ∈ z
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.addCommGroup : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → {N : LieSubmodule R L M} → AddCommGroup (M ⧸ N)
-- Mathlib.Tactic.FunProp.Types
/-- Maximum number of transitions between function properties. For example inferring continuity
from differentiability and then differentiability from smoothness (`ContDiff ℝ ∞`) requires
`maxTransitionDepth = 2`. The default value of one expects that transition theorems are
transitively closed e.g. there is a transition theorem that infers continuity directly from
smoothness.

Setting `maxTransitionDepth` to zero will disable all transition theorems. This can be very
useful when `fun_prop` should fail quickly. For example when using `fun_prop` as discharger in
`simp`.
 -/
Mathlib.Meta.FunProp.Config.maxTransitionDepth : Mathlib.Meta.FunProp.Config → ℕ
-- Mathlib.Util.Notation3
Mathlib.Notation3.DelabKey.app.inj : ∀ {const : Option Lean.Name} {arity : ℕ} {const_1 : Option Lean.Name} {arity_1 : ℕ},
  Mathlib.Notation3.DelabKey.app const arity = Mathlib.Notation3.DelabKey.app const_1 arity_1 →
    const = const_1 ∧ arity = arity_1
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Real.nndist_eq' : ∀ (x y : ℝ), nndist x y = Real.nnabs (y - x)
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_comp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (w : C) {x y z : D} (f : x ⟶ y) (g : y ⟶ z),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight w (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight w f)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight w g)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.ConsumerNode.subgoals : Lean.Meta.SynthInstance.ConsumerNode → List Lean.Expr
-- Mathlib.Data.Finset.Sups
Finset.disjSups_assoc : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DistribLattice α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] (s t u : Finset α), (s.disjSups t).disjSups u = s.disjSups (t.disjSups u)
-- Init.Data.String.Lemmas.Iterate
String.Slice.revChars.eq_1 : ∀ (s : String.Slice),
  s.revChars =
    Std.Iter.map
      (fun x =>
        match x with
        | ⟨pos, h⟩ => pos.get h)
      s.revPositions
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- An arbitrary choice of biproduct of a pair of objects.  -/
CategoryTheory.Limits.biprod : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → (X Y : C) → [CategoryTheory.Limits.HasBinaryBiproduct X Y] → C
-- Mathlib.MeasureTheory.Integral.Bochner.SumMeasure
/-- **Alias** of `MeasureTheory.integral_countable`. -/
MeasureTheory.integral_countable' : ∀ {X : Type u_2} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] {f : X → E}
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [MeasurableSingletonClass X] {μ : MeasureTheory.Measure X} [Countable X],
  MeasureTheory.Integrable f μ → ∫ (x : X), f x ∂μ = ∑' (x : X), μ.real {x} • f x
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- One of two vectors is zero or the oriented angle between them is plus or minus `π / 2` if
and only if the inner product of those vectors is zero.  -/
Orientation.eq_zero_or_oangle_eq_iff_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V},
  x = 0 ∨ y = 0 ∨ o.oangle x y = ↑(Real.pi / 2) ∨ o.oangle x y = ↑(-Real.pi / 2) ↔ inner ℝ x y = 0
-- Mathlib.Analysis.LocallyConvex.Separation
/-- A closed convex set is the intersection of the half-spaces containing it.  -/
iInter_halfSpaces_eq : ∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [inst_2 : Module ℝ E] {s : Set E}
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E],
  Convex ℝ s → IsClosed s → ⋂ l, {x | ∃ y ∈ s, l x ≤ l y} = s
-- Mathlib.MeasureTheory.Measure.AEDisjoint
Set.PairwiseDisjoint.aedisjoint : ∀ {ι : Type u_1} {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ι → Set α} {s : Set ι},
  s.PairwiseDisjoint f → s.Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) f)
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.forget₂_commBialgCat_map : ∀ {R : Type u} [inst : CommRing R] {A B : CommHopfAlgCat R} (f : A ⟶ B),
  (CategoryTheory.forget₂ (CommHopfAlgCat R) (CommBialgCat R)).map f = CommBialgCat.ofHom (CommHopfAlgCat.Hom.hom f)
-- Mathlib.RingTheory.Noetherian.Defs
/-- `IsNoetherian R M` is the proposition that `M` is a Noetherian `R`-module,
implemented as the predicate that all `R`-submodules of `M` are finitely generated.
 -/
IsNoetherian.noetherian : ∀ {R : Type u_1} {M : Type u_2} {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M}
  [self : IsNoetherian R M] (s : Submodule R M), s.FG
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.isDiameter_iff_mem_and_mem_and_wbtw : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  s.IsDiameter p₁ p₂ ↔ p₁ ∈ s ∧ p₂ ∈ s ∧ Wbtw ℝ p₁ s.center p₂
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.ArchimedeanStrata.mk.injEq : ∀ {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] (stratum : FiniteArchimedeanClass M → Submodule K M)
  (disjoint_ball_stratum : ∀ (c : FiniteArchimedeanClass M), Disjoint (FiniteArchimedeanClass.ball K c) (stratum c))
  (ball_sup_stratum_eq :
    ∀ (c : FiniteArchimedeanClass M),
      FiniteArchimedeanClass.ball K c ⊔ stratum c = FiniteArchimedeanClass.closedBall K c)
  (stratum_1 : FiniteArchimedeanClass M → Submodule K M)
  (disjoint_ball_stratum_1 : ∀ (c : FiniteArchimedeanClass M), Disjoint (FiniteArchimedeanClass.ball K c) (stratum_1 c))
  (ball_sup_stratum_eq_1 :
    ∀ (c : FiniteArchimedeanClass M),
      FiniteArchimedeanClass.ball K c ⊔ stratum_1 c = FiniteArchimedeanClass.closedBall K c),
  ({ stratum := stratum, disjoint_ball_stratum := disjoint_ball_stratum, ball_sup_stratum_eq := ball_sup_stratum_eq } =
      { stratum := stratum_1, disjoint_ball_stratum := disjoint_ball_stratum_1,
        ball_sup_stratum_eq := ball_sup_stratum_eq_1 }) =
    (stratum = stratum_1)
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- If `f` is a morphism `X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂` whose `X₁ ⟶ Y₁` entry is an isomorphism,
then we can construct isomorphisms `L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂` and `R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂`
so that `L.hom ≫ g ≫ R.hom` is diagonal (with `X₁ ⟶ Y₁` component still `f`),
via Gaussian elimination.

(This is the version of `Biprod.gaussian` written in terms of components.)
 -/
CategoryTheory.Biprod.gaussian' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {X₁ X₂ Y₁ Y₂ : C} →
          (f₁₁ : X₁ ⟶ Y₁) →
            (f₁₂ : X₁ ⟶ Y₂) →
              (f₂₁ : X₂ ⟶ Y₁) →
                (f₂₂ : X₂ ⟶ Y₂) →
                  [CategoryTheory.IsIso f₁₁] →
                    (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) ×'
                      (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) ×'
                        (g₂₂ : X₂ ⟶ Y₂) ×'
                          CategoryTheory.CategoryStruct.comp L.hom
                              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂)
                                R.hom) =
                            CategoryTheory.Limits.biprod.map f₁₁ g₂₂
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.PolyCnstr.mk.inj : ∀ {eq : Bool} {lhs rhs : Nat.Internal.Linear.Poly} {eq_1 : Bool} {lhs_1 rhs_1 : Nat.Internal.Linear.Poly},
  { eq := eq, lhs := lhs, rhs := rhs } = { eq := eq_1, lhs := lhs_1, rhs := rhs_1 } →
    eq = eq_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.norm_embedding_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (w : NumberField.FinitePlace K) (x : K),
  ‖(NumberField.FinitePlace.embedding w.maximalIdeal) x‖ = w x
-- Init.Data.List.MapIdx
/-- Applies a monadic function to each element of the list along with the index at which that element is
found, returning the list of results.

`List.mapFinIdxM` is a variant that additionally provides the function with a proof that the index
is valid.
 -/
List.mapIdxM : {m : Type u_1 → Type u_2} → {α : Type u_3} → {β : Type u_1} → [Monad m] → (ℕ → α → m β) → List α → m (List β)
-- Mathlib.RingTheory.ClassGroup.Basic
/-- A fractional ideal is a unit iff its integral numerator `num` is a unit.  -/
FractionalIdeal.isUnit_num : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {I : FractionalIdeal (nonZeroDivisors R) (FractionRing R)},
  IsUnit ↑I.num ↔ IsUnit I
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.trans_symm_eq_symm_trans_symm : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) (e' : OpenPartialHomeomorph Y Z),
  (e.trans e').symm = e'.symm.trans e.symm
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_maxKey?_modify_eq_isSome : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : β → β}, (t.modify k f).maxKey?.isSome = t.maxKey?.isSome
-- Mathlib.CategoryTheory.GuitartExact.Opposite
CategoryTheory.TwoSquare.instGuitartExactOppositeOp : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w : CategoryTheory.TwoSquare T L R B)
  [w.GuitartExact], w.op.GuitartExact
-- Init.Data.Vector.Find
Vector.findSomeRev?_push_of_isSome : ∀ {α : Type u_1} {n : ℕ} {α_1 : Type u_2} {f : α → Option α_1} {a : α} {xs : Vector α n} {h : (f a).isSome = true},
  Vector.findSomeRev? f (xs.push a) = f a
-- Lean.Data.Json.Basic
Lean.Json.obj : Std.TreeMap.Raw String Lean.Json compare → Lean.Json
-- Mathlib.Topology.VectorBundle.Basic
/-- The projection from the total space of a fiber bundle core, on its base.  -/
VectorBundleCore.proj : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace R F] →
            [inst_3 : TopologicalSpace B] →
              {ι : Type u_5} → (Z : VectorBundleCore R B F ι) → Bundle.TotalSpace F Z.Fiber → B
-- Mathlib.Analysis.SpecialFunctions.Complex.Analytic
/-- `f z ^ g z` is analytic if `f z` is not a nonpositive real  -/
AnalyticAt.cpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f g : E → ℂ} {x : E},
  AnalyticAt ℂ f x → AnalyticAt ℂ g x → f x ∈ Complex.slitPlane → AnalyticAt ℂ (fun z => f z ^ g z) x
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.uniformContinuous_withVal_equiv : ∀ {K : Type u_2} [inst : Field K], UniformContinuous ⇑(WithVal.equiv (RatFunc.polynomialValuationX K))
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
instSubsingletonUniformOnFun : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [Subsingleton β], Subsingleton (UniformOnFun α β 𝔖)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
Units.mul_inv_le_iff : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulRightMono M] {a b : M} (u : Mˣ), a * ↑u⁻¹ ≤ b ↔ a ≤ b * ↑u
-- Mathlib.Analysis.Convex.Quasiconvex
QuasiconvexOn.convex : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LE β] [inst_4 : SMul 𝕜 E] {s : Set E} {f : E → β} [IsDirectedOrder β], QuasiconvexOn 𝕜 s f → Convex 𝕜 s
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_liftWith_refl_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α : Type u}
  {post : α → Pred} {epost : EPred} [inst_4 : Pure m] (f : ({β : Type u} → m β → m β) → m α),
  Std.Internal.Do.wp (liftWith f) post epost = Std.Internal.Do.wp (f fun {β} x => x) post epost
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofIso_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h : S₁.HomologyData),
  (CategoryTheory.ShortComplex.HomologyData.ofIso e h).iso = h.iso
-- Mathlib.Analysis.Meromorphic.Complex
MeromorphicNFOn.Gamma : MeromorphicNFOn Complex.Gamma Set.univ