mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.CircleIntegral
/-- Eta-expanded form of `CircleIntegrable.const_smul`

---

If `f` is circle integrable, then so are its scalar multiples.  -/
CircleIntegrable.const_fun_smul : ∀ {c : ℂ} {R : ℝ} {A : Type u_2} [inst : NormedRing A] {a : A} {f : ℂ → A},
  CircleIntegrable f c R → CircleIntegrable (fun i => a • f i) c R
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddSubmonoid.LocalizationMap.ofAddEquivOfLocalizations_id : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N), f.ofAddEquivOfLocalizations (AddEquiv.refl N) = f
-- Mathlib.Topology.Category.Profinite.EffectiveEpi
Profinite.effectiveEpi_tfae : ∀ {B X : Profinite} (π : X ⟶ B),
  [CategoryTheory.EffectiveEpi π, CategoryTheory.Epi π,
      Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)].TFAE
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.RightHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono φ h).ι = h.ι
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_nnrpow_inv : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] (a : A) {x : NNReal},
  x ≠ 0 → autoParam (0 ≤ a) CFC.nnrpow_nnrpow_inv._auto_1 → (a ^ x) ^ x⁻¹ = a
-- Mathlib.Algebra.Category.Grp.Limits
/-- The forgetful functor from commutative groups to groups preserves all limits.
(That is, the underlying group could have been computed instead as limits in the category
of groups.)
 -/
CommGrpCat.forget₂Group_preservesLimitsOfSize : CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ CommGrpCat GrpCat)
-- Mathlib.Data.Finset.Erase
Finset.erase_injOn : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α), Set.InjOn s.erase ↑s
-- Init.Data.Stream
Std.Stream.next? : {stream : Type u} → {value : outParam (Type v)} → [self : Std.Stream stream value] → stream → Option (value × stream)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.comp_τ₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ sq₃ : CategoryTheory.Square C} (f : sq₁.Hom sq₂)
  (g : sq₂.Hom sq₃), (f.comp g).τ₄ = CategoryTheory.CategoryStruct.comp f.τ₄ g.τ₄
-- Mathlib.Data.Set.Prod
Set.eval_preimage : ∀ {ι : Type u_1} {α : ι → Type u_2} {i : ι} [inst : DecidableEq ι] {s : Set (α i)},
  Function.eval i ⁻¹' s = Set.univ.pi (Function.update (fun x => Set.univ) i s)
