ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>p a : Associates α<VAR>hp : Irreducible p<VAR>n : ℕ<VAR>h : a ∣ p ^ n<VAR>a✝ : Nontrivial α<GOAL>a = p ^ p.count a.factors
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>p a : Associates α<VAR>hp : Irreducible p<VAR>n : ℕ<VAR>h : a ∣ p ^ n<VAR>a✝ : Nontrivial α<VAR>hph : p ^ n ≠ 0<GOAL>a = p ^ p.count a.factors
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>p a : Associates α<VAR>hp : Irreducible p<VAR>n : ℕ<VAR>h : a ∣ p ^ n<VAR>a✝ : Nontrivial α<VAR>hph : p ^ n ≠ 0<VAR>ha : a ≠ 0<GOAL>a = p ^ p.count a.factors
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>p a : Associates α<VAR>hp : Irreducible p<VAR>n : ℕ<VAR>h : a ∣ p ^ n<VAR>a✝ : Nontrivial α<VAR>hph : p ^ n ≠ 0<VAR>ha : a ≠ 0<GOAL>∀ (p_1 : Associates α), Irreducible p_1 → p_1.count a.factors = p_1.count (p ^ p.count a.factors).factors
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>p a : Associates α<VAR>hp : Irreducible p<VAR>n : ℕ<VAR>h : a ∣ p ^ n<VAR>a✝ : Nontrivial α<VAR>hph : p ^ n ≠ 0<VAR>ha : a ≠ 0<VAR>eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → q.count a.factors = 0<GOAL>∀ (p_1 : Associates α), Irreducible p_1 → p_1.count a.factors = p_1.count (p ^ p.count a.factors).factors
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>p a : Associates α<VAR>hp : Irreducible p<VAR>n : ℕ<VAR>h : a ∣ p ^ n<VAR>a✝ : Nontrivial α<VAR>hph : p ^ n ≠ 0<VAR>ha : a ≠ 0<VAR>eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → q.count a.factors = 0<VAR>q : Associates α<VAR>hq : Irreducible q<GOAL>q.count a.factors = q.count (p ^ p.count a.factors).factors
<VAR>α : Type u_1<VAR>inst✝⁴ : CancelCommMonoidWithZero α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>inst✝² : DecidableEq (Associates α)<VAR>inst✝¹ : (p : Associates α) → Decidable (Irreducible p)<VAR>inst✝ : DecidableEq (Associates α)<VAR>p a : Associates α<VAR>hp : Irreducible p<VAR>n : ℕ<VAR>h : a ∣ p ^ n<VAR>a✝ : Nontrivial α<VAR>hph : p ^ n ≠ 0<VAR>ha : a ≠ 0<VAR>eq_zero_of_ne : ∀ (q : Associates α), Irreducible q → q ≠ p → q.count a.factors = 0<VAR>q : Associates α<VAR>hq : Irreducible q<GOAL>q.count a.factors = p.count a.factors * q.count p.factors
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>k : ℤ<VAR>h : ↑p ∣ k ^ 2<GOAL>p ∣ k.natAbs
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>k : ℤ<VAR>h : ↑p ∣ k ^ 2<GOAL>p ∣ k.natAbs ^ 2
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NormedCommRing 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜<VAR>s : Set E<VAR>x✝ : F<GOAL>x✝ ∈ B.polar s ↔ x✝ ∈ ⋂ x ∈ s, {y | ‖(B x) y‖ ≤ 1}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<GOAL>dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c = LinearMap.id
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<GOAL>∀ (i : ι × κ), (dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c) ((b.tensorProduct c).dualBasis i) = LinearMap.id ((b.tensorProduct c).dualBasis i)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<VAR>i : ι<VAR>j : κ<GOAL>(dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c) ((b.tensorProduct c).dualBasis (i, j)) = LinearMap.id ((b.tensorProduct c).dualBasis (i, j))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<VAR>i : ι<VAR>j : κ<GOAL>∀ (i_1 : ι × κ), ((dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c) ((b.tensorProduct c).dualBasis (i, j))) ((b.tensorProduct c) i_1) = (LinearMap.id ((b.tensorProduct c).dualBasis (i, j))) ((b.tensorProduct c) i_1)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<VAR>i : ι<VAR>j : κ<VAR>i' : ι<VAR>j' : κ<GOAL>((dualDistrib R M N ∘ₗ dualDistribInvOfBasis b c) ((b.tensorProduct c).dualBasis (i, j))) ((b.tensorProduct c) (i', j')) = (LinearMap.id ((b.tensorProduct c).dualBasis (i, j))) ((b.tensorProduct c) (i', j'))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<VAR>i : ι<VAR>j : κ<VAR>i' : ι<VAR>j' : κ<GOAL>∑ x : ι, ∑ x_1 : κ, (Finsupp.single x_1 1) j * (Finsupp.single x 1) i * ((Finsupp.single i' 1) x * (Finsupp.single j' 1) x_1) = (Finsupp.single j' 1) j * (Finsupp.single i' 1) i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<VAR>i : ι<VAR>j : κ<VAR>i' : ι<VAR>j' : κ<GOAL>(Finsupp.single j 1) j * (Finsupp.single i 1) i * ((Finsupp.single i' 1) i * (Finsupp.single j' 1) j) = (Finsupp.single j' 1) j * (Finsupp.single i' 1) i
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<VAR>i : ι<VAR>j : κ<VAR>i' : ι<VAR>j' : κ<GOAL>∀ b ∈ Finset.univ, b ≠ j → (Finsupp.single b 1) j * (Finsupp.single i 1) i * ((Finsupp.single i' 1) i * (Finsupp.single j' 1) b) = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<VAR>i : ι<VAR>j : κ<VAR>i' : ι<VAR>j' : κ<GOAL>j ∉ Finset.univ → (Finsupp.single j 1) j * (Finsupp.single i 1) i * ((Finsupp.single i' 1) i * (Finsupp.single j' 1) j) = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<VAR>i : ι<VAR>j : κ<VAR>i' : ι<VAR>j' : κ<GOAL>∀ b ∈ Finset.univ, b ≠ i → ∑ x : κ, (Finsupp.single x 1) j * (Finsupp.single b 1) i * ((Finsupp.single i' 1) b * (Finsupp.single j' 1) x) = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : DecidableEq κ<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : Fintype κ<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>b : Basis ι R M<VAR>c : Basis κ R N<VAR>i : ι<VAR>j : κ<VAR>i' : ι<VAR>j' : κ<GOAL>i ∉ Finset.univ → ∑ x : κ, (Finsupp.single x 1) j * (Finsupp.single i 1) i * ((Finsupp.single i' 1) i * (Finsupp.single j' 1) x) = 0
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : Finite ι<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : (i : ι) → AddCommGroup (E i)<VAR>inst✝ : (i : ι) → Module 𝕜 (E i)<VAR>s : Set ι<VAR>t : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>h : ∀ i ∈ s, x i ∈ (convexHull 𝕜) (t i)<GOAL>x ∈ (convexHull 𝕜) (s.pi t)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : Finite ι<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : (i : ι) → AddCommGroup (E i)<VAR>inst✝ : (i : ι) → Module 𝕜 (E i)<VAR>s : Set ι<VAR>t : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>h : ∀ i ∈ s, x i ∈ (convexHull 𝕜) (t i)<VAR>val✝ : Fintype ι<GOAL>x ∈ (convexHull 𝕜) (s.pi t)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : Finite ι<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : (i : ι) → AddCommGroup (E i)<VAR>inst✝ : (i : ι) → Module 𝕜 (E i)<VAR>s : Set ι<VAR>t✝ : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>val✝ : Fintype ι<VAR>t : (i : ι) → Set (E i)<VAR>h : ∀ i ∈ Set.univ, x i ∈ (convexHull 𝕜) (t i)<GOAL>x ∈ (convexHull 𝕜) (Set.univ.pi t)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : Finite ι<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : (i : ι) → AddCommGroup (E i)<VAR>inst✝ : (i : ι) → Module 𝕜 (E i)<VAR>s : Set ι<VAR>t✝ : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>val✝ : Fintype ι<VAR>t : (i : ι) → Set (E i)<VAR>h : ∀ (i : ι), ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i : ι, w i = 1 ∧ (∀ (i_1 : ι), z i_1 ∈ t i) ∧ ∑ i_1 : ι, w i_1 • z i_1 = x i<GOAL>x ∈ (convexHull 𝕜) (Set.univ.pi t)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : Finite ι<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : (i : ι) → AddCommGroup (E i)<VAR>inst✝ : (i : ι) → Module 𝕜 (E i)<VAR>s : Set ι<VAR>t✝ : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>val✝ : Fintype ι<VAR>t : (i : ι) → Set (E i)<VAR>κ : ι → Type<VAR>x✝ : (i : ι) → Fintype (κ i)<VAR>w : (i : ι) → κ i → 𝕜<VAR>f : (i : ι) → κ i → E i<VAR>hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1<VAR>hw₁ : ∀ (i : ι), ∑ i_1 : κ i, w i i_1 = 1<VAR>hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i<VAR>hf : ∀ (i : ι), ∑ i_1 : κ i, w i i_1 • f i i_1 = x i<GOAL>x ∈ (convexHull 𝕜) (Set.univ.pi t)
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : Finite ι<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : (i : ι) → AddCommGroup (E i)<VAR>inst✝ : (i : ι) → Module 𝕜 (E i)<VAR>s : Set ι<VAR>t✝ : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>val✝ : Fintype ι<VAR>t : (i : ι) → Set (E i)<VAR>κ : ι → Type<VAR>x✝ : (i : ι) → Fintype (κ i)<VAR>w : (i : ι) → κ i → 𝕜<VAR>f : (i : ι) → κ i → E i<VAR>hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1<VAR>hw₁ : ∀ (i : ι), ∑ i_1 : κ i, w i i_1 = 1<VAR>hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i<VAR>hf : ∀ (i : ι), ∑ i_1 : κ i, w i i_1 • f i i_1 = x i<GOAL>∑ i : (i : ι) → κ i, (fun k => ∏ i : ι, w i (k i)) i = 1
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : Finite ι<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : (i : ι) → AddCommGroup (E i)<VAR>inst✝ : (i : ι) → Module 𝕜 (E i)<VAR>s : Set ι<VAR>t✝ : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>val✝ : Fintype ι<VAR>t : (i : ι) → Set (E i)<VAR>κ : ι → Type<VAR>x✝ : (i : ι) → Fintype (κ i)<VAR>w : (i : ι) → κ i → 𝕜<VAR>f : (i : ι) → κ i → E i<VAR>hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1<VAR>hw₁ : ∀ (i : ι), ∑ i_1 : κ i, w i i_1 = 1<VAR>hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i<VAR>hf : ∀ (i : ι), ∑ i_1 : κ i, w i i_1 • f i i_1 = x i<GOAL>∑ i : (i : ι) → κ i, (fun k => ∏ i : ι, w i (k i)) i • (fun g i => f i (g i)) i = x
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : Finite ι<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : (i : ι) → AddCommGroup (E i)<VAR>inst✝ : (i : ι) → Module 𝕜 (E i)<VAR>s : Set ι<VAR>t✝ : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>val✝ : Fintype ι<VAR>t : (i : ι) → Set (E i)<VAR>κ : ι → Type<VAR>x✝ : (i : ι) → Fintype (κ i)<VAR>w : (i : ι) → κ i → 𝕜<VAR>f : (i : ι) → κ i → E i<VAR>hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1<VAR>hw₁ : ∀ (i : ι), ∑ i_1 : κ i, w i i_1 = 1<VAR>hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i<VAR>hf : ∀ (i : ι), ∑ i_1 : κ i, w i i_1 • f i i_1 = x i<VAR>i : ι<GOAL>(∑ i : (i : ι) → κ i, (fun k => ∏ i : ι, w i (k i)) i • (fun g i => f i (g i)) i) i = x i
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : Finite ι<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : (i : ι) → AddCommGroup (E i)<VAR>inst✝ : (i : ι) → Module 𝕜 (E i)<VAR>s : Set ι<VAR>t✝ : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>val✝ : Fintype ι<VAR>t : (i : ι) → Set (E i)<VAR>κ : ι → Type<VAR>x✝ : (i : ι) → Fintype (κ i)<VAR>w : (i : ι) → κ i → 𝕜<VAR>f : (i : ι) → κ i → E i<VAR>hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1<VAR>hw₁ : ∀ (i : ι), ∑ i_1 : κ i, w i i_1 = 1<VAR>hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i<VAR>hf : ∀ (i : ι), ∑ i_1 : κ i, w i i_1 • f i i_1 = x i<VAR>i : ι<GOAL>∑ j : κ i, (∑ g : { g // g i = j }, ∏ k : ι, w k (↑g k)) • f i j = ∑ j : κ i, w i j • f i j
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>inst✝³ : Finite ι<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : (i : ι) → AddCommGroup (E i)<VAR>inst✝ : (i : ι) → Module 𝕜 (E i)<VAR>s : Set ι<VAR>t✝ : (i : ι) → Set (E i)<VAR>x : (i : ι) → E i<VAR>val✝ : Fintype ι<VAR>t : (i : ι) → Set (E i)<VAR>κ : ι → Type<VAR>x✝ : (i : ι) → Fintype (κ i)<VAR>w : (i : ι) → κ i → 𝕜<VAR>f : (i : ι) → κ i → E i<VAR>hw₀ : ∀ (i : ι) (i_1 : κ i), 0 ≤ w i i_1<VAR>hw₁ : ∀ (i : ι), ∑ i_1 : κ i, w i i_1 = 1<VAR>hft : ∀ (i : ι) (i_1 : κ i), f i i_1 ∈ t i<VAR>hf : ∀ (i : ι), ∑ i_1 : κ i, w i i_1 • f i i_1 = x i<VAR>i : ι<VAR>j : κ i<VAR>a✝ : j ∈ Finset.univ<GOAL>∑ g : { g // g i = j }, ∏ k : ι, w k (↑g k) = w i j
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : G → H<VAR>f' : G → G →L[𝕜] H<VAR>x : G<VAR>hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt f (f' y) y<VAR>hcont : ContinuousAt f' x<GOAL>HasStrictFDerivAt f (f' x) x
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : G → H<VAR>f' : G → G →L[𝕜] H<VAR>x : G<VAR>hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt f (f' y) y<VAR>hcont : ContinuousAt f' x<VAR>c : ℝ<VAR>hc : 0 < c<GOAL>∃ ε > 0, ∀ y ∈ ball (x, x) ε, ‖f y.1 - f y.2 - (f' x) (y.1 - y.2)‖ ≤ c * ‖y.1 - y.2‖
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : G → H<VAR>f' : G → G →L[𝕜] H<VAR>x : G<VAR>hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt f (f' y) y<VAR>hcont : ContinuousAt f' x<VAR>c : ℝ<VAR>hc : 0 < c<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hε : ball x ε ⊆ {x | (fun y => HasFDerivAt f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c<GOAL>∃ ε > 0, ∀ y ∈ ball (x, x) ε, ‖f y.1 - f y.2 - (f' x) (y.1 - y.2)‖ ≤ c * ‖y.1 - y.2‖
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : G → H<VAR>f' : G → G →L[𝕜] H<VAR>x : G<VAR>hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt f (f' y) y<VAR>hcont : ContinuousAt f' x<VAR>c : ℝ<VAR>hc : 0 < c<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hε : ball x ε ⊆ {x | (fun y => HasFDerivAt f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c<VAR>a b : G<VAR>h : (a, b) ∈ ball (x, x) ε<GOAL>‖f (a, b).1 - f (a, b).2 - (f' x) ((a, b).1 - (a, b).2)‖ ≤ c * ‖(a, b).1 - (a, b).2‖
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : G → H<VAR>f' : G → G →L[𝕜] H<VAR>x : G<VAR>hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt f (f' y) y<VAR>hcont : ContinuousAt f' x<VAR>c : ℝ<VAR>hc : 0 < c<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hε : ball x ε ⊆ {x | (fun y => HasFDerivAt f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c<VAR>a b : G<VAR>h : a ∈ ball x ε ∧ b ∈ ball x ε<GOAL>‖f (a, b).1 - f (a, b).2 - (f' x) ((a, b).1 - (a, b).2)‖ ≤ c * ‖(a, b).1 - (a, b).2‖
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : G → H<VAR>f' : G → G →L[𝕜] H<VAR>x : G<VAR>hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt f (f' y) y<VAR>hcont : ContinuousAt f' x<VAR>c : ℝ<VAR>hc : 0 < c<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hε : ball x ε ⊆ {x | (fun y => HasFDerivAt f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c<VAR>a b : G<VAR>h : a ∈ ball x ε ∧ b ∈ ball x ε<VAR>hf' : ∀ x' ∈ ball x ε, ‖f' x' - f' x‖ ≤ c<GOAL>‖f (a, b).1 - f (a, b).2 - (f' x) ((a, b).1 - (a, b).2)‖ ≤ c * ‖(a, b).1 - (a, b).2‖
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : G → H<VAR>f' : G → G →L[𝕜] H<VAR>x : G<VAR>hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt f (f' y) y<VAR>hcont : ContinuousAt f' x<VAR>c : ℝ<VAR>hc : 0 < c<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hε : ball x ε ⊆ {x | (fun y => HasFDerivAt f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c<VAR>a b : G<VAR>h : a ∈ ball x ε ∧ b ∈ ball x ε<VAR>hf' : ∀ x' ∈ ball x ε, ‖f' x' - f' x‖ ≤ c<VAR>this : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G<GOAL>‖f (a, b).1 - f (a, b).2 - (f' x) ((a, b).1 - (a, b).2)‖ ≤ c * ‖(a, b).1 - (a, b).2‖
<VAR>E : Type u_1<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>H : Type u_5<VAR>inst✝¹ : NormedAddCommGroup H<VAR>inst✝ : NormedSpace 𝕜 H<VAR>f : G → H<VAR>f' : G → G →L[𝕜] H<VAR>x : G<VAR>hder : ∀ᶠ (y : G) in 𝓝 x, HasFDerivAt f (f' y) y<VAR>hcont : ContinuousAt f' x<VAR>c : ℝ<VAR>hc : 0 < c<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hε : ball x ε ⊆ {x | (fun y => HasFDerivAt f (f' y) y) x} ∩ f' ⁻¹' ball (f' x) c<VAR>a b : G<VAR>h : a ∈ ball x ε ∧ b ∈ ball x ε<VAR>hf' : ∀ x' ∈ ball x ε, ‖f' x' - f' x‖ ≤ c<VAR>this : NormedSpace ℝ G := RestrictScalars.normedSpace ℝ 𝕜 G<GOAL>∀ x_1 ∈ ball x ε, HasFDerivWithinAt f (f' x_1) (ball x ε) x_1
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : LieRing L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : IsIrreducible R L M<GOAL>∃ x y, x ≠ y
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : LieRing L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : IsIrreducible R L M<VAR>aux : ⊥ ≠ ⊤<GOAL>∃ x y, x ≠ y
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : LieRing L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : IsIrreducible R L M<VAR>aux : ∀ (x y : M), x = y<GOAL>⊥ = ⊤
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝ : DivisionRing α<VAR>p q : ℚ<VAR>hp : ↑p.den ≠ 0<VAR>hq : ↑q.den ≠ 0<GOAL>↑(p - q) = ↑p - ↑q
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>P : C → Prop<VAR>A : Type u_2<VAR>inst✝² : AddMonoid A<VAR>inst✝¹ : HasShift C A<VAR>inst✝ : ClosedUnderIsomorphisms P<VAR>X : C<GOAL>PredicateShift P 0 X ↔ P X
<VAR>R : Type u_1<VAR>inst✝² : Monoid R<VAR>S : Submonoid R<VAR>inst✝¹ : OreSet S<VAR>X : Type ?u.97943<VAR>inst✝ : MulAction R X<VAR>s s' : ↥S<GOAL>↑s /ₒ s' * (↑s' /ₒ s) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<VAR>a : α<GOAL>{a}.biUnion t = t a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>f : R →+* S<GOAL>map f (dickson k a 0) = dickson k (f a) 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>f : R →+* S<GOAL>map f (dickson k a 1) = dickson k (f a) 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>f : R →+* S<VAR>n : ℕ<GOAL>map f (dickson k a (n + 2)) = dickson k (f a) (n + 2)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>k : ℕ<VAR>a : R<VAR>f : R →+* S<VAR>n : ℕ<GOAL>X * map f (dickson k a (n + 1)) - C (f a) * map f (dickson k a n) = X * dickson k (f a) (n + 1) - C (f a) * dickson k (f a) n
<VAR>n : ℕ<GOAL>Fintype.card ↑(incl.obj (mk n)) = n
<VAR>n : ℕ<GOAL>Fintype.card ↑(incl.obj (mk n)) = Finset.univ.card
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<GOAL>(↑n).comp p = ↑n
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasPushouts C<VAR>W X Y Z : C<VAR>f : X ⟶ Y<VAR>g : X ⟶ Z<VAR>inst✝ : Mono f<VAR>s : PushoutCocone f g<VAR>hs : IsColimit s<VAR>this : Mono ((colimit.cocone (span f g)).ι.app WalkingCospan.right)<GOAL>Mono s.inr