mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.HierarchyDesign
/-- Certain instances always apply during type-class resolution. For example, the instance
`AddCommGroup.toAddGroup {α} [AddCommGroup α] : AddGroup α` applies to all type-class
resolution problems of the form `AddGroup _`, and type-class inference will then do an
exhaustive search to find a commutative group. These instances take a long time to fail.
Other instances will only apply if the goal has a certain shape. For example
`Int.instAddGroup : AddGroup ℤ` or
`Prod.instAddGroup {α β} [AddGroup α] [AddGroup β] : AddGroup (α × β)`. Usually these instances
will fail quickly, and when they apply, they are almost always the desired instance.
For this reason, we want the instances of the second type (that only apply in specific cases) to
always have higher priority than the instances of the first type (that always apply).
See also [mathlib#1561](https://github.com/leanprover-community/mathlib/issues/1561).

Therefore, if we create an instance that always applies, we set the priority of these instances to
100 (or something similar, which is below the default value of 1000).
 -/
LibraryNote.lower_instance_priority : Batteries.Util.LibraryNote
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Expr.denote.match_1.eq_7 : ∀ (motive : Int.Internal.Linear.Expr → Sort u_1) (e : Int.Internal.Linear.Expr) (k : ℤ)
  (h_1 : (a b : Int.Internal.Linear.Expr) → motive (a.add b))
  (h_2 : (a b : Int.Internal.Linear.Expr) → motive (a.sub b)) (h_3 : (a : Int.Internal.Linear.Expr) → motive a.neg)
  (h_4 : (k : ℤ) → motive (Int.Internal.Linear.Expr.num k))
  (h_5 : (v : Int.Internal.Linear.Var) → motive (Int.Internal.Linear.Expr.var v))
  (h_6 : (k : ℤ) → (e : Int.Internal.Linear.Expr) → motive (Int.Internal.Linear.Expr.mulL k e))
  (h_7 : (e : Int.Internal.Linear.Expr) → (k : ℤ) → motive (e.mulR k)),
  (match e.mulR k with
    | a.add b => h_1 a b
    | a.sub b => h_2 a b
    | a.neg => h_3 a
    | Int.Internal.Linear.Expr.num k => h_4 k
    | Int.Internal.Linear.Expr.var v => h_5 v
    | Int.Internal.Linear.Expr.mulL k e => h_6 k e
    | e.mulR k => h_7 e k) =
    h_7 e k
-- Mathlib.Topology.Algebra.InfiniteSum.Group
cauchySeq_finset_iff_sum_vanishing : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddCommGroup α] [IsUniformAddGroup α] {f : β → α},
  (CauchySeq fun s => ∑ b ∈ s, f b) ↔ ∀ e ∈ nhds 0, ∃ s, ∀ (t : Finset β), Disjoint t s → ∑ b ∈ t, f b ∈ e
-- Mathlib.Algebra.Prime.Defs
/-- If `p` and `q` are irreducible, then `p ∣ q` implies `q ∣ p`.  -/
Irreducible.dvd_symm : ∀ {M : Type u_1} [inst : Monoid M] {p q : M}, Irreducible p → Irreducible q → p ∣ q → q ∣ p
-- Mathlib.Probability.Kernel.RadonNikodym
/-- The set of points `a : α` such that `κ a ⟂ₘ η a` is measurable.  -/
ProbabilityTheory.Kernel.measurableSet_mutuallySingular : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ)
  [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsFiniteKernel η],
  MeasurableSet {a | (κ a).MutuallySingular (η a)}
-- Mathlib.Data.Bool.Basic
Bool.coe_false : (false = true) = False
-- Mathlib.Data.Matrix.Basic
Matrix.transpose_pow : ∀ {m : Type u_2} {α : Type u_11} [inst : CommSemiring α] [inst_1 : Fintype m] [inst_2 : DecidableEq m]
  (M : Matrix m m α) (k : ℕ), (M ^ k).transpose = M.transpose ^ k