-- Lean.Structure
Lean.StructureResolutionOrderConflict.isDirectParent : Lean.StructureResolutionOrderConflict → Bool
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.rotateL.eq_2 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (rk : α) (rv : β rk)
  (rr : Std.DTreeMap.Internal.Impl α β) (ls : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.rotateL k v l rk rv (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr) rr =
    if (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size < Std.DTreeMap.Internal.ratio * rr.size then
      Std.DTreeMap.Internal.Impl.singleL k v l rk rv (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr) rr
    else Std.DTreeMap.Internal.Impl.doubleL k v l rk rv lk lv ll lr rr
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.mk.injEq : ∀ (G : Option Std.Time.Year.Era) (y u Y : Option Std.Time.Year.Offset) (D : Option (Sigma Std.Time.Day.Ordinal.OfYear))
  (M L : Option Std.Time.Month.Ordinal) (d : Option Std.Time.Day.Ordinal) (Q q : Option Std.Time.Month.Quarter)
  (w : Option Std.Time.Week.OfYear.Ordinal) (W : Option Std.Time.Week.Ordinal) (E e c : Option Std.Time.Weekday)
  (F : Option (Std.Time.Internal.Bounded.LE 1 5)) (a : Option Std.Time.HourMarker) (b : Option Std.Time.DayPeriod)
  (B : Option Std.Time.ExtendedDayPeriod) (h : Option (Std.Time.Internal.Bounded.LE 1 12))
  (K : Option (Std.Time.Internal.Bounded.LE 0 11)) (k : Option (Std.Time.Internal.Bounded.LE 1 24))
  (H : Option Std.Time.Hour.Ordinal) (m : Option Std.Time.Minute.Ordinal) (s : Option (Std.Time.Second.Ordinal true))
  (S : Option Std.Time.Nanosecond.Ordinal) (A : Option Std.Time.Millisecond.Offset)
  (n : Option Std.Time.Nanosecond.Ordinal) (N : Option Std.Time.Nanosecond.Offset) (V z zabbrev v : Option String)
  (O X x Z : Option Std.Time.TimeZone.Offset) (G_1 : Option Std.Time.Year.Era)
  (y_1 u_1 Y_1 : Option Std.Time.Year.Offset) (D_1 : Option (Sigma Std.Time.Day.Ordinal.OfYear))
  (M_1 L_1 : Option Std.Time.Month.Ordinal) (d_1 : Option Std.Time.Day.Ordinal)
  (Q_1 q_1 : Option Std.Time.Month.Quarter) (w_1 : Option Std.Time.Week.OfYear.Ordinal)
  (W_1 : Option Std.Time.Week.Ordinal) (E_1 e_1 c_1 : Option Std.Time.Weekday)
  (F_1 : Option (Std.Time.Internal.Bounded.LE 1 5)) (a_1 : Option Std.Time.HourMarker) (b_1 : Option Std.Time.DayPeriod)
  (B_1 : Option Std.Time.ExtendedDayPeriod) (h_1 : Option (Std.Time.Internal.Bounded.LE 1 12))
  (K_1 : Option (Std.Time.Internal.Bounded.LE 0 11)) (k_1 : Option (Std.Time.Internal.Bounded.LE 1 24))
  (H_1 : Option Std.Time.Hour.Ordinal) (m_1 : Option Std.Time.Minute.Ordinal)
  (s_1 : Option (Std.Time.Second.Ordinal true)) (S_1 : Option Std.Time.Nanosecond.Ordinal)
  (A_1 : Option Std.Time.Millisecond.Offset) (n_1 : Option Std.Time.Nanosecond.Ordinal)
  (N_1 : Option Std.Time.Nanosecond.Offset) (V_1 z_1 zabbrev_1 v_1 : Option String)
  (O_1 X_1 x_1 Z_1 : Option Std.Time.TimeZone.Offset), ⋯ = ⋯
-- Std.Time.DateTime
Std.Time.DateTime.instHSubOffset_5 : HSub Std.Time.DateTime Std.Time.Millisecond.Offset Std.Time.DateTime
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_preimage_vadd : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) (s : Set α),
  μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s
-- Init.Grind.Module.Basic
_private.Init.Grind.Module.Basic.0.Lean.Grind.IntModule.mul_zsmul_aux : ∀ {M : Type u} [inst : Lean.Grind.IntModule M] (n : ℕ) (m : ℤ) (a : M), (↑n * m) • a = ↑n • m • a
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_app_snd_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) {X : Type u₄} {Y : Type u₅}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] [inst_4 : CategoryTheory.Category.{v₅, u₅} Y]
  {U V : CategoryTheory.Functor X Y} (α : U ⟶ V) (x : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y)
  (X_1 : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).map α).app x).snd.app X_1 =
    x.snd.map (α.app X_1)
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- Expression for `hurwitzZetaEven a 1` as a limit. (Mathematically `hurwitzZetaEven a 1` is
undefined, but our construction assigns some value to it; this lemma is mostly of interest for
determining what that value is).  -/
HurwitzZeta.tendsto_hurwitzZetaEven_sub_one_div_nhds_one : ∀ (a : UnitAddCircle),
  Filter.Tendsto (fun s => HurwitzZeta.hurwitzZetaEven a s - 1 / (s - 1) / s.Gammaℝ) (nhds 1)
    (nhds (HurwitzZeta.hurwitzZetaEven a 1))
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.mul_X_pow_inj : ∀ {R : Type u_1} [inst : Semiring R] {k : ℕ} {φ ψ : PowerSeries R},
  φ * PowerSeries.X ^ k = ψ * PowerSeries.X ^ k ↔ φ = ψ
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ContinuousOn.ennreal_mul : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f g : α → ENNReal} {s : Set α},
  ContinuousOn f s →
    ContinuousOn g s → (∀ x ∈ s, f x ≠ 0 ∨ g x ≠ ⊤) → (∀ x ∈ s, g x ≠ 0 ∨ f x ≠ ⊤) → ContinuousOn (fun x => f x * g x) s
