mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Logic.Nontrivial.Defs
exists_ne : ∀ {α : Type u_1} [Nontrivial α] (x : α), ∃ y, y ≠ x
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a differentiable vector field by a `C^n` function with `2 ≤ n` is
differentiable. Version within a set at a point.  -/
MDifferentiableWithinAt.mpullbackWithin_vectorField_inter : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x₀ : M}
  {V : (x : M') → TangentSpace I' x} {n : WithTop ℕ∞} {t : Set M'} [inst_11 : IsManifold I 2 M]
  [inst_12 : IsManifold I' 2 M'] [CompleteSpace E],
  MDiffAt[t] (T% V) (f x₀) →
    ContMDiffWithinAt I I' n f s x₀ →
      (mfderiv[s] f x₀).IsInvertible →
        x₀ ∈ s →
          UniqueMDiff[s] → 2 ≤ n → (MDiffAt[s ∩ f ⁻¹' t] fun x => ⟨x, VectorField.mpullbackWithin I I' f V s x⟩) x₀
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_right_idem : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), s ∩ t ∩ t = s ∩ t
-- Lean.Elab.MutualDef
/-- - `sectionVars`:   The section variables used in the `mutual` block.
- `mainHeaders`:   The elaborated header of the top-level definitions being defined by the mutual block.
- `mainFVars`:     The auxiliary variables used to represent the top-level definitions being defined by the mutual block.
- `mainVals`:      The elaborated value for the top-level definitions
- `letRecsToLift`: The let-rec's definitions that need to be lifted
 -/
Lean.Elab.Term.MutualClosure.main : Array Lean.Expr →
  Array Lean.Elab.DefViewElabHeader →
    Array Lean.Expr →
      Array Lean.Expr → List Lean.Elab.Term.LetRecToLift → Lean.Elab.TermElabM (Array Lean.Elab.PreDefinition)
-- Mathlib.Data.Set.Card
Set.encard_ne_add_one : ∀ {α : Type u_1} (a : α), {x | x ≠ a}.encard + 1 = ENat.card α
-- Mathlib.Topology.Algebra.Group.Basic
Specializes.neg : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Neg G] [ContinuousNeg G] {x y : G}, x ⤳ y → (-x) ⤳ (-y)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- **Alias** of `Order.cof_le`. -/
Ordinal.cof_type_le : ∀ {α : Type u} [inst : Preorder α] {s : Set α}, IsCofinal s → Order.cof α ≤ Cardinal.mk ↑s
-- Mathlib.CategoryTheory.Dialectica.Basic
CategoryTheory.Dial.isoMk_hom_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y : CategoryTheory.Dial C} (e₁ : X.src ≅ Y.src)
  (e₂ : X.tgt ≅ Y.tgt)
  (eq : X.rel = (CategoryTheory.Subobject.pullback (CategoryTheory.Limits.prod.map e₁.hom e₂.hom)).obj Y.rel),
  (CategoryTheory.Dial.isoMk e₁ e₂ eq).hom.f = e₁.hom
-- Mathlib.Order.Disjoint
IsCompl.right_le_iff : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : BoundedOrder α] {x y z : α}, IsCompl x y → (y ≤ z ↔ Codisjoint z x)
-- Mathlib.Algebra.Group.Equiv.Opposite
/-- An additive semigroup homomorphism `f : AddHom M N` such that `f x` additively
commutes with `f y` for all `x, y` defines an additive semigroup homomorphism to `Sᵃᵒᵖ`.  -/
AddHom.toOpposite : {M : Type u_3} →
  {N : Type u_4} →
    [inst : Add M] → [inst_1 : Add N] → (f : M →ₙ+ N) → (∀ (x y : M), AddCommute (f x) (f y)) → M →ₙ+ Nᵃᵒᵖ
-- Mathlib.Order.Hom.WithTopBot
LatticeHom.withTopWithBot_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Lattice α] [inst_1 : Lattice β] (f : LatticeHom α β) (a : WithTop (WithBot α)),
  f.withTopWithBot a = WithTop.map (WithBot.map ⇑f) a
-- Mathlib.Algebra.Group.Units.Hom
IsAddUnit.addUnit_map : ∀ {F : Type u_1} {M : Type u_3} {N : Type u_4} [inst : FunLike F M N] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N]
  [inst_3 : AddMonoidHomClass F M N] (f : F) {x : M} (h : IsAddUnit x), ↑⋯.addUnit = f ↑h.addUnit
-- Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup
AddSubgroup.addSubgroupOfContinuousAddEquivOfLe_apply : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {H K : AddSubgroup G} (hHK : H ≤ K)
  (a : ↥(H.addSubgroupOf K)),
  (AddSubgroup.addSubgroupOfContinuousAddEquivOfLe hHK) a = (AddSubgroup.addSubgroupOfEquivOfLe hHK) a
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
/-- A class registering that a real vector space admits bump functions. This will be instantiated
first for inner product spaces, and then for finite-dimensional normed spaces.
We use a specific class instead of `Nonempty (ContDiffBumpBase E)` for performance reasons.  -/
HasContDiffBump : (E : Type u_3) → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → Prop
-- Init.Data.Array.Find
Array.mem_of_find?_eq_some : ∀ {α : Type u_1} {p : α → Bool} {a : α} {xs : Array α}, Array.find? p xs = some a → a ∈ xs
-- Std.Async.Signal
Std.Async.Signal.sigusr2.sizeOf_spec : sizeOf Std.Async.Signal.sigusr2 = 1
-- Lean.Elab.DeclarationRange
/-- For most builtin declarations, the selection range is just its name, which is stored in the second position.
Example:
```
"def " >> declId >> optDeclSig >> declVal
```
If the declaration name is absent, we use the keyword instead.
This function converts the given `Syntax` into one that represents its "selection range".
 -/
Lean.Elab.getDeclarationSelectionRef : Lean.Syntax → Lean.Syntax
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- Given `j : Fin n`, the index of the part to which it belongs.  -/
OrderedFinpartition.index : {n : ℕ} → (c : OrderedFinpartition n) → Fin n → Fin c.length
-- Mathlib.Algebra.Category.Grp.EpiMono
/-- Define `X'` to be the set of all left cosets with an extra point at "infinity".
 -/