-- Mathlib.Analysis.Normed.Ring.Basic
/-- A subalgebra of a normed commutative ring is also a normed commutative ring, with the
restriction of the norm.  -/
Subalgebra.normedCommRing : {𝕜 : Type u_5} →
  [inst : CommRing 𝕜] →
    {E : Type u_6} → [inst_1 : NormedCommRing E] → [inst_2 : Algebra 𝕜 E] → (s : Subalgebra 𝕜 E) → NormedCommRing ↥s
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.SpecialLinearGroup.map_mapGL : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  [inst_3 : CommRing S] [inst_4 : Algebra R S] {T : Type u_2} [inst_5 : CommRing T] [inst_6 : Algebra R T]
  [inst_7 : Algebra S T] [IsScalarTower R S T] (g : Matrix.SpecialLinearGroup n R),
  (Matrix.GeneralLinearGroup.map (algebraMap S T)) ((Matrix.SpecialLinearGroup.mapGL S) g) =
    (Matrix.SpecialLinearGroup.mapGL T) g
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.instTensorProduct_1 : ∀ (R : Type u) (M : Type v) (A : Type u_4) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Invertible R M] [inst_4 : CommSemiring A] [inst_5 : Algebra R A], Module.Invertible A (TensorProduct R A M)
-- ProofWidgets.Component.PenroseDiagram
ProofWidgets.Penrose.DiagramProps : Type
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instIsScalarTower : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace R]
  [inst_3 : AddCommMonoid R] {M : Type u_3} {N : Type u_4} [inst_4 : SMulZeroClass M R]
  [inst_5 : ContinuousConstSMul M R] [inst_6 : SMulZeroClass N R] [inst_7 : ContinuousConstSMul N R] [inst_8 : SMul M N]
  [IsScalarTower M N R], IsScalarTower M N (ContinuousMapZero X R)
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_eq_compl_inter : ∀ {α : Type u_1} {s t : Set α}, s \ t = tᶜ ∩ s
-- Lean.ExtraModUses
Lean.IndirectModUse.mk.inj : ∀ {kind : String} {declName : Lean.Name} {kind_1 : String} {declName_1 : Lean.Name},
  { kind := kind, declName := declName } = { kind := kind_1, declName := declName_1 } →
    kind = kind_1 ∧ declName = declName_1
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_injective : Function.Injective Real.arctan
-- Mathlib.Analysis.LocallyConvex.Bounded
NormedSpace.isVonNBounded_of_isBounded : ∀ (𝕜 : Type u_1) {E : Type u_3} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {s : Set E}, Bornology.IsBounded s → Bornology.IsVonNBounded 𝕜 s
-- Mathlib.Logic.Function.Basic
/-- **Alias** of `Function.symm_apply_eq_iff`. -/
Function.symmetric_apply_eq_iff : ∀ {α : Sort u_1} {f : α → α}, (Std.Symm fun x1 x2 => f x1 = x2) ↔ Function.Involutive f
-- Std.Http.Data.Chunk
/-- Removes a trailer header with the given name.
 -/
Std.Http.Trailer.erase : Std.Http.Trailer → Std.Http.Header.Name → Std.Http.Trailer
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.instMonadParentDeclTermElabM : Lean.Elab.MonadParentDecl Lean.Elab.TermElabM
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inv_filter : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveInv α] (s : Finset α) (p : α → Prop)
  [inst_2 : DecidablePred p], ({x ∈ s | p x})⁻¹ = {x ∈ s⁻¹ | p x⁻¹}
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.ins.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_3 ()
-- Lean.Data.RArray
_private.Lean.Data.RArray.0.Lean.RArray.ofFn.go.induct_unfolding : ∀ {α : Type u_1} {n : ℕ} (f : Fin n → α) (motive : (lb ub : ℕ) → lb < ub → ub ≤ n → Lean.RArray α → Prop),
  (∀ (lb : ℕ) (h1 : lb < lb + 1) (h2 : lb + 1 ≤ n), motive lb (lb + 1) h1 h2 (Lean.RArray.leaf (f ⟨lb, ⋯⟩))) →
    (∀ (lb ub : ℕ) (h1 : lb < ub) (h2 : ub ≤ n) (h : ¬lb + 1 = ub),
        let mid := (lb + ub) / 2;
        motive lb mid ⋯ ⋯ (Lean.RArray.ofFn.go✝ f lb mid ⋯ ⋯) →
          motive mid ub ⋯ h2 (Lean.RArray.ofFn.go✝ f mid ub ⋯ h2) →
            motive lb ub h1 h2
              (Lean.RArray.branch mid (Lean.RArray.ofFn.go✝ f lb mid ⋯ ⋯) (Lean.RArray.ofFn.go✝ f mid ub ⋯ h2))) →
      ∀ (lb ub : ℕ) (h1 : lb < ub) (h2 : ub ≤ n), motive lb ub h1 h2 (Lean.RArray.ofFn.go✝ f lb ub h1 h2)