-- Mathlib.CategoryTheory.Preadditive.Biproducts
CategoryTheory.Preadditive.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {x y : CategoryTheory.Preadditive C},
  x = y ↔ CategoryTheory.Preadditive.homGroup = CategoryTheory.Preadditive.homGroup
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.unopFunctorCompFst_hom_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L.op R.op),
  (CategoryTheory.Comma.unopFunctorCompFst L R).hom.app X = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.RingTheory.Coalgebra.MonoidAlgebra
AddMonoidAlgebra.comul_single : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] {X : Type u_3} [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] (x : X) (a : A),
  CoalgebraStruct.comul (AddMonoidAlgebra.single x a) =
    (TensorProduct.map (AddMonoidAlgebra.lsingle x) (AddMonoidAlgebra.lsingle x)) (CoalgebraStruct.comul a)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.nameNotRoundtrippable.containsNum : Lean.Name → Bool
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.uSwitchEquiv_naturality : ∀ {X Y : FintypeCat} (f : X ⟶ Y) (x : (FintypeCat.uSwitch.obj X).obj),
  (CategoryTheory.ConcreteCategory.hom f) (X.uSwitchEquiv x) =
    Y.uSwitchEquiv ((CategoryTheory.ConcreteCategory.hom (FintypeCat.uSwitch.map f)) x)
-- Init.Data.Order.Lemmas
Classical.Order.instLawfulOrderBEq : ∀ {α : Type u} [inst : LE α], Std.LawfulOrderBEq α
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.State.mk.injEq : ∀ (cache : Lean.Meta.Simp.Cache) (failureCache : Lean.ExprSet) (numSteps : ℕ) (msgLog : List String)
  (morTheorems transitionTheorems : Mathlib.Meta.FunProp.GeneralTheorems) (cache_1 : Lean.Meta.Simp.Cache)
  (failureCache_1 : Lean.ExprSet) (numSteps_1 : ℕ) (msgLog_1 : List String)
  (morTheorems_1 transitionTheorems_1 : Mathlib.Meta.FunProp.GeneralTheorems),
  ({ cache := cache, failureCache := failureCache, numSteps := numSteps, msgLog := msgLog, morTheorems := morTheorems,
        transitionTheorems := transitionTheorems } =
      { cache := cache_1, failureCache := failureCache_1, numSteps := numSteps_1, msgLog := msgLog_1,
        morTheorems := morTheorems_1, transitionTheorems := transitionTheorems_1 }) =
    (cache = cache_1 ∧
      failureCache = failureCache_1 ∧
        numSteps = numSteps_1 ∧
          msgLog = msgLog_1 ∧ morTheorems = morTheorems_1 ∧ transitionTheorems = transitionTheorems_1)
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.rightCont_eq_of_exists_gt : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : LinearOrder ι] (𝓕 : MeasureTheory.Filtration ι m)
  {i : ι}, (∃ j > i, Set.Ioo i j = ∅) → ↑𝓕.rightCont i = ↑𝓕 i
