ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>a : ℕ<VAR>IH : ∀ m < a, ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0}, b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)<VAR>b : ℕ<VAR>flip : Bool<VAR>ha0 : a > 0<VAR>hb2 : b % 2 = 1<VAR>hb1 : b > 1<VAR>ha4 : ¬a % 4 = 0<VAR>ha2 : ¬a % 2 = 0<VAR>ha1 : ¬a = 1<VAR>hba : ¬b % a = 0<GOAL>fastJacobiSymAux (b % a) a (xor (decide (a % 4 = 3 ∧ b % 4 = 3)) flip) ⋯ = if flip = true then -J(↑a | b) else J(↑a | b)
<VAR>a : ℕ<VAR>IH : ∀ m < a, ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0}, b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)<VAR>b : ℕ<VAR>flip : Bool<VAR>ha0 : a > 0<VAR>hb2 : b % 2 = 1<VAR>hb1 : b > 1<VAR>ha4 : ¬a % 4 = 0<VAR>ha2 : ¬a % 2 = 0<VAR>ha1 : ¬a = 1<VAR>hba : ¬b % a = 0<GOAL>(if xor (decide (a % 4 = 3 ∧ b % 4 = 3)) flip = true then -J(↑(b % a) | a) else J(↑(b % a) | a)) = if flip = true then -J(↑a | b) else J(↑a | b)
<VAR>a : ℕ<VAR>IH : ∀ m < a, ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0}, b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)<VAR>b : ℕ<VAR>flip : Bool<VAR>ha0 : a > 0<VAR>hb2 : b % 2 = 1<VAR>hb1 : b > 1<VAR>ha4 : ¬a % 4 = 0<VAR>ha2 : ¬a % 2 = 0<VAR>ha1 : ¬a = 1<VAR>hba : ¬b % a = 0<GOAL>(if xor (decide (a % 4 = 3 ∧ b % 4 = 3)) flip = true then -J(↑b | a) else J(↑b | a)) = if flip = true then -J(↑a | b) else J(↑a | b)
<VAR>a : ℕ<VAR>IH : ∀ m < a, ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0}, b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)<VAR>b : ℕ<VAR>flip : Bool<VAR>ha0 : a > 0<VAR>hb2 : b % 2 = 1<VAR>hb1 : b > 1<VAR>ha4 : ¬a % 4 = 0<VAR>ha2 : ¬a % 2 = 0<VAR>ha1 : ¬a = 1<VAR>hba : ¬b % a = 0<GOAL>(if xor (decide (a % 4 = 3 ∧ b % 4 = 3)) flip = true then -J(↑b | a) else J(↑b | a)) = if flip = true then -if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a) else if a % 4 = 3 ∧ b % 4 = 3 then -J(↑b | a) else J(↑b | a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p✝ : PMF α<VAR>f✝ : (a : α) → a ∈ p✝.support → PMF β<VAR>p : PMF α<VAR>f : α → PMF β<VAR>b : β<GOAL>(p.bindOnSupport fun a x => f a) b = (p.bind f) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p✝ : PMF α<VAR>f✝ : (a : α) → a ∈ p✝.support → PMF β<VAR>p : PMF α<VAR>f : α → PMF β<VAR>b : β<VAR>this : ∀ (a : α), (if p a = 0 then 0 else p a * (f a) b) = p a * (f a) b<GOAL>(p.bindOnSupport fun a x => f a) b = (p.bind f) b
<VAR>Γ : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : AddGroup R<VAR>x y : HahnSeries Γ R<VAR>x✝ : Γ<GOAL>(x - y).coeff x✝ = (x.coeff - y.coeff) x✝
<VAR>K✝ : Type u_1<VAR>inst✝⁶ : Field K✝<VAR>A✝ : Type u_2<VAR>inst✝⁵ : NormedField A✝<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : NormedField A<VAR>inst✝¹ : IsAlgClosed A<VAR>inst✝ : NormedAlgebra ℚ A<VAR>x : K<VAR>hxi : IsIntegral ℤ x<VAR>hx : ∀ (φ : K →+* A), ‖φ x‖ = 1<VAR>a b : ℕ<VAR>habne : a ≠ b<VAR>h : x ^ a = x ^ b<VAR>hlt : b < a<GOAL>∃ n, ∃ (_ : 0 < n), x ^ n = 1
<VAR>K✝ : Type u_1<VAR>inst✝⁶ : Field K✝<VAR>A✝ : Type u_2<VAR>inst✝⁵ : NormedField A✝<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : NormedField A<VAR>inst✝¹ : IsAlgClosed A<VAR>inst✝ : NormedAlgebra ℚ A<VAR>x : K<VAR>hxi : IsIntegral ℤ x<VAR>hx : ∀ (φ : K →+* A), ‖φ x‖ = 1<VAR>a b : ℕ<VAR>habne : a ≠ b<VAR>h : x ^ a = x ^ b<VAR>hlt : b < a<GOAL>x ^ (a - b) = 1
<VAR>K✝ : Type u_1<VAR>inst✝⁶ : Field K✝<VAR>A✝ : Type u_2<VAR>inst✝⁵ : NormedField A✝<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : NormedField A<VAR>inst✝¹ : IsAlgClosed A<VAR>inst✝ : NormedAlgebra ℚ A<VAR>x : K<VAR>hxi : IsIntegral ℤ x<VAR>hx : ∀ (φ : K →+* A), ‖φ x‖ = 1<VAR>a b : ℕ<VAR>habne : a ≠ b<VAR>h : x ^ (a - b) = 1 ∨ x ^ b = 0<VAR>hlt : b < a<GOAL>x ^ (a - b) = 1
<VAR>K✝ : Type u_1<VAR>inst✝⁶ : Field K✝<VAR>A✝ : Type u_2<VAR>inst✝⁵ : NormedField A✝<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : NormedField A<VAR>inst✝¹ : IsAlgClosed A<VAR>inst✝ : NormedAlgebra ℚ A<VAR>x : K<VAR>hxi : IsIntegral ℤ x<VAR>hx : ∀ (φ : K →+* A), ‖φ x‖ = 1<VAR>a b : ℕ<VAR>habne : a ≠ b<VAR>h : x ^ (a - b) = 1 ∨ x ^ b = 0<VAR>hlt : b < a<VAR>hp : x ^ b = 0<GOAL>False
<VAR>K✝ : Type u_1<VAR>inst✝⁶ : Field K✝<VAR>A✝ : Type u_2<VAR>inst✝⁵ : NormedField A✝<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : NormedField A<VAR>inst✝¹ : IsAlgClosed A<VAR>inst✝ : NormedAlgebra ℚ A<VAR>x : K<VAR>hxi : IsIntegral ℤ x<VAR>a b : ℕ<VAR>habne : a ≠ b<VAR>h : x ^ (a - b) = 1 ∨ x ^ b = 0<VAR>hlt : b < a<VAR>hp : x ^ b = 0<VAR>hx : ‖IsAlgClosed.lift.toRingHom x‖ = 1<GOAL>False
<VAR>K✝ : Type u_1<VAR>inst✝⁶ : Field K✝<VAR>A✝ : Type u_2<VAR>inst✝⁵ : NormedField A✝<VAR>K : Type u_1<VAR>inst✝⁴ : Field K<VAR>inst✝³ : NumberField K<VAR>A : Type u_2<VAR>inst✝² : NormedField A<VAR>inst✝¹ : IsAlgClosed A<VAR>inst✝ : NormedAlgebra ℚ A<VAR>x : K<VAR>hxi : IsIntegral ℤ x<VAR>a b : ℕ<VAR>habne : a ≠ b<VAR>h : x ^ (a - b) = 1 ∨ x ^ b = 0<VAR>hlt : b < a<VAR>hp : x ^ b = 0<VAR>hx : 0 = 1<GOAL>False
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : TopologicalSpace α'<VAR>inst✝⁵ : One β<VAR>inst✝⁴ : One γ<VAR>inst✝³ : One δ<VAR>g✝ : β → γ<VAR>f✝ : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>inst✝² : T2Space α'<VAR>hf : HasCompactMulSupport f✝<VAR>g : α → α'<VAR>cont : Continuous g<VAR>f : α → γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : One γ<VAR>h : HasCompactMulSupport f<VAR>N : Set γ<VAR>hN : N ∈ 𝓝 1<GOAL>N ∈ map f (cocompact α)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : TopologicalSpace α'<VAR>inst✝⁵ : One β<VAR>inst✝⁴ : One γ<VAR>inst✝³ : One δ<VAR>g✝ : β → γ<VAR>f✝ : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>inst✝² : T2Space α'<VAR>hf : HasCompactMulSupport f✝<VAR>g : α → α'<VAR>cont : Continuous g<VAR>f : α → γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : One γ<VAR>h : HasCompactMulSupport f<VAR>N : Set γ<VAR>hN : N ∈ 𝓝 1<GOAL>∃ t, IsCompact t ∧ (f ⁻¹' N)ᶜ ⊆ t
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : TopologicalSpace α'<VAR>inst✝⁵ : One β<VAR>inst✝⁴ : One γ<VAR>inst✝³ : One δ<VAR>g✝ : β → γ<VAR>f✝ : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>inst✝² : T2Space α'<VAR>hf : HasCompactMulSupport f✝<VAR>g : α → α'<VAR>cont : Continuous g<VAR>f : α → γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : One γ<VAR>h : HasCompactMulSupport f<VAR>N : Set γ<VAR>hN : N ∈ 𝓝 1<GOAL>(f ⁻¹' N)ᶜ ⊆ mulTSupport f
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : TopologicalSpace α'<VAR>inst✝⁵ : One β<VAR>inst✝⁴ : One γ<VAR>inst✝³ : One δ<VAR>g✝ : β → γ<VAR>f✝ : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>inst✝² : T2Space α'<VAR>hf : HasCompactMulSupport f✝<VAR>g : α → α'<VAR>cont : Continuous g<VAR>f : α → γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : One γ<VAR>h : HasCompactMulSupport f<VAR>N : Set γ<VAR>hN : N ∈ 𝓝 1<GOAL>(mulTSupport f)ᶜ ⊆ f ⁻¹' N
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : TopologicalSpace α'<VAR>inst✝⁵ : One β<VAR>inst✝⁴ : One γ<VAR>inst✝³ : One δ<VAR>g✝ : β → γ<VAR>f✝ : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>inst✝² : T2Space α'<VAR>hf : HasCompactMulSupport f✝<VAR>g : α → α'<VAR>cont : Continuous g<VAR>f : α → γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : One γ<VAR>h : HasCompactMulSupport f<VAR>N : Set γ<VAR>hN : N ∈ 𝓝 1<VAR>v : α<VAR>hv : v ∈ (mulTSupport f)ᶜ<GOAL>v ∈ f ⁻¹' N
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : TopologicalSpace α'<VAR>inst✝⁵ : One β<VAR>inst✝⁴ : One γ<VAR>inst✝³ : One δ<VAR>g✝ : β → γ<VAR>f✝ : α → β<VAR>f₂ : α → γ<VAR>m : β → γ → δ<VAR>x : α<VAR>inst✝² : T2Space α'<VAR>hf : HasCompactMulSupport f✝<VAR>g : α → α'<VAR>cont : Continuous g<VAR>f : α → γ<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : One γ<VAR>h : HasCompactMulSupport f<VAR>N : Set γ<VAR>hN : N ∈ 𝓝 1<VAR>v : α<VAR>hv : v ∈ (mulTSupport f)ᶜ<GOAL>1 ∈ N
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : Preorder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>s : Set Ω<VAR>i : ι<GOAL>MeasurableSet (s ∩ {ω | τ ω = i}) ↔ MeasurableSet (s ∩ {ω | τ ω = i})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : Preorder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>s : Set Ω<VAR>i : ι<VAR>this : ∀ (j : ι), {ω | τ ω = i} ∩ {ω | τ ω ≤ j} = {ω | τ ω = i} ∩ {_ω | i ≤ j}<GOAL>MeasurableSet (s ∩ {ω | τ ω = i}) ↔ MeasurableSet (s ∩ {ω | τ ω = i})
<VAR>m : ℕ∞<GOAL>1 < ↑m ↔ 1 < m
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a : α<VAR>b : β a<VAR>s✝ : Finmap β<VAR>s : AList β<GOAL>lookup a (insert a b ⟦s⟧) = some b
<VAR>α β : Type<VAR>n : ℕ<VAR>f : Vector3 ℕ n → ℕ<VAR>df : DiophFn f<VAR>g : Vector3 ((α → ℕ) → ℕ) n<VAR>dg : VectorAllP DiophFn g<GOAL>VectorAllP DiophFn ((fun v => v none) :: fun i v => g i (v ∘ some))
<VAR>α β : Type<VAR>n : ℕ<VAR>f : Vector3 ℕ n → ℕ<VAR>df : DiophFn f<VAR>g : Vector3 ((α → ℕ) → ℕ) n<VAR>dg : VectorAllP DiophFn g<GOAL>(DiophFn fun v => v none) ∧ VectorAllP DiophFn fun i v => g i (v ∘ some)
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>{x} / closedBall y δ = closedBall (x / y) δ
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>x y z : α<VAR>h : [x, y, z].Nodup<GOAL>(swap x y * swap y z).support = {x, y, z}
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>x y z : α<VAR>h : ¬(x = y ∨ x = z ∨ False) ∧ ¬(y = z ∨ False)<GOAL>(swap x y * swap y z).support = {x, y, z}
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>x y z : α<VAR>h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False<GOAL>(swap x y * swap y z).support = {x, y, z}
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>x y z : α<VAR>h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False<GOAL>(swap x y * swap y z).support ≤ {x, y, z}
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f g : Perm α<VAR>x y z : α<VAR>h : (x ≠ y ∧ x ≠ z ∧ ¬False) ∧ y ≠ z ∧ ¬False<GOAL>{x, y, z} ≤ (swap x y * swap y z).support
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>E : EllipticCurve R<VAR>inst✝ : Invertible 2<GOAL>(ofJ1728 R).j = 1728
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>E : EllipticCurve R<VAR>inst✝ : Invertible 2<GOAL>-(1728 * 2 ^ 6) = (-48) ^ 3
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x✝ y : α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderTopology α<VAR>x : α<GOAL>Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x✝ y : α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderTopology α<VAR>x : α<VAR>h' : 𝓝[<] x = ⊥<GOAL>Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x✝ y : α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderTopology α<VAR>x : α<VAR>h' : 𝓝[<] x ≠ ⊥<GOAL>Tendsto f (𝓝[<] x) (𝓝 (leftLim f x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : LinearOrder α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>f : α → β<VAR>hf : Monotone f<VAR>x✝ y : α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderTopology α<VAR>x : α<VAR>h' : 𝓝[<] x ≠ ⊥<GOAL>Tendsto f (𝓝[<] x) (𝓝 (sSup (f '' Iio x)))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f g : Filter β<VAR>p q : β → Prop<VAR>u v : β → α<VAR>h : ∀ (x : β), p x → q x<VAR>a : α<VAR>ha : a ∈ {a | ∀ᶠ (x : β) in f, q x → u x ≤ a}<GOAL>∀ (x : β), (q x → u x ≤ a) → p x → u x ≤ a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<GOAL>a ⊓ sSup s ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<GOAL>∀ (c : α), CompleteLattice.IsCompactElement c → c ≤ a ⊓ sSup s → c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<VAR>c : α<VAR>hc : CompleteLattice.IsCompactElement c<VAR>hcinf : c ≤ a ⊓ sSup s<GOAL>c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<VAR>c : α<VAR>hc : CompleteLattice.IsCompactElement c<VAR>hcinf : c ≤ a ∧ c ≤ sSup s<GOAL>c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<VAR>c : α<VAR>hc : CompleteLattice.IsCompactElement c<VAR>hcinf : c ≤ a ∧ c ≤ sSup s<VAR>t : Finset α<VAR>ht1 : ↑t ⊆ s<VAR>ht2 : c ≤ t.sup id<GOAL>c ≤ ⨆ t, ⨆ (_ : ↑t ⊆ s), a ⊓ t.sup id
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>inst✝² : CompleteLattice α<VAR>f : ι → α<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsCompactlyGenerated α<VAR>a b : α<VAR>s : Set α<VAR>c : α<VAR>hc : CompleteLattice.IsCompactElement c<VAR>hcinf : c ≤ a ∧ c ≤ sSup s<VAR>t : Finset α<VAR>ht1 : ↑t ⊆ s<VAR>ht2 : c ≤ t.sup id<GOAL>a ⊓ t.sup id ≤ a ⊓ t.sup id
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α (n + 1)<VAR>h : T.SemanticallyEquivalent φ ψ<GOAL>T.SemanticallyEquivalent (∃'φ) (∃'ψ)
<VAR>L : Language<VAR>T : L.Theory<VAR>α : Type w<VAR>n : ℕ<VAR>φ ψ : L.BoundedFormula α (n + 1)<VAR>h : T.SemanticallyEquivalent φ ψ<GOAL>∀ (M : T.ModelType) (v : α → ↑M) (xs : Fin n → ↑M), (∃ a, φ.Realize v (Fin.snoc xs a)) ↔ ∃ a, ψ.Realize v (Fin.snoc xs a)
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Fintype β<VAR>r : α → β → Prop<VAR>inst✝ : (a : α) → DecidablePred (r a)<VAR>this : DecidableEq β<VAR>r' : α → Finset β := fun a => filter (fun b => r a b) univ<VAR>h : ∀ (A : Finset α), filter (fun b => ∃ a ∈ A, r a b) univ = A.biUnion r'<VAR>h' : ∀ (f : α → β) (x : α), r x (f x) ↔ f x ∈ r' x<GOAL>(∀ (A : Finset α), A.card ≤ (A.biUnion r').card) ↔ ∃ f, Function.Injective f ∧ ∀ (x : α), f x ∈ r' x
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<GOAL>IsTotallyDisconnected Set.univ
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<GOAL>Pairwise fun x y => ∃ U, IsClopen U ∧ x ∈ U ∧ y ∉ U
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>σ τ : L ≃ₐ[K] L<VAR>h_diff : σ ≠ τ<GOAL>∃ U, IsClopen U ∧ σ ∈ U ∧ τ ∉ U
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>σ τ : L ≃ₐ[K] L<VAR>h_diff : σ ≠ τ<VAR>hστ : σ⁻¹ * τ ≠ 1<GOAL>∃ U, IsClopen U ∧ σ ∈ U ∧ τ ∉ U
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>σ τ : L ≃ₐ[K] L<VAR>h_diff : σ ≠ τ<VAR>hστ : σ⁻¹ * τ ≠ 1<VAR>x : L<VAR>hx : (σ⁻¹ * τ) x ≠ x<GOAL>∃ U, IsClopen U ∧ σ ∈ U ∧ τ ∉ U
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>σ τ : L ≃ₐ[K] L<VAR>h_diff : σ ≠ τ<VAR>hστ : σ⁻¹ * τ ≠ 1<VAR>x : L<VAR>hx : (σ⁻¹ * τ) x ≠ x<VAR>E : IntermediateField K L := K⟮x⟯<GOAL>∃ U, IsClopen U ∧ σ ∈ U ∧ τ ∉ U
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>σ τ : L ≃ₐ[K] L<VAR>h_diff : σ ≠ τ<VAR>hστ : σ⁻¹ * τ ≠ 1<VAR>x : L<VAR>hx : (σ⁻¹ * τ) x ≠ x<VAR>E : IntermediateField K L := K⟮x⟯<VAR>this : FiniteDimensional K ↥K⟮x⟯<GOAL>∃ U, IsClopen U ∧ σ ∈ U ∧ τ ∉ U
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>σ τ : L ≃ₐ[K] L<VAR>h_diff : σ ≠ τ<VAR>hστ : σ⁻¹ * τ ≠ 1<VAR>x : L<VAR>hx : (σ⁻¹ * τ) x ≠ x<VAR>E : IntermediateField K L := K⟮x⟯<VAR>this : FiniteDimensional K ↥K⟮x⟯<GOAL>τ ∉ σ • ↑E.fixingSubgroup
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : Algebra.IsIntegral K L<VAR>σ τ : L ≃ₐ[K] L<VAR>h_diff : σ ≠ τ<VAR>hστ : σ⁻¹ * τ ≠ 1<VAR>x : L<VAR>hx : (σ⁻¹ * τ) x ≠ x<VAR>E : IntermediateField K L := K⟮x⟯<VAR>this : FiniteDimensional K ↥K⟮x⟯<GOAL>∃ x, ∃ (_ : x ∈ E), ¬(σ⁻¹ * τ) x = x
<VAR>x✝ y✝ z✝ : ℝ<VAR>n : ℕ<VAR>x : ℝ<VAR>hx : 0 ≤ x<VAR>y z : ℝ<GOAL>x ^ (y * z) = (x ^ y) ^ z
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>a b : GradedMonoid fun n => ⨂[R] (x : Fin n), M<VAR>h : a.fst = b.fst<VAR>h2 : (cast R M h) a.snd = b.snd<GOAL>a = b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>a b : GradedMonoid fun n => ⨂[R] (x : Fin n), M<VAR>h : a.fst = b.fst<VAR>h2 : (cast R M h) a.snd = b.snd<GOAL>(reindex R (fun x => M) (Equiv.cast ⋯)) a.snd = b.snd
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>a b : GradedMonoid fun n => ⨂[R] (x : Fin n), M<VAR>h : a.fst = b.fst<VAR>h2 : (reindex R (fun x => M) (finCongr h)) a.snd = b.snd<GOAL>(reindex R (fun x => M) (Equiv.cast ⋯)) a.snd = b.snd
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>cst : ℝ → ℝ := fun x => 1<GOAL>∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a}
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>cst : ℝ → ℝ := fun x => 1<VAR>cst_intble : ∀ t > 0, IntervalIntegrable cst volume 0 t<GOAL>∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a}
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>cst : ℝ → ℝ := fun x => 1<VAR>cst_intble : ∀ t > 0, IntervalIntegrable cst volume 0 t<VAR>key : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, cst t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (cst t)<GOAL>∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a}
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>cst : ℝ → ℝ := fun x => 1<VAR>cst_intble : ∀ t > 0, IntervalIntegrable cst volume 0 t<VAR>key : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, 1) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a}<GOAL>∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a}
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>g : ℝ → ℝ<VAR>s : Set α<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>cst : ℝ → ℝ := fun x => 1<VAR>cst_intble : ∀ t > 0, IntervalIntegrable cst volume 0 t<VAR>key : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, 1) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a}<VAR>ω : α<GOAL>ENNReal.ofReal (f ω) = ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, 1)
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>R : Type u_5<VAR>M : Type u_6<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>r s✝ : R<VAR>x y : M<VAR>s : Finset α<VAR>t : Finset β<VAR>f : α → R<VAR>g : β → M<GOAL>(∑ i ∈ s, f i) • ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i • g j
<VAR>G : PGame<VAR>inst✝ : G.Impartial<GOAL>G ≈ nim G.grundyValue
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>o : Ordinal.{u_1}<VAR>h : G ≈ nim o<GOAL>G.grundyValue = o
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>o : Ordinal.{u_1}<VAR>h : G ≈ nim o<GOAL>nim G.grundyValue ≈ nim o
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>s : Set X<VAR>t : Set Y<GOAL>frontier (s ×ˢ t) = closure s ×ˢ frontier t ∪ frontier s ×ˢ closure t
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>p q : α → Prop<VAR>a : Subtype p<VAR>b : α<GOAL>(∃ h, ⟨b, h⟩ = a) ↔ b = ↑a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : LeftCancelMonoid M<VAR>L L' : List M<VAR>h : L.length = L'.length<VAR>h' : ∀ i ≤ L.length, (take i L).prod = (take i L').prod<GOAL>L = L'
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : LeftCancelMonoid M<VAR>L L' : List M<VAR>h : L.length = L'.length<VAR>h' : ∀ i ≤ L.length, (take i L).prod = (take i L').prod<VAR>i : ℕ<VAR>h₁ : i < L.length<VAR>h₂ : i < L'.length<GOAL>L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : LeftCancelMonoid M<VAR>L L' : List M<VAR>h : L.length = L'.length<VAR>h' : ∀ i ≤ L.length, (take i L).prod = (take i L').prod<VAR>i : ℕ<VAR>h₁ : i < L.length<VAR>h₂ : i < L'.length<VAR>this : (take (i + 1) L).prod = (take (i + 1) L').prod<GOAL>L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : LeftCancelMonoid M<VAR>L L' : List M<VAR>h : L.length = L'.length<VAR>h' : ∀ i ≤ L.length, (take i L).prod = (take i L').prod<VAR>i : ℕ<VAR>h₁ : i < L.length<VAR>h₂ : i < L'.length<VAR>this : (take i L').prod * L[i] = (take i L').prod * L'[i]<GOAL>L.get ⟨i, h₁⟩ = L'.get ⟨i, h₂⟩
<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>N : Subgroup G<VAR>nN : N.Normal<VAR>H : Type v<VAR>inst✝³ : Group H<VAR>M : Type x<VAR>inst✝² : Monoid M<VAR>I : Type w<VAR>inst✝¹ : Group I<VAR>f : G →* H<VAR>inst✝ : f.range.Normal<VAR>g : H →* I<VAR>h : (mk' f.range).comp g.ker.subtype = 1<VAR>x : H<VAR>hx : x ∈ g.ker<GOAL>↑x = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U s✝ : Set α<VAR>ε r✝ : ℝ≥0∞<VAR>inst✝ : SigmaFinite μ<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>r : ℝ≥0∞<VAR>hr : r < μ s<VAR>B : ℕ → Set α := spanningSets μ<GOAL>∃ K ⊆ s, (fun s => MeasurableSet s ∧ μ s ≠ ⊤) K ∧ r < μ K