-- Mathlib.NumberTheory.Divisors
Nat.insert_self_properDivisors : ∀ {n : ℕ}, n ≠ 0 → insert n n.properDivisors = n.divisors
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.mapFunctor_map : ∀ (T : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : Tᵒᵖ} (f : X ⟶ Y),
  (CategoryTheory.Under.mapFunctor T).map f = (CategoryTheory.Under.map f.unop).toCatHom
-- Init.Data.AC
Lean.Data.AC.evalList.eq_3 : ∀ {α : Sort u_1} (β : Sort u) [inst : Lean.Data.AC.EvalInformation α β] (ctx : α) (x_1 : ℕ) (xs : List ℕ),
  (xs = [] → False) →
    Lean.Data.AC.evalList β ctx (x_1 :: xs) =
      Lean.Data.AC.EvalInformation.evalOp ctx (Lean.Data.AC.EvalInformation.evalVar ctx x_1)
        (Lean.Data.AC.evalList β ctx xs)
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.zero_le : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] {X : Type u_2} [inst_2 : Fintype X]
  (s : ↑(stdSimplex S X)) (x : X), 0 ≤ s x
-- Mathlib.GroupTheory.OreLocalization.OreSet
AddOreLocalization.addOreSetBot.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R],
  AddOreLocalization.addOreSetBot =
    { ore_right_cancel := ⋯, oreMin := fun r x => r, oreSubtra := fun x s => s, ore_eq := ⋯ }
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivWithinAt.derivWithin : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x → UniqueDiffWithinAt 𝕜 s x → derivWithin f s x = f'
-- Init.Data.String.TakeDrop
/-- If `pat` matches a prefix of `s`, returns the remainder. Returns `none` otherwise.

Use `String.dropPrefix` to return the slice
unchanged when `pat` does not match a prefix.

This is a cheap operation because it does not allocate a new string to hold the result.
To convert the result into a string, use `String.Slice.copy`.

This function is generic over all currently supported patterns.

Examples:

* `"red green blue".dropPrefix? "red " == some "green blue".toSlice`

* `"red green blue".dropPrefix? "reed " == none`

* `"red green blue".dropPrefix? 'r' == some "ed green blue".toSlice`

* `"red green blue".dropPrefix? Char.isLower == some "ed green blue".toSlice`
 -/
String.dropPrefix? : {ρ : Type} → String → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → Option String.Slice
-- Std.Data.Iterators.Lemmas.Producers.Array
Array.iterFromIdx_equiv_iter_drop_toList : ∀ {α : Type w} {array : Array α} {pos : ℕ}, (array.iterFromIdx pos).Equiv (List.drop pos array.toList).iter
-- Mathlib.Algebra.Group.Units.Defs
isAddUnit_of_add_isAddUnit_right : ∀ {M : Type u_1} [inst : AddMonoid M] [IsDedekindFiniteAddMonoid M] {x y : M}, IsAddUnit (x + y) → IsAddUnit y
-- Mathlib.Topology.Algebra.UniformRing
UniformSpace.Completion.coe_eq_one_iff : ∀ (α : Type u_1) [inst : Ring α] [inst_1 : UniformSpace α] [T0Space α] {x : α}, ↑x = 1 ↔ x = 1
-- Mathlib.Data.Rel
SetRel.isSymm_image : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α α} {f : α → β} [R.IsSymm], SetRel.IsSymm (Prod.map f f '' R)
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.instHasAffinePropertyAndIsAffineFiniteCarrierObjOppositeOpensCarrierCarrierCommRingCatPresheafOpOpensTopHomAppTop : AlgebraicGeometry.HasAffineProperty @AlgebraicGeometry.IsFinite fun X x f x_1 =>
  AlgebraicGeometry.IsAffine X ∧ (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop f)).Finite
