ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<VAR>r₁ : R<VAR>hr₁0 : 0 < r₁<VAR>hr₁1 : r₁ < 1<VAR>h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)<VAR>r₂ : R<VAR>hr₂0 : 0 < r₂<VAR>hr₂1 : r₂ < 1<VAR>h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)<VAR>w : Fin (2 + 1) → R<VAR>hw : ∑ i : Fin (2 + 1), w i = 1<VAR>hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)<VAR>h₁' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {(Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationSingleWeights R i₁), (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)}<VAR>h₂' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂}<VAR>h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)<VAR>h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)<GOAL>w i₁ ∈ Set.Ioo 0 1
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<VAR>r₁ : R<VAR>hr₁0 : 0 < r₁<VAR>hr₁1 : r₁ < 1<VAR>h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)<VAR>r₂ : R<VAR>hr₂0 : 0 < r₂<VAR>hr₂1 : r₂ < 1<VAR>h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)<VAR>w : Fin (2 + 1) → R<VAR>hw : ∑ i : Fin (2 + 1), w i = 1<VAR>hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)<VAR>h₁' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {(Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationSingleWeights R i₁), (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)}<VAR>h₂' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂}<VAR>h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)<VAR>h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)<VAR>hs : ∀ (i : Fin 3), SignType.sign (w i) = SignType.sign (w i₃)<VAR>hss : SignType.sign (∑ i : Fin (2 + 1), w i) = 1<GOAL>w i₁ ∈ Set.Ioo 0 1
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<VAR>r₁ : R<VAR>hr₁0 : 0 < r₁<VAR>hr₁1 : r₁ < 1<VAR>h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)<VAR>r₂ : R<VAR>hr₂0 : 0 < r₂<VAR>hr₂1 : r₂ < 1<VAR>h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)<VAR>w : Fin (2 + 1) → R<VAR>hw : ∑ i : Fin (2 + 1), w i = 1<VAR>hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)<VAR>h₁' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {(Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationSingleWeights R i₁), (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)}<VAR>h₂' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂}<VAR>h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)<VAR>h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)<VAR>hs : ∀ (i : Fin 3), SignType.sign (w i) = SignType.sign (w i₃)<VAR>hss : SignType.sign (∑ i : Fin (2 + 1), w i) = 1<VAR>hs' : SignType.sign (∑ i : Fin 3, w i) = SignType.sign (w i₃)<GOAL>w i₁ ∈ Set.Ioo 0 1
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<VAR>r₁ : R<VAR>hr₁0 : 0 < r₁<VAR>hr₁1 : r₁ < 1<VAR>h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)<VAR>r₂ : R<VAR>hr₂0 : 0 < r₂<VAR>hr₂1 : r₂ < 1<VAR>h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)<VAR>w : Fin (2 + 1) → R<VAR>hw : ∑ i : Fin (2 + 1), w i = 1<VAR>hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)<VAR>h₁' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {(Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationSingleWeights R i₁), (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)}<VAR>h₂' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂}<VAR>h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)<VAR>h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)<VAR>hs : ∀ (i : Fin 3), SignType.sign (w i) = SignType.sign (w i₃)<VAR>hss : SignType.sign (w i₃) = 1<VAR>hs' : SignType.sign (∑ i : Fin 3, w i) = SignType.sign (w i₃)<GOAL>w i₁ ∈ Set.Ioo 0 1
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<VAR>r₁ : R<VAR>hr₁0 : 0 < r₁<VAR>hr₁1 : r₁ < 1<VAR>h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)<VAR>r₂ : R<VAR>hr₂0 : 0 < r₂<VAR>hr₂1 : r₂ < 1<VAR>h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)<VAR>w : Fin (2 + 1) → R<VAR>hw : ∑ i : Fin (2 + 1), w i = 1<VAR>hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)<VAR>h₁' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {(Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationSingleWeights R i₁), (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)}<VAR>h₂' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂}<VAR>h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)<VAR>h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)<VAR>hss : SignType.sign (w i₃) = 1<VAR>hs' : SignType.sign (∑ i : Fin 3, w i) = SignType.sign (w i₃)<VAR>hs : ∀ (i : Fin 3), 0 < w i<GOAL>w i₁ ∈ Set.Ioo 0 1
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<VAR>r₁ : R<VAR>hr₁0 : 0 < r₁<VAR>hr₁1 : r₁ < 1<VAR>h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)<VAR>r₂ : R<VAR>hr₂0 : 0 < r₂<VAR>hr₂1 : r₂ < 1<VAR>h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)<VAR>w : Fin (2 + 1) → R<VAR>hw : ∑ i ∈ {i₁, i₂, i₃}, w i = 1<VAR>hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)<VAR>h₁' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {(Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationSingleWeights R i₁), (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)}<VAR>h₂' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂}<VAR>h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)<VAR>h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)<VAR>hss : SignType.sign (w i₃) = 1<VAR>hs' : SignType.sign (∑ i : Fin 3, w i) = SignType.sign (w i₃)<VAR>hs : ∀ (i : Fin 3), 0 < w i<GOAL>w i₁ < 1
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<VAR>r₁ : R<VAR>hr₁0 : 0 < r₁<VAR>hr₁1 : r₁ < 1<VAR>h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)<VAR>r₂ : R<VAR>hr₂0 : 0 < r₂<VAR>hr₂1 : r₂ < 1<VAR>h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)<VAR>w : Fin (2 + 1) → R<VAR>hw : w i₁ + (w i₂ + w i₃) = 1<VAR>hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)<VAR>h₁' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {(Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationSingleWeights R i₁), (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)}<VAR>h₂' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂}<VAR>h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)<VAR>h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)<VAR>hss : SignType.sign (w i₃) = 1<VAR>hs' : SignType.sign (∑ i : Fin 3, w i) = SignType.sign (w i₃)<VAR>hs : ∀ (i : Fin 3), 0 < w i<GOAL>w i₁ < 1
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<VAR>r₁ : R<VAR>hr₁0 : 0 < r₁<VAR>hr₁1 : r₁ < 1<VAR>h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)<VAR>r₂ : R<VAR>hr₂0 : 0 < r₂<VAR>hr₂1 : r₂ < 1<VAR>h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)<VAR>w : Fin (2 + 1) → R<VAR>hw : w i₁ + ∑ x ∈ {i₂, i₃}, w x = 1<VAR>hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)<VAR>h₁' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {(Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationSingleWeights R i₁), (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)}<VAR>h₂' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂}<VAR>h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)<VAR>h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)<VAR>hss : SignType.sign (w i₃) = 1<VAR>hs' : SignType.sign (∑ i : Fin 3, w i) = SignType.sign (w i₃)<VAR>hs : ∀ (i : Fin 3), 0 < w i<GOAL>i₂ ∉ {i₃}
<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✝⁴ : LinearOrderedRing R<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : Module R V<VAR>inst✝¹ : AddTorsor V P<VAR>inst✝ : NoZeroSMulDivisors R V<VAR>t : Affine.Triangle R P<VAR>i₁ i₂ i₃ : Fin 3<VAR>h₁₂ : i₁ ≠ i₂<VAR>this : DecidableRel fun x x_1 => x < x_1 := LinearOrderedRing.decidableLT<VAR>h₁₃ : i₁ ≠ i₃<VAR>h₂₃ : i₂ ≠ i₃<VAR>h3 : ∀ (i : Fin 3), i = i₁ ∨ i = i₂ ∨ i = i₃<VAR>hu : Finset.univ = {i₁, i₂, i₃}<VAR>r₁ : R<VAR>hr₁0 : 0 < r₁<VAR>hr₁1 : r₁ < 1<VAR>h₁ : Sbtw R (t.points i₂) ((lineMap (t.points i₂) (t.points i₃)) r₁) (t.points i₃)<VAR>r₂ : R<VAR>hr₂0 : 0 < r₂<VAR>hr₂1 : r₂ < 1<VAR>h₂ : Sbtw R (t.points i₁) ((lineMap (t.points i₁) (t.points i₃)) r₂) (t.points i₃)<VAR>w : Fin (2 + 1) → R<VAR>hw : ∑ i ∈ {i₁, i₂, i₃}, w i = 1<VAR>hp : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R (Set.range t.points)<VAR>h₁' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {(Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationSingleWeights R i₁), (Finset.affineCombination R Finset.univ t.points) (Finset.affineCombinationLineMapWeights i₂ i₃ r₁)}<VAR>h₂' : (Finset.affineCombination R Finset.univ t.points) w ∈ affineSpan R {t.points i₂, (lineMap (t.points i₁) (t.points i₃)) r₂}<VAR>h₁s : SignType.sign (w i₂) = SignType.sign (w i₃)<VAR>h₂s : SignType.sign (w i₁) = SignType.sign (w i₃)<VAR>hss : SignType.sign (w i₃) = 1<VAR>hs' : SignType.sign (∑ i : Fin 3, w i) = SignType.sign (w i₃)<VAR>hs : ∀ (i : Fin 3), 0 < w i<GOAL>i₁ ∉ {i₂, i₃}
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f✝¹ f✝ : ℂ → E<VAR>hf✝ : Differentiable ℂ f✝<VAR>c z : ℂ<VAR>f : ℂ → ℂ<VAR>hf : Differentiable ℂ f<GOAL>∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f✝¹ f✝ : ℂ → E<VAR>hf✝ : Differentiable ℂ f✝<VAR>c z : ℂ<VAR>f : ℂ → ℂ<VAR>hf : Differentiable ℂ f<VAR>n : ℕ<GOAL>(↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>E : Type u_3<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Algebra K E<VAR>inst✝ : IsScalarTower F K E<VAR>h : Normal F E<VAR>x : E<GOAL>IsIntegral K x ∧ Splits (algebraMap K E) (minpoly K x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>E : Type u_3<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Algebra K E<VAR>inst✝ : IsScalarTower F K E<VAR>h : Normal F E<VAR>x : E<VAR>hx : IsIntegral F x<VAR>hhx : Splits (algebraMap F E) (minpoly F x)<GOAL>IsIntegral K x ∧ Splits (algebraMap K E) (minpoly K x)
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field K<VAR>inst✝⁴ : Algebra F K<VAR>E : Type u_3<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>inst✝¹ : Algebra K E<VAR>inst✝ : IsScalarTower F K E<VAR>h : Normal F E<VAR>x : E<VAR>hx : IsIntegral F x<VAR>hhx : Splits ((algebraMap K E).comp (algebraMap F K)) (minpoly F x)<GOAL>IsIntegral K x ∧ Splits (algebraMap K E) (minpoly K x)
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>E : Type u_2<VAR>𝕜 : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>f✝ : α → E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : α → E<VAR>hf : Integrable f μ<VAR>hf_int : ∫ (x : α), ⟪∫ (x : α), f x ∂μ, f x⟫_𝕜 ∂μ = 0<GOAL>∫ (x : α), f x ∂μ = 0
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>p : Prop<GOAL>IsCoatom p ↔ ¬p
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>p : Prop<GOAL>¬p → ∀ (b : Prop), (p → b) → b → ¬p → b
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : Ring R<VAR>p q : R[X]<VAR>inst✝ : Nontrivial R<VAR>hq : q.Monic<VAR>h : p.degree < q.degree<GOAL>p %ₘ q = p
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l : List α<VAR>l' : List β<VAR>lp : List (α × β)<VAR>hl : map Prod.fst lp = l<VAR>hr : map Prod.snd lp = l'<GOAL>lp = l.zip l'
<VAR>p✝ : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>inst✝³ : Fact (1 ≤ p✝)<VAR>inst✝² : Fintype ι<VAR>p : ℝ≥0∞<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>β : ι → Type u_5<VAR>inst✝ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>n : ℕ<VAR>h : p = ↑n<VAR>f : PiLp p β<GOAL>‖f‖ = (∑ i : ι, ‖f i‖ ^ n) ^ (1 / ↑n)
<VAR>p✝ : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>inst✝³ : Fact (1 ≤ p✝)<VAR>inst✝² : Fintype ι<VAR>p : ℝ≥0∞<VAR>inst✝¹ : Fact (1 ≤ p)<VAR>β : ι → Type u_5<VAR>inst✝ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>n : ℕ<VAR>h : p = ↑n<VAR>f : PiLp p β<VAR>this : 0 < p.toReal<GOAL>‖f‖ = (∑ i : ι, ‖f i‖ ^ n) ^ (1 / ↑n)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁹ : Semiring A<VAR>inst✝⁸ : DecidableEq ι<VAR>inst✝⁷ : CanonicallyOrderedAddCommMonoid ι<VAR>inst✝⁶ : SetLike σ A<VAR>inst✝⁵ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝⁴ : GradedRing 𝒜<VAR>a : A<VAR>n✝ i : ι<VAR>inst✝³ : Sub ι<VAR>inst✝² : OrderedSub ι<VAR>inst✝¹ : ContravariantClass ι ι (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>n : ι<VAR>inst✝ : Decidable (i ≤ n)<VAR>b : ↥(𝒜 i)<GOAL>↑(((decompose 𝒜) (a * ↑b)) n) = if i ≤ n then ↑(((decompose 𝒜) a) (n - i)) * ↑b else 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>ca : Computation α<VAR>cb : Computation β<VAR>l : ∀ {a : α}, a ∈ ca → ∃ b, b ∈ cb ∧ R a b<VAR>right✝ : ∀ {b : β}, b ∈ cb → ∃ a, a ∈ ca ∧ R a b<VAR>a : α<VAR>b : β<VAR>ma : a ∈ ca<VAR>mb : b ∈ cb<VAR>b' : β<VAR>mb' : b' ∈ cb<VAR>ab' : R a b'<GOAL>R a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : α → β → Prop<VAR>ca : Computation α<VAR>cb : Computation β<VAR>l : ∀ {a : α}, a ∈ ca → ∃ b, b ∈ cb ∧ R a b<VAR>right✝ : ∀ {b : β}, b ∈ cb → ∃ a, a ∈ ca ∧ R a b<VAR>a : α<VAR>b : β<VAR>ma : a ∈ ca<VAR>mb : b ∈ cb<VAR>b' : β<VAR>mb' : b' ∈ cb<VAR>ab' : R a b'<GOAL>R a b'
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>f : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }<GOAL>((↑f).1.sigma fun i => ((↑f).2 i).toFinset).val.NodupKeys
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>f : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }<GOAL>∀ x ∈ ((↑f).1.sigma fun i => ((↑f).2 i).toFinset).val, ∀ y ∈ ((↑f).1.sigma fun i => ((↑f).2 i).toFinset).val, x.fst = y.fst → x = y
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>f : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }<GOAL>∀ (x : (a : α) × β a), x.fst ∈ (↑f).1 ∧ (↑f).2 x.fst = some x.snd → ∀ (y : (a : α) × β a), y.fst ∈ (↑f).1 ∧ (↑f).2 y.fst = some y.snd → x.fst = y.fst → x = y
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>f : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }<VAR>i : α<VAR>x : β i<VAR>left✝¹ : ⟨i, x⟩.fst ∈ (↑f).1<VAR>hx : (↑f).2 ⟨i, x⟩.fst = some ⟨i, x⟩.snd<VAR>y : β i<VAR>left✝ : ⟨i, y⟩.fst ∈ (↑f).1<VAR>hy : (↑f).2 ⟨i, y⟩.fst = some ⟨i, y⟩.snd<GOAL>⟨i, x⟩ = ⟨i, y⟩
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<GOAL>Tendsto (fun n => ((f ^ n) x - x) / ↑n) atTop (𝓝 (τ f))
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<GOAL>Tendsto (fun n => ((f ^ n) x - x) / ↑n) atTop (𝓝 (τ (↑(translate (Multiplicative.ofAdd x))⁻¹ * f * ↑(translate (Multiplicative.ofAdd x)))))
<VAR>f g : CircleDeg1Lift<VAR>x : ℝ<VAR>n : ℕ<GOAL>((↑(translate (Multiplicative.ofAdd x))⁻¹ * f * ↑(translate (Multiplicative.ofAdd x))) ^ n) 0 / ↑n = ((f ^ n) x - x) / ↑n
<VAR>G : Type u_1<VAR>inst✝² : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>f : NormedAddGroupHom G H<VAR>g : NormedAddGroupHom H K<VAR>x : Completion G<GOAL>(g.completion.comp f.completion) x = (g.comp f).completion x
<VAR>G : Type u_1<VAR>inst✝² : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>f : NormedAddGroupHom G H<VAR>g : NormedAddGroupHom H K<VAR>x : Completion G<GOAL>Completion.map (⇑g ∘ ⇑f) x = Completion.map (⇑(g.comp f)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>inst✝ : Fintype α<GOAL>IsInitSeg (initSeg s) s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>inst✝ : Fintype α<VAR>t₁ t₂ : Finset α<VAR>ht₁ : t₁ ∈ initSeg s<VAR>ht₂ : { ofColex := t₂ } < { ofColex := t₁ } ∧ t₂.card = s.card<GOAL>{ ofColex := t₂ } ≤ { ofColex := s }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>inst✝ : Fintype α<VAR>t₁ t₂ : Finset α<VAR>ht₁ : s.card = t₁.card ∧ { ofColex := t₁ } ≤ { ofColex := s }<VAR>ht₂ : { ofColex := t₂ } < { ofColex := t₁ } ∧ t₂.card = s.card<GOAL>{ ofColex := t₂ } ≤ { ofColex := s }
<GOAL>StrictConcaveOn ℝ (Ioi 1) fun x => √x * log x
<GOAL>ContinuousOn (fun x => √x * log x) (Ioi 1)
<VAR>x : ℝ<VAR>hx : x ∈ Ioi 1<GOAL>deriv^[2] (fun x => √x * log x) x < 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f✝¹ : α → β<VAR>μa μa' : Measure α<VAR>μb μb' : Measure β<VAR>μc : Measure γ<VAR>f✝ : α → β<VAR>s : Set α<VAR>f : α → α<VAR>hf : QuasiMeasurePreserving f μ μ<VAR>hs : f ⁻¹' s =ᵐ[μ] s<VAR>k : ℕ<VAR>ih : f^[k] ⁻¹' s =ᵐ[μ] s<GOAL>f^[k + 1] ⁻¹' s =ᵐ[μ] s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f✝¹ : α → β<VAR>μa μa' : Measure α<VAR>μb μb' : Measure β<VAR>μc : Measure γ<VAR>f✝ : α → β<VAR>s : Set α<VAR>f : α → α<VAR>hf : QuasiMeasurePreserving f μ μ<VAR>hs : f ⁻¹' s =ᵐ[μ] s<VAR>k : ℕ<VAR>ih : f^[k] ⁻¹' s =ᵐ[μ] s<GOAL>f ⁻¹' (f^[k] ⁻¹' s) =ᵐ[μ] s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι✝<VAR>g : ι✝ → α<VAR>inst✝² : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>ι : Type u_5<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>t : ι → Set α<VAR>V : ι → Set (β × β)<VAR>ht : ∀ (n : ι), t n ∈ 𝔖<VAR>hmono : Monotone t<VAR>hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n<VAR>hb : (𝓤 β).HasAntitoneBasis V<GOAL>(𝓤 (α →ᵤ[𝔖] β)).HasAntitoneBasis fun n => UniformOnFun.gen 𝔖 (t n) (V n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι✝<VAR>g : ι✝ → α<VAR>inst✝² : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>ι : Type u_5<VAR>inst✝¹ : Preorder ι<VAR>inst✝ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>t : ι → Set α<VAR>V : ι → Set (β × β)<VAR>ht : ∀ (n : ι), t n ∈ 𝔖<VAR>hmono : Monotone t<VAR>hex : ∀ s ∈ 𝔖, ∃ n, s ⊆ t n<VAR>hb : (𝓤 β).HasAntitoneBasis V<VAR>this : Nonempty ι<GOAL>(𝓤 (α →ᵤ[𝔖] β)).HasAntitoneBasis fun n => UniformOnFun.gen 𝔖 (t n) (V n)