GrpCat.SurjectiveOfEpiAuxs.XWithInfinity : {A B : GrpCat} → (A ⟶ B) → Type u
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_inj : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {a b : SkewMonoidAlgebra k G}, a.coeff = b.coeff ↔ a = b
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.ext_hom_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (φ : c.pt ≅ c'.pt)
  (w :
    autoParam (∀ (j : J), c.π.app j = CategoryTheory.CategoryStruct.comp φ.hom (c'.π.app j))
      CategoryTheory.Limits.Cone.ext._auto_1),
  (CategoryTheory.Limits.Cone.ext φ w).hom.hom = φ.hom
-- Mathlib.Order.Bounds.Basic
/-- If `s` has a greatest element, then it is bounded above.  -/
IsGreatest.bddAbove : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, IsGreatest s a → BddAbove s
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.instFullUliftFunctor : ∀ (R : Type u) [inst : CommRing R], (CommAlgCat.uliftFunctor R).Full
-- Mathlib.Algebra.Lie.Submodule
LieModuleHom.mem_range : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] [inst_7 : LieRingModule L N] (f : M →ₗ⁅R,L⁆ N) (n : N), n ∈ f.range ↔ ∃ m, f m = n
-- Lean.Data.Lsp.Basic
Lean.Lsp.DeleteFile.uri : Lean.Lsp.DeleteFile → Lean.Lsp.DocumentUri
-- Mathlib.Algebra.Ring.NegOnePow
Int.negOnePow_eq_one_iff : ∀ (n : ℤ), n.negOnePow = 1 ↔ Even n
-- Mathlib.Computability.Halting
/-- **Rice's Theorem**  -/
ComputablePred.rice : ∀ (C : Set (ℕ →. ℕ)),
  (ComputablePred fun c => c.eval ∈ C) → ∀ {f g : ℕ →. ℕ}, Nat.Partrec f → Nat.Partrec g → f ∈ C → g ∈ C
-- Mathlib.Data.Fintype.Basic
Quotient.fintype : {α : Type u_1} → [Fintype α] → (s : Setoid α) → [DecidableRel fun x1 x2 => x1 ≈ x2] → Fintype (Quotient s)
-- Mathlib.Order.LatticeIntervals
Set.Ioc.coe_sup : ∀ {α : Type u_1} [inst : SemilatticeSup α] {a b : α} {x y : ↑(Set.Ioc a b)}, ↑(x ⊔ y) = ↑x ⊔ ↑y
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.instIsRightAdjointSheafSkyscraperSheafFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A], Φ.skyscraperSheafFunctor.IsRightAdjoint
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.top_covers : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (S : CategoryTheory.Sieve X) (f : Y ⟶ X),
  ⊤.Covers S f
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.TerminationHints.ref : Lean.Elab.TerminationHints → Lean.Syntax
-- Lean.Parser.Tactic.Doc
/-- Enumerate the tactic tags that are available, with their user-facing name and docstring  -/
Lean.Parser.Tactic.Doc.allTagsWithInfo : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → m (List (Lean.Name × String × Option String))
-- Mathlib.CategoryTheory.Sites.Canonical
/-- **Alias** of `CategoryTheory.Presieve.isSheafFor_bind`. -/
CategoryTheory.Sheaf.isSheafFor_bind : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type u_1))
  (U : CategoryTheory.Sieve X) (B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → CategoryTheory.Sieve Y),
  CategoryTheory.Presieve.IsSheafFor P U.arrows →
    (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), CategoryTheory.Presieve.IsSheafFor P (B hf).arrows) →
      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y),
          CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.pullback g (B h)).arrows) →
        CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.bind U.arrows B).arrows
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Equiv.refl_symm_apply : ∀ {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) (a : E), (GroupExtension.Equiv.refl S).symm a = a
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.assocOfMapSMul_tmul : ∀ {R : Type u_9} {S : Type u_10} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {M₁ : Type u_11} {M₂ : Type u_12} {M₃ : Type u_13} {M₁₂ : Type u_14} {M₂₃ : Type u_15} [inst_3 : AddCommMonoid M₁]
  [inst_4 : AddCommMonoid M₂] [inst_5 : AddCommMonoid M₃] [inst_6 : AddCommMonoid M₁₂] [inst_7 : AddCommMonoid M₂₃]
  [inst_8 : Module R M₁] [inst_9 : Module R M₂] [inst_10 : Module S M₂] [inst_11 : IsScalarTower R S M₂]
  [inst_12 : Module R M₃] [inst_13 : Module S M₃] [inst_14 : IsScalarTower R S M₃] [inst_15 : Module R M₁₂]
  [inst_16 : Module S M₁₂] [inst_17 : IsScalarTower R S M₁₂] [inst_18 : Module R M₂₃] [inst_19 : Module S M₂₃]
  [inst_20 : IsScalarTower R S M₂₃] {T : Type u_16} [inst_21 : CommSemiring T] [inst_22 : Algebra R T]
  [inst_23 : Module T M₁] [inst_24 : IsScalarTower R T M₁] [inst_25 : Module T M₁₂] [inst_26 : SMulCommClass S T M₁₂]
  [inst_27 : IsScalarTower R T M₁₂] (f : M₁ →ₗ[R] M₂ →ₗ[R] M₁₂) (hf : IsTensorProduct f) (g : M₂ →ₗ[S] M₃ →ₗ[S] M₂₃)
  (hg : IsTensorProduct g) (h₁ : ∀ (t : T) (x : M₁) (y : M₂), (f (t • x)) y = t • (f x) y)
  (h₂ : ∀ (s : S) (x : M₁) (y : M₂), (f x) (s • y) = s • (f x) y) (x₁ : M₁) (x₂ : M₂) (x₃ : M₃),
  (IsTensorProduct.assocOfMapSMul f hf g hg h₁ h₂) ((f x₁) x₂ ⊗ₜ[S] x₃) = x₁ ⊗ₜ[R] (g x₂) x₃
-- Lean.Structure
Lean.StructureDescr.mk.injEq : ∀ (structName : Lean.Name) (fields : Array Lean.StructureFieldInfo) (structName_1 : Lean.Name)
  (fields_1 : Array Lean.StructureFieldInfo),
  ({ structName := structName, fields := fields } = { structName := structName_1, fields := fields_1 }) =
    (structName = structName_1 ∧ fields = fields_1)
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.Precheck.Context.mk.inj : ∀ {quotLCtx quotLCtx_1 : Lean.NameSet}, { quotLCtx := quotLCtx } = { quotLCtx := quotLCtx_1 } → quotLCtx = quotLCtx_1
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.ι_mapBifunctor₂₃Desc_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃}
  (c₁₂ : ComplexShape ι₁₂) {c₂₃ : ComplexShape ι₂₃} {c₄ : ComplexShape ι₄} [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
  [inst_23 : HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] {j : ι₄} {A : C₄}
  (f : (i₁ : ι₁) → (i₂ : ι₂) → ⋯) (i₁ : ι₁) (i₂ : ι₂), ⋯
-- Mathlib.Order.Hom.Lattice
SupHom.top_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : SemilatticeSup β] [inst_2 : Top β] (a : α), ⊤ a = ⊤
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a b : α}, (a == b) = true → (a ∈ m ↔ b ∈ m)
-- Mathlib.Data.Set.Sups
/-- Notation typeclass for pointwise infimum `⊼`.  -/
HasInfs : Type u_4 → Type u_4
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.findSomeM?.eq_2 : ∀ {m : Type u → Type v} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) (a : α) (as : List α),
  List.findSomeM? f (a :: as) = do
    let __do_lift ← f a
    match __do_lift with
      | some b => pure (some b)
      | none => List.findSomeM? f as