-- Mathlib.Algebra.Prime.Defs
not_prime_zero : ∀ {M : Type u_1} [inst : CommMonoidWithZero M], ¬Prime 0
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- A closed monoidal category is left distributive.  -/
CategoryTheory.MonoidalClosed.isMonoidalLeftDistrib : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.MonoidalClosed C],
  CategoryTheory.IsMonoidalLeftDistrib C
-- Mathlib.Algebra.Group.Units.Basic
Units.inv_mul_cancel_right : ∀ {α : Type u} [inst : Monoid α] (a : α) (b : αˣ), a * ↑b⁻¹ * ↑b = a
-- Mathlib.Algebra.Homology.ComplexShapeSigns
TotalComplexShapeSymmetrySymmetry.σ_symm : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  {c₁₂ : ComplexShape I₁₂} {inst : TotalComplexShape c₁ c₂ c₁₂} {inst_1 : TotalComplexShape c₂ c₁ c₁₂}
  {inst_2 : TotalComplexShapeSymmetry c₁ c₂ c₁₂} {inst_3 : TotalComplexShapeSymmetry c₂ c₁ c₁₂}
  [self : TotalComplexShapeSymmetrySymmetry c₁ c₂ c₁₂] (i₁ : I₁) (i₂ : I₂), c₂.σ c₁ c₁₂ i₂ i₁ = c₁.σ c₂ c₁₂ i₁ i₂
-- Mathlib.Order.Category.BddOrd
BddOrd.inv_hom_apply : ∀ {X Y : BddOrd} (e : X ≅ Y) (x : ↑X.toPartOrd),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_lt_one_iff : ∀ {p : NNReal}, ↑p < 1 ↔ p < 1
-- Init.Data.UInt.Lemmas
UInt32.ofBitVec_uInt64ToBitVec : ∀ (n : UInt64), { toBitVec := BitVec.setWidth 32 n.toBitVec } = n.toUInt32
-- Mathlib.Data.Nat.GCD.Basic
Nat.add_coprime_iff_right : ∀ {a b c : ℕ}, c ∣ a → ((a + b).Coprime c ↔ b.Coprime c)
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon_inv_hom_hom_hom_inv_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e)
  {Z : a ⟶ e}
  (h_1 :
    CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g h) i) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom h_1)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).inv) h_1)
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.tfaeType.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
/-- The notation for the submonoid of non-zero divisors.  -/
nonZeroDivisors.«term_⁰» : Lean.TrailingParserDescr
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsNonloop.mem_closure_singleton : ∀ {α : Type u_1} {M : Matroid α} {e f : α}, M.IsNonloop e → e ∈ M.closure {f} → f ∈ M.closure {e}
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.contains_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, (m.insert k).contains k = true
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inl_pow : ∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : AddMonoid M] [inst_2 : DistribMulAction R M]
  [inst_3 : DistribMulAction Rᵐᵒᵖ M] (r : R) (n : ℕ), TrivSqZeroExt.inl r ^ n = TrivSqZeroExt.inl (r ^ n)
-- Mathlib.Data.Tree.Basic
/-- **Alias** of `BinaryTree.map`.  -/
Tree.map : {α : Type u_1} → {β : Type u_2} → (α → β) → Tree α → Tree β
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkInductiveAux₂_zero : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : ChainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 0 ⟶ Q.X 1)
  (comm_zero : e.f 0 = CategoryTheory.CategoryStruct.comp zero (Q.d 1 0)) (one : P.X 1 ⟶ Q.X 2)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1))
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X n ⟶ Q.X (n + 1)) ×'
            (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f +
                  CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) →
        (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst +
              CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))),
  Homotopy.mkInductiveAux₂ e zero comm_zero one comm_one succ 0 =
    ⟨0, ⟨CategoryTheory.CategoryStruct.comp zero (HomologicalComplex.xPrevIso Q ⋯).inv, ⋯⟩⟩
-- Mathlib.Data.Quot
Quotient.liftOn₂_mk : ∀ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} {x : Setoid α} {x_1 : Setoid β} (f : α → β → γ)
  (h : ∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) (x_2 : α) (y : β),
  ⟦x_2⟧.liftOn₂ ⟦y⟧ f h = f x_2 y
