mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Distributions.TwoValued
/-- If a random variable is ae equal to `0` or `1`, then one minus its expectation is equal to the
probability that it equals `0`.  -/
MeasureTheory.integral_one_sub_of_ae_eq_zero_or_one : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  AEMeasurable X μ → (∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) → ∫ (ω : Ω), 1 - X ω ∂μ = μ.real {ω | X ω = 0}
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
CategoryTheory.Limits.PreservesPullback.iso_inv_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) G]
  [inst_3 : CategoryTheory.Limits.HasPullback f g] [inst_4 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)]
  {Z_1 : D} (h : G.obj Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PreservesPullback.iso G f g).inv
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pullback.snd f g)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (G.map f) (G.map g)) h
-- Init.Data.SInt.Lemmas
Int32.toInt8_add : ∀ (a b : Int32), (a + b).toInt8 = a.toInt8 + b.toInt8
-- Mathlib.Data.Semiquot
Semiquot.ext : ∀ {α : Type u_1} {q₁ q₂ : Semiquot α}, q₁ = q₂ ↔ ∀ (a : α), a ∈ q₁ ↔ a ∈ q₂
-- Mathlib.GroupTheory.Coset.Basic
/-- An equivalence between any fiber of a surjective `AddMonoidHom` and its kernel.  -/
AddMonoidHom.fiberEquivKerOfSurjective : {α : Type u_1} →
  [inst : AddGroup α] →
    {H : Type u_2} → [inst_1 : AddGroup H] → {f : α →+ H} → Function.Surjective ⇑f → (h : H) → ↑(⇑f ⁻¹' {h}) ≃ ↥f.ker
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N →ₗ[R] P) (m : M) (n : N), (LinearMap.lTensor M f) (m ⊗ₜ[R] n) = m ⊗ₜ[R] f n
-- Std.Http.Data.Headers.Basic
Std.Http.Header.instReprExpect : Repr Std.Http.Header.Expect
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Not
Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastNot : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (target : aig.RefVec w)
  (assign : α → Bool) (idx : ℕ) (hidx : idx < w),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastNot aig target).aig,
        ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastNot aig target).vec.get idx hidx }⟧ =
    !⟦assign, { aig := aig, ref := target.get idx hidx }⟧
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_self_sub_tmod : ∀ {x m : ℤ}, m ∣ x - x.tmod m
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
GenContFract.le_of_succ_succ_get?_contsAux_b : ∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : FloorRing K] {b : K},
  (GenContFract.of v).partDens.get? n = some b →
    b * ((GenContFract.of v).contsAux (n + 1)).b ≤ ((GenContFract.of v).contsAux (n + 2)).b
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsRat.den_nz : ∀ {α : Type u_1} [inst : DivisionRing α] {a : α} {n : ℤ} {d : ℕ}, Mathlib.Meta.NormNum.IsRat a n d → ↑d ≠ 0
-- Mathlib.Topology.Algebra.Module.FiniteDimension
isClosedMap_smul_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] [inst_5 : Module 𝕜 E] [ContinuousSMul 𝕜 E] [T2Space E]
  (c : E), IsClosedMap fun x => x • c
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_prodMk_left : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {x : α}, Measurable (Prod.mk x)
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.term_eq : ∀ {α : Type u_1} [inst : AddCommMonoid α] (n : ℕ) (x a : α), Mathlib.Tactic.Abel.term n x a = n • x + a
-- Mathlib.Analysis.Convex.Caratheodory
Caratheodory.mem_minCardFinsetOfMemConvexHull : ∀ {𝕜 : Type u_1} {E : Type u} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s : Set E} {x : E} (hx : x ∈ (convexHull 𝕜) s),
  x ∈ (convexHull 𝕜) ↑(Caratheodory.minCardFinsetOfMemConvexHull hx)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableAt_iff_target_of_mem_source : ∀ {𝕜 : 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'} [IsManifold I' 1 M']
  {x : M} {y : M'}, f x ∈ (chartAt H' y).source → (MDiffAt f x ↔ ContinuousAt f x ∧ MDiffAt (↑(extChartAt I' y) ∘ f) x)
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- A predicate class on a ring extension saying that there is a natural number `e`
such that `a ^ ringExpChar K ^ e ∈ K` for all `a ∈ L`.  -/
IsPurelyInseparable.HasExponent : (K : Type u_2) → (L : Type u_3) → [inst : CommRing K] → [inst_1 : Ring L] → [Algebra K L] → Prop
-- Mathlib.Data.Seq.Computation
_private.Mathlib.Data.Seq.Computation.0.Computation.Corec.f.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : α ⊕ β → Sort u_3) →
      (x : α ⊕ β) → ((a : α) → motive (Sum.inl a)) → ((val : β) → motive (Sum.inr val)) → motive x
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_eq_of_mem_finset : ∀ {Ω : Type u_1} {ι : Type u_3} [inst : Nonempty ι] {τ : Ω → WithTop ι} {E : Type u_4} {u : ι → Ω → E}
  [inst_1 : LinearOrder ι] [inst_2 : AddCommMonoid E] {s : Finset ι} (n : ι),
  (∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s) →
    MeasureTheory.stoppedProcess u τ n =
      {a | ↑n ≤ τ a}.indicator (u n) + ∑ i ∈ s with i < n, {ω | τ ω = ↑i}.indicator (u i)
-- Mathlib.FieldTheory.IntermediateField.ExtendRight
IntermediateField.extendRight.instIsScalarTowerSubtypeMem_1 : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L)
  (M : Type u_3) [inst_3 : Field M] [inst_4 : Algebra K M] [inst_5 : Algebra L M] [inst_6 : IsScalarTower K L M]
  {S : Type u_5} [inst_7 : CommRing S] [inst_8 : Algebra S ↥F] [inst_9 : Algebra S M]
  [inst_10 : IsScalarTower S (↥F) M], IsScalarTower S ↥F ↥(F.extendRight M)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The triangle consisting of the two natural transformations and `hom` commutes  -/
CategoryTheory.Limits.BinaryBiconeMorphism.wsnd_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} {A B : CategoryTheory.Limits.BinaryBicone P Q} (self : CategoryTheory.Limits.BinaryBiconeMorphism A B)
  {Z : C} (h : Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.hom (CategoryTheory.CategoryStruct.comp B.snd h) =
    CategoryTheory.CategoryStruct.comp A.snd h
-- Mathlib.Data.Finset.NoncommProd
/-- Sum of a `s : Multiset α` with `[AddMonoid α]`, given a proof that `+` commutes
on all elements `x ∈ s`.  -/
Multiset.noncommSum : {α : Type u_3} → [inst : AddMonoid α] → (s : Multiset α) → {x | x ∈ s}.Pairwise AddCommute → α
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_left_le_size_union : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → t₁.size ≤ (t₁ ∪ t₂).size
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
/-- Constructor for `RestrictedProduct`.  -/
RestrictedProduct.mk : {ι : Type u_1} →
  {R : ι → Type u_2} →
    {A : (i : ι) → Set (R i)} →
      {𝓕 : Filter ι} →
        (x : (i : ι) → R i) → (∀ᶠ (i : ι) in 𝓕, x i ∈ A i) → RestrictedProduct (fun i => R i) (fun i => A i) 𝓕
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.isWide_iff_objs_eq_univ : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C), S.IsWide ↔ S.objs = Set.univ
-- Mathlib.CategoryTheory.Limits.Creates
/-- When `F` is fully faithful, and `HasColimit (K ⋙ F)`, to show that `F` creates the colimit for `K`
it suffices to exhibit a lift of the chosen colimit cocone for `K ⋙ F`.
 -/
CategoryTheory.createsColimitOfFullyFaithfulOfLift : {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 : CategoryTheory.Functor C D} →
                [F.Full] →
                  [F.Faithful] →
                    [inst_5 : CategoryTheory.Limits.HasColimit (K.comp F)] →
                      (c : CategoryTheory.Limits.Cocone K) →
                        (F.mapCocone c ≅ CategoryTheory.Limits.colimit.cocone (K.comp F)) →
                          CategoryTheory.CreatesColimit K F
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero
SSet.π₀.fromChainComplexXZero.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C),
  SSet.π₀.fromChainComplexXZero X R = (CategoryTheory.Limits.sigmaConst.obj R).map (TypeCat.ofHom SSet.π₀.mk)