-- Mathlib.SetTheory.Lists
Lists.Equiv.antisymm : ∀ {α : Type u_1} {l₁ l₂ : Lists' α true}, l₁.Subset l₂ → l₂.Subset l₁ → Lists.Equiv ⟨true, l₁⟩ ⟨true, l₂⟩
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived
CategoryTheory.LocalizerMorphism.isIso_iff_of_isRightDerivabilityStructure : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {H : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} H] {D₁ : Type u₄}
  {D₂ : Type u₅} [inst_3 : CategoryTheory.Category.{v₄, u₄} D₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} D₂]
  {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂}
  (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂)
  [inst_5 : L₁.IsLocalization W₁] [inst_6 : L₂.IsLocalization W₂] (F : CategoryTheory.Functor C₂ H)
  (F₁ : CategoryTheory.Functor D₁ H) (α₁ : Φ.functor.comp F ⟶ L₁.comp F₁) (F₂ : CategoryTheory.Functor D₂ H)
  (α₂ : F ⟶ L₂.comp F₂) [F₁.IsRightDerivedFunctor α₁ W₁] [Φ.IsRightDerivabilityStructure]
  [(Φ.functor.comp F).HasPointwiseRightDerivedFunctor W₁] [F₂.IsRightDerivedFunctor α₂ W₂] (X : C₁),
  CategoryTheory.IsIso (α₁.app X) ↔ CategoryTheory.IsIso (α₂.app (Φ.functor.obj X))
-- Mathlib.RingTheory.PowerSeries.Basic
/-- Change of coefficients in power series, as an `AlgHom`  -/
PowerSeries.mapAlgHom : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Semiring B] → [inst_4 : Algebra R B] → (A →ₐ[R] B) → PowerSeries A →ₐ[R] PowerSeries B
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.instOneHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier : (X : TopCat) → (R : TopCommRingCat) → One (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
-- Mathlib.Algebra.Lie.Free
instInhabitedFreeLieAlgebra : (R : Type u) → (X : Type v) → [inst : CommRing R] → Inhabited (FreeLieAlgebra R X)
-- Init.Data.Nat.Div.Lemmas
Nat.add_mod_eq_sub : ∀ {a b c : ℕ}, (a + b) % c = a % c + b % c - if a % c + b % c < c then 0 else c
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.mem_of_mem_map : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w} [EquivBEq α]
  [LawfulHashable α] {f : (a : α) → β a → γ a} {k : α}, k ∈ Std.DHashMap.map f m → k ∈ m
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.SimprocsArray : Type
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roo_eq_nil_iff : ∀ {m n : ℕ}, (m<...n).toList = [] ↔ n ≤ m + 1
-- Mathlib.FieldTheory.Minpoly.Basic
/-- A minimal polynomial is monic.  -/
minpoly.monic : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B},
  IsIntegral A x → (minpoly A x).Monic
-- Lean.Data.Trie
Lean.Data.Trie.instToString : {α : Type} → ToString (Lean.Data.Trie α)
-- Init.Data.Vector.Lemmas
Vector.reverse_eq_iff : ∀ {α : Type u_1} {n : ℕ} {xs ys : Vector α n}, xs.reverse = ys ↔ xs = ys.reverse
-- Mathlib.LinearAlgebra.Matrix.Adjugate
/-- `cramerMap A b i` is the determinant of the matrix `A` with column `i` replaced with `b`,
and thus `cramerMap A b` is the vector output by Cramer's rule on `A` and `b`.

If `A * x = b` has a unique solution in `x`, `cramerMap A` sends the vector `b` to `A.det • x`.
Otherwise, the outcome of `cramerMap` is well-defined but not necessarily useful.
 -/
Matrix.cramerMap : {n : Type v} → {α : Type w} → [DecidableEq n] → [Fintype n] → [CommRing α] → Matrix n n α → (n → α) → n → α
-- Mathlib.Data.Nat.Factorization.Defs
/-- If `a = ∏ pᵢ ^ nᵢ` and `b = ∏ pᵢ ^ mᵢ`, then `factorizationLCMLeft = ∏ pᵢ ^ kᵢ`, where
`kᵢ = nᵢ` if `mᵢ ≤ nᵢ` and `0` otherwise. Note that the product is over the divisors of `lcm a b`,
so if one of `a` or `b` is `0` then the result is `1`.  -/
Nat.factorizationLCMLeft : ℕ → ℕ → ℕ
-- Mathlib.Algebra.GroupWithZero.Defs
CancelMonoidWithZero.mk : {M₀ : Type u_2} → (toMonoidWithZero : MonoidWithZero M₀) → IsCancelMulZero M₀ → CancelMonoidWithZero M₀
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndependent.pair_smul_smul_iff : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M} {u v : R},
  IsUnit u → IsUnit v → (LinearIndependent R ![u • x, v • y] ↔ LinearIndependent R ![x, y])
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.mem_right_iff_eq_zero_of_disjoint : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p p' : Submodule R M}, Disjoint p p' → ∀ {x : ↥p}, ↑x ∈ p' ↔ x = 0
-- Mathlib.Data.Finsupp.Single
Finsupp.support_single_disjoint : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {b b' : M},
  b ≠ 0 → b' ≠ 0 → ∀ {i j : α}, Disjoint (fun₀ | i => b).support (fun₀ | j => b').support ↔ i ≠ j