-- Mathlib.RingTheory.RamificationInertia.Basic
Ideal.ResidueField.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (I I_1 : Ideal R) (e_I : I = I_1) [inst_1 : I.IsPrime],
  I.ResidueField = I_1.ResidueField
-- Mathlib.Algebra.Group.Basic
mul_rotate' : ∀ {G : Type u_3} [inst : CommSemigroup G] (a b c : G), a * (b * c) = b * (c * a)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_diff_of_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α}, k ∈ t₂ → Std.DTreeMap.Const.get? (t₁ \ t₂) k = none
-- Mathlib.GroupTheory.Exponent
addCommMonoidOfExponentTwo.eq_1 : ∀ {G : Type u} [inst : AddMonoid G] [inst_1 : IsCancelAdd G] (hG : AddMonoid.exponent G = 2),
  addCommMonoidOfExponentTwo hG = { toAddMonoid := inst, add_comm := ⋯ }
-- Mathlib.Geometry.Euclidean.Triangle
/-- **Stewart's Theorem**.  -/
EuclideanGeometry.dist_sq_mul_dist_add_dist_sq_mul_dist : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (a b c p : P),
  EuclideanGeometry.angle b p c = Real.pi →
    dist a b ^ 2 * dist c p + dist a c ^ 2 * dist b p = dist b c * (dist a p ^ 2 + dist b p * dist c p)
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.instBEqPoly.beq.match_1.eq_2 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (a : ℤ) (a_1 : Int.Internal.Linear.Var)
  (a_2 : Int.Internal.Linear.Poly) (b : ℤ) (b_1 : Int.Internal.Linear.Var) (b_2 : Int.Internal.Linear.Poly)
  (h_1 : (a b : ℤ) → motive (Int.Internal.Linear.Poly.num a) (Int.Internal.Linear.Poly.num b))
  (h_2 :
    (a : ℤ) →
      (a_3 : Int.Internal.Linear.Var) →
        (a_4 : Int.Internal.Linear.Poly) →
          (b : ℤ) →
            (b_3 : Int.Internal.Linear.Var) →
              (b_4 : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a a_3 a_4) (Int.Internal.Linear.Poly.add b b_3 b_4))
  (h_3 : (x x_1 : Int.Internal.Linear.Poly) → motive x x_1),
  (match Int.Internal.Linear.Poly.add a a_1 a_2, Int.Internal.Linear.Poly.add b b_1 b_2 with
    | Int.Internal.Linear.Poly.num a, Int.Internal.Linear.Poly.num b => h_1 a b
    | Int.Internal.Linear.Poly.add a a_3 a_4, Int.Internal.Linear.Poly.add b b_3 b_4 => h_2 a a_3 a_4 b b_3 b_4
    | x, x_1 => h_3 x x_1) =
    h_2 a a_1 a_2 b b_1 b_2
-- Mathlib.GroupTheory.Goursat
Subgroup.mem_goursatFst : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {I : Subgroup (G × H)} {g : G},
  g ∈ I.goursatFst ↔ (g, 1) ∈ I
-- Std.Data.DHashMap.Basic
Std.DHashMap.Equiv.mk : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β},
  m₁.inner.Equiv m₂.inner → m₁.Equiv m₂
-- Mathlib.GroupTheory.GroupAction.Iwasawa
/-- The Iwasawa criterion for simplicity  -/
MulAction.IwasawaStructure.isSimpleGroup : ∀ {M : Type u_1} [inst : Group M] {α : Type u_2} [inst_1 : MulAction M α] [Nontrivial M],
  commutator M = ⊤ →
    ∀ [MulAction.IsQuasiPreprimitive M α] (IwaS : MulAction.IwasawaStructure M α), FaithfulSMul M α → IsSimpleGroup M
-- Mathlib.GroupTheory.Index
AddSubgroup.inf_relIndex_right : ∀ {G : Type u_1} [inst : AddGroup G] (H K : AddSubgroup G), (H ⊓ K).relIndex K = H.relIndex K
-- Mathlib.Topology.MetricSpace.Isometry
Isometry.mapsTo_closedBall : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  Isometry f → ∀ (x : α) (r : ℝ), Set.MapsTo f (Metric.closedBall x r) (Metric.closedBall (f x) r)
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.inhabited.eq_1 : ∀ {α : Type u}, WithZero.inhabited = { default := 0 }
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
/-- The epimorphism `projective.π : projective.over X ⟶ X`
from the arbitrarily chosen projective object over `X`.
 -/
