ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x y : F<VAR>h : W.Nonsingular x y<GOAL>↑(WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x (Polynomial.C y)) * (↑(WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x (Polynomial.C (W.negY x y))) * (↑(WeierstrassCurve.Affine.CoordinateRing.XIdeal W x))⁻¹) = 1
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<GOAL>WeierstrassCurve.Affine.CoordinateRing.XIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) * (WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x₁ (Polynomial.C y₁) * WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x₂ (Polynomial.C y₂)) = WeierstrassCurve.Affine.CoordinateRing.YIdeal W (WeierstrassCurve.Affine.linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) * WeierstrassCurve.Affine.CoordinateRing.XYIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (Polynomial.C (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)))
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x y : F<VAR>h : W.Nonsingular x y<GOAL>↑(WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h) = ↑(WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x (Polynomial.C y))
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x y : F<VAR>h : W.Nonsingular x y<GOAL>ClassGroup.mk (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' ⋯) * ClassGroup.mk (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h) = 1
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Nonsingular x₁ y₁<VAR>h₂ : W.Nonsingular x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<GOAL>ClassGroup.mk (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h₁) * ClassGroup.mk (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h₂) = ClassGroup.mk (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' ⋯)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>p q : R[X]<GOAL>(Algebra.norm R[X]) (p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W) Y) = p ^ 2 - p * q * (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃) - q ^ 2 * (Polynomial.X ^ 3 + Polynomial.C W.a₂ * Polynomial.X ^ 2 + Polynomial.C W.a₄ * Polynomial.X + Polynomial.C W.a₆)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>p q : R[X]<GOAL>(AdjoinRoot.of W.polynomial) ((Algebra.norm R[X]) (p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W) Y)) = (WeierstrassCurve.Affine.CoordinateRing.mk W) ((Polynomial.C p + Polynomial.C q * Y) * (Polynomial.C p + Polynomial.C q * (-Y - Polynomial.C (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃))))
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>IsDomain R<VAR>p q : R[X]<GOAL>((Algebra.norm R[X]) (p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W) Y)).degree = max (2 • p.degree) (2 • q.degree + 3)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>IsDomain R<VAR>x : W.CoordinateRing<GOAL>((Algebra.norm R[X]) x).degree ≠ 1
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>IsDomain R<VAR>x : W.CoordinateRing<GOAL>((Algebra.norm R[X]) x).natDegree ≠ 1
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<GOAL>∀ (a : W.Point), WeierstrassCurve.Affine.Point.toClass a = a.toClassFun
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<GOAL>WeierstrassCurve.Affine.Point.toClass 0 = 0
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>x y : F<VAR>h : W.Nonsingular x y<GOAL>WeierstrassCurve.Affine.Point.toClass (WeierstrassCurve.Affine.Point.some h) = ClassGroup.mk (WeierstrassCurve.Affine.CoordinateRing.XYIdeal' h)
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>P Q : W.Point<GOAL>P + Q = 0 ↔ P = -Q
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<VAR>P : W.Point<GOAL>WeierstrassCurve.Affine.Point.toClass P = 0 ↔ P = 0
<VAR>F : Type u<VAR>Field F<VAR>W : WeierstrassCurve.Affine F<GOAL>Function.Injective ⇑WeierstrassCurve.Affine.Point.toClass
<VAR>α : Type u_2<VAR>One α<GOAL>{1} = 1
<VAR>α : Type u_2<VAR>Zero α<GOAL>{0} = 0
<VAR>α : Type u_2<VAR>Zero α<VAR>a : α<GOAL>a ∈ 0 ↔ a = 0
<VAR>α : Type u_2<VAR>One α<VAR>a : α<GOAL>a ∈ 1 ↔ a = 1
<VAR>α : Type u_2<VAR>Zero α<VAR>s : Set α<GOAL>0 ⊆ s ↔ 0 ∈ s
<VAR>α : Type u_2<VAR>One α<VAR>s : Set α<GOAL>1 ⊆ s ↔ 1 ∈ s
<VAR>α : Type u_2<VAR>One α<GOAL>Set.Nonempty 1
<VAR>α : Type u_2<VAR>Zero α<GOAL>Set.Nonempty 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>One α<VAR>f : α → β<GOAL>f '' 1 = {f 1}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>f : α → β<GOAL>f '' 0 = {f 0}
<VAR>α : Type u_2<VAR>One α<VAR>s : Set α<GOAL>s ⊆ 1 ↔ s = ∅ ∨ s = 1
<VAR>α : Type u_2<VAR>Zero α<VAR>s : Set α<GOAL>s ⊆ 0 ↔ s = ∅ ∨ s = 0
<VAR>α : Type u_2<VAR>One α<VAR>s : Set α<VAR>h : s.Nonempty<GOAL>s ⊆ 1 ↔ s = 1
<VAR>α : Type u_2<VAR>Zero α<VAR>s : Set α<VAR>h : s.Nonempty<GOAL>s ⊆ 0 ↔ s = 0
<VAR>α : Type u_2<VAR>One α<GOAL>⇑Set.singletonOneHom = singleton
<VAR>α : Type u_2<VAR>Zero α<GOAL>⇑Set.singletonZeroHom = singleton
<VAR>α : Type u_2<VAR>Neg α<VAR>s : Set α<VAR>a : α<GOAL>a ∈ -s ↔ -a ∈ s
<VAR>α : Type u_2<VAR>Inv α<VAR>s : Set α<VAR>a : α<GOAL>a ∈ s⁻¹ ↔ a⁻¹ ∈ s
<VAR>α : Type u_2<VAR>Inv α<VAR>s : Set α<GOAL>Inv.inv ⁻¹' s = s⁻¹
<VAR>α : Type u_2<VAR>Neg α<VAR>s : Set α<GOAL>Neg.neg ⁻¹' s = -s
<VAR>α : Type u_2<VAR>Inv α<GOAL>∅⁻¹ = ∅
<VAR>α : Type u_2<VAR>Neg α<GOAL>-∅ = ∅
<VAR>α : Type u_2<VAR>Neg α<GOAL>-Set.univ = Set.univ
<VAR>α : Type u_2<VAR>Inv α<GOAL>Set.univ⁻¹ = Set.univ
<VAR>α : Type u_2<VAR>Neg α<VAR>s t : Set α<GOAL>-(s ∩ t) = -s ∩ -t
<VAR>α : Type u_2<VAR>Inv α<VAR>s t : Set α<GOAL>(s ∩ t)⁻¹ = s⁻¹ ∩ t⁻¹
<VAR>α : Type u_2<VAR>Inv α<VAR>s t : Set α<GOAL>(s ∪ t)⁻¹ = s⁻¹ ∪ t⁻¹
<VAR>α : Type u_2<VAR>Neg α<VAR>s t : Set α<GOAL>-(s ∪ t) = -s ∪ -t
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Neg α<VAR>s : ι → Set α<GOAL>-⋂ i, s i = ⋂ i, -s i
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Inv α<VAR>s : ι → Set α<GOAL>(⋂ i, s i)⁻¹ = ⋂ i, (s i)⁻¹
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Neg α<VAR>s : ι → Set α<GOAL>-⋃ i, s i = ⋃ i, -s i
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Inv α<VAR>s : ι → Set α<GOAL>(⋃ i, s i)⁻¹ = ⋃ i, (s i)⁻¹
<VAR>α : Type u_2<VAR>Neg α<VAR>s : Set α<GOAL>-sᶜ = (-s)ᶜ
<VAR>α : Type u_2<VAR>Inv α<VAR>s : Set α<GOAL>sᶜ⁻¹ = s⁻¹ᶜ
<VAR>α : Type u_2<VAR>InvolutiveInv α<VAR>s : Set α<VAR>a : α<GOAL>a⁻¹ ∈ s⁻¹ ↔ a ∈ s
<VAR>α : Type u_2<VAR>InvolutiveNeg α<VAR>s : Set α<VAR>a : α<GOAL>-a ∈ -s ↔ a ∈ s
<VAR>α : Type u_2<VAR>InvolutiveNeg α<VAR>s : Set α<GOAL>(-s).Nonempty ↔ s.Nonempty
<VAR>α : Type u_2<VAR>InvolutiveInv α<VAR>s : Set α<GOAL>s⁻¹.Nonempty ↔ s.Nonempty
<VAR>α : Type u_2<VAR>InvolutiveNeg α<VAR>s : Set α<VAR>h : s.Nonempty<GOAL>(-s).Nonempty
<VAR>α : Type u_2<VAR>InvolutiveInv α<VAR>s : Set α<VAR>h : s.Nonempty<GOAL>s⁻¹.Nonempty
<VAR>α : Type u_2<VAR>InvolutiveNeg α<VAR>s : Set α<GOAL>Neg.neg '' s = -s
<VAR>α : Type u_2<VAR>InvolutiveInv α<VAR>s : Set α<GOAL>Inv.inv '' s = s⁻¹
<VAR>α : Type u_2<VAR>InvolutiveInv α<VAR>s : Set α<GOAL>s⁻¹ = ∅ ↔ s = ∅
<VAR>α : Type u_2<VAR>InvolutiveNeg α<VAR>s : Set α<GOAL>-s = ∅ ↔ s = ∅
<VAR>α : Type u_2<VAR>InvolutiveNeg α<VAR>s t : Set α<GOAL>-s ⊆ -t ↔ s ⊆ t
<VAR>α : Type u_2<VAR>InvolutiveInv α<VAR>s t : Set α<GOAL>s⁻¹ ⊆ t⁻¹ ↔ s ⊆ t
<VAR>α : Type u_2<VAR>InvolutiveNeg α<VAR>s t : Set α<GOAL>-s ⊆ t ↔ s ⊆ -t
<VAR>α : Type u_2<VAR>InvolutiveInv α<VAR>s t : Set α<GOAL>s⁻¹ ⊆ t ↔ s ⊆ t⁻¹
<VAR>α : Type u_2<VAR>InvolutiveNeg α<VAR>a : α<GOAL>-{a} = {-a}
<VAR>α : Type u_2<VAR>InvolutiveInv α<VAR>a : α<GOAL>{a}⁻¹ = {a⁻¹}
<VAR>α : Type u_2<VAR>InvolutiveNeg α<VAR>a : α<VAR>s : Set α<GOAL>-insert a s = insert (-a) (-s)
<VAR>α : Type u_2<VAR>InvolutiveInv α<VAR>a : α<VAR>s : Set α<GOAL>(insert a s)⁻¹ = insert a⁻¹ s⁻¹
<VAR>α : Type u_2<VAR>InvolutiveNeg α<VAR>ι : Sort u_5<VAR>f : ι → α<GOAL>-Set.range f = Set.range fun i => -f i
<VAR>α : Type u_2<VAR>InvolutiveInv α<VAR>ι : Sort u_5<VAR>f : ι → α<GOAL>(Set.range f)⁻¹ = Set.range fun i => (f i)⁻¹
<VAR>α : Type u_2<VAR>InvolutiveNeg α<VAR>s : Set α<GOAL>AddOpposite.op '' (-s) = -AddOpposite.op '' s
<VAR>α : Type u_2<VAR>InvolutiveInv α<VAR>s : Set α<GOAL>MulOpposite.op '' s⁻¹ = (MulOpposite.op '' s)⁻¹
<VAR>α : Type u_2<VAR>Add α<VAR>s t : Set α<GOAL>Set.image2 (fun x x_1 => x + x_1) s t = s + t
<VAR>α : Type u_2<VAR>Mul α<VAR>s t : Set α<GOAL>Set.image2 (fun x x_1 => x * x_1) s t = s * t
<VAR>α : Type u_2<VAR>Mul α<VAR>s t : Set α<VAR>a : α<GOAL>a ∈ s * t ↔ ∃ x ∈ s, ∃ y ∈ t, x * y = a
<VAR>α : Type u_2<VAR>Add α<VAR>s t : Set α<VAR>a : α<GOAL>a ∈ s + t ↔ ∃ x ∈ s, ∃ y ∈ t, x + y = a
<VAR>α : Type u_2<VAR>Add α<VAR>s t : Set α<VAR>a b : α<GOAL>a ∈ s → b ∈ t → a + b ∈ s + t
<VAR>α : Type u_2<VAR>Mul α<VAR>s t : Set α<VAR>a b : α<GOAL>a ∈ s → b ∈ t → a * b ∈ s * t
<VAR>α : Type u_2<VAR>Add α<VAR>s t : Set α<GOAL>(fun x => x.1 + x.2) '' s ×ˢ t = s + t
<VAR>α : Type u_2<VAR>Mul α<VAR>s t : Set α<GOAL>(fun x => x.1 * x.2) '' s ×ˢ t = s * t
<VAR>α : Type u_2<VAR>Mul α<VAR>s : Set α<GOAL>∅ * s = ∅
<VAR>α : Type u_2<VAR>Add α<VAR>s : Set α<GOAL>∅ + s = ∅
<VAR>α : Type u_2<VAR>Mul α<VAR>s : Set α<GOAL>s * ∅ = ∅
<VAR>α : Type u_2<VAR>Add α<VAR>s : Set α<GOAL>s + ∅ = ∅
<VAR>α : Type u_2<VAR>Add α<VAR>s t : Set α<GOAL>s + t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>Mul α<VAR>s t : Set α<GOAL>s * t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>Mul α<VAR>s t : Set α<GOAL>(s * t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_2<VAR>Add α<VAR>s t : Set α<GOAL>(s + t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_2<VAR>Add α<VAR>s t : Set α<GOAL>s.Nonempty → t.Nonempty → (s + t).Nonempty
<VAR>α : Type u_2<VAR>Mul α<VAR>s t : Set α<GOAL>s.Nonempty → t.Nonempty → (s * t).Nonempty
<VAR>α : Type u_2<VAR>Add α<VAR>s t : Set α<GOAL>(s + t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>Mul α<VAR>s t : Set α<GOAL>(s * t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>Add α<VAR>s t : Set α<GOAL>(s + t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>Mul α<VAR>s t : Set α<GOAL>(s * t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>Add α<VAR>s : Set α<VAR>b : α<GOAL>s + {b} = (fun x => x + b) '' s
<VAR>α : Type u_2<VAR>Mul α<VAR>s : Set α<VAR>b : α<GOAL>s * {b} = (fun x => x * b) '' s
<VAR>α : Type u_2<VAR>Mul α<VAR>t : Set α<VAR>a : α<GOAL>{a} * t = (fun x => a * x) '' t
<VAR>α : Type u_2<VAR>Add α<VAR>t : Set α<VAR>a : α<GOAL>{a} + t = (fun x => a + x) '' t
<VAR>α : Type u_2<VAR>Add α<VAR>a b : α<GOAL>{a} + {b} = {a + b}
<VAR>α : Type u_2<VAR>Mul α<VAR>a b : α<GOAL>{a} * {b} = {a * b}
<VAR>α : Type u_2<VAR>Add α<VAR>s₁ s₂ t₁ t₂ : Set α<GOAL>s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ + s₂ ⊆ t₁ + t₂
<VAR>α : Type u_2<VAR>Mul α<VAR>s₁ s₂ t₁ t₂ : Set α<GOAL>s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ * s₂ ⊆ t₁ * t₂
<VAR>α : Type u_2<VAR>Mul α<VAR>s t₁ t₂ : Set α<GOAL>t₁ ⊆ t₂ → s * t₁ ⊆ s * t₂
<VAR>α : Type u_2<VAR>Add α<VAR>s t₁ t₂ : Set α<GOAL>t₁ ⊆ t₂ → s + t₁ ⊆ s + t₂
<VAR>α : Type u_2<VAR>Add α<VAR>s₁ s₂ t : Set α<GOAL>s₁ ⊆ s₂ → s₁ + t ⊆ s₂ + t
<VAR>α : Type u_2<VAR>Mul α<VAR>s₁ s₂ t : Set α<GOAL>s₁ ⊆ s₂ → s₁ * t ⊆ s₂ * t
<VAR>α : Type u_2<VAR>Add α<VAR>s t u : Set α<GOAL>s + t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x + y ∈ u
<VAR>α : Type u_2<VAR>Mul α<VAR>s t u : Set α<GOAL>s * t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x * y ∈ u
<VAR>α : Type u_2<VAR>Add α<VAR>s₁ s₂ t : Set α<GOAL>s₁ ∪ s₂ + t = s₁ + t ∪ (s₂ + t)
<VAR>α : Type u_2<VAR>Mul α<VAR>s₁ s₂ t : Set α<GOAL>(s₁ ∪ s₂) * t = s₁ * t ∪ s₂ * t
<VAR>α : Type u_2<VAR>Mul α<VAR>s t₁ t₂ : Set α<GOAL>s * (t₁ ∪ t₂) = s * t₁ ∪ s * t₂
<VAR>α : Type u_2<VAR>Add α<VAR>s t₁ t₂ : Set α<GOAL>s + (t₁ ∪ t₂) = s + t₁ ∪ (s + t₂)
<VAR>α : Type u_2<VAR>Add α<VAR>s₁ s₂ t : Set α<GOAL>s₁ ∩ s₂ + t ⊆ (s₁ + t) ∩ (s₂ + t)
<VAR>α : Type u_2<VAR>Mul α<VAR>s₁ s₂ t : Set α<GOAL>s₁ ∩ s₂ * t ⊆ s₁ * t ∩ (s₂ * t)
<VAR>α : Type u_2<VAR>Mul α<VAR>s t₁ t₂ : Set α<GOAL>s * (t₁ ∩ t₂) ⊆ s * t₁ ∩ (s * t₂)
<VAR>α : Type u_2<VAR>Add α<VAR>s t₁ t₂ : Set α<GOAL>s + t₁ ∩ t₂ ⊆ (s + t₁) ∩ (s + t₂)
<VAR>α : Type u_2<VAR>Add α<VAR>s₁ s₂ t₁ t₂ : Set α<GOAL>s₁ ∩ s₂ + (t₁ ∪ t₂) ⊆ s₁ + t₁ ∪ (s₂ + t₂)
<VAR>α : Type u_2<VAR>Mul α<VAR>s₁ s₂ t₁ t₂ : Set α<GOAL>s₁ ∩ s₂ * (t₁ ∪ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂
<VAR>α : Type u_2<VAR>Add α<VAR>s₁ s₂ t₁ t₂ : Set α<GOAL>s₁ ∪ s₂ + t₁ ∩ t₂ ⊆ s₁ + t₁ ∪ (s₂ + t₂)
<VAR>α : Type u_2<VAR>Mul α<VAR>s₁ s₂ t₁ t₂ : Set α<GOAL>(s₁ ∪ s₂) * (t₁ ∩ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂
<VAR>α : Type u_2<VAR>Add α<VAR>s t : Set α<GOAL>⋃ a ∈ s, (fun x => a + x) '' t = s + t
<VAR>α : Type u_2<VAR>Mul α<VAR>s t : Set α<GOAL>⋃ a ∈ s, (fun x => a * x) '' t = s * t
<VAR>α : Type u_2<VAR>Mul α<VAR>s t : Set α<GOAL>⋃ a ∈ t, (fun x => x * a) '' s = s * t
<VAR>α : Type u_2<VAR>Add α<VAR>s t : Set α<GOAL>⋃ a ∈ t, (fun x => x + a) '' s = s + t
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Mul α<VAR>s : ι → Set α<VAR>t : Set α<GOAL>(⋃ i, s i) * t = ⋃ i, s i * t
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Add α<VAR>s : ι → Set α<VAR>t : Set α<GOAL>(⋃ i, s i) + t = ⋃ i, s i + t
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Add α<VAR>s : Set α<VAR>t : ι → Set α<GOAL>s + ⋃ i, t i = ⋃ i, s + t i
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Mul α<VAR>s : Set α<VAR>t : ι → Set α<GOAL>s * ⋃ i, t i = ⋃ i, s * t i
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>Mul α<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set α<GOAL>(⋃ i, ⋃ j, s i j) * t = ⋃ i, ⋃ j, s i j * t
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>Add α<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set α<GOAL>(⋃ i, ⋃ j, s i j) + t = ⋃ i, ⋃ j, s i j + t
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>Mul α<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set α<GOAL>s * ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s * t i j
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>Add α<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set α<GOAL>s + ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s + t i j
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Add α<VAR>s : ι → Set α<VAR>t : Set α<GOAL>(⋂ i, s i) + t ⊆ ⋂ i, s i + t
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Mul α<VAR>s : ι → Set α<VAR>t : Set α<GOAL>(⋂ i, s i) * t ⊆ ⋂ i, s i * t
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Add α<VAR>s : Set α<VAR>t : ι → Set α<GOAL>s + ⋂ i, t i ⊆ ⋂ i, s + t i
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Mul α<VAR>s : Set α<VAR>t : ι → Set α<GOAL>s * ⋂ i, t i ⊆ ⋂ i, s * t i
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>Mul α<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set α<GOAL>(⋂ i, ⋂ j, s i j) * t ⊆ ⋂ i, ⋂ j, s i j * t
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>Add α<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set α<GOAL>(⋂ i, ⋂ j, s i j) + t ⊆ ⋂ i, ⋂ j, s i j + t
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>Add α<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set α<GOAL>s + ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, s + t i j
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>Mul α<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set α<GOAL>s * ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, s * t i j
<VAR>α : Type u_2<VAR>Mul α<GOAL>⇑Set.singletonMulHom = singleton
<VAR>α : Type u_2<VAR>Add α<GOAL>⇑Set.singletonAddHom = singleton
<VAR>α : Type u_2<VAR>Add α<VAR>a : α<GOAL>Set.singletonAddHom a = {a}
<VAR>α : Type u_2<VAR>Mul α<VAR>a : α<GOAL>Set.singletonMulHom a = {a}
<VAR>α : Type u_2<VAR>Mul α<VAR>s t : Set α<GOAL>MulOpposite.op '' (s * t) = MulOpposite.op '' t * MulOpposite.op '' s
<VAR>α : Type u_2<VAR>Add α<VAR>s t : Set α<GOAL>AddOpposite.op '' (s + t) = AddOpposite.op '' t + AddOpposite.op '' s
<VAR>α : Type u_2<VAR>Div α<VAR>s t : Set α<GOAL>Set.image2 Div.div s t = s / t
<VAR>α : Type u_2<VAR>Sub α<VAR>s t : Set α<GOAL>Set.image2 Sub.sub s t = s - t
<VAR>α : Type u_2<VAR>Sub α<VAR>s t : Set α<VAR>a : α<GOAL>a ∈ s - t ↔ ∃ x ∈ s, ∃ y ∈ t, x - y = a
<VAR>α : Type u_2<VAR>Div α<VAR>s t : Set α<VAR>a : α<GOAL>a ∈ s / t ↔ ∃ x ∈ s, ∃ y ∈ t, x / y = a
<VAR>α : Type u_2<VAR>Div α<VAR>s t : Set α<VAR>a b : α<GOAL>a ∈ s → b ∈ t → a / b ∈ s / t
<VAR>α : Type u_2<VAR>Sub α<VAR>s t : Set α<VAR>a b : α<GOAL>a ∈ s → b ∈ t → a - b ∈ s - t
<VAR>α : Type u_2<VAR>Div α<VAR>s t : Set α<GOAL>(fun x => x.1 / x.2) '' s ×ˢ t = s / t
<VAR>α : Type u_2<VAR>Sub α<VAR>s t : Set α<GOAL>(fun x => x.1 - x.2) '' s ×ˢ t = s - t
<VAR>α : Type u_2<VAR>Div α<VAR>s : Set α<GOAL>∅ / s = ∅
<VAR>α : Type u_2<VAR>Sub α<VAR>s : Set α<GOAL>∅ - s = ∅
<VAR>α : Type u_2<VAR>Div α<VAR>s : Set α<GOAL>s / ∅ = ∅
<VAR>α : Type u_2<VAR>Sub α<VAR>s : Set α<GOAL>s - ∅ = ∅
<VAR>α : Type u_2<VAR>Sub α<VAR>s t : Set α<GOAL>s - t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>Div α<VAR>s t : Set α<GOAL>s / t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>Div α<VAR>s t : Set α<GOAL>(s / t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_2<VAR>Sub α<VAR>s t : Set α<GOAL>(s - t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_2<VAR>Sub α<VAR>s t : Set α<GOAL>s.Nonempty → t.Nonempty → (s - t).Nonempty
<VAR>α : Type u_2<VAR>Div α<VAR>s t : Set α<GOAL>s.Nonempty → t.Nonempty → (s / t).Nonempty
<VAR>α : Type u_2<VAR>Div α<VAR>s t : Set α<GOAL>(s / t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>Sub α<VAR>s t : Set α<GOAL>(s - t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>Div α<VAR>s t : Set α<GOAL>(s / t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>Sub α<VAR>s t : Set α<GOAL>(s - t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>Sub α<VAR>s : Set α<VAR>b : α<GOAL>s - {b} = (fun x => x - b) '' s
<VAR>α : Type u_2<VAR>Div α<VAR>s : Set α<VAR>b : α<GOAL>s / {b} = (fun x => x / b) '' s
<VAR>α : Type u_2<VAR>Div α<VAR>t : Set α<VAR>a : α<GOAL>{a} / t = (fun x x_1 => x / x_1) a '' t
<VAR>α : Type u_2<VAR>Sub α<VAR>t : Set α<VAR>a : α<GOAL>{a} - t = (fun x x_1 => x - x_1) a '' t
<VAR>α : Type u_2<VAR>Div α<VAR>a b : α<GOAL>{a} / {b} = {a / b}
<VAR>α : Type u_2<VAR>Sub α<VAR>a b : α<GOAL>{a} - {b} = {a - b}
<VAR>α : Type u_2<VAR>Sub α<VAR>s₁ s₂ t₁ t₂ : Set α<GOAL>s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ - s₂ ⊆ t₁ - t₂
<VAR>α : Type u_2<VAR>Div α<VAR>s₁ s₂ t₁ t₂ : Set α<GOAL>s₁ ⊆ t₁ → s₂ ⊆ t₂ → s₁ / s₂ ⊆ t₁ / t₂
<VAR>α : Type u_2<VAR>Div α<VAR>s t₁ t₂ : Set α<GOAL>t₁ ⊆ t₂ → s / t₁ ⊆ s / t₂
<VAR>α : Type u_2<VAR>Sub α<VAR>s t₁ t₂ : Set α<GOAL>t₁ ⊆ t₂ → s - t₁ ⊆ s - t₂
<VAR>α : Type u_2<VAR>Sub α<VAR>s₁ s₂ t : Set α<GOAL>s₁ ⊆ s₂ → s₁ - t ⊆ s₂ - t
<VAR>α : Type u_2<VAR>Div α<VAR>s₁ s₂ t : Set α<GOAL>s₁ ⊆ s₂ → s₁ / t ⊆ s₂ / t
<VAR>α : Type u_2<VAR>Div α<VAR>s t u : Set α<GOAL>s / t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x / y ∈ u
<VAR>α : Type u_2<VAR>Sub α<VAR>s t u : Set α<GOAL>s - t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x - y ∈ u
<VAR>α : Type u_2<VAR>Sub α<VAR>s₁ s₂ t : Set α<GOAL>s₁ ∪ s₂ - t = s₁ - t ∪ (s₂ - t)
<VAR>α : Type u_2<VAR>Div α<VAR>s₁ s₂ t : Set α<GOAL>(s₁ ∪ s₂) / t = s₁ / t ∪ s₂ / t
<VAR>α : Type u_2<VAR>Div α<VAR>s t₁ t₂ : Set α<GOAL>s / (t₁ ∪ t₂) = s / t₁ ∪ s / t₂
<VAR>α : Type u_2<VAR>Sub α<VAR>s t₁ t₂ : Set α<GOAL>s - (t₁ ∪ t₂) = s - t₁ ∪ (s - t₂)
<VAR>α : Type u_2<VAR>Sub α<VAR>s₁ s₂ t : Set α<GOAL>s₁ ∩ s₂ - t ⊆ (s₁ - t) ∩ (s₂ - t)
<VAR>α : Type u_2<VAR>Div α<VAR>s₁ s₂ t : Set α<GOAL>s₁ ∩ s₂ / t ⊆ s₁ / t ∩ (s₂ / t)
<VAR>α : Type u_2<VAR>Sub α<VAR>s t₁ t₂ : Set α<GOAL>s - t₁ ∩ t₂ ⊆ (s - t₁) ∩ (s - t₂)
<VAR>α : Type u_2<VAR>Div α<VAR>s t₁ t₂ : Set α<GOAL>s / (t₁ ∩ t₂) ⊆ s / t₁ ∩ (s / t₂)
<VAR>α : Type u_2<VAR>Sub α<VAR>s₁ s₂ t₁ t₂ : Set α<GOAL>s₁ ∩ s₂ - (t₁ ∪ t₂) ⊆ s₁ - t₁ ∪ (s₂ - t₂)
<VAR>α : Type u_2<VAR>Div α<VAR>s₁ s₂ t₁ t₂ : Set α<GOAL>s₁ ∩ s₂ / (t₁ ∪ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂
<VAR>α : Type u_2<VAR>Div α<VAR>s₁ s₂ t₁ t₂ : Set α<GOAL>(s₁ ∪ s₂) / (t₁ ∩ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂
<VAR>α : Type u_2<VAR>Sub α<VAR>s₁ s₂ t₁ t₂ : Set α<GOAL>s₁ ∪ s₂ - t₁ ∩ t₂ ⊆ s₁ - t₁ ∪ (s₂ - t₂)
<VAR>α : Type u_2<VAR>Sub α<VAR>s t : Set α<GOAL>⋃ a ∈ s, (fun x => a - x) '' t = s - t
<VAR>α : Type u_2<VAR>Div α<VAR>s t : Set α<GOAL>⋃ a ∈ s, (fun x => a / x) '' t = s / t
<VAR>α : Type u_2<VAR>Sub α<VAR>s t : Set α<GOAL>⋃ a ∈ t, (fun x => x - a) '' s = s - t
<VAR>α : Type u_2<VAR>Div α<VAR>s t : Set α<GOAL>⋃ a ∈ t, (fun x => x / a) '' s = s / t
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Div α<VAR>s : ι → Set α<VAR>t : Set α<GOAL>(⋃ i, s i) / t = ⋃ i, s i / t
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Sub α<VAR>s : ι → Set α<VAR>t : Set α<GOAL>(⋃ i, s i) - t = ⋃ i, s i - t
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Sub α<VAR>s : Set α<VAR>t : ι → Set α<GOAL>s - ⋃ i, t i = ⋃ i, s - t i
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Div α<VAR>s : Set α<VAR>t : ι → Set α<GOAL>s / ⋃ i, t i = ⋃ i, s / t i
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>Div α<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set α<GOAL>(⋃ i, ⋃ j, s i j) / t = ⋃ i, ⋃ j, s i j / t
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>Sub α<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set α<GOAL>(⋃ i, ⋃ j, s i j) - t = ⋃ i, ⋃ j, s i j - t
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>Div α<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set α<GOAL>s / ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s / t i j
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>Sub α<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set α<GOAL>s - ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s - t i j
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Div α<VAR>s : ι → Set α<VAR>t : Set α<GOAL>(⋂ i, s i) / t ⊆ ⋂ i, s i / t
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Sub α<VAR>s : ι → Set α<VAR>t : Set α<GOAL>(⋂ i, s i) - t ⊆ ⋂ i, s i - t
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Sub α<VAR>s : Set α<VAR>t : ι → Set α<GOAL>s - ⋂ i, t i ⊆ ⋂ i, s - t i
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>Div α<VAR>s : Set α<VAR>t : ι → Set α<GOAL>s / ⋂ i, t i ⊆ ⋂ i, s / t i
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>Sub α<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set α<GOAL>(⋂ i, ⋂ j, s i j) - t ⊆ ⋂ i, ⋂ j, s i j - t
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>Div α<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set α<GOAL>(⋂ i, ⋂ j, s i j) / t ⊆ ⋂ i, ⋂ j, s i j / t
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>Div α<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set α<GOAL>s / ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, s / t i j
<VAR>α : Type u_2<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>Sub α<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set α<GOAL>s - ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, s - t i j
<VAR>α : Type u_2<VAR>CommSemigroup α<VAR>s t : Set α<GOAL>s ∩ t * (s ∪ t) ⊆ s * t
<VAR>α : Type u_2<VAR>AddCommSemigroup α<VAR>s t : Set α<GOAL>s ∩ t + (s ∪ t) ⊆ s + t
<VAR>α : Type u_2<VAR>CommSemigroup α<VAR>s t : Set α<GOAL>(s ∪ t) * (s ∩ t) ⊆ s * t
<VAR>α : Type u_2<VAR>AddCommSemigroup α<VAR>s t : Set α<GOAL>s ∪ t + s ∩ t ⊆ s + t
<VAR>α : Type u_2<VAR>AddZeroClass α<VAR>s : Set α<VAR>t : Set α<VAR>ht : 0 ∈ t<GOAL>s ⊆ s + t
<VAR>α : Type u_2<VAR>MulOneClass α<VAR>s : Set α<VAR>t : Set α<VAR>ht : 1 ∈ t<GOAL>s ⊆ s * t
<VAR>α : Type u_2<VAR>MulOneClass α<VAR>s : Set α<VAR>t : Set α<VAR>hs : 1 ∈ s<GOAL>t ⊆ s * t
<VAR>α : Type u_2<VAR>AddZeroClass α<VAR>s : Set α<VAR>t : Set α<VAR>hs : 0 ∈ s<GOAL>t ⊆ s + t
<VAR>α : Type u_2<VAR>MulOneClass α<GOAL>⇑Set.singletonMonoidHom = singleton
<VAR>α : Type u_2<VAR>AddZeroClass α<GOAL>⇑Set.singletonAddMonoidHom = singleton
<VAR>α : Type u_2<VAR>AddZeroClass α<VAR>a : α<GOAL>Set.singletonAddMonoidHom a = {a}
<VAR>α : Type u_2<VAR>MulOneClass α<VAR>a : α<GOAL>Set.singletonMonoidHom a = {a}
<VAR>α : Type u_2<VAR>Monoid α<VAR>s : Set α<VAR>a : α<VAR>ha : a ∈ s<VAR>n : ℕ<GOAL>a ^ n ∈ s ^ n
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>s : Set α<VAR>a : α<VAR>ha : a ∈ s<VAR>n : ℕ<GOAL>n • a ∈ n • s
<VAR>α : Type u_2<VAR>Monoid α<VAR>s t : Set α<VAR>hst : s ⊆ t<VAR>n : ℕ<GOAL>s ^ n ⊆ t ^ n
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>s t : Set α<VAR>hst : s ⊆ t<VAR>n : ℕ<GOAL>n • s ⊆ n • t
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>s : Set α<VAR>m n : ℕ<VAR>hs : 0 ∈ s<VAR>hn : m ≤ n<GOAL>m • s ⊆ n • s
<VAR>α : Type u_2<VAR>Monoid α<VAR>s : Set α<VAR>m n : ℕ<VAR>hs : 1 ∈ s<VAR>hn : m ≤ n<GOAL>s ^ m ⊆ s ^ n
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>n • ∅ = ∅
<VAR>α : Type u_2<VAR>Monoid α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>∅ ^ n = ∅
<VAR>α : Type u_2<VAR>Monoid α<VAR>s : Set α<VAR>hs : 1 ∈ s<GOAL>s * Set.univ = Set.univ
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>s : Set α<VAR>hs : 0 ∈ s<GOAL>s + Set.univ = Set.univ
<VAR>α : Type u_2<VAR>Monoid α<VAR>t : Set α<VAR>ht : 1 ∈ t<GOAL>Set.univ * t = Set.univ
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>t : Set α<VAR>ht : 0 ∈ t<GOAL>Set.univ + t = Set.univ
<VAR>α : Type u_2<VAR>AddMonoid α<GOAL>Set.univ + Set.univ = Set.univ
<VAR>α : Type u_2<VAR>Monoid α<GOAL>Set.univ * Set.univ = Set.univ
<VAR>α : Type u_5<VAR>AddMonoid α<VAR>n : ℕ<GOAL>n ≠ 0 → n • Set.univ = Set.univ
<VAR>α : Type u_2<VAR>Monoid α<VAR>n : ℕ<GOAL>n ≠ 0 → Set.univ ^ n = Set.univ
<VAR>α : Type u_2<VAR>Monoid α<VAR>a : α<GOAL>IsUnit a → IsUnit {a}
<VAR>α : Type u_2<VAR>AddMonoid α<VAR>a : α<GOAL>IsAddUnit a → IsAddUnit {a}