mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Fintype.Sets
/-- `quot_precheck` for the `finset%` syntax.  -/
precheckFinsetStx : Lean.Elab.Term.Quotation.Precheck
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The associator isomorphism can be passed through a map by swapping the order.  -/
CategoryTheory.Limits.biprod.associator_natural : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map (CategoryTheory.Limits.biprod.map f g) h)
      (CategoryTheory.Limits.biprod.associator X Y Z).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.associator U V W).hom
      (CategoryTheory.Limits.biprod.map f (CategoryTheory.Limits.biprod.map g h))
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.commute_id_left : ∀ {R : Type u_9} {M : Type u_10} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M),
  Commute LinearMap.id f
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.SupportsStmt.match_1.eq_4 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5)
  (a : σ → σ) (q : Turing.TM2.Stmt Γ Λ σ)
  (h_1 : (k : K) → (a : σ → Γ k) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.push k a q))
  (h_2 : (k : K) → (a : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.peek k a q))
  (h_3 : (k : K) → (a : σ → Option (Γ k) → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.pop k a q))
  (h_4 : (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.load a q))
  (h_5 : (a : σ → Bool) → (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (l : σ → Λ) → motive (Turing.TM2.Stmt.goto l)) (h_7 : Unit → motive Turing.TM2.Stmt.halt),
  (match Turing.TM2.Stmt.load a q with
    | Turing.TM2.Stmt.push k a q => h_1 k a q
    | Turing.TM2.Stmt.peek k a q => h_2 k a q
    | Turing.TM2.Stmt.pop k a q => h_3 k a q
    | Turing.TM2.Stmt.load a q => h_4 a q
    | Turing.TM2.Stmt.branch a q₁ q₂ => h_5 a q₁ q₂
    | Turing.TM2.Stmt.goto l => h_6 l
    | Turing.TM2.Stmt.halt => h_7 ()) =
    h_4 a q
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.instDecidableEqAndKind : DecidableEq Mathlib.Tactic.ITauto.AndKind
-- Mathlib.CategoryTheory.Groupoid.VertexGroup
/-- The inverse in the group is equal to the inverse given by `CategoryTheory.inv`.  -/
CategoryTheory.Groupoid.vertexGroup.inv_eq_inv : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (c : C) (γ : c ⟶ c), γ⁻¹ = CategoryTheory.inv γ
-- Init.Data.Nat.Lemmas
Nat.sub_add_eq_max : ∀ (a b : ℕ), a - b + b = max a b
-- Init.Data.List.ToArray
List.findFinIdx?_toArray : ∀ {α : Type u_1} (p : α → Bool) (l : List α), Array.findFinIdx? p l.toArray = List.findFinIdx? p l
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.instIsAlgClosure : ∀ (k : Type u) [inst : Field k], IsAlgClosure k (AlgebraicClosure k)
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.isZero_spectralSequence_page_X_iff : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r : ℤ) (hr : r₀ ≤ r) (pq : κ) (i₀ i₁ i₂ i₃ : ι) (h₀ : i₀ = data.i₀ r pq ⋯)
  (h₁ : i₁ = data.i₁ pq) (h₂ : i₂ = data.i₂ pq) (h₃ : i₃ = data.i₃ r pq ⋯) (n₀ n₁ n₂ : ℤ),
  n₁ = data.deg pq →
    ∀ (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.isZero_spectralSequence_page_X_iff._auto_1)
      (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.isZero_spectralSequence_page_X_iff._auto_3),
      CategoryTheory.Limits.IsZero (((X.spectralSequence data).page r ⋯).X pq) ↔
        CategoryTheory.Limits.IsZero
          (X.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯)