-- Mathlib.Logic.Equiv.Functor
Bifunctor.mapEquiv_apply : ∀ {α β : Type u} {α' β' : Type v} (F : Type u → Type v → Type w) [inst : Bifunctor F] [inst_1 : LawfulBifunctor F]
  (h : α ≃ β) (h' : α' ≃ β') (x : F α α'), (Bifunctor.mapEquiv F h h') x = bimap (⇑h) (⇑h') x
-- Init.Data.List.Lemmas
List.flatMap_eq_foldl : ∀ {α : Type u_1} {β : Type u_2} {f : α → List β} {l : List α},
  List.flatMap f l = List.foldl (fun acc a => acc ++ f a) [] l
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.FullyFaithful.addGrpObj_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] (hF : F.FullyFaithful) (X : C)
  [inst_5 : CategoryTheory.AddGrpObj (F.obj X)],
  CategoryTheory.AddMonObj.zero =
    hF.preimage
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F) CategoryTheory.AddMonObj.zero)
-- Init.Control.Lawful.Basic
id_map' : ∀ {f : Type u_1 → Type u_2} {α : Type u_1} [inst : Functor f] [LawfulFunctor f] (x : f α), (fun a => a) <$> x = x
-- Mathlib.Order.CompleteBooleanAlgebra
/-- Pullback an `Order.Coframe.MinimalAxioms` along a function.  -/
Function.coframeMinimalAxioms : ∀ {α : Type u} {β : Type v} [inst : CompleteLattice α] [inst_1 : CompleteLattice β],
  Order.Coframe.MinimalAxioms β →
    ∀ (f : α → β),
      (∀ {x y : α}, f y ≤ f x ↔ y ≤ x) →
        (∀ (a b : α), f (a ⊔ b) = f a ⊔ f b) →
          (∀ (s : Set α), f (sInf s) = ⨅ a ∈ s, f a) → Order.Coframe.MinimalAxioms α
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.coeff_k_eq_coeff : ∀ (p : Int.Internal.Linear.Poly) (x : Int.Internal.Linear.Var), p.coeff_k x = p.coeff x
-- Lean.Server.FileWorker.RequestHandling
_private.Lean.Server.FileWorker.RequestHandling.0.Lean.Server.FileWorker.handleFoldingRange.addCommandRange : Lean.FileMap → Lean.Syntax → StateT (Array Lean.Lsp.FoldingRange) Lean.Server.RequestM Unit
-- Mathlib.Combinatorics.Matroid.IndepAxioms
/-- An `M : IndepMatroid α` gives a `Matroid α` whose bases are the maximal `M`-independent sets.  -/
IndepMatroid.matroid : {α : Type u_1} → IndepMatroid α → Matroid α
-- Mathlib.Analysis.Normed.Group.AddTorsor
instNormedAddTorsorProd : {V : Type u_2} →
  {P : Type u_3} →
    {W : Type u_4} →
      {Q : Type u_5} →
        [inst : SeminormedAddCommGroup V] →
          [inst_1 : PseudoMetricSpace P] →
            [NormedAddTorsor V P] →
              [inst_3 : SeminormedAddCommGroup W] →
                [inst_4 : PseudoMetricSpace Q] → [NormedAddTorsor W Q] → NormedAddTorsor (V × W) (P × Q)
