ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : Category.{?u.45742, u_1} C<VAR>inst✝⁵ : Category.{?u.45746, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>G : Type u_4<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : HasShift C G<VAR>inst✝ : F.ShiftSequence M<VAR>n m a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>m + n + a = a''
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : Category.{u_6, u_1} C<VAR>inst✝⁵ : Category.{u_5, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>G : Type u_4<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : HasShift C G<VAR>inst✝ : F.ShiftSequence M<VAR>n m a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>(F.shiftIso (m + n) a a'' ⋯).hom.app X = (F.shift a).map ((shiftFunctorAdd C m n).hom.app X) ≫ (F.shiftIso n a a' ha').hom.app ((shiftFunctor C m).obj X) ≫ (F.shiftIso m a' a'' ha'').hom.app X
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>α β : PartialFun<VAR>e : α ≃ β<GOAL>↑(⇑e.symm ∘ ⇑e) = 𝟙 α
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>α β : PartialFun<VAR>e : α ≃ β<GOAL>PFun.id α = 𝟙 α
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>α β : PartialFun<VAR>e : α ≃ β<GOAL>↑(⇑e ∘ ⇑e.symm) = 𝟙 β
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>α β : PartialFun<VAR>e : α ≃ β<GOAL>PFun.id β = 𝟙 β
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>inst✝ : (↑P).Normal<VAR>fP : (↑P).FiniteIndex<VAR>h : p ∣ (↑P).index<GOAL>False
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>inst✝ : (↑P).Normal<VAR>fP : (↑P).FiniteIndex<VAR>h : p ∣ Nat.card (G ⧸ ↑P)<GOAL>False
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>inst✝ : (↑P).Normal<VAR>fP : (↑P).FiniteIndex<VAR>h : p ∣ Nat.card (G ⧸ ↑P)<VAR>x : G ⧸ ↑P<VAR>hx : orderOf x = p<GOAL>False
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>inst✝ : (↑P).Normal<VAR>fP : (↑P).FiniteIndex<VAR>h✝ : p ∣ Nat.card (G ⧸ ↑P)<VAR>x : G ⧸ ↑P<VAR>hx : orderOf x = p<VAR>h : IsPGroup p ↥(zpowers x)<GOAL>False
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>inst✝ : (↑P).Normal<VAR>fP : (↑P).FiniteIndex<VAR>h✝ : p ∣ Nat.card (G ⧸ ↑P)<VAR>x : G ⧸ ↑P<VAR>hx : orderOf x = p<VAR>h : IsPGroup p ↥(zpowers x)<VAR>Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)<GOAL>False
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>inst✝ : (↑P).Normal<VAR>fP : (↑P).FiniteIndex<VAR>h✝ : p ∣ Nat.card (G ⧸ ↑P)<VAR>x : G ⧸ ↑P<VAR>hx : orderOf x = p<VAR>h : IsPGroup p ↥(zpowers x)<VAR>Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)<VAR>hQ : IsPGroup p ↥Q<GOAL>False
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>P : Sylow p G<VAR>inst✝ : (↑P).Normal<VAR>fP : (↑P).FiniteIndex<VAR>h✝ : p ∣ Nat.card (G ⧸ ↑P)<VAR>x : G ⧸ ↑P<VAR>hx : orderOf x = p<VAR>h : IsPGroup p ↥(zpowers x)<VAR>Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)<VAR>hQ : IsPGroup p ↥Q<VAR>hp : ¬x = 1<GOAL>False
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>P : Sylow p G<VAR>inst✝ : (↑P).Normal<VAR>fP : (↑P).FiniteIndex<VAR>h✝ : p ∣ Nat.card (G ⧸ ↑P)<VAR>x : G ⧸ ↑P<VAR>hx : orderOf x = p<VAR>h : IsPGroup p ↥(zpowers x)<VAR>Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)<VAR>hQ : IsPGroup p ↥Q<VAR>hp : ↑P < comap (QuotientGroup.mk' ↑P) (zpowers x)<GOAL>False
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>r : Rˣ<VAR>s : R<VAR>a : A<VAR>h : IsUnit (r • ↑ₐ s - a)<GOAL>(↑ₐ s - r⁻¹ • a) * r • ↑h.unit⁻¹ = 1
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>r : Rˣ<VAR>s : R<VAR>a : A<VAR>h : IsUnit (r • ↑ₐ s - a)<GOAL>r • ↑h.unit⁻¹ * (↑ₐ s - r⁻¹ • a) = 1
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝ : CommMonoid M<VAR>s₂ s₁ s : Finset α<VAR>a : α<VAR>g f : α → M<VAR>n : ℕ<GOAL>∏ x ∈ Ico 1 (n + 1 + 1), x = (n + 1)!
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b✝ c u : αˣ<VAR>a b : α<VAR>h : a = b * ↑c⁻¹<GOAL>a * ↑c = b
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b✝ c u : αˣ<VAR>a b : α<VAR>h : a * ↑c = b<GOAL>a = b * ↑c⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p✝ : PMF α<VAR>f✝ : (a : α) → a ∈ p✝.support → PMF β<VAR>p : PMF α<VAR>q : PMF β<VAR>f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ<GOAL>(p.bindOnSupport fun a ha => q.bindOnSupport (f a ha)) = q.bindOnSupport fun b hb => p.bindOnSupport fun a ha => f a ha b hb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p✝ : PMF α<VAR>f✝ : (a : α) → a ∈ p✝.support → PMF β<VAR>p : PMF α<VAR>q : PMF β<VAR>f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ<GOAL>∀ (x : γ), (p.bindOnSupport fun a ha => q.bindOnSupport (f a ha)) x = (q.bindOnSupport fun b hb => p.bindOnSupport fun a ha => f a ha b hb) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p✝ : PMF α<VAR>f✝ : (a : α) → a ∈ p✝.support → PMF β<VAR>p : PMF α<VAR>q : PMF β<VAR>f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ<VAR>c : γ<GOAL>(p.bindOnSupport fun a ha => q.bindOnSupport (f a ha)) c = (q.bindOnSupport fun b hb => p.bindOnSupport fun a ha => f a ha b hb) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p✝ : PMF α<VAR>f✝ : (a : α) → a ∈ p✝.support → PMF β<VAR>p : PMF α<VAR>q : PMF β<VAR>f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ<VAR>c : γ<GOAL>(∑' (a : α) (i : β), p a * if h : p a = 0 then 0 else q i * if h : q i = 0 then 0 else (f a ⋯ i h) c) = ∑' (a : β) (i : α), q a * if h : q a = 0 then 0 else p i * if h : p i = 0 then 0 else (f i h a ⋯) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p✝ : PMF α<VAR>f✝ : (a : α) → a ∈ p✝.support → PMF β<VAR>p : PMF α<VAR>q : PMF β<VAR>f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ<VAR>c : γ<VAR>b : β<VAR>a : α<GOAL>(p a * if h : p a = 0 then 0 else q b * if h : q b = 0 then 0 else (f a ⋯ b h) c) = q b * if h : q b = 0 then 0 else p a * if h : p a = 0 then 0 else (f a h b ⋯) c
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>W X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝ : HasPushout f g<GOAL>pushout.inl g f ≫ (pushoutSymmetry f g).inv = pushout.inr f g
<VAR>x y : ℂ<GOAL>tanh ((starRingEnd ℂ) x) = (starRingEnd ℂ) (tanh x)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>c✝ c : Con M<GOAL>conGen ⇑c ≤ c
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Mul M<VAR>inst✝¹ : Mul N<VAR>inst✝ : Mul P<VAR>c✝ c : Con M<GOAL>sInf {s | ∀ (x y : M), c x y → s x y} ≤ c
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>K : Type u_3<VAR>V : Type u_4<VAR>V' : Type u_5<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>hs : LinearIndependent (ι := { x // x ∈ s }) K Subtype.val<GOAL>range ⇑(extend hs) = hs.extend ⋯
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f g : R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>hu₁ : ∀ x ∈ U, g ∈ x.asIdeal.primeCompl<VAR>hu₂ : ∀ x ∈ U, f ∈ x.asIdeal.primeCompl<GOAL>const R f g U hu₁ * const R g f U hu₂ = 1
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>υ : Type u_3<VAR>R : Type u_4<VAR>inst✝ : CommSemiring R<VAR>x : σ → R<GOAL>comap (AlgHom.id R (MvPolynomial σ R)) x = x
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>υ : Type u_3<VAR>R : Type u_4<VAR>inst✝ : CommSemiring R<VAR>x : σ → R<VAR>i : σ<GOAL>comap (AlgHom.id R (MvPolynomial σ R)) x i = x i
<VAR>a b c : ℕ<GOAL>Ico a (a + 1) = {a}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module ℝ E<VAR>s✝ t : Set E<VAR>x✝ : E<VAR>a✝ : ℝ<VAR>α : Type u_4<VAR>inst✝⁴ : LinearOrderedField α<VAR>inst✝³ : MulActionWithZero α ℝ<VAR>inst✝² : OrderedSMul α ℝ<VAR>inst✝¹ : MulActionWithZero α E<VAR>inst✝ : IsScalarTower α ℝ (Set E)<VAR>s : Set E<VAR>a : α<VAR>ha : 0 ≤ a<VAR>x : E<VAR>ha' : 0 < a<GOAL>gauge s (a • x) = a • gauge s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module ℝ E<VAR>s✝ t : Set E<VAR>x✝ : E<VAR>a✝ : ℝ<VAR>α : Type u_4<VAR>inst✝⁴ : LinearOrderedField α<VAR>inst✝³ : MulActionWithZero α ℝ<VAR>inst✝² : OrderedSMul α ℝ<VAR>inst✝¹ : MulActionWithZero α E<VAR>inst✝ : IsScalarTower α ℝ (Set E)<VAR>s : Set E<VAR>a : α<VAR>ha : 0 ≤ a<VAR>x : E<VAR>ha' : 0 < a<GOAL>sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s} = sInf (a • {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s})
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module ℝ E<VAR>s✝ t : Set E<VAR>x✝ : E<VAR>a✝ : ℝ<VAR>α : Type u_4<VAR>inst✝⁴ : LinearOrderedField α<VAR>inst✝³ : MulActionWithZero α ℝ<VAR>inst✝² : OrderedSMul α ℝ<VAR>inst✝¹ : MulActionWithZero α E<VAR>inst✝ : IsScalarTower α ℝ (Set E)<VAR>s : Set E<VAR>a : α<VAR>ha : 0 ≤ a<VAR>x : E<VAR>ha' : 0 < a<VAR>r : ℝ<GOAL>r ∈ {r | r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s} ↔ r ∈ a • {r | r ∈ Ioi 0 ∧ r⁻¹ • x ∈ s}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module ℝ E<VAR>s✝ t : Set E<VAR>x✝ : E<VAR>a✝ : ℝ<VAR>α : Type u_4<VAR>inst✝⁴ : LinearOrderedField α<VAR>inst✝³ : MulActionWithZero α ℝ<VAR>inst✝² : OrderedSMul α ℝ<VAR>inst✝¹ : MulActionWithZero α E<VAR>inst✝ : IsScalarTower α ℝ (Set E)<VAR>s : Set E<VAR>a : α<VAR>ha : 0 ≤ a<VAR>x : E<VAR>ha' : 0 < a<VAR>r : ℝ<GOAL>r ∈ Ioi 0 ∧ r⁻¹ • a • x ∈ s ↔ ∃ y, (y ∈ Ioi 0 ∧ y⁻¹ • x ∈ s) ∧ a • y = r
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Ring S<VAR>inst✝⁷ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Algebra K L<VAR>inst✝² : Algebra K F<VAR>ι : Type w<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R S<VAR>s : S<GOAL>(norm R) s = ((leftMulMatrix b) s).det
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Ring S<VAR>inst✝⁷ : Algebra R S<VAR>K : Type u_4<VAR>L : Type u_5<VAR>F : Type u_6<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Algebra K L<VAR>inst✝² : Algebra K F<VAR>ι : Type w<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R S<VAR>s : S<GOAL>((toMatrix b b) ((lmul R S) s)).det = ((toMatrix b b) (mulLeft R s)).det
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{v}<VAR>α : Type v<VAR>r : α → α → Prop<VAR>x✝¹ : IsWellOrder α r<VAR>β : Type v<VAR>s : β → β → Prop<VAR>x✝ : IsWellOrder β s<GOAL>lift.{u, v} (type r) ≤ lift.{u, v} (type s) ↔ type r ≤ type s
<VAR>α✝ : Type u<VAR>β✝ : Type u_1<VAR>γ : Type u_2<VAR>r✝ : α✝ → α✝ → Prop<VAR>s✝ : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{v}<VAR>α : Type v<VAR>r : α → α → Prop<VAR>x✝¹ : IsWellOrder α r<VAR>β : Type v<VAR>s : β → β → Prop<VAR>x✝ : IsWellOrder β s<GOAL>lift.{max v u, v} (type r) ≤ lift.{max v u, v} (type s) ↔ type r ≤ type s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>f : X → Y<VAR>hf : Isometry f<VAR>H : Monotone m ∨ Surjective f<GOAL>(comap f) (mkMetric m) = mkMetric m
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>f : X → Y<VAR>hf : Isometry f<VAR>H : Monotone m ∨ Surjective f<GOAL>⨆ i, ⨆ (_ : i > 0), (comap f) (boundedBy (extend fun s x => m (diam s))) = ⨆ r, ⨆ (_ : r > 0), boundedBy (extend fun s x => m (diam s))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>f : X → Y<VAR>hf : Isometry f<VAR>H : Monotone m ∨ Surjective f<VAR>ε : ℝ≥0∞<VAR>hε : id ε > 0<GOAL>(comap f) (boundedBy (extend fun s x => m (diam s))) = boundedBy (extend fun s x => m (diam s))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>f : X → Y<VAR>hf : Isometry f<VAR>H : Monotone m ∨ Surjective f<VAR>ε : ℝ≥0∞<VAR>hε : id ε > 0<GOAL>(boundedBy fun s => extend (fun s x => m (diam s)) (f '' s)) = boundedBy (extend fun s x => m (diam s))
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>m : ℝ≥0∞ → ℝ≥0∞<VAR>f : X → Y<VAR>hf : Isometry f<VAR>H : Monotone m ∨ Surjective f<VAR>ε : ℝ≥0∞<VAR>hε : id ε > 0<GOAL>Monotone m → Monotone fun s => extend (fun s x => m (diam s)) ↑s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>F : Type u_5<VAR>inst✝³ : AddMonoidWithOne B<VAR>inst✝² : FunLike F ℕ A<VAR>inst✝¹ : AddMonoid A<VAR>inst✝ : AddMonoidHomClass F ℕ A<VAR>f g : F<VAR>h : f 1 = g 1<VAR>n : ℕ<GOAL>f n = g n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : EDist α<VAR>x y : α<VAR>s t : Set α<VAR>inst✝ : Finite ↑s<VAR>hs : s.Nontrivial<GOAL>∃ x ∈ s, ∃ y ∈ s, x ≠ y ∧ s.einfsep = edist x y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x✝ y✝ z : P<VAR>x y : V<GOAL>0 -ᵥ x = y -ᵥ (x + y)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π✝ : TaggedPrepartition I<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>π : TaggedPrepartition I<GOAL>integralSum (f + g) vol π = integralSum f vol π + integralSum g vol π
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Monoid M<VAR>x✝ : Mˣ<VAR>ha : x✝ ∈ Units.val ⁻¹' center M<GOAL>x✝ ∈ center Mˣ
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Monoid M<VAR>x✝ : Mˣ<VAR>ha : x✝ ∈ Units.val ⁻¹' center M<GOAL>∀ (g : Mˣ), g * x✝ = x✝ * g
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Monoid M<VAR>x✝ : Mˣ<VAR>ha : x✝ ∈ Units.val ⁻¹' center M<VAR>g✝ : Mˣ<GOAL>g✝ * x✝ = x✝ * g✝
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s✝ t : Set M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : ChartedSpace H' M'<VAR>x : M<VAR>s : Set E<VAR>hs : IsOpen s<GOAL>IsOpen ((chartAt H x).source ∩ ↑(extChartAt I x) ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>M : Type u_3<VAR>H : Type u_4<VAR>E' : Type u_5<VAR>M' : Type u_6<VAR>H' : Type u_7<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : TopologicalSpace H<VAR>inst✝⁶ : TopologicalSpace M<VAR>f f' : PartialHomeomorph M H<VAR>I : ModelWithCorners 𝕜 E H<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>s✝ t : Set M<VAR>inst✝¹ : ChartedSpace H M<VAR>inst✝ : ChartedSpace H' M'<VAR>x : M<VAR>s : Set E<VAR>hs : IsOpen s<GOAL>IsOpen ((extChartAt I x).source ∩ ↑(extChartAt I x) ⁻¹' s)
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>T : F →L[ℝ] F<VAR>hT : IsSelfAdjoint T<VAR>x₀ : F<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>H : IsLocalExtrOn T.reApplyInnerSelf {x | ‖x‖ ^ 2 = ‖x₀‖ ^ 2} x₀<GOAL>∃ a b, (a, b) ≠ 0 ∧ a • x₀ + b • T x₀ = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>T : F →L[ℝ] F<VAR>hT : IsSelfAdjoint T<VAR>x₀ : F<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>H : IsLocalExtrOn T.reApplyInnerSelf {x | ‖x‖ ^ 2 = ‖x₀‖ ^ 2} x₀<VAR>a b : ℝ<VAR>h₁ : (a, b) ≠ 0<VAR>h₂ : a • 2 • (innerSL ℝ) x₀ + b • 2 • (innerSL ℝ) (T x₀) = 0<GOAL>∃ a b, (a, b) ≠ 0 ∧ a • x₀ + b • T x₀ = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>T : F →L[ℝ] F<VAR>hT : IsSelfAdjoint T<VAR>x₀ : F<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>H : IsLocalExtrOn T.reApplyInnerSelf {x | ‖x‖ ^ 2 = ‖x₀‖ ^ 2} x₀<VAR>a b : ℝ<VAR>h₁ : (a, b) ≠ 0<VAR>h₂ : a • 2 • (innerSL ℝ) x₀ + b • 2 • (innerSL ℝ) (T x₀) = 0<GOAL>a • x₀ + b • T x₀ = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>T : F →L[ℝ] F<VAR>hT : IsSelfAdjoint T<VAR>x₀ : F<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>H : IsLocalExtrOn T.reApplyInnerSelf {x | ‖x‖ ^ 2 = ‖x₀‖ ^ 2} x₀<VAR>a b : ℝ<VAR>h₁ : (a, b) ≠ 0<VAR>h₂ : a • 2 • (innerSL ℝ) x₀ + b • 2 • (innerSL ℝ) (T x₀) = 0<GOAL>(InnerProductSpace.toDualMap ℝ F) (a • x₀ + b • T x₀) = (InnerProductSpace.toDualMap ℝ F) 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>T : F →L[ℝ] F<VAR>hT : IsSelfAdjoint T<VAR>x₀ : F<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>H : IsLocalExtrOn T.reApplyInnerSelf {x | ‖x‖ ^ 2 = ‖x₀‖ ^ 2} x₀<VAR>a b : ℝ<VAR>h₁ : (a, b) ≠ 0<VAR>h₂ : a • 2 • (innerSL ℝ) x₀ + b • 2 • (innerSL ℝ) (T x₀) = 0<GOAL>(InnerProductSpace.toDualMap ℝ F) (a • x₀) + (InnerProductSpace.toDualMap ℝ F) (b • T x₀) = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>T : F →L[ℝ] F<VAR>hT : IsSelfAdjoint T<VAR>x₀ : F<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>H : IsLocalExtrOn T.reApplyInnerSelf {x | ‖x‖ ^ 2 = ‖x₀‖ ^ 2} x₀<VAR>a b : ℝ<VAR>h₁ : (a, b) ≠ 0<VAR>h₂ : a • 2 • (innerSL ℝ) x₀ + b • 2 • (innerSL ℝ) (T x₀) = 0<GOAL>a • (InnerProductSpace.toDualMap ℝ F) x₀ + b • (InnerProductSpace.toDualMap ℝ F) (T x₀) = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>T : F →L[ℝ] F<VAR>hT : IsSelfAdjoint T<VAR>x₀ : F<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>H : IsLocalExtrOn T.reApplyInnerSelf {x | ‖x‖ ^ 2 = ‖x₀‖ ^ 2} x₀<VAR>a b : ℝ<VAR>h₁ : (a, b) ≠ 0<VAR>h₂ : a • 2 • (innerSL ℝ) x₀ + b • 2 • (innerSL ℝ) (T x₀) = 0<GOAL>a • (innerSL ℝ) x₀ + b • (innerSL ℝ) (T x₀) = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>T : F →L[ℝ] F<VAR>hT : IsSelfAdjoint T<VAR>x₀ : F<VAR>hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀<VAR>H : IsLocalExtrOn T.reApplyInnerSelf {x | ‖x‖ ^ 2 = ‖x₀‖ ^ 2} x₀<VAR>a b : ℝ<VAR>h₁ : (a, b) ≠ 0<VAR>h₂ : a • 2 • (innerSL ℝ) x₀ + b • 2 • (innerSL ℝ) (T x₀) = 0<GOAL>(fun x => 2 • x) (a • (innerSL ℝ) x₀ + b • (innerSL ℝ) (T x₀)) = (fun x => 2 • x) 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y : F<GOAL>re (⟪x, y⟫_𝕜 * ⟪y, x⟫_𝕜) = ‖⟪x, y⟫_𝕜 * ⟪y, x⟫_𝕜‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y : F<GOAL>re (⟪y, x⟫_𝕜 * (starRingEnd 𝕜) ⟪y, x⟫_𝕜) = ‖⟪y, x⟫_𝕜 * (starRingEnd 𝕜) ⟪y, x⟫_𝕜‖
<VAR>β : Type u_1<VAR>inst✝² : AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.7275, u_2} V<VAR>inst✝ : HasZeroMorphisms V<VAR>X : DifferentialObject ℤ (GradedObjectWithShift b V)<VAR>i j : β<VAR>w : ¬i + b = j<GOAL>(fun i j => if h : i + b = j then X.d i ≫ X.objEqToHom ⋯ else 0) i j = 0
<VAR>β : Type u_1<VAR>inst✝² : AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.7275, u_2} V<VAR>inst✝ : HasZeroMorphisms V<VAR>X Y : DifferentialObject ℤ (GradedObjectWithShift b V)<VAR>f : X ⟶ Y<VAR>i : β<GOAL>(f.f i ≫ if h : i + b = i + b then Y.d i ≫ Y.objEqToHom ⋯ else 0) = (if h : i + b = i + b then X.d i ≫ X.objEqToHom ⋯ else 0) ≫ f.f (i + b)
<VAR>β : Type u_1<VAR>inst✝² : AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.7275, u_2} V<VAR>inst✝ : HasZeroMorphisms V<VAR>X Y : DifferentialObject ℤ (GradedObjectWithShift b V)<VAR>f : X ⟶ Y<VAR>i : β<GOAL>f.f i ≫ Y.d i ≫ Y.objEqToHom ⋯ = X.d i ≫ f.f (i + 1 • b) ≫ Y.objEqToHom ⋯
<VAR>β : Type u_1<VAR>inst✝² : AddCommGroup β<VAR>b : β<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.7275, u_2} V<VAR>inst✝ : HasZeroMorphisms V<VAR>X Y : DifferentialObject ℤ (GradedObjectWithShift b V)<VAR>f : X ⟶ Y<VAR>i : β<VAR>this : f.f i ≫ Y.d i = X.d i ≫ f.f ((fun b_1 => b_1 + { as := 1 }.as • b) i)<GOAL>f.f i ≫ Y.d i ≫ Y.objEqToHom ⋯ = X.d i ≫ f.f (i + 1 • b) ≫ Y.objEqToHom ⋯
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : TopologicalSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<GOAL>Inducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ Inducing ((⋃₀ 𝔖).restrict ∘ F)
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : TopologicalSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<GOAL>inst✝ = TopologicalSpace.induced (⇑(UniformOnFun.ofFun 𝔖) ∘ F) (UniformOnFun.topologicalSpace X α 𝔖) ↔ inst✝ = TopologicalSpace.induced ((⋃₀ 𝔖).restrict ∘ F) Pi.topologicalSpace
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → X → α<VAR>G : ι → β → α<VAR>inst✝ : TopologicalSpace ι<VAR>𝔖 : Set (Set X)<VAR>𝔖_compact : ∀ K ∈ 𝔖, IsCompact K<VAR>F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K<GOAL>inst✝ = UniformSpace.toTopologicalSpace ↔ inst✝ = UniformSpace.toTopologicalSpace
<VAR>D : Type u_1<VAR>inst✝² : Finite D<VAR>inst✝¹ : Ring D<VAR>inst✝ : IsDomain D<GOAL>IsField D
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.121680, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>inst✝¹ : S₁.HasLeftHomology<VAR>inst✝ : S₂.HasLeftHomology<GOAL>cyclesMap e.hom ≫ cyclesMap e.inv = 𝟙 S₁.cycles
<VAR>C : Type u_1<VAR>inst✝³ : Category.{?u.121680, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>e : S₁ ≅ S₂<VAR>inst✝¹ : S₁.HasLeftHomology<VAR>inst✝ : S₂.HasLeftHomology<GOAL>cyclesMap e.inv ≫ cyclesMap e.hom = 𝟙 S₂.cycles