ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b✝ x y : α<VAR>hf : f.IsCycleOn s<VAR>hs : s.Nontrivial<VAR>ha : a ∈ s<VAR>b : α<VAR>hb : b ∈ s<VAR>hba : b ≠ a<GOAL>f a ≠ a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s t : Set α<VAR>a b x y : α<VAR>hf : f.IsCycleOn s<VAR>hs : s.Nontrivial<VAR>ha : a ∈ s<VAR>n : ℤ<VAR>hb : (f ^ n) a ∈ s<VAR>hba : (f ^ n) a ≠ a<GOAL>f a ≠ a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Monoid α<VAR>inst✝¹ : AddGroup β<VAR>inst✝ : DistribMulAction α β<VAR>a : α<VAR>s : Set α<VAR>t : Set β<GOAL>s • -t = -(s • t)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Monoid α<VAR>inst✝¹ : AddGroup β<VAR>inst✝ : DistribMulAction α β<VAR>a : α<VAR>s : Set α<VAR>t : Set β<GOAL>s • Neg.neg '' t = Neg.neg '' (s • t)
<VAR>R : Type u_1<VAR>inst✝²⁰ : Semiring 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>P : Type u_4<VAR>inst✝¹⁵ : AddCommMonoid P<VAR>inst✝¹⁴ : Module R P<VAR>M' : Type u_5<VAR>inst✝¹³ : AddCommGroup M'<VAR>inst✝¹² : Module R M'<VAR>N' : Type u_6<VAR>inst✝¹¹ : AddCommGroup N'<VAR>inst✝¹⁰ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : Module R M₃<VAR>f✝ f' : M✝ [⋀^ι]→ₗ[R] N✝<VAR>g g₂ : M✝ [⋀^ι]→ₗ[R] N'<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v✝ : ι → M✝<VAR>v' : ι → M'<VAR>K : Type u_12<VAR>inst✝⁵ : Ring K<VAR>M : Type u_13<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module K M<VAR>N : Type u_14<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module K N<VAR>inst✝ : NoZeroSMulDivisors K N<VAR>f : M [⋀^ι]→ₗ[K] N<VAR>v : ι → M<VAR>h : ¬LinearIndependent K v<GOAL>f v = 0
<VAR>R : Type u_1<VAR>inst✝²⁰ : Semiring 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>P : Type u_4<VAR>inst✝¹⁵ : AddCommMonoid P<VAR>inst✝¹⁴ : Module R P<VAR>M' : Type u_5<VAR>inst✝¹³ : AddCommGroup M'<VAR>inst✝¹² : Module R M'<VAR>N' : Type u_6<VAR>inst✝¹¹ : AddCommGroup N'<VAR>inst✝¹⁰ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : Module R M₃<VAR>f✝ f' : M✝ [⋀^ι]→ₗ[R] N✝<VAR>g✝ g₂ : M✝ [⋀^ι]→ₗ[R] N'<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v✝ : ι → M✝<VAR>v' : ι → M'<VAR>K : Type u_12<VAR>inst✝⁵ : Ring K<VAR>M : Type u_13<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module K M<VAR>N : Type u_14<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module K N<VAR>inst✝ : NoZeroSMulDivisors K N<VAR>f : M [⋀^ι]→ₗ[K] N<VAR>v : ι → M<VAR>h✝ : ¬LinearIndependent K v<VAR>s : Finset ι<VAR>g : ι → K<VAR>h : ∑ i ∈ s, g i • v i = 0<VAR>i : ι<VAR>hi : i ∈ s<VAR>hz : g i ≠ 0<GOAL>f v = 0
<VAR>R : Type u_1<VAR>inst✝²⁰ : Semiring 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>P : Type u_4<VAR>inst✝¹⁵ : AddCommMonoid P<VAR>inst✝¹⁴ : Module R P<VAR>M' : Type u_5<VAR>inst✝¹³ : AddCommGroup M'<VAR>inst✝¹² : Module R M'<VAR>N' : Type u_6<VAR>inst✝¹¹ : AddCommGroup N'<VAR>inst✝¹⁰ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : Module R M₃<VAR>f✝ f' : M✝ [⋀^ι]→ₗ[R] N✝<VAR>g✝ g₂ : M✝ [⋀^ι]→ₗ[R] N'<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v✝ : ι → M✝<VAR>v' : ι → M'<VAR>K : Type u_12<VAR>inst✝⁵ : Ring K<VAR>M : Type u_13<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module K M<VAR>N : Type u_14<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module K N<VAR>inst✝ : NoZeroSMulDivisors K N<VAR>f : M [⋀^ι]→ₗ[K] N<VAR>v : ι → M<VAR>h✝ : ¬LinearIndependent K v<VAR>s : Finset ι<VAR>g : ι → K<VAR>h : ∑ i ∈ s, g i • v i = 0<VAR>i : ι<VAR>hi : i ∈ s<VAR>hz : g i ≠ 0<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>f v = 0
<VAR>R : Type u_1<VAR>inst✝²⁰ : Semiring 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>P : Type u_4<VAR>inst✝¹⁵ : AddCommMonoid P<VAR>inst✝¹⁴ : Module R P<VAR>M' : Type u_5<VAR>inst✝¹³ : AddCommGroup M'<VAR>inst✝¹² : Module R M'<VAR>N' : Type u_6<VAR>inst✝¹¹ : AddCommGroup N'<VAR>inst✝¹⁰ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : Module R M₃<VAR>f✝ f' : M✝ [⋀^ι]→ₗ[R] N✝<VAR>g✝ g₂ : M✝ [⋀^ι]→ₗ[R] N'<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v✝ : ι → M✝<VAR>v' : ι → M'<VAR>K : Type u_12<VAR>inst✝⁵ : Ring K<VAR>M : Type u_13<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module K M<VAR>N : Type u_14<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module K N<VAR>inst✝ : NoZeroSMulDivisors K N<VAR>f : M [⋀^ι]→ₗ[K] N<VAR>v : ι → M<VAR>h✝ : ¬LinearIndependent K v<VAR>s : Finset ι<VAR>g : ι → K<VAR>h : ∑ i ∈ s, g i • v i = 0<VAR>i : ι<VAR>hi : i ∈ s<VAR>hz : g i ≠ 0<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>f (update v i (g i • v i)) = 0
<VAR>R : Type u_1<VAR>inst✝²⁰ : Semiring 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>P : Type u_4<VAR>inst✝¹⁵ : AddCommMonoid P<VAR>inst✝¹⁴ : Module R P<VAR>M' : Type u_5<VAR>inst✝¹³ : AddCommGroup M'<VAR>inst✝¹² : Module R M'<VAR>N' : Type u_6<VAR>inst✝¹¹ : AddCommGroup N'<VAR>inst✝¹⁰ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : Module R M₃<VAR>f✝ f' : M✝ [⋀^ι]→ₗ[R] N✝<VAR>g✝ g₂ : M✝ [⋀^ι]→ₗ[R] N'<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v✝ : ι → M✝<VAR>v' : ι → M'<VAR>K : Type u_12<VAR>inst✝⁵ : Ring K<VAR>M : Type u_13<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module K M<VAR>N : Type u_14<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module K N<VAR>inst✝ : NoZeroSMulDivisors K N<VAR>f : M [⋀^ι]→ₗ[K] N<VAR>v : ι → M<VAR>h✝ : ¬LinearIndependent K v<VAR>s : Finset ι<VAR>g : ι → K<VAR>i : ι<VAR>h : (∑ x ∈ s, if i = x then g x • v x else g x • v x) = 0<VAR>hi : i ∈ s<VAR>hz : g i ≠ 0<VAR>this : DecidableEq ι := Classical.decEq ι<GOAL>f (update v i (g i • v i)) = 0
<VAR>R : Type u_1<VAR>inst✝²⁰ : Semiring 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>P : Type u_4<VAR>inst✝¹⁵ : AddCommMonoid P<VAR>inst✝¹⁴ : Module R P<VAR>M' : Type u_5<VAR>inst✝¹³ : AddCommGroup M'<VAR>inst✝¹² : Module R M'<VAR>N' : Type u_6<VAR>inst✝¹¹ : AddCommGroup N'<VAR>inst✝¹⁰ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : Module R M₃<VAR>f✝ f' : M✝ [⋀^ι]→ₗ[R] N✝<VAR>g✝ g₂ : M✝ [⋀^ι]→ₗ[R] N'<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v✝ : ι → M✝<VAR>v' : ι → M'<VAR>K : Type u_12<VAR>inst✝⁵ : Ring K<VAR>M : Type u_13<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module K M<VAR>N : Type u_14<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module K N<VAR>inst✝ : NoZeroSMulDivisors K N<VAR>f : M [⋀^ι]→ₗ[K] N<VAR>v : ι → M<VAR>h✝ : ¬LinearIndependent K v<VAR>s : Finset ι<VAR>g : ι → K<VAR>i : ι<VAR>hi : i ∈ s<VAR>hz : g i ≠ 0<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>h : g i • v i = -∑ x ∈ s.erase i, g x • v x<GOAL>f (update v i (g i • v i)) = 0
<VAR>R : Type u_1<VAR>inst✝²⁰ : Semiring 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>P : Type u_4<VAR>inst✝¹⁵ : AddCommMonoid P<VAR>inst✝¹⁴ : Module R P<VAR>M' : Type u_5<VAR>inst✝¹³ : AddCommGroup M'<VAR>inst✝¹² : Module R M'<VAR>N' : Type u_6<VAR>inst✝¹¹ : AddCommGroup N'<VAR>inst✝¹⁰ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : Module R M₃<VAR>f✝ f' : M✝ [⋀^ι]→ₗ[R] N✝<VAR>g✝ g₂ : M✝ [⋀^ι]→ₗ[R] N'<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v✝ : ι → M✝<VAR>v' : ι → M'<VAR>K : Type u_12<VAR>inst✝⁵ : Ring K<VAR>M : Type u_13<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module K M<VAR>N : Type u_14<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module K N<VAR>inst✝ : NoZeroSMulDivisors K N<VAR>f : M [⋀^ι]→ₗ[K] N<VAR>v : ι → M<VAR>h✝ : ¬LinearIndependent K v<VAR>s : Finset ι<VAR>g : ι → K<VAR>i : ι<VAR>hi : i ∈ s<VAR>hz : g i ≠ 0<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>h : g i • v i = -∑ x ∈ s.erase i, g x • v x<GOAL>∑ a ∈ s.erase i, f (update v i (g a • v a)) = 0
<VAR>R : Type u_1<VAR>inst✝²⁰ : Semiring 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>P : Type u_4<VAR>inst✝¹⁵ : AddCommMonoid P<VAR>inst✝¹⁴ : Module R P<VAR>M' : Type u_5<VAR>inst✝¹³ : AddCommGroup M'<VAR>inst✝¹² : Module R M'<VAR>N' : Type u_6<VAR>inst✝¹¹ : AddCommGroup N'<VAR>inst✝¹⁰ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : Module R M₃<VAR>f✝ f' : M✝ [⋀^ι]→ₗ[R] N✝<VAR>g✝ g₂ : M✝ [⋀^ι]→ₗ[R] N'<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v✝ : ι → M✝<VAR>v' : ι → M'<VAR>K : Type u_12<VAR>inst✝⁵ : Ring K<VAR>M : Type u_13<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module K M<VAR>N : Type u_14<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module K N<VAR>inst✝ : NoZeroSMulDivisors K N<VAR>f : M [⋀^ι]→ₗ[K] N<VAR>v : ι → M<VAR>h✝ : ¬LinearIndependent K v<VAR>s : Finset ι<VAR>g : ι → K<VAR>i : ι<VAR>hi : i ∈ s<VAR>hz : g i ≠ 0<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>h : g i • v i = -∑ x ∈ s.erase i, g x • v x<GOAL>∀ x ∈ s.erase i, f (update v i (g x • v x)) = 0
<VAR>R : Type u_1<VAR>inst✝²⁰ : Semiring 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>P : Type u_4<VAR>inst✝¹⁵ : AddCommMonoid P<VAR>inst✝¹⁴ : Module R P<VAR>M' : Type u_5<VAR>inst✝¹³ : AddCommGroup M'<VAR>inst✝¹² : Module R M'<VAR>N' : Type u_6<VAR>inst✝¹¹ : AddCommGroup N'<VAR>inst✝¹⁰ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : Module R M₃<VAR>f✝ f' : M✝ [⋀^ι]→ₗ[R] N✝<VAR>g✝ g₂ : M✝ [⋀^ι]→ₗ[R] N'<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v✝ : ι → M✝<VAR>v' : ι → M'<VAR>K : Type u_12<VAR>inst✝⁵ : Ring K<VAR>M : Type u_13<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module K M<VAR>N : Type u_14<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module K N<VAR>inst✝ : NoZeroSMulDivisors K N<VAR>f : M [⋀^ι]→ₗ[K] N<VAR>v : ι → M<VAR>h✝ : ¬LinearIndependent K v<VAR>s : Finset ι<VAR>g : ι → K<VAR>i : ι<VAR>hi : i ∈ s<VAR>hz : g i ≠ 0<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>h : g i • v i = -∑ x ∈ s.erase i, g x • v x<VAR>j : ι<VAR>hj : j ∈ s.erase i<GOAL>f (update v i (g j • v j)) = 0
<VAR>R : Type u_1<VAR>inst✝²⁰ : Semiring 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>P : Type u_4<VAR>inst✝¹⁵ : AddCommMonoid P<VAR>inst✝¹⁴ : Module R P<VAR>M' : Type u_5<VAR>inst✝¹³ : AddCommGroup M'<VAR>inst✝¹² : Module R M'<VAR>N' : Type u_6<VAR>inst✝¹¹ : AddCommGroup N'<VAR>inst✝¹⁰ : Module R N'<VAR>ι : Type u_7<VAR>ι' : Type u_8<VAR>ι'' : Type u_9<VAR>M₂ : Type u_10<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : Module R M₂<VAR>M₃ : Type u_11<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>inst✝⁶ : Module R M₃<VAR>f✝ f' : M✝ [⋀^ι]→ₗ[R] N✝<VAR>g✝ g₂ : M✝ [⋀^ι]→ₗ[R] N'<VAR>g' : M' [⋀^ι]→ₗ[R] N'<VAR>v✝ : ι → M✝<VAR>v' : ι → M'<VAR>K : Type u_12<VAR>inst✝⁵ : Ring K<VAR>M : Type u_13<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module K M<VAR>N : Type u_14<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module K N<VAR>inst✝ : NoZeroSMulDivisors K N<VAR>f : M [⋀^ι]→ₗ[K] N<VAR>v : ι → M<VAR>h✝ : ¬LinearIndependent K v<VAR>s : Finset ι<VAR>g : ι → K<VAR>i : ι<VAR>hi : i ∈ s<VAR>hz : g i ≠ 0<VAR>this : DecidableEq ι := Classical.decEq ι<VAR>h : g i • v i = -∑ x ∈ s.erase i, g x • v x<VAR>j : ι<VAR>hj : j ∈ s.erase i<VAR>hij : j ≠ i<VAR>right✝ : j ∈ s<GOAL>f (update v i (g j • v j)) = 0
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>f : α → α<VAR>g : α → β<GOAL>Measurable g ↔ Measurable g ∧ ∀ (s : Set β), MeasurableSet s → g ∘ f ⁻¹' s = g ⁻¹' s
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>f : α → α<VAR>g : α → β<GOAL>(∀ ⦃t : Set β⦄, MeasurableSet t → MeasurableSet (g ⁻¹' t)) ↔ ∀ (x : Set β), MeasurableSet x → MeasurableSet (g ⁻¹' x) ∧ g ∘ f ⁻¹' x = g ⁻¹' x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : OrderedCommSemiring 𝕜<VAR>inst✝⁴ : AddCommMonoid E<VAR>inst✝³ : OrderedAddCommMonoid β<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>c : 𝕜<VAR>hc : 0 ≤ c<VAR>hf : ConvexOn 𝕜 s f<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>c • (a • f x + b • f y) = a • c • f x + b • c • f y
<VAR>α : Sort u_1<VAR>r : α → α → Prop<VAR>motive : (a : α) → Acc r a → Sort u_2<VAR>intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (a : r y x) → motive y ⋯) → motive x ⋯<VAR>a : α<VAR>t : Acc r a<GOAL>rec intro t = Acc.recC intro t
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝² : (i : ι) → AddCommMonoid (β i)<VAR>inst✝¹ : DecidableEq ι<VAR>γ : Type u₁<VAR>inst✝ : AddCommMonoid γ<VAR>φ : (i : ι) → β i →+ γ<VAR>ψ : (⨁ (i : ι), β i) →+ γ<VAR>f : ⨁ (i : ι), β i<GOAL>ψ = toAddMonoid fun i => ψ.comp (of β i)
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝² : (i : ι) → AddCommMonoid (β i)<VAR>inst✝¹ : DecidableEq ι<VAR>γ : Type u₁<VAR>inst✝ : AddCommMonoid γ<VAR>φ : (i : ι) → β i →+ γ<VAR>ψ : (⨁ (i : ι), β i) →+ γ<VAR>f : ⨁ (i : ι), β i<GOAL>∀ (x : ι), ψ.comp (DFinsupp.singleAddHom (fun i => β i) x) = (toAddMonoid fun i => ψ.comp (of β i)).comp (DFinsupp.singleAddHom (fun i => β i) x)
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<GOAL>↑univUnitBall 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s✝ s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f✝ f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>f : α → α<VAR>s : Set α<VAR>h : MapsTo f s s<VAR>n : ℕ<GOAL>(restrict f s s h)^[n] = restrict f^[n] s s ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s✝ s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f✝ f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>f : α → α<VAR>s : Set α<VAR>h : MapsTo f s s<VAR>n : ℕ<VAR>x : ↑s<GOAL>(restrict f s s h)^[n] x = restrict f^[n] s s ⋯ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s✝ s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>p : Set γ<VAR>f✝ f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>f : α → α<VAR>s : Set α<VAR>h : MapsTo f s s<VAR>n : ℕ<VAR>x : ↑s<GOAL>↑((restrict f s s h)^[n] x) = f^[n] ↑x
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>hxy : dist x y = 0<GOAL>x = y
<VAR>E : ℕ → Type u_1<VAR>x : (n : ℕ) → E n<VAR>hxy : dist x x = 0<GOAL>x = x
<VAR>E : ℕ → Type u_1<VAR>x y : (n : ℕ) → E n<VAR>hxy : dist x y = 0<VAR>h : x ≠ y<GOAL>x = y
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : LinearOrderedSemiring R<VAR>a b : R<VAR>m n : ℕ<VAR>hb : 0 ≤ b<GOAL>a ^ 2 < b ^ 2 → a < b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>n : ℕ<VAR>a b c : α<GOAL>a ^ 2 < b ^ 2 ↔ |a| < |b|
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<GOAL>card α ≤ 1 ↔ Subsingleton α
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<GOAL>card α ≤ 1 ↔ #α ≤ 1
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<GOAL>card α ≤ 1 ↔ #α ≤ ↑1
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>α : Type u_3<GOAL>card α ≤ 1 ↔ toPartENat #α ≤ ↑1
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>r : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>i : σ<GOAL>i ∈ p.vars ↔ ∃ d ∈ p.support, i ∈ d.support
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>r : ℝ<VAR>h : x ∈ s<VAR>H : hausdorffDist s t < r<VAR>fin : hausdorffEdist s t ≠ ⊤<GOAL>∃ y ∈ t, dist x y < r
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>r : ℝ<VAR>h : x ∈ s<VAR>H : hausdorffDist s t < r<VAR>fin : hausdorffEdist s t ≠ ⊤<VAR>r0 : 0 < r<GOAL>∃ y ∈ t, dist x y < r
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>r : ℝ<VAR>h : x ∈ s<VAR>H : hausdorffDist s t < r<VAR>fin : hausdorffEdist s t ≠ ⊤<VAR>r0 : 0 < r<VAR>this : hausdorffEdist s t < ENNReal.ofReal r<GOAL>∃ y ∈ t, dist x y < r
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y✝ : α<VAR>Φ : α → β<VAR>r : ℝ<VAR>h : x ∈ s<VAR>H : hausdorffDist s t < r<VAR>fin : hausdorffEdist s t ≠ ⊤<VAR>r0 : 0 < r<VAR>this : hausdorffEdist s t < ENNReal.ofReal r<VAR>y : α<VAR>hy : y ∈ t<VAR>yr : edist x y < ENNReal.ofReal r<GOAL>∃ y ∈ t, dist x y < r
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y✝ : α<VAR>Φ : α → β<VAR>r : ℝ<VAR>h : x ∈ s<VAR>H : hausdorffDist s t < r<VAR>fin : hausdorffEdist s t ≠ ⊤<VAR>r0 : 0 < r<VAR>this : hausdorffEdist s t < ENNReal.ofReal r<VAR>y : α<VAR>hy : y ∈ t<VAR>yr : dist x y < r<GOAL>∃ y ∈ t, dist x y < r
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<GOAL>iteratedFDeriv 𝕜 n f = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘ iteratedDeriv n f
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t t₁ t₂ : (i : ι) → Set (α i)<VAR>i✝ : ι<VAR>ht : (s.pi t).Nonempty<VAR>i : ι<GOAL>t i ⊆ eval i '' s.pi t
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝⁴ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ'₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>ι : Type u_7<VAR>s : Finset ι<VAR>f : ι → R<VAR>g : Γ₀<VAR>hg : g ≠ 0<VAR>hf : ∀ i ∈ s, v (f i) < g<GOAL>v (∑ i ∈ s, f i) < g
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝⁴ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ'₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>ι : Type u_7<VAR>s✝ : Finset ι<VAR>f : ι → R<VAR>g : Γ₀<VAR>hg : g ≠ 0<VAR>hf✝ : ∀ i ∈ s✝, v (f i) < g<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>ih : (∀ i ∈ s, v (f i) < g) → v (∑ i ∈ s, f i) < g<VAR>hf : ∀ i ∈ insert a s, v (f i) < g<GOAL>v (∑ i ∈ insert a s, f i) < g
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝⁴ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ'₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>ι : Type u_7<VAR>s✝ : Finset ι<VAR>f : ι → R<VAR>g : Γ₀<VAR>hg : g ≠ 0<VAR>hf✝ : ∀ i ∈ s✝, v (f i) < g<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>ih : (∀ i ∈ s, v (f i) < g) → v (∑ i ∈ s, f i) < g<VAR>hf : v (f a) < g ∧ ∀ x ∈ s, v (f x) < g<GOAL>v (∑ i ∈ insert a s, f i) < g
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝⁴ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝³ : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝² : Ring R<VAR>inst✝¹ : LinearOrderedCommMonoidWithZero Γ₀<VAR>inst✝ : LinearOrderedCommMonoidWithZero Γ'₀<VAR>v : Valuation R Γ₀<VAR>x y z : R<VAR>ι : Type u_7<VAR>s✝ : Finset ι<VAR>f : ι → R<VAR>g : Γ₀<VAR>hg : g ≠ 0<VAR>hf✝ : ∀ i ∈ s✝, v (f i) < g<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>ih : (∀ i ∈ s, v (f i) < g) → v (∑ i ∈ s, f i) < g<VAR>hf : v (f a) < g ∧ ∀ x ∈ s, v (f x) < g<GOAL>v (f a + ∑ x ∈ s, f x) < g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>x : E<GOAL>(setToFun μ T hT fun x_1 => x) = (T Set.univ) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>x : E<VAR>this : (fun x_1 => x) = Set.univ.indicator fun x_1 => x<GOAL>(setToFun μ T hT fun x_1 => x) = (T Set.univ) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>inst✝² : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝¹ : CompleteSpace F<VAR>T T' T'' : Set α → E →L[ℝ] F<VAR>C C' C'' : ℝ<VAR>f g : α → E<VAR>inst✝ : IsFiniteMeasure μ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>x : E<VAR>this : (fun x_1 => x) = Set.univ.indicator fun x_1 => x<GOAL>setToFun μ T hT (Set.univ.indicator fun x_1 => x) = (T Set.univ) x
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<VAR>x✝¹ : ℕ<VAR>x✝ : R<VAR>n✝ : ℕ<GOAL>x✝¹.choose k • x✝ = ↑(x✝¹.choose k) * x✝
<VAR>x y : ℂ<GOAL>cexp x = cexp y ↔ cexp (x - y) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f g : α →ₘ[μ] β<VAR>h : ↑f =ᶠ[ae μ] ↑g<GOAL>f = g
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁵ : Semiring α<VAR>inst✝⁴ : PartialOrder α<VAR>a b c d : α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : PosMulStrictMono α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>ha : a < 0<VAR>h : b < 1<GOAL>a < a * b