-- Batteries.Data.Float.Lemmas
/-- Boolean equality on `Float32`s is symmetric and transitive, but not reflexive, as demonstrated
by `nan != nan`.
 -/
instPartialEquivBEqFloat32_batteries : PartialEquivBEq Float32
-- Mathlib.Algebra.Group.Basic
/-- Variant of `mul_eq_one_iff_eq_inv` with swapped equality.  -/
mul_eq_one_iff_eq_inv' : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a * b = 1 ↔ b = a⁻¹
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.inter_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ m₃ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF), m₂.WF → m₃.WF → m₂.Equiv m₃ → (m₁.inter m₂ ⋯).Equiv (m₁.inter m₃ ⋯)
-- Lean.Meta.ReduceEval
Lean.Meta.instReduceEvalLiteral : Lean.Meta.ReduceEval Lean.Literal
-- Init.Data.Option.Instances
Option.instDecidableMemOfDecidableEq : {α : Type u_1} → [DecidableEq α] → (j : α) → (o : Option α) → Decidable (j ∈ o)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Answer.resultType : Lean.Meta.SynthInstance.Answer → Lean.Expr
-- Mathlib.LinearAlgebra.Semisimple
Module.End.IsSemisimple.of_mem_adjoin_pair : ∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_1 : Field K] [inst_2 : Module K M] {f g : Module.End K M}
  [FiniteDimensional K M] [PerfectField K],
  Commute f g → f.IsSemisimple → g.IsSemisimple → ∀ {a : Module.End K M}, a ∈ K[f, g] → a.IsSemisimple
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.alter_eq_empty_iff_erase_eq_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β},
  Std.ExtDHashMap.Const.alter m k f = ∅ ↔ m.erase k = ∅ ∧ f (Std.ExtDHashMap.Const.get? m k) = none
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.equivMapOfInjective.eq_1 : ∀ {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.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑H) hf, map_mul' := ⋯ }
-- Mathlib.Algebra.Group.Subgroup.Ker
/-- Computable alternative to `MonoidHom.ofInjective`.  -/
MonoidHom.ofLeftInverse : {G : Type u_1} →
  [inst : Group G] →
    {N : Type u_5} → [inst_1 : Group N] → {f : G →* N} → {g : N →* G} → Function.LeftInverse ⇑g ⇑f → G ≃* ↥f.range