-- Mathlib.Analysis.InnerProductSpace.JointEigenspace
/-- Given a commuting pair of symmetric linear operators on a finite-dimensional inner product
space, the space decomposes as an internal direct sum of simultaneous eigenspaces of these
operators.  -/
LinearMap.IsSymmetric.directSum_isInternal_of_commute : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {A B : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E],
  A.IsSymmetric →
    B.IsSymmetric →
      Commute A B → DirectSum.IsInternal fun i => Module.End.eigenspace A i.2 ⊓ Module.End.eigenspace B i.1
-- Lean.Meta.Basic
Lean.Meta.Config.mk.injEq : ∀
  (foApprox ctxApprox quasiPatternApprox constApprox isDefEqStuckEx unificationHints proofIrrelevance
    assignSyntheticOpaque offsetCnstrs : Bool)
  (transparency : Lean.Meta.TransparencyMode) (etaStruct : Lean.Meta.EtaStructMode) (univApprox iota beta : Bool)
  (proj : Lean.Meta.ProjReductionKind)
  (zeta zetaDelta zetaUnused zetaHave foApprox_1 ctxApprox_1 quasiPatternApprox_1 constApprox_1 isDefEqStuckEx_1
    unificationHints_1 proofIrrelevance_1 assignSyntheticOpaque_1 offsetCnstrs_1 : Bool)
  (transparency_1 : Lean.Meta.TransparencyMode) (etaStruct_1 : Lean.Meta.EtaStructMode)
  (univApprox_1 iota_1 beta_1 : Bool) (proj_1 : Lean.Meta.ProjReductionKind)
  (zeta_1 zetaDelta_1 zetaUnused_1 zetaHave_1 : Bool),
  ({ foApprox := foApprox, ctxApprox := ctxApprox, quasiPatternApprox := quasiPatternApprox, constApprox := constApprox,
        isDefEqStuckEx := isDefEqStuckEx, unificationHints := unificationHints, proofIrrelevance := proofIrrelevance,
        assignSyntheticOpaque := assignSyntheticOpaque, offsetCnstrs := offsetCnstrs, transparency := transparency,
        etaStruct := etaStruct, univApprox := univApprox, iota := iota, beta := beta, proj := proj, zeta := zeta,
        zetaDelta := zetaDelta, zetaUnused := zetaUnused, zetaHave := zetaHave } =
      { foApprox := foApprox_1, ctxApprox := ctxApprox_1, quasiPatternApprox := quasiPatternApprox_1,
        constApprox := constApprox_1, isDefEqStuckEx := isDefEqStuckEx_1, unificationHints := unificationHints_1,
        proofIrrelevance := proofIrrelevance_1, assignSyntheticOpaque := assignSyntheticOpaque_1,
        offsetCnstrs := offsetCnstrs_1, transparency := transparency_1, etaStruct := etaStruct_1,
        univApprox := univApprox_1, iota := iota_1, beta := beta_1, proj := proj_1, zeta := zeta_1,
        zetaDelta := zetaDelta_1, zetaUnused := zetaUnused_1, zetaHave := zetaHave_1 }) =
    (foApprox = foApprox_1 ∧
      ctxApprox = ctxApprox_1 ∧
        quasiPatternApprox = quasiPatternApprox_1 ∧
          constApprox = constApprox_1 ∧
            isDefEqStuckEx = isDefEqStuckEx_1 ∧
              unificationHints = unificationHints_1 ∧
                proofIrrelevance = proofIrrelevance_1 ∧
                  assignSyntheticOpaque = assignSyntheticOpaque_1 ∧
                    offsetCnstrs = offsetCnstrs_1 ∧
                      transparency = transparency_1 ∧
                        etaStruct = etaStruct_1 ∧
                          univApprox = univApprox_1 ∧
                            iota = iota_1 ∧
                              beta = beta_1 ∧
                                proj = proj_1 ∧
                                  zeta = zeta_1 ∧
                                    zetaDelta = zetaDelta_1 ∧ zetaUnused = zetaUnused_1 ∧ zetaHave = zetaHave_1)
