ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{?u.24327, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.24334, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.24341, u_3} E<VAR>M : Type u_4<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : HasShift C M<VAR>inst✝¹ : HasShift D M<VAR>inst✝ : HasShift E M<VAR>X Y Z T : C<VAR>a : M<VAR>f : ShiftedHom X Y a<VAR>m₀ : M<VAR>hm₀ : m₀ = 0<GOAL>m₀ + a = a
<VAR>C : Type u_1<VAR>inst✝⁶ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{?u.24334, u_2} D<VAR>E : Type u_3<VAR>inst✝⁴ : Category.{?u.24341, u_3} E<VAR>M : Type u_4<VAR>inst✝³ : AddMonoid M<VAR>inst✝² : HasShift C M<VAR>inst✝¹ : HasShift D M<VAR>inst✝ : HasShift E M<VAR>X Y Z T : C<VAR>a : M<VAR>f : ShiftedHom X Y a<VAR>m₀ : M<VAR>hm₀ : m₀ = 0<GOAL>f.comp (mk₀ m₀ hm₀ (𝟙 Y)) ⋯ = f
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hab : a + b ≤ 1<VAR>hp1 : 1 ≤ p<GOAL>a ^ p + b ^ p ≤ 1
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hab : a + b ≤ 1<VAR>hp1 : 1 ≤ p<VAR>h_le_one : ∀ x ≤ 1, x ^ p ≤ x<GOAL>a ^ p + b ^ p ≤ 1
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hab : a + b ≤ 1<VAR>hp1 : 1 ≤ p<VAR>h_le_one : ∀ x ≤ 1, x ^ p ≤ x<VAR>ha : a ≤ 1<GOAL>a ^ p + b ^ p ≤ 1
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0<VAR>hab : a + b ≤ 1<VAR>hp1 : 1 ≤ p<VAR>h_le_one : ∀ x ≤ 1, x ^ p ≤ x<VAR>ha : a ≤ 1<VAR>hb : b ≤ 1<GOAL>a ^ p + b ^ p ≤ 1
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : OrderedSMul α β<VAR>s : Finset ι<VAR>σ : Perm ι<VAR>f : ι → α<VAR>g : ι → β<VAR>hfg : AntivaryOn f g ↑s<GOAL>s.card • ∑ i ∈ s, f i • g i ≤ (∑ i ∈ s, f i) • ∑ i ∈ s, g i
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>w : E<VAR>hw : w ∈ (Submodule.span ℝ {v})ᗮ<VAR>h₁ : 0 < ‖w‖ ^ 2 + 4<GOAL>stereoInvFunAux v w ∈ sphere 0 1
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>w : E<VAR>hw : w ∈ (Submodule.span ℝ {v})ᗮ<VAR>h₁ : 0 < ‖w‖ ^ 2 + 4<GOAL>‖4 • w + (‖w‖ ^ 2 - 4) • v‖ = ‖w‖ ^ 2 + 4
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>w : E<VAR>hw : w ∈ (Submodule.span ℝ {v})ᗮ<VAR>h₁ : 0 < ‖w‖ ^ 2 + 4<GOAL>‖4 • w + (‖w‖ ^ 2 - 4) • v‖ ^ 2 = (‖w‖ ^ 2 + 4) ^ 2
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>w : E<VAR>hw : ⟪w, v⟫_ℝ = 0<VAR>h₁ : 0 < ‖w‖ ^ 2 + 4<GOAL>‖4 • w + (‖w‖ ^ 2 - 4) • v‖ ^ 2 = (‖w‖ ^ 2 + 4) ^ 2
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>v : E<VAR>hv : ‖v‖ = 1<VAR>w : E<VAR>hw : ⟪w, v⟫_ℝ = 0<VAR>h₁ : 0 < ‖w‖ ^ 2 + 4<GOAL>4 ^ 2 * ‖w‖ ^ 2 + (‖w‖ ^ 2 - 4) ^ 2 = (‖w‖ ^ 2 + 4) ^ 2
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x y : K_hat R K<VAR>hx : x.IsFiniteAdele<VAR>hy : y.IsFiniteAdele<GOAL>(x * y).IsFiniteAdele
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x y : K_hat R K<VAR>hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite<VAR>hy : {x | y x ∉ adicCompletionIntegers K x}.Finite<GOAL>{x_1 | (x * y) x_1 ∉ adicCompletionIntegers K x_1}.Finite
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>x y : K_hat R K<VAR>hx : {x_1 | x x_1 ∉ adicCompletionIntegers K x_1}.Finite<VAR>hy : {x | y x ∉ adicCompletionIntegers K x}.Finite<VAR>h_subset : {v | (x * y) v ∉ adicCompletionIntegers K v} ⊆ {v | x v ∉ adicCompletionIntegers K v} ∪ {v | y v ∉ adicCompletionIntegers K v}<GOAL>{x_1 | (x * y) x_1 ∉ adicCompletionIntegers K x_1}.Finite
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K L M : HomologicalComplex C c<VAR>φ : K ⟶ L<VAR>ψ : L ⟶ M<VAR>i j k : ι<VAR>inst✝¹ : K.HasHomology i<VAR>inst✝ : K.HasHomology k<GOAL>K.d i j ≫ K.toCycles j k = 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f✝ : ℝ → E<VAR>μ : Measure ℝ<VAR>inst✝ : Countable ι<VAR>f : ι → C(ℝ, E)<VAR>hf_sum : Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := uIcc a b, isCompact' := ⋯ }) (f i)‖<VAR>hE : CompleteSpace E<GOAL>HasSum (fun i => ∫ (x : ℝ) in a..b, (f i) x) (∫ (x : ℝ) in a..b, ∑' (i : ι), (f i) x)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f✝ : ℝ → E<VAR>μ : Measure ℝ<VAR>inst✝ : Countable ι<VAR>f : ι → C(ℝ, E)<VAR>hf_sum : Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := uIcc a b, isCompact' := ⋯ }) (f i)‖<VAR>hE : CompleteSpace E<GOAL>∀ (n : ι), ∀ᵐ (t : ℝ), t ∈ Ι a b → ‖(f n) t‖ ≤ ‖ContinuousMap.restrict (↑{ carrier := uIcc a b, isCompact' := ⋯ }) (f n)‖
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f✝ : ℝ → E<VAR>μ : Measure ℝ<VAR>inst✝ : Countable ι<VAR>f : ι → C(ℝ, E)<VAR>hf_sum : Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := uIcc a b, isCompact' := ⋯ }) (f i)‖<VAR>hE : CompleteSpace E<GOAL>∀ᵐ (t : ℝ), t ∈ Ι a b → Summable fun n => ‖ContinuousMap.restrict (↑{ carrier := uIcc a b, isCompact' := ⋯ }) (f n)‖
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f✝ : ℝ → E<VAR>μ : Measure ℝ<VAR>inst✝ : Countable ι<VAR>f : ι → C(ℝ, E)<VAR>hf_sum : Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := uIcc a b, isCompact' := ⋯ }) (f i)‖<VAR>hE : CompleteSpace E<GOAL>IntervalIntegrable (fun t => ∑' (n : ι), ‖ContinuousMap.restrict (↑{ carrier := uIcc a b, isCompact' := ⋯ }) (f n)‖) volume a b
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>a b : ℝ<VAR>f✝ : ℝ → E<VAR>μ : Measure ℝ<VAR>inst✝ : Countable ι<VAR>f : ι → C(ℝ, E)<VAR>hf_sum : Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := uIcc a b, isCompact' := ⋯ }) (f i)‖<VAR>hE : CompleteSpace E<GOAL>∀ᵐ (t : ℝ), t ∈ Ι a b → HasSum (fun n => (f n) t) (∑' (i : ι), (f i) t)
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>σ : Type u_2<VAR>f : σ → R<VAR>s : Finset σ<VAR>n : ℕ<GOAL>(map f s.val).esymm n = ∑ t ∈ Finset.powersetCard n s, t.prod f
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>σ : Type u_2<VAR>f : σ → R<VAR>s : Finset σ<VAR>n : ℕ<GOAL>(map ((fun x => x.prod) ∘ (fun x => map f x) ∘ Finset.val) (Finset.powersetCard n s).val).sum = ∑ t ∈ Finset.powersetCard n s, t.prod f
<VAR>ι : Sort u_1<VAR>κ : ι → Sort u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>s✝ t✝ : Set α<VAR>a x y : α<VAR>inst✝¹ : AlexandrovDiscrete α<VAR>inst✝ : AlexandrovDiscrete β<VAR>s t : Set α<GOAL>exterior s ≤ t ↔ s ≤ interior t
<VAR>α✝ : Sort u_1<VAR>β : Sort u_2<VAR>p✝ q : α✝ → Prop<VAR>α : Sort u_3<VAR>p : α → Prop<VAR>b : Prop<VAR>ha : Nonempty α<VAR>a : α<GOAL>(∀ (x : α), p x) → b ↔ ∃ x, p x → b
<VAR>α✝ : Sort u_1<VAR>β : Sort u_2<VAR>p✝ q : α✝ → Prop<VAR>α : Sort u_3<VAR>p : α → Prop<VAR>b : Prop<VAR>ha : Nonempty α<VAR>a : α<VAR>h : (∀ (x : α), p x) → b<VAR>h' : ∀ (x : α), ¬(p x → b)<GOAL>False
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>N : Type u_3<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>S : Type u_5<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>t : M ⊗[R] (ι →₀ R)<VAR>i : ι<GOAL>((finsuppScalarRight R M ι) t) i = (TensorProduct.rid R M) ((lTensor M (Finsupp.lapply i)) t)
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>(mk W) (W.Ψ n) ^ 2 = (mk W) (C (W.ΨSq n))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>α : Type u_4<VAR>inst✝ : Finite α<VAR>f : M →ₗ[R] α → R<VAR>s : Surjective ⇑f<GOAL>f ∘ₗ f.splittingOfFunOnFintypeSurjective s = id
<VAR>R : Type u<VAR>S✝ : Type v<VAR>K : Type w<VAR>inst✝⁴ : CommRing R<VAR>f✝ : R[X]<VAR>inst✝³ : CommRing S✝<VAR>i : R →+* S✝<VAR>a : S✝<VAR>h : eval₂ i a f✝ = 0<VAR>inst✝² : Algebra R S✝<VAR>hfx : (aeval a) f✝ = 0<VAR>S : Type u_1<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>r : R<VAR>f g : AdjoinRoot (C r * X - 1) →ₐ[R] S<GOAL>(algebraMap R S) r * f (root (C r * X - 1)) = 1
<VAR>R : Type u<VAR>S✝ : Type v<VAR>K : Type w<VAR>inst✝⁴ : CommRing R<VAR>f✝ : R[X]<VAR>inst✝³ : CommRing S✝<VAR>i : R →+* S✝<VAR>a : S✝<VAR>h : eval₂ i a f✝ = 0<VAR>inst✝² : Algebra R S✝<VAR>hfx : (aeval a) f✝ = 0<VAR>S : Type u_1<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>r : R<VAR>f g : AdjoinRoot (C r * X - 1) →ₐ[R] S<GOAL>(algebraMap R S) r * g (root (C r * X - 1)) = 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : β → Option (α × β)<VAR>b : β<VAR>h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).1<VAR>a : α<VAR>b' : β<VAR>h : f b = some (a, b')<GOAL>tail ⟨corec' (Corec.f f) (some b), ⋯⟩ = ⟨corec' (Corec.f f) (some b'), ⋯⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : β → Option (α × β)<VAR>b : β<VAR>h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).1<VAR>a : α<VAR>b' : β<VAR>h : f b = some (a, b')<GOAL>↑(tail ⟨corec' (Corec.f f) (some b), ⋯⟩) = ↑⟨corec' (Corec.f f) (some b'), ⋯⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : β → Option (α × β)<VAR>b : β<VAR>h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).1<VAR>a : α<VAR>b' : β<VAR>h : f b = some (a, b')<GOAL>(corec' (Corec.f f) (some b)).tail = corec' (Corec.f f) (some b')
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : β → Option (α × β)<VAR>b : β<VAR>h✝ : corec' (Corec.f f) (some b) 0 = (Corec.f f (some b)).1<VAR>a : α<VAR>b' : β<VAR>h : f b = some (a, b')<GOAL>corec' (Corec.f f) (Corec.f f (some b)).2 = corec' (Corec.f f) (some b')
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>x : 𝕎 (ZMod p)<GOAL>((fromPadicInt p).comp (toPadicInt p)) x = (RingHom.id (𝕎 (ZMod p))) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>f : α → β<VAR>s t : Set β<VAR>hf : Surjective f<GOAL>f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>f : α → β<VAR>s t : Set β<VAR>hf : Surjective f<GOAL>s ⊆ range f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>f : α → β<VAR>s t : Set β<VAR>hf : Surjective f<GOAL>s ⊆ univ
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>n : ℕ<VAR>x : 𝕎 R<GOAL>(ghostComponent n) x.frobeniusFun = (ghostComponent (n + 1)) x
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<VAR>h : Directed (fun x x_1 => x ≤ x_1) f<GOAL>a ⊓ ⨆ i, f i = ⨆ i, a ⊓ f i
<VAR>𝕜 : Type u<VAR>𝕜' : Type u'<VAR>E : Type v<VAR>F : Type w<VAR>G : Type x<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>y : Fin n → 𝕜<GOAL>p.coeff n = 0 ↔ p n = 0
<VAR>R : Type u_1<VAR>inst✝² : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>v₂ : M<VAR>r : Rˣ<VAR>hr : 0 < ↑r<GOAL>SameRay R (r • v₂) v₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c✝ c₁ c₂ c₃ s t : Set α<VAR>a✝ b✝ x y : α<VAR>inst✝ : IsRefl α r<VAR>f : β → α<VAR>c : Set β<VAR>h : IsChain (f ⁻¹'o r) c<VAR>x✝¹ x✝ : { a // a ∈ c }<VAR>a : β<VAR>ha : a ∈ c<VAR>b : β<VAR>hb : b ∈ c<VAR>hab : a = b<GOAL>∃ z, r ((fun x => f ↑x) ⟨a, ha⟩) ((fun x => f ↑x) z) ∧ r ((fun x => f ↑x) ⟨b, hb⟩) ((fun x => f ↑x) z)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → α → Prop<VAR>c✝ c₁ c₂ c₃ s t : Set α<VAR>a✝ b✝ x y : α<VAR>inst✝ : IsRefl α r<VAR>f : β → α<VAR>c : Set β<VAR>h : IsChain (f ⁻¹'o r) c<VAR>x✝¹ x✝ : { a // a ∈ c }<VAR>a : β<VAR>ha : a ∈ c<VAR>b : β<VAR>hb : b ∈ c<VAR>hab : a = b<GOAL>∃ a ∈ c, r (f b) (f a)
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I✝ J K L : Ideal R<VAR>x y : R<VAR>I : Ideal R<GOAL>x ∈ span {y} * I ↔ ∃ z ∈ I, y * z = x
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<GOAL>prod.snd ⊚ prod.diag = id
<VAR>n : ℕ<VAR>α : TypeVec.{u_1} n<VAR>i : Fin2 n<GOAL>(prod.snd ⊚ prod.diag) i = id i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>f : α → β<VAR>inst✝ : SecondCountableTopology β<VAR>hf : Inducing f<GOAL>SecondCountableTopology α
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>x : M<VAR>xs : List M<GOAL>involute (List.map (⇑(ι Q)) (x :: xs)).prod = (-1) ^ (x :: xs).length • (List.map (⇑(ι Q)) (x :: xs)).prod
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w a b : K<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hab : a ≤ b<GOAL>r • a ≤ r • b
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w a b : K<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hab : re a ≤ re b ∧ im a = im b<GOAL>r • a ≤ r • b
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w a b : K<VAR>r : ℝ<VAR>hr : 0 < r<VAR>hab : re a ≤ re b ∧ im a = im b<GOAL>r * re a ≤ r * re b ∧ r * im a = r * im b
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m : M<VAR>s : Finset F<VAR>this : IsEmpty ↑↑∅<GOAL>(LinearIndependent ↥(subfield G F) fun (i : ↑↑s) => ↑i) → LinearIndependent F fun (i : ↑↑s) => (toFun G F) ↑i
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m : M<VAR>s✝ : Finset F<VAR>this : IsEmpty ↑↑∅<VAR>a : F<VAR>s : Finset F<VAR>has : a ∉ s<VAR>ih : (LinearIndependent ↥(subfield G F) fun (i : ↑↑s) => ↑i) → LinearIndependent F fun (i : ↑↑s) => (toFun G F) ↑i<VAR>hs : LinearIndependent ↥(subfield G F) fun (i : ↑↑(insert a s)) => ↑i<GOAL>LinearIndependent F fun (i : ↑↑(insert a s)) => (toFun G F) ↑i
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m : M<VAR>s✝ : Finset F<VAR>this : IsEmpty ↑↑∅<VAR>a : F<VAR>s : Finset F<VAR>has : a ∉ s<VAR>ih : (LinearIndependent ↥(subfield G F) fun (i : ↑↑s) => ↑i) → LinearIndependent F fun (i : ↑↑s) => (toFun G F) ↑i<VAR>hs : LinearIndependent ↥(subfield G F) fun (i : ↑(insert a ↑s)) => ↑i<GOAL>LinearIndependent F fun (i : ↑(insert a ↑s)) => (toFun G F) ↑i
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m : M<VAR>s✝ : Finset F<VAR>this : IsEmpty ↑↑∅<VAR>a : F<VAR>s : Finset F<VAR>has : a ∉ s<VAR>ih : (LinearIndependent ↥(subfield G F) fun (i : ↑↑s) => ↑i) → LinearIndependent F fun (i : ↑↑s) => (toFun G F) ↑i<VAR>hs : (LinearIndependent ↥(subfield G F) fun (b : ↑↑s) => ↑b) ∧ a ∉ Submodule.span ↥(subfield G F) ↑s<GOAL>LinearIndependent F fun (i : ↑(insert a ↑s)) => (toFun G F) ↑i
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m : M<VAR>s✝ : Finset F<VAR>this : IsEmpty ↑↑∅<VAR>a : F<VAR>s : Finset F<VAR>has : a ∉ s<VAR>ih : (LinearIndependent ↥(subfield G F) fun (i : ↑↑s) => ↑i) → LinearIndependent F fun (i : ↑↑s) => (toFun G F) ↑i<VAR>hs : (LinearIndependent ↥(subfield G F) fun (b : ↑↑s) => ↑b) ∧ a ∉ Submodule.span ↥(subfield G F) ↑s<GOAL>(LinearIndependent F fun (x : ↑↑s) => (toFun G F) ↑x) ∧ (toFun G F) a ∉ Submodule.span F (⇑(toFun G F) '' ↑s)
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m : M<VAR>s✝ : Finset F<VAR>this : IsEmpty ↑↑∅<VAR>a : F<VAR>s : Finset F<VAR>has : a ∉ s<VAR>ih : (LinearIndependent ↥(subfield G F) fun (i : ↑↑s) => ↑i) → LinearIndependent F fun (i : ↑↑s) => (toFun G F) ↑i<VAR>hs : (LinearIndependent ↥(subfield G F) fun (b : ↑↑s) => ↑b) ∧ a ∉ Submodule.span ↥(subfield G F) ↑s<VAR>ha : (toFun G F) a ∈ Submodule.span F (⇑(toFun G F) '' ↑s)<GOAL>False
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m : M<VAR>s✝ : Finset F<VAR>this : IsEmpty ↑↑∅<VAR>a : F<VAR>s : Finset F<VAR>has : a ∉ s<VAR>ih : (LinearIndependent ↥(subfield G F) fun (i : ↑↑s) => ↑i) → LinearIndependent F fun (i : ↑↑s) => (toFun G F) ↑i<VAR>hs : (LinearIndependent ↥(subfield G F) fun (b : ↑↑s) => ↑b) ∧ a ∉ Submodule.span ↥(subfield G F) ↑s<VAR>ha : ∃ l ∈ Finsupp.supported F F ↑s, (Finsupp.total F (G → F) F ⇑(toFun G F)) l = (toFun G F) a<GOAL>False
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m : M<VAR>s✝ : Finset F<VAR>this : IsEmpty ↑↑∅<VAR>a : F<VAR>s : Finset F<VAR>has : a ∉ s<VAR>ih : (LinearIndependent ↥(subfield G F) fun (i : ↑↑s) => ↑i) → LinearIndependent F fun (i : ↑↑s) => (toFun G F) ↑i<VAR>hs : (LinearIndependent ↥(subfield G F) fun (b : ↑↑s) => ↑b) ∧ a ∉ Submodule.span ↥(subfield G F) ↑s<VAR>l : F →₀ F<VAR>hl : l ∈ Finsupp.supported F F ↑s<VAR>hla : (Finsupp.total F (G → F) F ⇑(toFun G F)) l = (toFun G F) a<GOAL>False
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m : M<VAR>s✝ : Finset F<VAR>this : IsEmpty ↑↑∅<VAR>a : F<VAR>s : Finset F<VAR>has : a ∉ s<VAR>ih : (LinearIndependent ↥(subfield G F) fun (i : ↑↑s) => ↑i) → LinearIndependent F fun (i : ↑↑s) => (toFun G F) ↑i<VAR>hs : (LinearIndependent ↥(subfield G F) fun (b : ↑↑s) => ↑b) ∧ a ∉ Submodule.span ↥(subfield G F) ↑s<VAR>l : F →₀ F<VAR>hl : l ∈ Finsupp.supported F F ↑s<VAR>hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a<GOAL>False
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m : M<VAR>s✝ : Finset F<VAR>this : IsEmpty ↑↑∅<VAR>a : F<VAR>s : Finset F<VAR>has : a ∉ s<VAR>ih : (LinearIndependent ↥(subfield G F) fun (i : ↑↑s) => ↑i) → LinearIndependent F fun (i : ↑↑s) => (toFun G F) ↑i<VAR>hs : (LinearIndependent ↥(subfield G F) fun (b : ↑↑s) => ↑b) ∧ a ∉ Submodule.span ↥(subfield G F) ↑s<VAR>l : F →₀ F<VAR>hl : l ∈ Finsupp.supported F F ↑s<VAR>hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a<GOAL>∀ i ∈ s, l i ∈ subfield G F
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m : M<VAR>s✝ : Finset F<VAR>this : IsEmpty ↑↑∅<VAR>a : F<VAR>s : Finset F<VAR>has : a ∉ s<VAR>ih : (LinearIndependent ↥(subfield G F) fun (i : ↑↑s) => ↑i) → LinearIndependent F fun (i : ↑↑s) => (toFun G F) ↑i<VAR>hs : (LinearIndependent ↥(subfield G F) fun (b : ↑↑s) => ↑b) ∧ a ∉ Submodule.span ↥(subfield G F) ↑s<VAR>l : F →₀ F<VAR>hl : l ∈ Finsupp.supported F F ↑s<VAR>hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a<VAR>i : F<VAR>his : i ∈ s<VAR>g : G<GOAL>g • l i = l i
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m : M<VAR>s✝ : Finset F<VAR>this : IsEmpty ↑↑∅<VAR>a : F<VAR>s : Finset F<VAR>has : a ∉ s<VAR>ih : (LinearIndependent ↥(subfield G F) fun (i : ↑↑s) => ↑i) → LinearIndependent F fun (i : ↑↑s) => (toFun G F) ↑i<VAR>hs : (LinearIndependent ↥(subfield G F) fun (b : ↑↑s) => ↑b) ∧ a ∉ Submodule.span ↥(subfield G F) ↑s<VAR>l : F →₀ F<VAR>hl : l ∈ Finsupp.supported F F ↑s<VAR>hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a<VAR>i : F<VAR>his : i ∈ s<VAR>g : G<GOAL>∑ i ∈ s.attach, (fun i => g • l ↑i - l ↑i) i • (toFun G F) ↑i = 0
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m : M<VAR>s✝ : Finset F<VAR>this : IsEmpty ↑↑∅<VAR>a : F<VAR>s : Finset F<VAR>has : a ∉ s<VAR>ih : (LinearIndependent ↥(subfield G F) fun (i : ↑↑s) => ↑i) → LinearIndependent F fun (i : ↑↑s) => (toFun G F) ↑i<VAR>hs : (LinearIndependent ↥(subfield G F) fun (b : ↑↑s) => ↑b) ∧ a ∉ Submodule.span ↥(subfield G F) ↑s<VAR>l : F →₀ F<VAR>hl : l ∈ Finsupp.supported F F ↑s<VAR>hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a<VAR>i : F<VAR>his : i ∈ s<VAR>g : G<GOAL>∑ x ∈ s, (g • l x - l x) • (toFun G F) x = 0
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m : M<VAR>s✝ : Finset F<VAR>this : IsEmpty ↑↑∅<VAR>a : F<VAR>s : Finset F<VAR>has : a ∉ s<VAR>ih : (LinearIndependent ↥(subfield G F) fun (i : ↑↑s) => ↑i) → LinearIndependent F fun (i : ↑↑s) => (toFun G F) ↑i<VAR>hs : (LinearIndependent ↥(subfield G F) fun (b : ↑↑s) => ↑b) ∧ a ∉ Submodule.span ↥(subfield G F) ↑s<VAR>l : F →₀ F<VAR>hl : l ∈ Finsupp.supported F F ↑s<VAR>hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a<VAR>i : F<VAR>his : i ∈ s<VAR>g g' : G<GOAL>∑ x ∈ s, (g • l x * (toFun G F) x g' - l x • (toFun G F) x g') = 0 g'
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m : M<VAR>s✝ : Finset F<VAR>this : IsEmpty ↑↑∅<VAR>a : F<VAR>s : Finset F<VAR>has : a ∉ s<VAR>ih : (LinearIndependent ↥(subfield G F) fun (i : ↑↑s) => ↑i) → LinearIndependent F fun (i : ↑↑s) => (toFun G F) ↑i<VAR>hs : (LinearIndependent ↥(subfield G F) fun (b : ↑↑s) => ↑b) ∧ a ∉ Submodule.span ↥(subfield G F) ↑s<VAR>l : F →₀ F<VAR>hl : l ∈ Finsupp.supported F F ↑s<VAR>hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a<VAR>i : F<VAR>his : i ∈ s<VAR>g g' : G<GOAL>∑ x ∈ s, g • l x * (toFun G F) x g' = ∑ x ∈ s, l x • (toFun G F) x g'
<VAR>M : Type u<VAR>inst✝⁴ : Monoid M<VAR>G : Type u<VAR>inst✝³ : Group G<VAR>F : Type v<VAR>inst✝² : Field F<VAR>inst✝¹ : MulSemiringAction M F<VAR>inst✝ : MulSemiringAction G F<VAR>m : M<VAR>s✝ : Finset F<VAR>this : IsEmpty ↑↑∅<VAR>a : F<VAR>s : Finset F<VAR>has : a ∉ s<VAR>ih : (LinearIndependent ↥(subfield G F) fun (i : ↑↑s) => ↑i) → LinearIndependent F fun (i : ↑↑s) => (toFun G F) ↑i<VAR>hs : (LinearIndependent ↥(subfield G F) fun (b : ↑↑s) => ↑b) ∧ a ∉ Submodule.span ↥(subfield G F) ↑s<VAR>l : F →₀ F<VAR>hl : l ∈ Finsupp.supported F F ↑s<VAR>hla : ∑ i ∈ s, l i • (toFun G F) i = (toFun G F) a<VAR>i : F<VAR>his : i ∈ s<VAR>g g' : G<GOAL>∑ x ∈ s, g • (fun y => l y • (toFun G F) y) x (g⁻¹ * g') = ∑ x ∈ s, (fun y => l y • (toFun G F) y) x g'