-- Mathlib.Util.Superscript
/-- Formatter for the subscript parser.  -/
Mathlib.Tactic.subscript.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- Equality of elements of `AutGalois F` can be checked on the projections on each pointed
Galois object.  -/
CategoryTheory.PreGaloisCategory.AutGalois.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) {f g : CategoryTheory.PreGaloisCategory.AutGalois F},
  (∀ (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F),
      (CategoryTheory.PreGaloisCategory.AutGalois.π F A) f = (CategoryTheory.PreGaloisCategory.AutGalois.π F A) g) →
    f = g
-- Std.Data.DHashMap.Raw
Std.DHashMap.Internal.Raw₀.getThenInsertIfNew?.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (m m_1 : Std.DHashMap.Internal.Raw₀ α β),
  m = m_1 → ∀ (a : α) (b b_1 : β a), b = b_1 → m.getThenInsertIfNew? a b = m_1.getThenInsertIfNew? a b_1
-- Mathlib.Algebra.Order.Group.Ideal
/-- A canonically ordered and well-quasi-ordered additive monoid, the semigroup ideals
satisfy the ascending chain condition.  -/
AddSemigroupIdeal.instWellFoundedGT : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [WellQuasiOrderedLE M] [CanonicallyOrderedAdd M],
  WellFoundedGT (AddSemigroupIdeal M)