-- Mathlib.Topology.Constructions
Filter.Tendsto.finInsertNth : ∀ {Y : Type v} {n : ℕ} {A : Fin (n + 1) → Type u_9} [inst : (i : Fin (n + 1)) → TopologicalSpace (A i)]
  (i : Fin (n + 1)) {f : Y → A i} {g : Y → (j : Fin n) → A (i.succAbove j)} {l : Filter Y} {x : A i}
  {y : (j : Fin n) → A (i.succAbove j)},
  Filter.Tendsto f l (nhds x) →
    Filter.Tendsto g l (nhds y) → Filter.Tendsto (fun a => i.insertNth (f a) (g a)) l (nhds (i.insertNth x y))
-- Mathlib.Algebra.Group.Translate
support_translate : ∀ {G : Type u_5} {H : Type u_6} [inst : AddCommGroup G] [inst_1 : AddCommGroup H] (a : G) (f : G → H),
  Function.support (translate a f) = a +ᵥ Function.support f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [inst_2 : Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α}
  (contains_eq_false : (List.map Sigma.fst l).contains k = false) {h' : k ∈ t.insertMany l},
  (t.insertMany l).getKey k h' = t.getKey k ⋯
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Coproduct of two continuous homomorphisms to the same space.  -/
ContinuousAddMonoidHom.coprod : {A : Type u_2} →
  {B : Type u_3} →
    {E : Type u_6} →
      [inst : AddMonoid A] →
        [inst_1 : AddMonoid B] →
          [inst_2 : TopologicalSpace A] →
            [inst_3 : TopologicalSpace B] →
              [inst_4 : AddCommMonoid E] →
                [inst_5 : TopologicalSpace E] → [ContinuousAdd E] → (A →ₜ+ E) → (B →ₜ+ E) → A × B →ₜ+ E
-- Init.Data.Nat.Lemmas
Nat.one_add_sub_one : ∀ (n : ℕ), 1 + n - 1 = n
-- Std.Data.TreeMap.Raw.Lemmas
/-- Simpler variant of `getD_filterMap` when `LawfulEqCmp` is available.  -/
Std.TreeMap.Raw.getD_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → Option γ} {k : α} {fallback : γ},
  t.WF → (Std.TreeMap.Raw.filterMap f t).getD k fallback = (t[k]?.bind (f k)).getD fallback
-- Std.Data.HashSet.Lemmas
Std.HashSet.all_eq_false_iff_exists_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [LawfulBEq α] {p : α → Bool},
  m.all p = false ↔ ∃ a ∈ m, p a = false
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.braiding_hom_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {s : CategoryTheory.Limits.BinaryFan X Y}
  (P : CategoryTheory.Limits.IsLimit s) {t : CategoryTheory.Limits.BinaryFan Y X} (Q : CategoryTheory.Limits.IsLimit t),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding P Q).hom t.fst = s.snd
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
Homeomorph.transOpenPartialHomeomorph_trans : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} {Z' : Type u_6} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] [inst_3 : TopologicalSpace Z'] (e : X ≃ₜ Y) (f : OpenPartialHomeomorph Y Z)
  (f' : OpenPartialHomeomorph Z Z'),
  (e.transOpenPartialHomeomorph f).trans f' = e.transOpenPartialHomeomorph (f.trans f')