-- Mathlib.Algebra.Category.FGModuleCat.Basic
instCoeSortFGModuleCatType : {R : Type u} → [inst : Ring R] → CoeSort (FGModuleCat R) (Type v)
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.rel_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) (a a_1 : α ⊕ β ⊕ γ),
  SimpleGraph.TripartiteFromTriangles.Rel t a a_1 ↔
    (∃ a_2 b c, (a_2, b, c) ∈ t ∧ a = Sum3.in₀ a_2 ∧ a_1 = Sum3.in₁ b) ∨
      (∃ a_2 b c, (a_2, b, c) ∈ t ∧ a = Sum3.in₁ b ∧ a_1 = Sum3.in₀ a_2) ∨
        (∃ a_2 b c, (a_2, b, c) ∈ t ∧ a = Sum3.in₀ a_2 ∧ a_1 = Sum3.in₂ c) ∨
          (∃ a_2 b c, (a_2, b, c) ∈ t ∧ a = Sum3.in₂ c ∧ a_1 = Sum3.in₀ a_2) ∨
            (∃ a_2 b c, (a_2, b, c) ∈ t ∧ a = Sum3.in₁ b ∧ a_1 = Sum3.in₂ c) ∨
              ∃ a_2 b c, (a_2, b, c) ∈ t ∧ a = Sum3.in₂ c ∧ a_1 = Sum3.in₁ b
-- Mathlib.Algebra.Group.Hom.Defs
AddHom.inverse.eq_1 : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) (g : N → M)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f), f.inverse g h₁ h₂ = { toFun := g, map_add' := ⋯ }
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.getLast.match_1.eq_1 : ∀ {α : Type u_1} (motive : (x : List α) → x ≠ [] → Sort u_2) (h : [] ≠ []) (h_1 : (h : [] ≠ []) → motive [] h)
  (h_2 : (a : α) → (x : [a] ≠ []) → motive [a] x)
  (h_3 : (head b : α) → (as : List α) → (x : head :: b :: as ≠ []) → motive (head :: b :: as) x),
  (match [], h with
    | [], h => h_1 h
    | [a], x => h_2 a x
    | head :: b :: as, x => h_3 head b as x) =
    h_1 h
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.map₂_hom_inv_isIso_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.PrelaxFunctor B C) {a b : B} {f g : a ⟶ b} (η : f ⟶ g) [inst_2 : CategoryTheory.IsIso η]
  {Z : F.obj a ⟶ F.obj b} (h : F.map f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map₂ η) (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.inv η)) h) =
    h
-- Mathlib.Combinatorics.Quiver.ConnectedComponent
/-- Strong connectivity: every ordered pair of vertices is joined by a (possibly empty)
directed path.  -/
Quiver.IsStronglyConnected : (V : Type u_2) → [Quiver V] → Prop
-- Mathlib.RingTheory.Multiplicity
emultiplicity_eq_zero : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, emultiplicity a b = 0 ↔ ¬a ∣ b
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.distortion_of_const : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) [inst : Fintype ι] {c : NNReal},
  π.boxes.Nonempty → (∀ J ∈ π, J.distortion = c) → π.distortion = c
-- Init.Data.Option.Basic
instAlternativeOption : Alternative Option
-- Mathlib.Topology.Sober
IsIrreducible.genericPoint.congr_simp : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : QuasiSober α] {S S_1 : Set α} (e_S : S = S_1)
  (hS : IsIrreducible S), hS.genericPoint = ⋯.genericPoint