-- Mathlib.Data.Set.Lattice
Set.sUnion_eq_biUnion : ∀ {α : Type u_1} {s : Set (Set α)}, ⋃₀ s = ⋃ i ∈ s, i
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.bilinearComp_zero_left : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  {E' : Type u_11} {F' : Type u_12} [inst_9 : SeminormedAddCommGroup E'] [inst_10 : SeminormedAddCommGroup F']
  {𝕜₁' : Type u_13} {𝕜₂' : Type u_14} [inst_11 : NontriviallyNormedField 𝕜₁'] [inst_12 : NontriviallyNormedField 𝕜₂']
  [inst_13 : NormedSpace 𝕜₁' E'] [inst_14 : NormedSpace 𝕜₂' F'] {σ₁' : 𝕜₁' →+* 𝕜} {σ₁₃' : 𝕜₁' →+* 𝕜₃} {σ₂' : 𝕜₂' →+* 𝕜₂}
  {σ₂₃' : 𝕜₂' →+* 𝕜₃} [inst_15 : RingHomCompTriple σ₁' σ₁₃ σ₁₃'] [inst_16 : RingHomCompTriple σ₂' σ₂₃ σ₂₃']
  [inst_17 : RingHomIsometric σ₂₃] [inst_18 : RingHomIsometric σ₁₃'] [inst_19 : RingHomIsometric σ₂₃']
  {f : E →SL[σ₁₃] F →SL[σ₂₃] G} {gF : F' →SL[σ₂'] F}, f.bilinearComp 0 gF = 0
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.instInhabitedAuxLemmas.default : Lean.Meta.AuxLemmas
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.biUnion_top : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), (π.biUnion fun x => ⊤) = π
-- Mathlib.Data.Finset.Sigma
Finset.disjiUnion_map_sigma_mk : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Finset ι} {t : (i : ι) → Finset (α i)},
  s.disjiUnion (fun i => Finset.map (Function.Embedding.sigmaMk i) (t i)) ⋯ = s.sigma t
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron'.mem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : Z₁₂ ⟶ X₁}
  {w₁₂ : X₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₂}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk v₁₂ u₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : Z₂₃ ⟶ X₂} {w₂₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₂₃}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk v₂₃ u₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : Z₁₃ ⟶ X₁} {w₁₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj Z₁₃}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk v₁₃ u₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (self : CategoryTheory.Triangulated.Octahedron' comm h₁₂ h₂₃ h₁₃),
  CategoryTheory.Pretriangulated.Triangle.mk self.m₁ self.m₃ (CategoryTheory.CategoryStruct.comp v₂₃ w₁₂) ∈
    CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionSemiHomClass.toAddMonoidHomClass : ∀ {F : Type u_10} {M : outParam (Type u_11)} {N : outParam (Type u_12)} {φ : outParam (M → N)}
  {A : outParam (Type u_13)} {B : outParam (Type u_14)} {inst : Monoid M} {inst_1 : Monoid N} {inst_2 : AddMonoid A}
  {inst_3 : AddMonoid B} {inst_4 : DistribMulAction M A} {inst_5 : DistribMulAction N B} {inst_6 : FunLike F A B}
  [self : DistribMulActionSemiHomClass F φ A B], AddMonoidHomClass F A B
-- Mathlib.Analysis.Normed.Ring.Basic
NonUnitalSeminormedRing.mk : {α : Type u_5} →
  [toNorm : Norm α] →
    [toNonUnitalRing : NonUnitalRing α] →
      [toPseudoMetricSpace : PseudoMetricSpace α] →
        (∀ (x y : α), dist x y = ‖-x + y‖) → (∀ (a b : α), ‖a * b‖ ≤ ‖a‖ * ‖b‖) → NonUnitalSeminormedRing α
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- When `m` and `n` are odd, then the square of `qrSign m n` is `1`.  -/
qrSign.sq_eq_one : ∀ {m n : ℕ}, Odd m → Odd n → qrSign m n ^ 2 = 1
-- Mathlib.Data.Nat.Choose.Factorization
/-- The factorization of `p` in `choose (n + k) k` is the number of carries when `k` and `n` are
added in base `p`. The set is expressed by filtering `Ico 1 b` where `b` is any bound greater
than `log p (n + k)`.  -/
Nat.factorization_choose' : ∀ {p n k b : ℕ},
  Nat.Prime p →
    Nat.log p (n + k) < b →
      ((n + k).choose k).factorization p = {i ∈ Finset.Ico 1 b | p ^ i ≤ k % p ^ i + n % p ^ i}.card
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.instFullOppositeIdealSheafDataOverSubschemeFunctor : ∀ {Y : AlgebraicGeometry.Scheme}, (AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctor Y).Full
-- Mathlib.CategoryTheory.Abelian.Transfer
CategoryTheory.AsSmall.instAdditiveDown : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C],
  CategoryTheory.AsSmall.down.Additive
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.VectorsProdEqOne.one_eq : ∀ (G : Type u_2) [inst : Group G], Equiv.Perm.vectorsProdEqOne G 1 = {1 ::ᵥ List.Vector.nil}
-- Init.Data.UInt.Lemmas
UInt8.not_lt : ∀ {a b : UInt8}, ¬a < b ↔ b ≤ a
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α} {k : α} (mem : k ∈ m)
  {h : k ∈ Std.ExtDHashMap.Const.insertManyIfNewUnit m l},
  (Std.ExtDHashMap.Const.insertManyIfNewUnit m l).getKey k h = m.getKey k mem