-- Mathlib.MeasureTheory.Measure.Haar.OfBasis
/-- Reindexing a family of vectors does not change their parallelepiped.  -/
parallelepiped_comp_equiv : ∀ {ι : Type u_1} {ι' : Type u_2} {E : Type u_3} [inst : Fintype ι] [inst_1 : Fintype ι'] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℝ E] (v : ι → E) (e : ι' ≃ ι), parallelepiped (v ∘ ⇑e) = parallelepiped v
-- Mathlib.Data.Nat.Log
/-- This lemma says that `⌈log (b ^ k) n⌉ = ⌈(⌈log b n⌉ / k)⌉`, using operations on natural numbers
to express this equality.

Since Lean has no dedicated function for the ceiling division,
we use `(a + (b - 1)) / b` for `⌈a / b⌉`.  -/
Nat.clog_pow_left : ∀ (b k n : ℕ), Nat.clog (b ^ k) n = (Nat.clog b n + (k - 1)) / k
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
Multiset.esymm.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] (s : Multiset R) (n : ℕ),
  s.esymm n = (Multiset.map Multiset.prod (Multiset.powersetCard n s)).sum
-- Mathlib.Order.WithBot
/-- **Alias** of the reverse direction of `WithBot.monotone_map_iff`. -/
Monotone.withBot_map : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → Monotone (WithBot.map f)
-- Lean.Data.Options
Lean.OptionDecl.mk.sizeOf_spec : ∀ (name : Lean.Name) (declName : autoParam Lean.Name Lean.OptionDecl.declName._autoParam) (defValue : Lean.DataValue)
  (descr : String) (deprecation? : Option Lean.OptionDeprecation),
  sizeOf { name := name, declName := declName, defValue := defValue, descr := descr, deprecation? := deprecation? } =
    1 + sizeOf name + sizeOf declName + sizeOf defValue + sizeOf descr + sizeOf deprecation?
