ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CompletePartialOrder α<VAR>inst✝ : Preorder β<VAR>f✝ : ι → α<VAR>d✝ : Set α<VAR>a✝ : α<VAR>f : α → β<VAR>h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun x x_1 => x ≤ x_1) d → IsLUB (f '' d) (f (sSup d))<VAR>d : Set α<VAR>hne : d.Nonempty<VAR>hd : DirectedOn (fun x x_1 => x ≤ x_1) d<VAR>a : α<VAR>hda : IsLUB d a<GOAL>IsLUB (f '' d) (f (sSup d))
<VAR>u : ℕ → ℝ<VAR>h : Subadditive u<VAR>k n r : ℕ<GOAL>u (k * n + r) ≤ ↑k * u n + u r
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<GOAL>f ≫ toSpecΓ S = toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>x : ↑R<VAR>x' : ↥(unop (op ⊤))<GOAL>↑((f ≫ toSpecΓ S) x) x' = ↑((toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op) x) x'
<VAR>R S : CommRingCat<VAR>f : R ⟶ S<VAR>x : ↑R<VAR>x' : ↥(unop (op ⊤))<GOAL>↑((toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op) x) x' = ↑((f ≫ toSpecΓ S) x) x'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : CommMonoid α<VAR>a b : α<VAR>h : a ~ᵤ b<VAR>n : ℕ<VAR>ih : a ^ n ~ᵤ b ^ n<GOAL>a ^ (n + 1) ~ᵤ b ^ (n + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : Zero β<VAR>inst✝¹ : SemilatticeInf β<VAR>inst✝ : ContinuousInf β<VAR>hf : FinStronglyMeasurable f μ<VAR>hg : FinStronglyMeasurable g μ<GOAL>FinStronglyMeasurable (f ⊓ g) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : Zero β<VAR>inst✝¹ : SemilatticeInf β<VAR>inst✝ : ContinuousInf β<VAR>hf : FinStronglyMeasurable f μ<VAR>hg : FinStronglyMeasurable g μ<VAR>n : ℕ<GOAL>μ (support ↑((fun n => hf.approx n ⊓ hg.approx n) n)) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝⁴ : Countable ι<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : Zero β<VAR>inst✝¹ : SemilatticeInf β<VAR>inst✝ : ContinuousInf β<VAR>hf : FinStronglyMeasurable f μ<VAR>hg : FinStronglyMeasurable g μ<VAR>n : ℕ<GOAL>μ (support ↑(hf.approx n) ∪ support ↑(hg.approx n)) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>m : α → ℝ≥0∞<VAR>f : Filter α<VAR>h : ∀ (x : ℝ≥0), ∀ᶠ (a : α) in f, ↑x < m a<VAR>n : ℕ<GOAL>∀ᶠ (a : α) in f, ↑n < m a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y✝ z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>m : α → ℝ≥0∞<VAR>f : Filter α<VAR>h : ∀ (n : ℕ), ∀ᶠ (a : α) in f, ↑n < m a<VAR>x : ℝ≥0<VAR>n : ℕ<VAR>hn : x < ↑n<VAR>y : α<GOAL>↑x < ↑n
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<GOAL>(pderiv 1) (X 1 ^ 2 * X 2 + C W.a₁ * X 0 * X 1 * X 2 + C W.a₃ * X 1 * X 2 ^ 2 - (X 0 ^ 3 + C W.a₂ * X 0 ^ 2 * X 2 + C W.a₄ * X 0 * X 2 ^ 2 + C W.a₆ * X 2 ^ 3)) = C 2 * X 1 * X 2 + C W.a₁ * X 0 * X 2 + C W.a₃ * X 2 ^ 2
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Projective R<GOAL>↑2 * X 1 ^ (2 - 1) * 1 * X 2 + X 1 ^ 2 * 0 + (((0 * X 0 + C W.a₁ * 0) * X 1 + C W.a₁ * X 0 * 1) * X 2 + C W.a₁ * X 0 * X 1 * 0) + ((0 * X 1 + C W.a₃ * 1) * X 2 ^ 2 + C W.a₃ * X 1 * (↑2 * X 2 ^ (2 - 1) * 0)) - (↑3 * X 0 ^ (3 - 1) * 0 + ((0 * X 0 ^ 2 + C W.a₂ * (↑2 * X 0 ^ (2 - 1) * 0)) * X 2 + C W.a₂ * X 0 ^ 2 * 0) + ((0 * X 0 + C W.a₄ * 0) * X 2 ^ 2 + C W.a₄ * X 0 * (↑2 * X 2 ^ (2 - 1) * 0)) + (0 * X 2 ^ 3 + C W.a₆ * (↑3 * X 2 ^ (3 - 1) * 0))) = 2 * X 1 * X 2 + C W.a₁ * X 0 * X 2 + C W.a₃ * X 2 ^ 2
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommRing R<VAR>p q : MvPolynomial σ R<GOAL>(-p).vars = p.vars
<VAR>R : Type u<VAR>inst✝⁴ : Ring R<VAR>ι : Type v<VAR>inst✝³ : Preorder ι<VAR>G : ι → Type w<VAR>inst✝² : Nonempty ι<VAR>inst✝¹ : IsDirected ι fun x x_1 => x ≤ x_1<VAR>inst✝ : (i : ι) → Field (G i)<VAR>f : (i j : ι) → i ≤ j → G i → G j<VAR>f' : (i j : ι) → i ≤ j → G i →+* G j<VAR>p : Ring.DirectLimit G f<VAR>hp : p ≠ 0<GOAL>p * inv G f p = 1
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>pb : PowerBasis R S<VAR>I : Ideal R<VAR>x : R<GOAL>(aeval (root (minpoly R pb.gen))) (minpoly R pb.gen) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>pb : PowerBasis R S<VAR>I : Ideal R<VAR>x : R<GOAL>Ideal.map (of (minpoly R pb.gen)) I = Ideal.map (↑(equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm.toRingEquiv) (Ideal.map (algebraMap R S) I)
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>pb : PowerBasis R S<VAR>I : Ideal R<VAR>x : R<GOAL>((Ideal.map (algebraMap R S) I).quotientEquiv (Ideal.map (of (minpoly R pb.gen)) I) (equiv' (minpoly R pb.gen) pb ⋯ ⋯).symm.toRingEquiv ⋯) ((algebraMap R (S ⧸ Ideal.map (algebraMap R S) I)) x) = (algebraMap R (AdjoinRoot (minpoly R pb.gen) ⧸ Ideal.map (of (minpoly R pb.gen)) I)) x
<VAR>m n : ℕ<GOAL>↑(m / n) ≤ ↑m / ↑n
<VAR>m n : ℕ<GOAL>↑↑(m / n) ≤ ↑m / ↑n
<VAR>m n : ℕ<GOAL>↑↑(m / n) ≤ ↑↑m / ↑n
<VAR>m n : ℕ<GOAL>↑↑(m / n) ≤ ↑↑m / ↑↑n
<VAR>m n : ℕ<GOAL>↑↑(m / n) ≤ ↑(↑m / ↑n)
<VAR>a b : ℕ+<VAR>d : ℕ+ := a.gcdD b<VAR>w : ℕ+ := a.gcdW b<VAR>x : ℕ := a.gcdX b<VAR>y : ℕ := a.gcdY b<VAR>z : ℕ+ := a.gcdZ b<VAR>a' : ℕ+ := a.gcdA' b<VAR>b' : ℕ+ := a.gcdB' b<VAR>u : XgcdType := XgcdType.start a b<VAR>ur : XgcdType := u.reduce<VAR>x✝ : d = ur.a<GOAL>w * z = (x * y).succPNat ∧ a = a' * d ∧ b = b' * d ∧ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
<VAR>a b : ℕ+<VAR>d : ℕ+ := a.gcdD b<VAR>w : ℕ+ := a.gcdW b<VAR>x : ℕ := a.gcdX b<VAR>y : ℕ := a.gcdY b<VAR>z : ℕ+ := a.gcdZ b<VAR>a' : ℕ+ := a.gcdA' b<VAR>b' : ℕ+ := a.gcdB' b<VAR>u : XgcdType := XgcdType.start a b<VAR>ur : XgcdType := u.reduce<VAR>x✝ : d = ur.a<VAR>hb : d = ur.b<GOAL>w * z = (x * y).succPNat ∧ a = a' * d ∧ b = b' * d ∧ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
<VAR>a b : ℕ+<VAR>d : ℕ+ := a.gcdD b<VAR>w : ℕ+ := a.gcdW b<VAR>x : ℕ := a.gcdX b<VAR>y : ℕ := a.gcdY b<VAR>z : ℕ+ := a.gcdZ b<VAR>a' : ℕ+ := a.gcdA' b<VAR>b' : ℕ+ := a.gcdB' b<VAR>u : XgcdType := XgcdType.start a b<VAR>ur : XgcdType := u.reduce<VAR>x✝ : d = ur.a<VAR>hb : d = ur.b<VAR>ha' : ↑a' = ↑w + x<GOAL>w * z = (x * y).succPNat ∧ a = a' * d ∧ b = b' * d ∧ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
<VAR>a b : ℕ+<VAR>d : ℕ+ := a.gcdD b<VAR>w : ℕ+ := a.gcdW b<VAR>x : ℕ := a.gcdX b<VAR>y : ℕ := a.gcdY b<VAR>z : ℕ+ := a.gcdZ b<VAR>a' : ℕ+ := a.gcdA' b<VAR>b' : ℕ+ := a.gcdB' b<VAR>u : XgcdType := XgcdType.start a b<VAR>ur : XgcdType := u.reduce<VAR>x✝ : d = ur.a<VAR>hb : d = ur.b<VAR>ha' : ↑a' = ↑w + x<VAR>hb' : ↑b' = y + ↑z<GOAL>w * z = (x * y).succPNat ∧ a = a' * d ∧ b = b' * d ∧ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
<VAR>a b : ℕ+<VAR>d : ℕ+ := a.gcdD b<VAR>w : ℕ+ := a.gcdW b<VAR>x : ℕ := a.gcdX b<VAR>y : ℕ := a.gcdY b<VAR>z : ℕ+ := a.gcdZ b<VAR>a' : ℕ+ := a.gcdA' b<VAR>b' : ℕ+ := a.gcdB' b<VAR>u : XgcdType := XgcdType.start a b<VAR>ur : XgcdType := u.reduce<VAR>x✝ : d = ur.a<VAR>hb : d = ur.b<VAR>ha' : ↑a' = ↑w + x<VAR>hb' : ↑b' = y + ↑z<VAR>hdet : w * z = (x * y).succPNat<GOAL>w * z = (x * y).succPNat ∧ a = a' * d ∧ b = b' * d ∧ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
<VAR>a b : ℕ+<VAR>d : ℕ+ := a.gcdD b<VAR>w : ℕ+ := a.gcdW b<VAR>x : ℕ := a.gcdX b<VAR>y : ℕ := a.gcdY b<VAR>z : ℕ+ := a.gcdZ b<VAR>a' : ℕ+ := a.gcdA' b<VAR>b' : ℕ+ := a.gcdB' b<VAR>u : XgcdType := XgcdType.start a b<VAR>ur : XgcdType := u.reduce<VAR>x✝ : d = ur.a<VAR>hb : d = ur.b<VAR>ha' : ↑a' = ↑w + x<VAR>hb' : ↑b' = y + ↑z<VAR>hdet : w * z = (x * y).succPNat<GOAL>a = a' * d ∧ b = b' * d ∧ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
<VAR>a b : ℕ+<VAR>d : ℕ+ := a.gcdD b<VAR>w : ℕ+ := a.gcdW b<VAR>x : ℕ := a.gcdX b<VAR>y : ℕ := a.gcdY b<VAR>z : ℕ+ := a.gcdZ b<VAR>a' : ℕ+ := a.gcdA' b<VAR>b' : ℕ+ := a.gcdB' b<VAR>u : XgcdType := XgcdType.start a b<VAR>ur : XgcdType := u.reduce<VAR>x✝ : d = ur.a<VAR>hb : d = ur.b<VAR>ha' : ↑a' = ↑w + x<VAR>hb' : ↑b' = y + ↑z<VAR>hdet : w * z = (x * y).succPNat<VAR>hdet' : ↑w * ↑z = x * y + 1<GOAL>a = a' * d ∧ b = b' * d ∧ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
<VAR>a b : ℕ+<VAR>d : ℕ+ := a.gcdD b<VAR>w : ℕ+ := a.gcdW b<VAR>x : ℕ := a.gcdX b<VAR>y : ℕ := a.gcdY b<VAR>z : ℕ+ := a.gcdZ b<VAR>a' : ℕ+ := a.gcdA' b<VAR>b' : ℕ+ := a.gcdB' b<VAR>u : XgcdType := XgcdType.start a b<VAR>ur : XgcdType := u.reduce<VAR>x✝¹ : d = ur.a<VAR>hb : d = ur.b<VAR>ha' : ↑a' = ↑w + x<VAR>hb' : ↑b' = y + ↑z<VAR>hdet : w * z = (x * y).succPNat<VAR>hdet' : ↑w * ↑z = x * y + 1<VAR>x✝ : u.v = (↑a, ↑b)<GOAL>a = a' * d ∧ b = b' * d ∧ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
<VAR>a b : ℕ+<VAR>d : ℕ+ := a.gcdD b<VAR>w : ℕ+ := a.gcdW b<VAR>x : ℕ := a.gcdX b<VAR>y : ℕ := a.gcdY b<VAR>z : ℕ+ := a.gcdZ b<VAR>a' : ℕ+ := a.gcdA' b<VAR>b' : ℕ+ := a.gcdB' b<VAR>u : XgcdType := XgcdType.start a b<VAR>ur : XgcdType := u.reduce<VAR>x✝¹ : d = ur.a<VAR>hb : d = ur.b<VAR>ha' : ↑a' = ↑w + x<VAR>hb' : ↑b' = y + ↑z<VAR>hdet : w * z = (x * y).succPNat<VAR>hdet' : ↑w * ↑z = x * y + 1<VAR>x✝ : u.v = (↑a, ↑b)<VAR>hv : (↑w * ↑d + x * ↑ur.b, y * ↑d + ↑z * ↑ur.b) = (↑a, ↑b) := Eq.trans (XgcdType.reduce_v u) (XgcdType.start_v a b)<GOAL>a = a' * d ∧ b = b' * d ∧ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
<VAR>a b : ℕ+<VAR>d : ℕ+ := a.gcdD b<VAR>w : ℕ+ := a.gcdW b<VAR>x : ℕ := a.gcdX b<VAR>y : ℕ := a.gcdY b<VAR>z : ℕ+ := a.gcdZ b<VAR>a' : ℕ+ := a.gcdA' b<VAR>b' : ℕ+ := a.gcdB' b<VAR>u : XgcdType := XgcdType.start a b<VAR>ur : XgcdType := u.reduce<VAR>x✝¹ : d = ur.a<VAR>hb : d = ur.b<VAR>ha' : ↑a' = ↑w + x<VAR>hb' : ↑b' = y + ↑z<VAR>hdet : w * z = (x * y).succPNat<VAR>hdet' : ↑w * ↑z = x * y + 1<VAR>x✝ : u.v = (↑a, ↑b)<VAR>hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)<GOAL>a = a' * d ∧ b = b' * d ∧ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
<VAR>a b : ℕ+<VAR>d : ℕ+ := a.gcdD b<VAR>w : ℕ+ := a.gcdW b<VAR>x : ℕ := a.gcdX b<VAR>y : ℕ := a.gcdY b<VAR>z : ℕ+ := a.gcdZ b<VAR>a' : ℕ+ := a.gcdA' b<VAR>b' : ℕ+ := a.gcdB' b<VAR>u : XgcdType := XgcdType.start a b<VAR>ur : XgcdType := u.reduce<VAR>x✝¹ : d = ur.a<VAR>hb : d = ur.b<VAR>ha' : ↑a' = ↑w + x<VAR>hb' : ↑b' = y + ↑z<VAR>hdet : w * z = (x * y).succPNat<VAR>hdet' : ↑w * ↑z = x * y + 1<VAR>x✝ : u.v = (↑a, ↑b)<VAR>hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)<VAR>ha'' : ↑a = ↑a' * ↑d<GOAL>a = a' * d ∧ b = b' * d ∧ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
<VAR>a b : ℕ+<VAR>d : ℕ+ := a.gcdD b<VAR>w : ℕ+ := a.gcdW b<VAR>x : ℕ := a.gcdX b<VAR>y : ℕ := a.gcdY b<VAR>z : ℕ+ := a.gcdZ b<VAR>a' : ℕ+ := a.gcdA' b<VAR>b' : ℕ+ := a.gcdB' b<VAR>u : XgcdType := XgcdType.start a b<VAR>ur : XgcdType := u.reduce<VAR>x✝¹ : d = ur.a<VAR>hb : d = ur.b<VAR>ha' : ↑a' = ↑w + x<VAR>hb' : ↑b' = y + ↑z<VAR>hdet : w * z = (x * y).succPNat<VAR>hdet' : ↑w * ↑z = x * y + 1<VAR>x✝ : u.v = (↑a, ↑b)<VAR>hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)<VAR>ha'' : ↑a = ↑a' * ↑d<VAR>hb'' : ↑b = ↑b' * ↑d<GOAL>a = a' * d ∧ b = b' * d ∧ z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
<VAR>a b : ℕ+<VAR>d : ℕ+ := a.gcdD b<VAR>w : ℕ+ := a.gcdW b<VAR>x : ℕ := a.gcdX b<VAR>y : ℕ := a.gcdY b<VAR>z : ℕ+ := a.gcdZ b<VAR>a' : ℕ+ := a.gcdA' b<VAR>b' : ℕ+ := a.gcdB' b<VAR>u : XgcdType := XgcdType.start a b<VAR>ur : XgcdType := u.reduce<VAR>x✝¹ : d = ur.a<VAR>hb : d = ur.b<VAR>ha' : ↑a' = ↑w + x<VAR>hb' : ↑b' = y + ↑z<VAR>hdet : w * z = (x * y).succPNat<VAR>hdet' : ↑w * ↑z = x * y + 1<VAR>x✝ : u.v = (↑a, ↑b)<VAR>hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)<VAR>ha'' : ↑a = ↑a' * ↑d<VAR>hb'' : ↑b = ↑b' * ↑d<GOAL>z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
<VAR>a b : ℕ+<VAR>d : ℕ+ := a.gcdD b<VAR>w : ℕ+ := a.gcdW b<VAR>x : ℕ := a.gcdX b<VAR>y : ℕ := a.gcdY b<VAR>z : ℕ+ := a.gcdZ b<VAR>a' : ℕ+ := a.gcdA' b<VAR>b' : ℕ+ := a.gcdB' b<VAR>u : XgcdType := XgcdType.start a b<VAR>ur : XgcdType := u.reduce<VAR>x✝¹ : d = ur.a<VAR>hb : d = ur.b<VAR>ha' : ↑a' = ↑w + x<VAR>hb' : ↑b' = y + ↑z<VAR>hdet : w * z = (x * y).succPNat<VAR>hdet' : ↑w * ↑z = x * y + 1<VAR>x✝ : u.v = (↑a, ↑b)<VAR>hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)<VAR>ha'' : ↑a = ↑a' * ↑d<VAR>hb'' : ↑b = ↑b' * ↑d<VAR>hza' : ↑z * ↑a' = x * ↑b' + 1<GOAL>z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
<VAR>a b : ℕ+<VAR>d : ℕ+ := a.gcdD b<VAR>w : ℕ+ := a.gcdW b<VAR>x : ℕ := a.gcdX b<VAR>y : ℕ := a.gcdY b<VAR>z : ℕ+ := a.gcdZ b<VAR>a' : ℕ+ := a.gcdA' b<VAR>b' : ℕ+ := a.gcdB' b<VAR>u : XgcdType := XgcdType.start a b<VAR>ur : XgcdType := u.reduce<VAR>x✝¹ : d = ur.a<VAR>hb : d = ur.b<VAR>ha' : ↑a' = ↑w + x<VAR>hb' : ↑b' = y + ↑z<VAR>hdet : w * z = (x * y).succPNat<VAR>hdet' : ↑w * ↑z = x * y + 1<VAR>x✝ : u.v = (↑a, ↑b)<VAR>hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)<VAR>ha'' : ↑a = ↑a' * ↑d<VAR>hb'' : ↑b = ↑b' * ↑d<VAR>hza' : ↑z * ↑a' = x * ↑b' + 1<VAR>hwb' : ↑w * ↑b' = y * ↑a' + 1<GOAL>↑z * (↑a' * ↑d) = x * (↑b' * ↑d) + ↑d ∧ ↑w * (↑b' * ↑d) = y * (↑a' * ↑d) + ↑d
<VAR>a b : ℕ+<VAR>d : ℕ+ := a.gcdD b<VAR>w : ℕ+ := a.gcdW b<VAR>x : ℕ := a.gcdX b<VAR>y : ℕ := a.gcdY b<VAR>z : ℕ+ := a.gcdZ b<VAR>a' : ℕ+ := a.gcdA' b<VAR>b' : ℕ+ := a.gcdB' b<VAR>u : XgcdType := XgcdType.start a b<VAR>ur : XgcdType := u.reduce<VAR>x✝¹ : d = ur.a<VAR>hb : d = ur.b<VAR>ha' : ↑a' = ↑w + x<VAR>hb' : ↑b' = y + ↑z<VAR>hdet : w * z = (x * y).succPNat<VAR>hdet' : ↑w * ↑z = x * y + 1<VAR>x✝ : u.v = (↑a, ↑b)<VAR>hv : (↑a' * ↑d, ↑b' * ↑d) = (↑a, ↑b)<VAR>ha'' : ↑a = ↑a' * ↑d<VAR>hb'' : ↑b = ↑b' * ↑d<VAR>hza' : ↑z * ↑a' = x * ↑b' + 1<VAR>hwb' : ↑w * ↑b' = y * ↑a' + 1<GOAL>↑z * ↑a' * ↑d = x * ↑b' * ↑d + ↑d ∧ ↑w * ↑b' * ↑d = y * ↑a' * ↑d + ↑d
<VAR>n : ℕ<VAR>inst✝ : NeZero n<GOAL>Fintype.card (QuaternionGroup n) = 4 * n
<VAR>n : ℕ<VAR>inst✝ : NeZero n<GOAL>n + n + (n + n) = 4 * n
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : StrongRankCondition R<VAR>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>b : ι → M<GOAL>Set.finrank R (range b) ≤ Fintype.card ι
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝¹ : CommRing R<VAR>f : R[X]<VAR>inst✝ : CommRing S<VAR>i : R →+* S<VAR>a : S<VAR>h : eval₂ i a f = 0<GOAL>(lift i a h) (root f) = a
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝¹ : Group H<VAR>M : Type u_3<VAR>inst✝ : Monoid M<VAR>d : TransversalPair G A B<VAR>u : ℤˣ<VAR>g : G<GOAL>(unitsSMulGroup φ d u g).2 = (⋯.equiv g).2
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>t : Set α<VAR>a b x y : α<VAR>s : Finset α<VAR>hs : (↑s).Finite<VAR>hf : f.IsCycleOn ↑s<VAR>ha : a ∈ ↑s<VAR>hb : b ∈ ↑s<GOAL>∃ n, (f ^ n) a = b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>t : Set α<VAR>a b x y : α<VAR>s : Finset α<VAR>hs : (↑s).Finite<VAR>hf : f.IsCycleOn ↑s<VAR>ha : a ∈ ↑s<VAR>hb : b ∈ ↑s<VAR>n : ℕ<VAR>hn : (f ^ n) a = b<GOAL>∃ n, (f ^ n) a = b
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>f g : ℕ →₀ R<GOAL>{ toFinsupp := f } = { toFinsupp := g } ↔ ∀ (n : ℕ), { toFinsupp := f }.coeff n = { toFinsupp := g }.coeff n
<VAR>ι✝ : Type u<VAR>γ : Type w<VAR>β✝ : ι✝ → Type v<VAR>β₁✝ : ι✝ → Type v₁<VAR>β₂✝ : ι✝ → Type v₂<VAR>inst✝¹¹ : DecidableEq ι✝<VAR>inst✝¹⁰ : (i : ι✝) → Zero (β✝ i)<VAR>inst✝⁹ : (i : ι✝) → (x : β✝ i) → Decidable (x ≠ 0)<VAR>inst✝⁸ : (i : ι✝) → Zero (β₁✝ i)<VAR>inst✝⁷ : (i : ι✝) → Zero (β₂✝ i)<VAR>inst✝⁶ : (i : ι✝) → (x : β₁✝ i) → Decidable (x ≠ 0)<VAR>inst✝⁵ : (i : ι✝) → (x : β₂✝ i) → Decidable (x ≠ 0)<VAR>ι : Type u<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>dec : DecidableEq ι<VAR>inst✝⁴ : (i : ι) → Zero (β i)<VAR>inst✝³ : (i : ι) → Zero (β₁ i)<VAR>inst✝² : (i : ι) → Zero (β₂ i)<VAR>inst✝¹ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)<VAR>inst✝ : (i : ι) → (x : β₂ i) → Decidable (x ≠ 0)<VAR>f : (i : ι) → β₁ i → β₂ i → β i<VAR>hf : ∀ (i : ι), f i 0 0 = 0<VAR>g₁ : Π₀ (i : ι), β₁ i<VAR>g₂ : Π₀ (i : ι), β₂ i<VAR>i : ι<GOAL>(zipWith f hf g₁ g₂) i = (mk (g₁.support ∪ g₂.support) fun i => f (↑i) (g₁ ↑i) (g₂ ↑i)) i
<VAR>x y : ℂ<GOAL>x ^ (-y) = (x ^ y)⁻¹
<VAR>x y : ℂ<GOAL>(if x = 0 then if y = 0 then 1 else 0 else cexp (-(log x * y))) = (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y))⁻¹
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>Y Y' Z : C<VAR>inst✝ : ExactPairing Y Y'<VAR>f : Y' ⟶ Z<GOAL>(tensorLeftHomEquiv (𝟙_ C) Y Y' Z).symm (η_ Y Y' ≫ Y ◁ f) = (ρ_ Y').hom ≫ f
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>inst✝ : SFinite μ<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>hg : AEMeasurable g (μ.restrict s)<VAR>hs : MeasurableSet s<GOAL>(μ.prod volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>inst✝ : SFinite μ<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>hg : AEMeasurable g (μ.restrict s)<VAR>hs : MeasurableSet s<VAR>h₁ : (fun y => ofReal ((g - f) y)) =ᶠ[ae (μ.restrict s)] fun y => ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)<GOAL>(μ.prod volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>inst✝ : SFinite μ<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>hg : AEMeasurable g (μ.restrict s)<VAR>hs : MeasurableSet s<VAR>h₁ : (fun y => ofReal ((g - f) y)) =ᶠ[ae (μ.restrict s)] fun y => ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)<VAR>h₂ : ((μ.restrict s).prod volume) (regionBetween f g s) = ((μ.restrict s).prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)<GOAL>(μ.prod volume) (regionBetween f g s) = ∫⁻ (y : α) in s, ofReal ((g - f) y) ∂μ
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>inst✝ : SFinite μ<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>hg : AEMeasurable g (μ.restrict s)<VAR>hs : MeasurableSet s<VAR>h₁ : (fun y => ofReal ((g - f) y)) =ᶠ[ae (μ.restrict s)] fun y => ofReal ((AEMeasurable.mk g hg - AEMeasurable.mk f hf) y)<VAR>h₂ : ((μ.restrict s).prod volume) (regionBetween f g s) = ((μ.restrict s).prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)<GOAL>(μ.prod volume) (regionBetween f g s) = (μ.prod volume) (regionBetween (AEMeasurable.mk f hf) (AEMeasurable.mk g hg) s)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : ν ≪ μ<GOAL>(fun x => rexp (-llr μ ν x)) =ᶠ[ae ν] fun x => (ν.rnDeriv μ x).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : ν ≪ μ<VAR>x : α<VAR>hx : (-llr ν μ) x = llr μ ν x<VAR>hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal<GOAL>rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : ν ≪ μ<VAR>x : α<VAR>hx : llr ν μ x = -llr μ ν x<VAR>hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal<GOAL>rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : CommSemiring R₁<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : Module R₁ M₁<VAR>I : R₁ →+* R<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : CharZero R<VAR>B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R<VAR>h : B = -B.flip<VAR>x : M₁<GOAL>(B x) x = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : CommSemiring R₁<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : Module R₁ M₁<VAR>I : R₁ →+* R<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : CharZero R<VAR>B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R<VAR>h : B = -B.flip<VAR>x : M₁<VAR>h' : (B x) x = ((-B.flip) x) x := congr_fun₂ h x x<GOAL>(B x) x = 0
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : CommSemiring R₁<VAR>inst✝³ : AddCommMonoid M₁<VAR>inst✝² : Module R₁ M₁<VAR>I : R₁ →+* R<VAR>inst✝¹ : NoZeroDivisors R<VAR>inst✝ : CharZero R<VAR>B : M₁ →ₛₗ[I] M₁ →ₛₗ[I] R<VAR>h : B = -B.flip<VAR>x : M₁<VAR>h' : (B x) x + (B x) x = 0<GOAL>(B x) x = 0
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0∞<VAR>hp1 : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>h_top : ¬a + b = ⊤<GOAL>a ^ p + b ^ p ≤ (a + b) ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>a b : ℝ≥0∞<VAR>hp1 : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>h_top : ¬a + b = ⊤<VAR>ha_top : a ≠ ⊤<VAR>hb_top : b ≠ ⊤<GOAL>a ^ p + b ^ p ≤ (a + b) ^ p
<VAR>ι : Type u<VAR>s : Finset ι<VAR>p : ℝ<VAR>hp1 : 1 ≤ p<VAR>hp_pos : 0 < p<VAR>a b : ℝ≥0<VAR>h_top : ¬↑a + ↑b = ⊤<GOAL>↑a ^ p + ↑b ^ p ≤ (↑a + ↑b) ^ p
<VAR>n b : ℕ<VAR>h : 1 ≤ b<GOAL>n.ProbablePrime b ↔ b ^ (n - 1) ≡ 1 [MOD n]
<VAR>n b : ℕ<VAR>h : 1 ≤ b<VAR>this : 1 ≤ b ^ (n - 1)<GOAL>n.ProbablePrime b ↔ b ^ (n - 1) ≡ 1 [MOD n]
<VAR>n b : ℕ<VAR>h : 1 ≤ b<VAR>this : 1 ≤ b ^ (n - 1)<GOAL>n.ProbablePrime b ↔ 1 ≡ b ^ (n - 1) [MOD n]
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b✝ b : EReal<GOAL>limsup u f ≤ b ↔ ∀ (c : ℝ), b < ↑c → ∀ᶠ (a : α) in f, u a ≤ ↑c
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b✝ b : EReal<GOAL>(∀ (z : ℝ), b < ↑z → limsup u f ≤ ↑z) ↔ ∀ (c : ℝ), b < ↑c → ∀ᶠ (a : α) in f, u a ≤ ↑c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a b : α<GOAL>_root_.Disjoint s (t ∪ u) ↔ _root_.Disjoint s t ∧ _root_.Disjoint s u
<VAR>R : Type u_1<VAR>inst✝⁵ : AddCommGroupWithOne R<VAR>inst✝⁴ : PartialOrder R<VAR>inst✝³ : CovariantClass R R (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝² : ZeroLEOneClass R<VAR>inst✝¹ : NeZero 1<VAR>inst✝ : Nontrivial R<VAR>m n : ℤ<GOAL>↑m ≤ ↑n ↔ m ≤ n
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R✝<VAR>n : ℕ<VAR>inst✝² : CommRing R✝<VAR>inst✝¹ : IsDomain R✝<VAR>p✝ q✝ : R✝[X]<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>p q : R[X]<VAR>hp : p.Monic<VAR>hq : q.Monic<VAR>hdiv : p ∣ q<VAR>hdeg : q.natDegree ≤ p.natDegree<GOAL>q = p