-- Mathlib.Order.Filter.NAry
Filter.map₂_eq_bot_iff : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {m : α → β → γ} {f : Filter α} {g : Filter β},
  Filter.map₂ m f g = ⊥ ↔ f = ⊥ ∨ g = ⊥
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
/-- When `L : C ⥤ D` is a localization functor with respect to a Serre class
in the abelian category `C`, the functor `whiskeringLeft L P E: (D ⥤ₑ E) ⥤ C ⥤ₑ E`
is fully faithful.  -/
CategoryTheory.ObjectProperty.SerreClassLocalization.fullyFaithfulWhiskeringLeft : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {D : Type u'} →
        [inst_2 : CategoryTheory.Category.{v', u'} D] →
          (L : CategoryTheory.Functor C D) →
            (P : CategoryTheory.ObjectProperty C) →
              [inst_3 : P.IsSerreClass] →
                (E : Type u'') →
                  [inst_4 : CategoryTheory.Category.{v'', u''} E] →
                    [inst_5 : CategoryTheory.Abelian E] →
                      [inst_6 : L.IsLocalization P.isoModSerre] →
                        [inst_7 : CategoryTheory.Preadditive D] →
                          [inst_8 : L.Additive] →
                            (CategoryTheory.ObjectProperty.SerreClassLocalization.whiskeringLeft L P E).FullyFaithful
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.Augmented.whiskeringObj.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (D : Type u_1) [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D),
  CategoryTheory.SimplicialObject.Augmented.whiskeringObj C D F =
    {
      obj := fun X =>
        {
          left :=
            ((CategoryTheory.SimplicialObject.whiskering C D).obj F).obj
              (CategoryTheory.SimplicialObject.Augmented.drop.obj X),
          right := F.obj (CategoryTheory.SimplicialObject.Augmented.point.obj X),
          hom :=
            CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight X.hom F)
              (CategoryTheory.Functor.constComp SimplexCategoryᵒᵖ X.right F).hom },
      map := fun {X Y} η => { left := CategoryTheory.Functor.whiskerRight η.left F, right := F.map η.right, w := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Init.Data.List.TakeDrop
List.head_takeWhile : ∀ {α : Type u_1} {p : α → Bool} {l : List α} (w : List.takeWhile p l ≠ []), (List.takeWhile p l).head w = l.head ⋯