-- Mathlib.CategoryTheory.ObjectProperty.Local
/-- Given `W : MorphismProperty C`, this is the property of `W`-local objects, i.e.
the objects `Z` such that for any `f : X ⟶ Y` such that `W f` holds, the precomposition
with `f` gives a bijection `(Y ⟶ Z) ≃ (X ⟶ Z)`.
(See the file `Mathlib/CategoryTheory/Localization/Bousfield.lean` for the "dual" construction
`ObjectProperty.isLocal : ObjectProperty C → MorphismProperty C`.)  -/
CategoryTheory.MorphismProperty.isLocal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → CategoryTheory.ObjectProperty C
-- Mathlib.CategoryTheory.Functor.Derived.RightDerived
CategoryTheory.Functor.rightDerivedNatIso_inv : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_2} D] [inst_2 : CategoryTheory.Category.{v_5, u_3} H]
  (RF RF' : CategoryTheory.Functor D H) {F F' : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α : F ⟶ L.comp RF) (α' : F' ⟶ L.comp RF') (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : RF.IsRightDerivedFunctor α W] [inst_5 : RF'.IsRightDerivedFunctor α' W] (τ : F ≅ F'),
  (RF.rightDerivedNatIso RF' α α' W τ).inv = RF'.rightDerivedNatTrans RF α' α W τ.inv
-- Mathlib.Tactic.Simproc.FinsetInterval
/-- Simproc to compute `Finset.Iio b` where `b` is a numeral.

**Warnings**:
* With the standard depth recursion limit, this simproc can compute intervals of size 250 at most.
* Make sure to exclude `Finset.insert_eq_of_mem` from your simp call when using this simproc. This
  avoids a quadratic time performance hit.  -/
Finset.Iio_ofNat : Lean.Meta.Simp.Simproc
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.map.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f f_1 : R →+* S) (e_f : f = f_1)
  (p : Polynomial R) (q : Polynomial S) (h : q ∣ Polynomial.map f p), AdjoinRoot.map f p q h = AdjoinRoot.map f_1 p q ⋯
-- Mathlib.Data.Nat.Choose.Lucas
/-- **Lucas's Theorem**: For primes `p`, `choose n k` is congruent to the product of
`choose (⌊n / p ^ i⌋ % p) (⌊k / p ^ i⌋ % p)` over `i` modulo `p`.  -/
Choose.choose_modEq_prod_range_choose : ∀ {n k p : ℕ} [Fact (Nat.Prime p)] {a : ℕ},
  n < p ^ a → k < p ^ a → ↑(n.choose k) ≡ ∏ i ∈ Finset.range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]
-- Init.Data.ByteArray.Lemmas
ByteArray.getElem!_set!_self : ∀ (data : ByteArray) (i : ℕ) (v : UInt8), i < data.size → (data.set! i v)[i]! = v
-- Std.Http.Protocol.H1.Error
/-- Bad request or response message.
 -/
Std.Http.Protocol.H1.Error.badMessage : Std.Http.Protocol.H1.Error
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.equivOfIso_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F)
  (i : E.I₀), (CategoryTheory.PreZeroHypercover.equivOfIso e) i = e.hom.s₀ i
-- Mathlib.CategoryTheory.Limits.MorphismProperty
CategoryTheory.MorphismProperty.CostructuredArrow.instPreservesLimitsOfShapeTopOverWalkingCospanToOver : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {A : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A] {L : CategoryTheory.Functor A T} (X : T) [P.IsStableUnderComposition]
  [P.IsStableUnderBaseChange] [P.HasOfPostcompProperty P] [CategoryTheory.Limits.HasPullbacks A]
  [CategoryTheory.Limits.HasPullbacks T]
  [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan L],
  CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan
    (CategoryTheory.MorphismProperty.CostructuredArrow.toOver P L X)
-- Mathlib.Topology.Homeomorph.Defs
Equiv.symm_toHomeomorph : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ Y)
  (he : ∀ (s : Set Y), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s), (e.toHomeomorph he).symm = e.symm.toHomeomorph ⋯
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- An isomorphism in `0`-hypercovers is an isomorphism of the underlying pre-`0`-hypercovers.  -/
CategoryTheory.Precoverage.ZeroHypercover.isoMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Precoverage C} →
      {S : C} → {E F : J.ZeroHypercover S} → (E.toPreZeroHypercover ≅ F.toPreZeroHypercover) → (E ≅ F)
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
/-- The base function from which one will construct a family of bump functions. One could
add more properties if they are useful and satisfied in the examples of inner product spaces
and finite-dimensional vector spaces, notably derivative norm control in terms of `R - 1`.

TODO: do we ever need `f x = 1 ↔ ‖x‖ ≤ 1`?  -/
ContDiffBumpBase : (E : Type u_3) → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → Type u_3