-- Mathlib.Logic.Basic
/-- Any prop `p` is decidable classically. A shorthand for `Classical.propDecidable`.  -/
Classical.dec : (p : Prop) → Decidable p
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- `I^N` is notation (in the Topology namespace) for `N → I`,
i.e. the unit cube indexed by a type `N`.  -/
Topology.«termI^_» : Lean.ParserDescr
-- Mathlib.Topology.Maps.Basic
Topology.IsOpenEmbedding.tendsto_nhds_iff : ∀ {Y : Type u_2} {Z : Type u_3} {ι : Type u_4} {g : Y → Z} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z]
  {f : ι → Y} {l : Filter ι} {y : Y},
  Topology.IsOpenEmbedding g → (Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (g ∘ f) l (nhds (g y)))
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
/-- The first index  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₁ : {ι : Type u_2} →
  {κ : Type u_3} →
    [inst : Preorder ι] →
      {c : ℤ → ComplexShape κ} →
        {r₀ : ℤ} → CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀ → κ → ι
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.mul_cast_floor_div_cancel : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R]
  {n : ℕ}, n ≠ 0 → ∀ (a : R), ⌊a * ↑n⌋₊ / n = ⌊a⌋₊
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
/-- **Alias** of `WeierstrassCurve.hasGoodReduction_iff_isElliptic_reduction`. -/
WeierstrassCurve.isGoodReduction_iff_isElliptic_reduction : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDiscreteValuationRing R] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] {W : WeierstrassCurve K}
  [hW : WeierstrassCurve.IsMinimal R W],
  WeierstrassCurve.HasGoodReduction R W ↔ (WeierstrassCurve.reduction R W).IsElliptic
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.ncard_sdiff_add_ncard_of_subset`. -/
Set.ncard_diff_add_ncard_of_subset : ∀ {α : Type u_1} {s t : Set α},
  s ⊆ t → autoParam t.Finite Set.ncard_sdiff_add_ncard_of_subset._auto_1 → (t \ s).ncard + s.ncard = t.ncard
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.IsOrthogonal.symm : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {i j : ι},
  P.IsOrthogonal i j → P.IsOrthogonal j i
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.map_apply : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] (f : Y → Z) (g : LocallyConstant X Y),
  ⇑(LocallyConstant.map f g) = f ∘ ⇑g
-- Lean.Meta.Injective
Lean.Meta.getCtorAppIndices? : Lean.Expr → Lean.MetaM (Option (Array Lean.Expr))
-- Mathlib.MeasureTheory.Measure.Support
MeasureTheory.Measure.compl_support_eq_sUnion : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X},
  μ.supportᶜ = ⋃₀ {t | IsOpen t ∧ μ t = 0}
-- Mathlib.Order.Monotone.Monovary
AntivaryOn.dual_right : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, AntivaryOn f g s → MonovaryOn f (⇑OrderDual.toDual ∘ g) s
-- Mathlib.Algebra.Polynomial.Degree.Units
Polynomial.natDegree_eq_zero_of_isUnit : ∀ {R : Type u} [inst : Semiring R] [NoZeroDivisors R] {p : Polynomial R}, IsUnit p → p.natDegree = 0
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_map : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (s : Finset γ)
  (f : γ ↪ β) (g : β → α), (Finset.map f s).inf g = s.inf (g ∘ ⇑f)
-- Mathlib.Analysis.Convex.Join
convexJoin.eq_1 : ∀ (𝕜 : Type u_2) {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] (s t : Set E), convexJoin 𝕜 s t = ⋃ x ∈ s, ⋃ y ∈ t, segment 𝕜 x y
-- Mathlib.FieldTheory.RatFunc.AsPolynomial
RatFunc.denom_X : ∀ {K : Type u} [inst : Field K], RatFunc.X.denom = 1
-- Mathlib.Data.Ordmap.Ordset
Ordnode.insert.valid : ∀ {α : Type u_1} [inst : Preorder α] [Std.Total fun x1 x2 => x1 ≤ x2] [inst_2 : DecidableLE α] (x : α) {t : Ordnode α},
  t.Valid → (Ordnode.insert x t).Valid
-- Mathlib.Analysis.LocallyConvex.Polar
LinearMap.sInter_polar_finite_subset_eq_polar : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedCommRing 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E),
  ⋂₀ (B.polar '' {F | F.Finite ∧ F ⊆ s}) = B.polar s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.map_smul : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] {W' : WeierstrassCurve.Affine R} (f : R →+* S)
  (x : Polynomial R) (y : W'.CoordinateRing),
  (WeierstrassCurve.Affine.CoordinateRing.map W' f) (x • y) =
    Polynomial.map f x • (WeierstrassCurve.Affine.CoordinateRing.map W' f) y
-- Aesop.Builder.Basic
Aesop.CoreRuleBuilderOutput.indexingMode : Aesop.CoreRuleBuilderOutput → Aesop.IndexingMode
-- Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
/-- The Taylor series of the complex logarithm at `1` converges to the logarithm in the
open unit disk.  -/
Complex.hasSum_taylorSeries_log : ∀ {z : ℂ}, ‖z‖ < 1 → HasSum (fun n => (-1) ^ (n + 1) * z ^ n / ↑n) (Complex.log (1 + z))
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- Postcomposing `f` with `Prod.snd` is `C^n`  -/
ContDiff.snd : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {f : E → F × G},
  ContDiff 𝕜 n f → ContDiff 𝕜 n fun x => (f x).2
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBiproduct.bicone_inl : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  (CategoryTheory.Limits.BinaryBiproduct.bicone X Y).inl = CategoryTheory.Limits.biprod.inl
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.comp_add_le : ∀ {E : Type u_3} {F : Type u_4} [inst : AddCommGroup E] [inst_1 : AddCommGroup F] (p : AddGroupSeminorm E)
  (f g : F →+ E), p.comp (f + g) ≤ p.comp f + p.comp g
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal.0.AugmentedSimplexCategory.leftUnitor.match_1.eq_1 : ∀ (motive : AugmentedSimplexCategory → Sort u_1) (a : SimplexCategory)
  (h_1 : (a : SimplexCategory) → motive (CategoryTheory.WithInitial.of a))
  (h_2 : Unit → motive CategoryTheory.WithInitial.star),
  (match CategoryTheory.WithInitial.of a with
    | CategoryTheory.WithInitial.of a => h_1 a
    | CategoryTheory.WithInitial.star => h_2 ()) =
    h_1 a
-- Mathlib.MeasureTheory.Measure.Complex
/-- A `ComplexMeasure` is a `ℂ`-vector measure.  -/
MeasureTheory.ComplexMeasure : (α : Type u_2) → [MeasurableSpace α] → Type (max u_2 0)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.op_isoWhiskerLeft : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {H : CategoryTheory.Functor E C} (α : F ≅ G),
  CategoryTheory.NatIso.op (H.isoWhiskerLeft α) =
    H.opComp G ≪≫ H.op.isoWhiskerLeft (CategoryTheory.NatIso.op α) ≪≫ (H.opComp F).symm
-- Init.Data.Rat.Lemmas
Rat.mul_def' : ∀ (a b : ℚ), a * b = mkRat (a.num * b.num) (a.den * b.den)
-- Init.Data.BitVec.Lemmas
BitVec.toInt_allOnes : ∀ {w : ℕ}, (BitVec.allOnes w).toInt = if 0 < w then -1 else 0
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.filter!.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (f : (a : α) → β a → Bool) (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.filter! f t =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => Std.DTreeMap.Internal.Impl.leaf
    | Std.DTreeMap.Internal.Impl.inner size k v l r =>
      match f k v with
      | false => (Std.DTreeMap.Internal.Impl.filter! f l).link2! (Std.DTreeMap.Internal.Impl.filter! f r)
      | true =>
        Std.DTreeMap.Internal.Impl.link! k v (Std.DTreeMap.Internal.Impl.filter! f l)
          (Std.DTreeMap.Internal.Impl.filter! f r)
-- Mathlib.Data.Finmap
Finmap.empty_union : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {s₁ : Finmap β}, ∅ ∪ s₁ = s₁
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.values_emptyWithCapacity : ∀ {α : Type u} {c : ℕ} {β : Type v}, (Std.DHashMap.Raw.emptyWithCapacity c).values = []
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- **Alias** of the forward direction of `SimpleGraph.isAcyclic_iff_subsingleton_path`. -/
SimpleGraph.IsAcyclic.subsingleton_path : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsAcyclic → ∀ (u v : V), Subsingleton (G.Path u v)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
/-- The first projection from the mapping cone, as a cocycle of degree `1`.  -/
CochainComplex.mappingCone.fst : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} →
        (φ : F ⟶ G) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            CochainComplex.HomComplex.Cocycle (CochainComplex.mappingCone φ) F 1
-- Mathlib.Analysis.Normed.Algebra.GelfandMazur
/-- Assuming that `‖x - algebraMap ℝ F ·‖` is bounded below by a positive constant, we show that
`φ x w` grows unboundedly as `w : ℝ × ℝ` does. We will use this to obtain a contradiction
when `φ x` does not attain the value zero.  -/
_private.Mathlib.Analysis.Normed.Algebra.GelfandMazur.0.NormedAlgebra.Real.tendsto_φ_cobounded : ∀ {F : Type u_1} [inst : NormedRing F] [inst_1 : NormedAlgebra ℝ F] [NormOneClass F] {x : F} {c : ℝ},
  0 < c →
    (∀ (r : ℝ), c ≤ ‖x - (algebraMap ℝ F) r‖) →
      Filter.Tendsto (fun x_1 => NormedAlgebra.Real.φ✝ x x_1) (Bornology.cobounded (ℝ × ℝ)) (Bornology.cobounded F)
-- Mathlib.Tactic.Linter.FindDeprecations
_private.Mathlib.Tactic.Linter.FindDeprecations.0.Mathlib.Tactic.DeprecationInfo.mk : Lean.Name → Lean.Name → Lean.Position → Lean.Position → String → Mathlib.Tactic.DeprecationInfo✝
-- Mathlib.LinearAlgebra.Matrix.ToLin
endVecAlgEquivMatrixEnd_apply_apply : ∀ (ι : Type u_1) [inst : Fintype ι] [inst_1 : DecidableEq ι] (R : Type u_2) [inst_2 : CommSemiring R] (A : Type u_3)
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (M : Type u_4) [inst_5 : AddCommMonoid M] [inst_6 : Module R M]
  [inst_7 : Module A M] [inst_8 : IsScalarTower R A M] (f : Module.End A (ι → M)) (i j : ι) (x : M),
  ((endVecAlgEquivMatrixEnd ι R A M) f i j) x = f (Pi.single j x) i
-- Init.Data.Array.Sort.Lemmas
Array.mergeSort_empty : ∀ {α : Type u_1} {r : α → α → Bool}, #[].mergeSort r = #[]
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- An additive action is `1`-pretransitive iff it is pretransitive.  -/
AddAction.is_zero_pretransitive_iff : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α],
  AddAction.IsMultiplyPretransitive G α 1 ↔ AddAction.IsPretransitive G α
-- Lean.Meta.DiscrTree.Main
Lean.Meta.DiscrTree.getUnify : {α : Type} → Lean.Meta.DiscrTree α → Lean.Expr → Lean.MetaM (Array α)
-- Init.Data.Int.Order
Int.add_le_zero_iff_le_neg : ∀ {a b : ℤ}, a + b ≤ 0 ↔ a ≤ -b
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.oddKernel_neg : ∀ (a : UnitAddCircle) (x : ℝ), HurwitzZeta.oddKernel (-a) x = -HurwitzZeta.oddKernel a x
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.lt_coe_iff : ∀ {α : Type u_1} [inst : LT α] {x : WithZero α} {b : α}, x < ↑b ↔ ∀ (a : α), x = ↑a → a < b
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_diag : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] (s : Finset ι) (f : ι × ι → M),
  ∏ i ∈ s.diag, f i = ∏ i ∈ s, f (i, i)
-- Mathlib.Data.Int.SuccPred
Int.instIsPredArchimedean : IsPredArchimedean ℤ
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.vadd_opposite_image_add_preimage : ∀ {G : Type u_2} [inst : AddGroup G] {H : AddSubgroup G} (g : G) (h : ↥H.op) (s : Set G),
  (fun y => h +ᵥ y) '' (fun x => g + x) ⁻¹' s = (fun x => g + x) ⁻¹' (fun y => h +ᵥ y) '' s
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_eq_none_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {a : α},
  t.contains a = false → t.get? a = none
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.secondCountableTopology : ∀ {𝕜 : 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] [SecondCountableTopology E]
  (I : ModelWithCorners 𝕜 E H), SecondCountableTopology H
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.SplittingField.instSMulOfIsScalarTower : {K : Type u_2} →
  [inst : Field K] →
    (f : Polynomial K) → {S : Type u_1} → [inst_1 : DistribSMul S K] → [IsScalarTower S K K] → SMul S f.SplittingField
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveCombine.sizeOf_spec : ∀ (c₁ c₂ : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.solveCombine c₁ c₂) = 1 + sizeOf c₁ + sizeOf c₂
-- Mathlib.Analysis.Calculus.ImplicitContDiff
/-- **Alias** of `ContDiffAt.implicitFunction_def`. -/
IsContDiffImplicitAt.implicitFunction_def : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁] [inst_2 : NormedSpace 𝕜 E₁]
  [inst_3 : CompleteSpace E₁] {E₂ : Type u_3} [inst_4 : NormedAddCommGroup E₂] [inst_5 : NormedSpace 𝕜 E₂]
  [inst_6 : CompleteSpace E₂] {F : Type u_4} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F]
  [inst_9 : CompleteSpace F] {u : E₁ × E₂} {f : E₁ × E₂ → F} {n : WithTop ℕ∞} (cdf : ContDiffAt 𝕜 n f u) (pn : n ≠ 0)
  (if₂ : (fderiv 𝕜 f u ∘SL ContinuousLinearMap.inr 𝕜 E₁ E₂).IsInvertible),
  cdf.implicitFunction pn if₂ = ⋯.implicitFunctionOfProdDomain if₂
-- Mathlib.Combinatorics.Matroid.Loop
/-- If two matroids agree on loops and coloops, and have the same independent sets after
loops/coloops are removed, they are equal.  -/
Matroid.ext_indep_disjoint_loops_coloops : ∀ {α : Type u_1} {M₁ M₂ : Matroid α},
  M₁.E = M₂.E →
    M₁.loops = M₂.loops →
      M₁.coloops = M₂.coloops → (∀ I ⊆ M₁.E, Disjoint I (M₁.loops ∪ M₁.coloops) → (M₁.Indep I ↔ M₂.Indep I)) → M₁ = M₂
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.constAlter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {a : α} {f : Option β → Option β}
  {t : Std.DTreeMap.Raw α (fun x => β) cmp}, t.WF → (Std.DTreeMap.Raw.Const.alter t a f).WF
-- Mathlib.MeasureTheory.Measure.AddContent
/-- The value of the content on a set.  -/
MeasureTheory.AddContent.toFun : {α : Type u_1} →
  {G : Type u_2} → [inst : AddCommMonoid G] → {C : Set (Set α)} → MeasureTheory.AddContent G C → Set α → G
-- Mathlib.CategoryTheory.Category.PartialFun
PartialFun.largeCategory : CategoryTheory.LargeCategory PartialFun
-- Mathlib.Algebra.Group.Conj
AddConjClasses.mem_carrier_mk : ∀ {α : Type u} [inst : AddMonoid α] {a : α}, a ∈ (AddConjClasses.mk a).carrier
-- Mathlib.Order.Hom.Order
OrderHom.instSupSet : {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : CompleteLattice β] → SupSet (α →o β)
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_mul_iff_mul_left_eq`. -/
Ordinal.principal_mul_iff_mul_left_eq : ∀ {o : Ordinal.{u}}, Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) o ↔ ∀ (a : Ordinal.{u}), 0 < a → a < o → a * o = o
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.State.steps : Lean.Meta.Grind.AC.State → ℕ
-- Lean.Data.Lsp.Internal
Lean.Lsp.instHashableRefIdent : Hashable Lean.Lsp.RefIdent
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.natCast_lt_of_isSuccLimit : ∀ {o : Ordinal.{u_4}}, Order.IsSuccLimit o → ∀ (n : ℕ), ↑n < o
-- Init.ShareCommon
ShareCommon.StateFactoryImpl.mk.injEq : ∀ (Map Set : Type) (mkState : Unit → Map × Set) (mapFind? : Map → ShareCommon.Object → Option ShareCommon.Object)
  (mapInsert : Map → ShareCommon.Object → ShareCommon.Object → Map)
  (setFind? : Set → ShareCommon.Object → Option ShareCommon.Object) (setInsert : Set → ShareCommon.Object → Set)
  (Map_1 Set_1 : Type) (mkState_1 : Unit → Map_1 × Set_1)
  (mapFind?_1 : Map_1 → ShareCommon.Object → Option ShareCommon.Object)
  (mapInsert_1 : Map_1 → ShareCommon.Object → ShareCommon.Object → Map_1)
  (setFind?_1 : Set_1 → ShareCommon.Object → Option ShareCommon.Object)
  (setInsert_1 : Set_1 → ShareCommon.Object → Set_1),
  ({ Map := Map, Set := Set, mkState := mkState, mapFind? := mapFind?, mapInsert := mapInsert, setFind? := setFind?,
        setInsert := setInsert } =
      { Map := Map_1, Set := Set_1, mkState := mkState_1, mapFind? := mapFind?_1, mapInsert := mapInsert_1,
        setFind? := setFind?_1, setInsert := setInsert_1 }) =
    (Map = Map_1 ∧
      Set = Set_1 ∧
        mkState ≍ mkState_1 ∧
          mapFind? ≍ mapFind?_1 ∧ mapInsert ≍ mapInsert_1 ∧ setFind? ≍ setFind?_1 ∧ setInsert ≍ setInsert_1)