CategoryTheory.Projective.π : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.EnoughProjectives C] → (X : C) → CategoryTheory.Projective.over X ⟶ X
-- Mathlib.GroupTheory.Congruence.Defs
/-- Definition of the infimum of two additive congruence relations.  -/
AddCon.inf_iff_and : ∀ {M : Type u_1} [inst : Add M] {c d : AddCon M} {x y : M}, (c ⊓ d) x y ↔ c x y ∧ d x y
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.minKeyD_alterKey_eq_self : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : Option β → Option β},
      (Std.Internal.List.Const.alterKey k f l).isEmpty = false →
        ∀ {fallback : α},
          Std.Internal.List.minKeyD (Std.Internal.List.Const.alterKey k f l) fallback = k ↔
            (f (Std.Internal.List.getValue? k l)).isSome = true ∧
              ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k k').isLE = true
-- Mathlib.Algebra.Lie.Basic
lie_zsmul : ∀ {L : Type v} {M : Type w} [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M] (x : L) (m : M)
  (a : ℤ), ⁅x, a • m⁆ = a • ⁅x, m⁆
-- Init.Data.String.Pattern.Pred
String.Slice.Pattern.CharPred.instBackwardPatternForallCharBool : {p : Char → Bool} → String.Slice.Pattern.BackwardPattern p
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : InfSet α] [inst_1 : InfSet β] (f : sInfHom α β), f.comp (sInfHom.id α) = f
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.op_pt : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F), c.op.pt = Opposite.op c.pt
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.lsingle_apply : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring S] [inst_1 : Semiring R] [inst_2 : Module R S] (a : M)
  (b : S), (MonoidAlgebra.lsingle a) b = MonoidAlgebra.single a b
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_H : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι],
  (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData S hkf hcc fac).H = H
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.toList_injective : ∀ {V : Type u} [inst : Quiver V] [∀ (a b : V), Subsingleton (a ⟶ b)] (a b : V), Function.Injective Quiver.Path.toList
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.map_injective : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Continuous f), Function.Injective f → Function.Injective (TopologicalSpace.NonemptyCompacts.map f hf)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.ofList_eq_empty_iff : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α}, Std.ExtTreeSet.ofList l cmp = ∅ ↔ l = []
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.mul_eq_mul : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : C) [inst_2 : CategoryTheory.MonObj M],
  CategoryTheory.MonObj.mul =
    CategoryTheory.SemiCartesianMonoidalCategory.fst M M * CategoryTheory.SemiCartesianMonoidalCategory.snd M M
-- Mathlib.CategoryTheory.Sites.Sieves
/-- Given a presieve `R` on `X`, the predicate `R.HasPairwisePullbacks` means that for all arrows
`f` and `g` in `R`, the pullback of `f` and `g` exists.  -/
CategoryTheory.Presieve.HasPairwisePullbacks : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → CategoryTheory.Presieve X → Prop
-- Mathlib.Topology.Category.TopCat.ULift
/-- The `ULift` functor on categories of topological spaces is compatible
with the one defined on categories of types.  -/
TopCat.uliftFunctorCompForgetIso : TopCat.uliftFunctor.comp (CategoryTheory.forget TopCat) ≅
  (CategoryTheory.forget TopCat).comp CategoryTheory.uliftFunctor.{v, u}
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.leftHomologyMap_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ φ' : S₁ ⟶ S₂) [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology],
  CategoryTheory.ShortComplex.leftHomologyMap (φ + φ') =
    CategoryTheory.ShortComplex.leftHomologyMap φ + CategoryTheory.ShortComplex.leftHomologyMap φ'
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.neg_nonempty_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Neg α] {s : Finset α}, (-s).Nonempty ↔ s.Nonempty
-- Mathlib.Data.Fin.Tuple.Basic
/-- Remove the `p`-th entry of a tuple.  -/
Fin.removeNth : {n : ℕ} → {α : Fin (n + 1) → Sort u_1} → (p : Fin (n + 1)) → ((i : Fin (n + 1)) → α i) → (i : Fin n) → α (p.succAbove i)
-- Init.Data.Vector.Lemmas
Vector.getElem?_set : ∀ {α : Type u_1} {n i j : ℕ} {xs : Vector α n} {x : α} (hi : i < n),
  (xs.set i x hi)[j]? = if i = j then some x else xs[j]?