ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>x✝ : Unit<VAR>p n : ℕ<GOAL>n ∈ List.range (unpair p).1 → Nat.rec Option.none (fun n_1 n_ih => rec (some 0) (some n.succ) (some (unpair n).1) (some (unpair n).2) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range p)) ((unpair p).1, cf) n let y ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range p)) ((unpair p).1, cg) n some (Nat.pair x y)) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range p)) ((unpair p).1, cg) n Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range p)) ((unpair p).1, cf) x) (fun cf cg x x => Nat.rec (Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range p)) ((unpair p).1, cf) (unpair n).1) (fun n_2 n_ih => do let i ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range p)) (n_1, ofNat Code (unpair p).2) (Nat.pair (unpair n).1 n_2) Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range p)) ((unpair p).1, cg) (Nat.pair (unpair n).1 (Nat.pair n_2 i))) (unpair n).2) (fun cf x => do let x ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range p)) ((unpair p).1, cf) n Nat.rec (some (unpair n).2) (fun n_2 n_ih => Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range p)) (n_1, ofNat Code (unpair p).2) (Nat.pair (unpair n).1 ((unpair n).2 + 1))) x) (ofNat Code (unpair p).2)) (unpair p).1 = evaln (unpair p).1 (ofNat Code (unpair p).2) n
<VAR>x✝ : Unit<VAR>p n : ℕ<VAR>this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))<VAR>c : Code<VAR>k' : ℕ<VAR>nk : n ∈ List.range (k' + 1)<VAR>k : ℕ := k' + 1<GOAL>rec (some 0) (some n.succ) (some (unpair n).1) (some (unpair n).2) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cf) n let y ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cg) n some (Nat.pair x y)) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cg) n Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cf) x) (fun cf cg x x => Nat.rec (Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cf) (unpair n).1) (fun n_1 n_ih => do let i ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k', c) (Nat.pair (unpair n).1 n_1) Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i))) (unpair n).2) (fun cf x => do let x ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cf) n Nat.rec (some (unpair n).2) (fun n_1 n_ih => Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k', c) (Nat.pair (unpair n).1 ((unpair n).2 + 1))) x) c = evaln (k' + 1) c n
<VAR>x✝ : Unit<VAR>p n : ℕ<VAR>this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))<VAR>c : Code<VAR>k' : ℕ<VAR>k : ℕ := k' + 1<VAR>nk : n ≤ k'<GOAL>rec (some 0) (some n.succ) (some (unpair n).1) (some (unpair n).2) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cf) n let y ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cg) n some (Nat.pair x y)) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cg) n Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cf) x) (fun cf cg x x => Nat.rec (Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cf) (unpair n).1) (fun n_1 n_ih => do let i ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k', c) (Nat.pair (unpair n).1 n_1) Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i))) (unpair n).2) (fun cf x => do let x ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cf) n Nat.rec (some (unpair n).2) (fun n_1 n_ih => Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k', c) (Nat.pair (unpair n).1 ((unpair n).2 + 1))) x) c = evaln (k' + 1) c n
<VAR>x✝ : Unit<VAR>p n : ℕ<VAR>this : List.range p = List.range (Nat.pair (unpair p).1 (encode (ofNat Code (unpair p).2)))<VAR>c : Code<VAR>k' : ℕ<VAR>k : ℕ := k' + 1<VAR>nk : n ≤ k'<VAR>hg : ∀ {k' : ℕ} {c' : Code} {n : ℕ}, Nat.pair k' (encode c') < Nat.pair k (encode c) → Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair k (encode c)))) (k', c') n = evaln k' c' n<GOAL>rec (some 0) (some n.succ) (some (unpair n).1) (some (unpair n).2) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cf) n let y ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cg) n some (Nat.pair x y)) (fun cf cg x x => do let x ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cg) n Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cf) x) (fun cf cg x x => Nat.rec (Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cf) (unpair n).1) (fun n_1 n_ih => do let i ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k', c) (Nat.pair (unpair n).1 n_1) Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cg) (Nat.pair (unpair n).1 (Nat.pair n_1 i))) (unpair n).2) (fun cf x => do let x ← Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k' + 1, cf) n Nat.rec (some (unpair n).2) (fun n_1 n_ih => Nat.Partrec.Code.lup (List.map (fun n => List.map (evaln (unpair n).1 (ofNat Code (unpair n).2)) (List.range (unpair n).1)) (List.range (Nat.pair (k' + 1) (encode c)))) (k', c) (Nat.pair (unpair n).1 ((unpair n).2 + 1))) x) c = evaln (k' + 1) c n
<VAR>this : Primrec₂ fun x n => let a := ofNat (ℕ × Code) n; List.map (evaln a.1 a.2) (List.range a.1)<VAR>x✝ : (ℕ × Code) × ℕ<VAR>k : ℕ<VAR>c : Code<VAR>n : ℕ<GOAL>(((let a := ofNat (ℕ × Code) (encode ((k, c), n).1); List.map (evaln a.1 a.2) (List.range a.1)).get? ((k, c), n).2).bind fun b => (((k, c), n), b).2) = evaln ((k, c), n).1.1 ((k, c), n).1.2 ((k, c), n).2
<VAR>α : Type u_1<VAR>s : Set α<GOAL>range val = s
<VAR>α : Type u_1<VAR>s : Set α<GOAL>val '' univ = s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s✝ t : Set α<VAR>f✝ g f : α → E<VAR>s : Set α<VAR>h : μ s ≠ ⊤<GOAL>(μ s).toReal • ⨍ (x : α) in s, f x ∂μ = ∫ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s✝ t : Set α<VAR>f✝ g f : α → E<VAR>s : Set α<VAR>h : μ s ≠ ⊤<VAR>this : Fact (μ s < ⊤)<GOAL>(μ s).toReal • ⨍ (x : α) in s, f x ∂μ = ∫ (x : α) in s, f x ∂μ
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f : R⟦X⟧<VAR>n d : ℕ<GOAL>(trunc n f.derivativeFun).coeff d = (derivative (trunc (n + 1) f)).coeff d
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f : R⟦X⟧<VAR>n d : ℕ<GOAL>(if d < n then (coeff R d) f.derivativeFun else 0) = (derivative (trunc (n + 1) f)).coeff d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u_4}<GOAL>0 - a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u_4}<GOAL>0 - a ≤ 0
<VAR>x : ℝ≥0<VAR>y : ℝ<VAR>h✝¹ : x ≠ 0 ∨ 0 ≤ y<VAR>h✝ : 0 ≤ y<VAR>h : 0 = y<GOAL>ContinuousAt (fun z => z ^ 0) x
<VAR>C : Ordinal.{u_2} → Sort u_1<VAR>b : Ordinal.{u_2}<VAR>H0 : C 0<VAR>H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o<GOAL>b.CNFRec H0 H 0 = H0
<VAR>C : Ordinal.{u_2} → Sort u_1<VAR>b : Ordinal.{u_2}<VAR>H0 : C 0<VAR>H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o<GOAL>⋯.mpr H0 = H0
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsNoetherianRing R<VAR>h : FiniteType R A<GOAL>FinitePresentation R A
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsNoetherianRing R<VAR>h : FiniteType R A<VAR>n : ℕ<VAR>f : MvPolynomial (Fin n) R →ₐ[R] A<VAR>hf : Surjective ⇑f<GOAL>FinitePresentation R A
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsNoetherianRing R<VAR>h : FiniteType R A<VAR>n : ℕ<VAR>f : MvPolynomial (Fin n) R →ₐ[R] A<VAR>hf : Surjective ⇑f<VAR>hnoet : IsNoetherianRing (MvPolynomial (Fin n) R)<GOAL>(RingHom.ker f.toRingHom).FG
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsNoetherianRing R<VAR>h : FiniteType R A<VAR>n : ℕ<VAR>f : MvPolynomial (Fin n) R →ₐ[R] A<VAR>hf : Surjective ⇑f<VAR>hnoet : IsNoetherian (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R)<GOAL>(RingHom.ker f.toRingHom).FG
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsNoetherianRing R<VAR>h : FiniteType R A<VAR>n : ℕ<VAR>f : MvPolynomial (Fin n) R →ₐ[R] A<VAR>hf : Surjective ⇑f<VAR>hnoet : IsNoetherian (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R)<VAR>this : Module (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R) := Semiring.toModule<GOAL>(RingHom.ker f.toRingHom).FG
<VAR>R : Type w₁<VAR>A : Type w₂<VAR>B : Type w₃<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsNoetherianRing R<VAR>h : FiniteType R A<VAR>n : ℕ<VAR>f : MvPolynomial (Fin n) R →ₐ[R] A<VAR>hf : Surjective ⇑f<VAR>hnoet : IsNoetherian (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R)<VAR>this✝ : Module (MvPolynomial (Fin n) R) (MvPolynomial (Fin n) R) := Semiring.toModule<VAR>this : Submodule.FG (RingHom.ker f.toRingHom)<GOAL>(RingHom.ker f.toRingHom).FG
<VAR>α : Type u<VAR>inst✝¹ : Monoid α<VAR>a b : α<VAR>inst✝ : Invertible b<GOAL>a * b * ⅟b = a
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<GOAL>zero + zero = 0 ↔ zero = -zero
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₂ y₂ : F<VAR>h✝ : W.Nonsingular x₂ y₂<GOAL>zero + some h✝ = 0 ↔ zero = -some h✝
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ y₁ : F<VAR>h✝ : W.Nonsingular x₁ y₁<GOAL>some h✝ + zero = 0 ↔ some h✝ = -zero
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>W✝ : Affine R<VAR>f : R →+* S<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ y₁ : F<VAR>h✝¹ : W.Nonsingular x₁ y₁<VAR>x₂ y₂ : F<VAR>h✝ : W.Nonsingular x₂ y₂<GOAL>some h✝¹ + some h✝ = 0 ↔ some h✝¹ = -some h✝
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : Category.{u_6, u_1} C<VAR>inst✝⁵ : Category.{u_5, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>G : Type u_4<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : HasShift C G<VAR>inst✝ : F.ShiftSequence M<VAR>a : M<VAR>X : C<GOAL>(F.shiftIso 0 a a ⋯).hom.app X = (F.shift a).map ((shiftFunctorZero C M).hom.app X)
<VAR>k✝ : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹³ : Ring k✝<VAR>inst✝¹² : AddCommGroup V1<VAR>inst✝¹¹ : Module k✝ V1<VAR>inst✝¹⁰ : AffineSpace V1 P1<VAR>inst✝⁹ : AddCommGroup V2<VAR>inst✝⁸ : Module k✝ V2<VAR>inst✝⁷ : AffineSpace V2 P2<VAR>inst✝⁶ : AddCommGroup V3<VAR>inst✝⁵ : Module k✝ V3<VAR>inst✝⁴ : AffineSpace V3 P3<VAR>inst✝³ : AddCommGroup V4<VAR>inst✝² : Module k✝ V4<VAR>inst✝¹ : AffineSpace V4 P4<VAR>k : Type u_10<VAR>inst✝ : LinearOrderedField k<VAR>f : k →ᵃ[k] k<VAR>a b : k<GOAL>⇑f '' Set.uIcc a b = Set.uIcc (f a) (f b)
<VAR>k✝ : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹³ : Ring k✝<VAR>inst✝¹² : AddCommGroup V1<VAR>inst✝¹¹ : Module k✝ V1<VAR>inst✝¹⁰ : AffineSpace V1 P1<VAR>inst✝⁹ : AddCommGroup V2<VAR>inst✝⁸ : Module k✝ V2<VAR>inst✝⁷ : AffineSpace V2 P2<VAR>inst✝⁶ : AddCommGroup V3<VAR>inst✝⁵ : Module k✝ V3<VAR>inst✝⁴ : AffineSpace V3 P3<VAR>inst✝³ : AddCommGroup V4<VAR>inst✝² : Module k✝ V4<VAR>inst✝¹ : AffineSpace V4 P4<VAR>k : Type u_10<VAR>inst✝ : LinearOrderedField k<VAR>f : k →ᵃ[k] k<VAR>a b : k<VAR>this : ⇑f = (fun x => x + f 0) ∘ fun x => x * (f 1 - f 0)<GOAL>⇑f '' Set.uIcc a b = Set.uIcc (f a) (f b)
<VAR>k✝ : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹³ : Ring k✝<VAR>inst✝¹² : AddCommGroup V1<VAR>inst✝¹¹ : Module k✝ V1<VAR>inst✝¹⁰ : AffineSpace V1 P1<VAR>inst✝⁹ : AddCommGroup V2<VAR>inst✝⁸ : Module k✝ V2<VAR>inst✝⁷ : AffineSpace V2 P2<VAR>inst✝⁶ : AddCommGroup V3<VAR>inst✝⁵ : Module k✝ V3<VAR>inst✝⁴ : AffineSpace V3 P3<VAR>inst✝³ : AddCommGroup V4<VAR>inst✝² : Module k✝ V4<VAR>inst✝¹ : AffineSpace V4 P4<VAR>k : Type u_10<VAR>inst✝ : LinearOrderedField k<VAR>f : k →ᵃ[k] k<VAR>a b : k<VAR>this : ⇑f = (fun x => x + f 0) ∘ fun x => x * (f 1 - f 0)<GOAL>(fun x => x + f 0) '' ((fun x => x * (f 1 - f 0)) '' Set.uIcc a b) = Set.uIcc (((fun x => x + f 0) ∘ fun x => x * (f 1 - f 0)) a) (((fun x => x + f 0) ∘ fun x => x * (f 1 - f 0)) b)
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>l : List α<GOAL>l.Nodup ↔ ∀ (i j : ℕ), i < j → j < l.length → l[i]? ≠ l[j]?
<VAR>α : Type u<VAR>β : Type v<VAR>l✝ l₁ l₂ : List α<VAR>r : α → α → Prop<VAR>a b : α<VAR>l : List α<GOAL>(∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → l[i] ≠ l[j]) ↔ ∀ (i j : ℕ), i < j → j < l.length → l[i]? ≠ l[j]?
<VAR>a b c : Ordinal.{u_1}<VAR>h : b ≤ c<GOAL>a ^ c = a ^ b * a ^ (c - b)
<VAR>x : ℝ<VAR>h : sin x = 0<VAR>h₃ : x - ↑⌊x / π⌋ * π > 0<GOAL>0 = sin (x - ↑⌊x / π⌋ * π)
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<GOAL>∑ i ∈ p.support, (monomial i) (p.coeff i) = ∑ i ∈ p.support, C (p.coeff i) * X ^ i
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>A B : ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : HasSum (fun i => f i ^ p) (A ^ p)<VAR>hg : HasSum (fun i => g i ^ q) (B ^ q)<GOAL>∃ C ≤ A * B, HasSum (fun i => f i * g i) C
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>A B : ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : HasSum (fun i => f i ^ p) (A ^ p)<VAR>hg : HasSum (fun i => g i ^ q) (B ^ q)<VAR>H₁ : Summable fun i => f i * g i<VAR>H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)<GOAL>∃ C ≤ A * B, HasSum (fun i => f i * g i) C
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>A B : ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : HasSum (fun i => f i ^ p) (A ^ p)<VAR>hg : HasSum (fun i => g i ^ q) (B ^ q)<VAR>H₁ : Summable fun i => f i * g i<VAR>H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)<VAR>hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)<GOAL>∃ C ≤ A * B, HasSum (fun i => f i * g i) C
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>A B : ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : HasSum (fun i => f i ^ p) (A ^ p)<VAR>hg : HasSum (fun i => g i ^ q) (B ^ q)<VAR>H₁ : Summable fun i => f i * g i<VAR>H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)<VAR>hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)<VAR>hB : B = (∑' (i : ι), g i ^ q) ^ (1 / q)<GOAL>∃ C ≤ A * B, HasSum (fun i => f i * g i) C
<VAR>x✝ y✝ z✝ : PGame<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u_1<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>zl zr : Type u_1<VAR>zL : zl → PGame<VAR>zR : zr → PGame<VAR>x : PGame := mk xl xr xL xR<VAR>y : PGame := mk yl yr yL yR<VAR>z : PGame := mk zl zr zL zR<GOAL>⟦mk xl xr xL xR * mk yl yr yL yR * mk zl zr zL zR⟧ = ⟦mk xl xr xL xR * (mk yl yr yL yR * mk zl zr zL zR)⟧
<VAR>x✝ y✝ z✝ : PGame<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u_1<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>zl zr : Type u_1<VAR>zL : zl → PGame<VAR>zR : zr → PGame<VAR>x : PGame := mk xl xr xL xR<VAR>y : PGame := mk yl yr yL yR<VAR>z : PGame := mk zl zr zL zR<GOAL>(mk xl xr xL xR * mk yl yr yL yR * mk zl zr zL zR).LeftMoves ≃ (mk xl xr xL xR * (mk yl yr yL yR * mk zl zr zL zR)).LeftMoves
<VAR>x✝ y✝ z✝ : PGame<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u_1<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>zl zr : Type u_1<VAR>zL : zl → PGame<VAR>zR : zr → PGame<VAR>x : PGame := mk xl xr xL xR<VAR>y : PGame := mk yl yr yL yR<VAR>z : PGame := mk zl zr zL zR<GOAL>(mk xl xr xL xR * mk yl yr yL yR * mk zl zr zL zR).RightMoves ≃ (mk xl xr xL xR * (mk yl yr yL yR * mk zl zr zL zR)).RightMoves
<VAR>x✝ y✝ z✝ : PGame<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u_1<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>zl zr : Type u_1<VAR>zL : zl → PGame<VAR>zR : zr → PGame<VAR>x : PGame := mk xl xr xL xR<VAR>y : PGame := mk yl yr yL yR<VAR>z : PGame := mk zl zr zL zR<GOAL>∀ (i : (mk xl xr xL xR * mk yl yr yL yR * mk zl zr zL zR).LeftMoves), ⟦(mk xl xr xL xR * mk yl yr yL yR * mk zl zr zL zR).moveLeft i⟧ = ⟦(mk xl xr xL xR * (mk yl yr yL yR * mk zl zr zL zR)).moveLeft (?refine_1 i)⟧
<VAR>x✝ y✝ z✝ : PGame<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>yl yr : Type u_1<VAR>yL : yl → PGame<VAR>yR : yr → PGame<VAR>zl zr : Type u_1<VAR>zL : zl → PGame<VAR>zR : zr → PGame<VAR>x : PGame := mk xl xr xL xR<VAR>y : PGame := mk yl yr yL yR<VAR>z : PGame := mk zl zr zL zR<GOAL>∀ (j : (mk xl xr xL xR * mk yl yr yL yR * mk zl zr zL zR).RightMoves), ⟦(mk xl xr xL xR * mk yl yr yL yR * mk zl zr zL zR).moveRight j⟧ = ⟦(mk xl xr xL xR * (mk yl yr yL yR * mk zl zr zL zR)).moveRight (?refine_2 j)⟧
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝² : PartialOrder Γ<VAR>inst✝¹ : Zero V<VAR>inst✝ : SMul R V<VAR>x y : HahnModule Γ R V<GOAL>((of R).symm x).coeff = ((of R).symm y).coeff ↔ x = y
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>s t : Set A<GOAL>adjoin R (s ∪ t) = Subalgebra.restrictScalars R (adjoin (↥(adjoin R s)) t)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝ : LinearOrderedRing R<VAR>a b : R<VAR>n : ℕ<GOAL>a ^ n = -1 ↔ a = -1 ∧ Odd n
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>q n m : ℕ<VAR>hnq : n < q<VAR>hnm : c.Rel m n<GOAL>0 ≫ eqToHom ⋯ = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>g : α → ℝ≥0∞<GOAL>μ.withDensity (f + g) = μ.withDensity f + μ.withDensity g
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>g : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.withDensity (f + g)) s = (μ.withDensity f + μ.withDensity g) s
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>g : α → ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>∫⁻ (a : α) in s, (f + g) a ∂μ = ∫⁻ (a : α) in s, f a + g a ∂μ
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝⁴ : MeasurableSpace β✝<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>β : Type u_5<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : T1Space β<VAR>inst✝¹ : SecondCountableTopology β<VAR>inst✝ : Nonempty β<VAR>f : α → β<VAR>h : ∀ (b : β), ∃ᵐ (x : α) ∂μ, f x ≠ b<VAR>m : OuterMeasure β := (OuterMeasure.map f) μ.toOuterMeasure<GOAL>∃ a b, a ≠ b ∧ (∀ s ∈ 𝓝 a, 0 < μ (f ⁻¹' s)) ∧ ∀ t ∈ 𝓝 b, 0 < μ (f ⁻¹' t)