-- Mathlib.Analysis.Normed.Ring.Basic
/-- If `α` is a seminormed ring, then `‖a ^ n‖ ≤ ‖a‖ ^ n` for `n > 0`. See also `norm_pow_le`.  -/
norm_pow_le' : ∀ {α : Type u_2} [inst : SeminormedRing α] (a : α) {n : ℕ}, 0 < n → ‖a ^ n‖ ≤ ‖a‖ ^ n
-- Mathlib.Topology.MetricSpace.Defs
instMetricSpacePUnit : MetricSpace PUnit.{u + 1}
-- Mathlib.Order.BoundedOrder.Basic
Pi.instOrderTop.eq_1 : ∀ {ι : Type u_1} {α' : ι → Type u_2} [inst : (i : ι) → LE (α' i)] [inst_1 : (i : ι) → OrderTop (α' i)],
  Pi.instOrderTop = { toTop := Pi.instTopForall, le_top := ⋯ }
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Var
Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go_denote_eq : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (a : ℕ) (assign : Std.Tactic.BVDecide.BVExpr.Assignment)
  (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ) (hidx1 : idx < w),
  curr ≤ idx →
    ⟦assign.toAIGAssignment,
        { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go aig w a curr s hcurr).aig,
          ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastVar.go aig w a curr s hcurr).vec.get idx hidx1 }⟧ =
      (Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.var a)).getLsbD idx