ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>s t : Set α<VAR>x : α<VAR>h1 : x ∈ s<VAR>h2 : ¬x ∈ t<GOAL>x ∈ s \ t
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set β<VAR>a : α<GOAL>a ∈ f ⁻¹' s ↔ f a ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<VAR>y : β<GOAL>y ∈ f '' s ↔ ∃ x, x ∈ s ∧ f x = y
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : α<VAR>a : Set α<VAR>h : x ∈ a<GOAL>f x ∈ f '' a
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set β<VAR>t : Set α<VAR>f : α → β<GOAL>s ⊆ Set.kernImage f t ↔ f ⁻¹' s ⊆ t
<VAR>α : Type u<VAR>ι : Sort u_1<VAR>f : ι → α<VAR>x : α<GOAL>x ∈ Set.range f ↔ ∃ y, f y = x
<VAR>α : Type u<VAR>ι : Sort u_1<VAR>f : ι → α<VAR>i : ι<GOAL>f i ∈ Set.range f
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x : ↑(Set.range f)<GOAL>f (Set.rangeSplitting f x) = ↑x
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<GOAL>f ∘ Set.rangeSplitting f = Subtype.val
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>t : Set β<GOAL>s ×ˢ t = Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>t : Set β<VAR>p : α × β<GOAL>(p ∈ s ×ˢ t) = (p.fst ∈ s ∧ p.snd ∈ t)
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>t : Set β<VAR>p : α × β<GOAL>p ∈ s ×ˢ t ↔ p.fst ∈ s ∧ p.snd ∈ t
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>b : β<VAR>s : Set α<VAR>t : Set β<GOAL>((a, b) ∈ s ×ˢ t) = (a ∈ s ∧ b ∈ t)
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>b : β<VAR>s : Set α<VAR>t : Set β<VAR>ha : a ∈ s<VAR>hb : b ∈ t<GOAL>(a, b) ∈ s ×ˢ t
<VAR>α : Type u<VAR>x : α<GOAL>(x, x) ∈ Set.diagonal α
<VAR>α : Type u<VAR>x : α × α<GOAL>x ∈ Set.diagonal α ↔ x.fst = x.snd
<VAR>α : Type u<VAR>x : α × α<VAR>s : Set α<GOAL>x ∈ s.offDiag ↔ x.fst ∈ s ∧ x.snd ∈ s ∧ x.fst ≠ x.snd
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>s : Set ι<VAR>t : (i : ι) → Set (α i)<VAR>f : (i : ι) → α i<GOAL>f ∈ s.pi t ↔ ∀ (i : ι), i ∈ s → f i ∈ t i
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>t : (i : ι) → Set (α i)<VAR>f : (i : ι) → α i<GOAL>f ∈ Set.univ.pi t ↔ ∀ (i : ι), f i ∈ t i
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s : Set α<GOAL>Set.MapsTo f s (f '' s)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>t : Set β<GOAL>Set.MapsTo f (f ⁻¹' t) t
<VAR>α : Type u<VAR>β : Type v<VAR>t : Set β<VAR>f : α → β<GOAL>∀ (a : ↑(f ⁻¹' t)), ↑(t.restrictPreimage f a) = f ↑a
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>c : γ<GOAL>c ∈ Set.image2 f s t ↔ ∃ a, a ∈ s ∧ ∃ b, b ∈ t ∧ f a b = c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>ha : a ∈ s<VAR>hb : b ∈ t<GOAL>f a b ∈ Set.image2 f s t
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set (α → β)<VAR>t : Set α<VAR>b : β<GOAL>b ∈ s.seq t ↔ ∃ f, f ∈ s ∧ ∃ a, a ∈ t ∧ f a = b
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set (α → β)<VAR>t : Set α<GOAL>s.seq t = Set.image2 (fun f a => f a) s t
<VAR>α : Type u_1<VAR>sel : Set α → Option α<VAR>s : Set α<VAR>h : sel s = none<VAR>n : ℕ<GOAL>Set.enumerate sel s n = none
<VAR>α : Type u_1<VAR>sel : Set α → Option α<VAR>s : Set α<VAR>n₁ n₂ : ℕ<GOAL>Set.enumerate sel s n₁ = none → n₁ ≤ n₂ → Set.enumerate sel s n₂ = none
<VAR>α : Type u_1<VAR>sel : Set α → Option α<VAR>h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s<VAR>s : Set α<VAR>n : ℕ<VAR>a : α<GOAL>Set.enumerate sel s n = some a → a ∈ s
<VAR>α : Type u_1<VAR>sel : Set α → Option α<VAR>n₁ n₂ : ℕ<VAR>a : α<VAR>s : Set α<VAR>h_sel : ∀ (s : Set α) (a : α), sel s = some a → a ∈ s<VAR>h₁ : Set.enumerate sel s n₁ = some a<VAR>h₂ : Set.enumerate sel s n₂ = some a<GOAL>n₁ = n₂
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<VAR>hf : Function.Injective2 f<GOAL>f a b ∈ Set.image2 f s t ↔ a ∈ s ∧ b ∈ t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s s' : Set α<VAR>t t' : Set β<VAR>hs : s ⊆ s'<VAR>ht : t ⊆ t'<GOAL>Set.image2 f s t ⊆ Set.image2 f s' t'
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t t' : Set β<VAR>ht : t ⊆ t'<GOAL>Set.image2 f s t ⊆ Set.image2 f s t'
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s s' : Set α<VAR>t : Set β<VAR>hs : s ⊆ s'<GOAL>Set.image2 f s t ⊆ Set.image2 f s' t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>b : β<VAR>hb : b ∈ t<GOAL>(fun a => f a b) '' s ⊆ Set.image2 f s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>ha : a ∈ s<GOAL>f a '' t ⊆ Set.image2 f s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>p : γ → Prop<GOAL>(∀ z ∈ Set.image2 f s t, p z) ↔ ∀ x ∈ s, ∀ y ∈ t, p (f x y)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>u : Set γ<GOAL>Set.image2 f s t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, f x y ∈ u
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>u : Set γ<GOAL>Set.image2 f s t ⊆ u ↔ ∀ a ∈ s, (fun b => f a b) '' t ⊆ u
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>u : Set γ<GOAL>Set.image2 f s t ⊆ u ↔ ∀ b ∈ t, (fun a => f a b) '' s ⊆ u
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>(fun x => f x.1 x.2) '' s ×ˢ t = Set.image2 f s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>Function.uncurry f '' s ×ˢ t = Set.image2 f s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>s : Set α<VAR>t : Set β<GOAL>Set.image2 Prod.mk s t = s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α × β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>Set.image2 (fun a b => f (a, b)) s t = f '' s ×ˢ t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>Set.image2 f s t = Set.image2 (fun a b => f b a) t s
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s s' : Set α<VAR>t : Set β<GOAL>Set.image2 f (s ∪ s') t = Set.image2 f s t ∪ Set.image2 f s' t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t t' : Set β<GOAL>Set.image2 f s (t ∪ t') = Set.image2 f s t ∪ Set.image2 f s t'
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s s' : Set α<VAR>t : Set β<VAR>hf : Function.Injective2 f<GOAL>Set.image2 f (s ∩ s') t = Set.image2 f s t ∩ Set.image2 f s' t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t t' : Set β<VAR>hf : Function.Injective2 f<GOAL>Set.image2 f s (t ∩ t') = Set.image2 f s t ∩ Set.image2 f s t'
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>t : Set β<GOAL>Set.image2 f ∅ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<GOAL>Set.image2 f s ∅ = ∅
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>s.Nonempty → t.Nonempty → (Set.image2 f s t).Nonempty
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>(Set.image2 f s t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h : (Set.image2 f s t).Nonempty<GOAL>s.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h : (Set.image2 f s t).Nonempty<GOAL>t.Nonempty
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>Set.image2 f s t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>s : Set α<VAR>t : Set β<VAR>hs : s.Subsingleton<VAR>ht : t.Subsingleton<VAR>f : α → β → γ<GOAL>(Set.image2 f s t).Subsingleton
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s s' : Set α<VAR>t : Set β<GOAL>Set.image2 f (s ∩ s') t ⊆ Set.image2 f s t ∩ Set.image2 f s' t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t t' : Set β<GOAL>Set.image2 f s (t ∩ t') ⊆ Set.image2 f s t ∩ Set.image2 f s t'
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>t : Set β<VAR>a : α<GOAL>Set.image2 f {a} t = f a '' t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>b : β<GOAL>Set.image2 f s {b} = (fun a => f a b) '' s
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>a : α<VAR>b : β<GOAL>Set.image2 f {a} {b} = {f a b}
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a : α<GOAL>Set.image2 f (insert a s) t = (fun b => f a b) '' t ∪ Set.image2 f s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>b : β<GOAL>Set.image2 f s (insert b t) = (fun a => f a b) '' s ∪ Set.image2 f s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f f' : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h : ∀ a ∈ s, ∀ b ∈ t, f a b = f' a b<GOAL>Set.image2 f s t = Set.image2 f' s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f f' : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>h : ∀ (a : α) (b : β), f a b = f' a b<GOAL>Set.image2 f s t = Set.image2 f' s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β → γ<VAR>g : γ → δ<GOAL>g '' Set.image2 f s t = Set.image2 (fun a b => g (f a b)) s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>s : Set α<VAR>t : Set β<VAR>f : γ → β → δ<VAR>g : α → γ<GOAL>Set.image2 f (g '' s) t = Set.image2 (fun a b => f (g a) b) s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>s : Set α<VAR>t : Set β<VAR>f : α → γ → δ<VAR>g : β → γ<GOAL>Set.image2 f s (g '' t) = Set.image2 (fun a b => f a (g b)) s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>h : t.Nonempty<GOAL>Set.image2 (fun x x_1 => x) s t = s
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>h : s.Nonempty<GOAL>Set.image2 (fun x y => y) s t = t
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>f : α' → β' → γ<VAR>g : α → α'<VAR>h : β → β'<GOAL>Set.image2 f (Set.range g) (Set.range h) = Set.range fun x => f (g x.1) (h x.2)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>s : Set α<VAR>t : Set β<VAR>u : Set γ<VAR>f : δ → γ → ε<VAR>g : α → β → δ<VAR>f' : α → ε' → ε<VAR>g' : β → γ → ε'<VAR>h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)<GOAL>Set.image2 f (Set.image2 g s t) u = Set.image2 f' s (Set.image2 g' t u)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>g : β → α → γ<VAR>h_comm : ∀ (a : α) (b : β), f a b = g b a<GOAL>Set.image2 f s t = Set.image2 g t s
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>s : Set α<VAR>t : Set β<VAR>u : Set γ<VAR>f : α → δ → ε<VAR>g : β → γ → δ<VAR>f' : α → γ → δ'<VAR>g' : β → δ' → ε<VAR>h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)<GOAL>Set.image2 f s (Set.image2 g t u) = Set.image2 g' t (Set.image2 f' s u)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>s : Set α<VAR>t : Set β<VAR>u : Set γ<VAR>f : δ → γ → ε<VAR>g : α → β → δ<VAR>f' : α → γ → δ'<VAR>g' : δ' → β → ε<VAR>h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b<GOAL>Set.image2 f (Set.image2 g s t) u = Set.image2 g' (Set.image2 f' s u) t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>s : Set α<VAR>t : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>f : ε → ζ → ν<VAR>g : α → β → ε<VAR>h : γ → δ → ζ<VAR>f' : ε' → ζ' → ν<VAR>g' : α → γ → ε'<VAR>h' : β → δ → ζ'<VAR>h_comm : ∀ (a : α) (b : β) (c : γ) (d : δ), f (g a b) (h c d) = f' (g' a c) (h' b d)<GOAL>Set.image2 f (Set.image2 g s t) (Set.image2 h u v) = Set.image2 f' (Set.image2 g' s u) (Set.image2 h' t v)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>g : γ → δ<VAR>f' : α' → β' → δ<VAR>g₁ : α → α'<VAR>g₂ : β → β'<VAR>h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)<GOAL>g '' Set.image2 f s t = Set.image2 f' (g₁ '' s) (g₂ '' t)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>g : γ → δ<VAR>f' : α' → β → δ<VAR>g' : α → α'<VAR>h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b<GOAL>g '' Set.image2 f s t = Set.image2 f' (g' '' s) t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>g : γ → δ<VAR>f' : α → β' → δ<VAR>g' : β → β'<VAR>h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)<GOAL>g '' Set.image2 f s t = Set.image2 f' s (g' '' t)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>s : Set α<VAR>t : Set β<VAR>f : α' → β → γ<VAR>g : α → α'<VAR>f' : α → β → δ<VAR>g' : δ → γ<VAR>h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)<GOAL>Set.image2 f (g '' s) t = g' '' Set.image2 f' s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β' → γ<VAR>g : β → β'<VAR>f' : α → β → δ<VAR>g' : δ → γ<VAR>h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)<GOAL>Set.image2 f s (g '' t) = g' '' Set.image2 f' s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>ε : Type u_9<VAR>s : Set α<VAR>t : Set β<VAR>u : Set γ<VAR>f : α → δ → ε<VAR>g : β → γ → δ<VAR>f₁ : α → β → β'<VAR>f₂ : α → γ → γ'<VAR>g' : β' → γ' → ε<VAR>h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)<GOAL>Set.image2 f s (Set.image2 g t u) ⊆ Set.image2 g' (Set.image2 f₁ s t) (Set.image2 f₂ s u)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>ε : Type u_9<VAR>s : Set α<VAR>t : Set β<VAR>u : Set γ<VAR>f : δ → γ → ε<VAR>g : α → β → δ<VAR>f₁ : α → γ → α'<VAR>f₂ : β → γ → β'<VAR>g' : α' → β' → ε<VAR>h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)<GOAL>Set.image2 f (Set.image2 g s t) u ⊆ Set.image2 g' (Set.image2 f₁ s u) (Set.image2 f₂ t u)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>g : γ → δ<VAR>f' : β' → α' → δ<VAR>g₁ : β → β'<VAR>g₂ : α → α'<VAR>h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)<GOAL>g '' Set.image2 f s t = Set.image2 f' (g₁ '' t) (g₂ '' s)
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>g : γ → δ<VAR>f' : β' → α → δ<VAR>g' : β → β'<VAR>h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a<GOAL>g '' Set.image2 f s t = Set.image2 f' (g' '' t) s
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>g : γ → δ<VAR>f' : β → α' → δ<VAR>g' : α → α'<VAR>h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)<GOAL>g '' Set.image2 f s t = Set.image2 f' t (g' '' s)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>s : Set α<VAR>t : Set β<VAR>f : α' → β → γ<VAR>g : α → α'<VAR>f' : β → α → δ<VAR>g' : δ → γ<VAR>h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)<GOAL>Set.image2 f (g '' s) t = g' '' Set.image2 f' t s
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_7<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β' → γ<VAR>g : β → β'<VAR>f' : β → α → δ<VAR>g' : δ → γ<VAR>h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)<GOAL>Set.image2 f s (g '' t) = g' '' Set.image2 f' t s
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : α → β → β<VAR>a : α<VAR>h : ∀ (b : β), f a b = b<VAR>t : Set β<GOAL>Set.image2 f {a} t = t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : α → β → α<VAR>b : β<VAR>h : ∀ (a : α), f a b = a<VAR>s : Set α<GOAL>Set.image2 f s {b} = s
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s s' : Set α<VAR>t t' : Set β<GOAL>Set.image2 f (s ∩ s') (t ∪ t') ⊆ Set.image2 f s t ∪ Set.image2 f s' t'
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>γ : Type u_5<VAR>f : α → β → γ<VAR>s s' : Set α<VAR>t t' : Set β<GOAL>Set.image2 f (s ∪ s') (t ∩ t') ⊆ Set.image2 f s t ∪ Set.image2 f s' t'
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : α → α → β<VAR>s t : Set α<VAR>hf : ∀ (a b : α), f a b = f b a<GOAL>Set.image2 f (s ∩ t) (s ∪ t) ⊆ Set.image2 f s t
<VAR>α : Type u_1<VAR>β : Type u_3<VAR>f : α → α → β<VAR>s t : Set α<VAR>hf : ∀ (a b : α), f a b = f b a<GOAL>Set.image2 f (s ∪ t) (s ∩ t) ⊆ Set.image2 f s t
<VAR>α : Type u_1<VAR>s : Set α<VAR>x : α<GOAL>x ∈ s ↔ s.boolIndicator x = true
<VAR>α : Type u_1<VAR>s : Set α<VAR>x : α<GOAL>x ∉ s ↔ s.boolIndicator x = false
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.boolIndicator ⁻¹' {true} = s
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.boolIndicator ⁻¹' {false} = sᶜ
<VAR>α : Type u_1<VAR>s : Set α<VAR>t : Set Bool<GOAL>s.boolIndicator ⁻¹' t = (if true ∈ t then s else ∅) ∪ if false ∈ t then sᶜ else ∅
<VAR>α : Type u_1<VAR>s : Set α<VAR>t : Set Bool<GOAL>s.boolIndicator ⁻¹' t = Set.univ ∨ s.boolIndicator ⁻¹' t = s ∨ s.boolIndicator ⁻¹' t = sᶜ ∨ s.boolIndicator ⁻¹' t = ∅
<VAR>α β : Type u<VAR>s : Set α<VAR>f : α → Set β<GOAL>s >>= f = ⋃ i ∈ s, f i
<VAR>α β : Type u<VAR>s : Set α<VAR>f : α → β<GOAL>f <$> s = f '' s
<VAR>α β : Type u<VAR>s : Set (α → β)<VAR>t : Set α<GOAL>(Seq.seq s fun x => t) = s.seq t
<VAR>α : Type u<VAR>a : α<GOAL>pure a = {a}
<VAR>α β γ : Type u<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>Set.image2 f s t = Seq.seq (f <$> s) fun x => t
<VAR>α : Type u<VAR>β : Set α<VAR>γ : Set ↑β<VAR>a : α<VAR>ha : a ∈ β<VAR>ha' : ⟨a, ha⟩ ∈ γ<GOAL>a ∈ do let a ← γ pure ↑a
<VAR>α : Type u<VAR>β : Set α<VAR>γ : Set ↑β<GOAL>(do let a ← γ pure ↑a) ⊆ β
<VAR>α : Type u<VAR>β : Set α<VAR>γ : Set ↑β<VAR>a : α<VAR>ha : a ∈ do let a ← γ pure ↑a<GOAL>⟨a, ⋯⟩ ∈ γ
<VAR>α : Type u<VAR>β : Set α<VAR>γ : Set ↑β<VAR>hγ : (do let a ← γ pure ↑a) = β<GOAL>γ = Set.univ
<VAR>α : Type u<VAR>β : Set α<VAR>γ : Set ↑β<VAR>δ : Type u_1<VAR>f : α → δ<GOAL>(f '' do let a ← γ pure ↑a) = β.restrict f '' γ
<VAR>α : Type u<VAR>s : Set α<VAR>t : Set ↑s<GOAL>Lean.Internal.coeM t = ↑t
<VAR>α : Type u<VAR>β : Set α<VAR>γ : Set ↑β<VAR>a : α<VAR>ha : a ∈ β<VAR>ha' : ⟨a, ha⟩ ∈ γ<GOAL>a ∈ ↑γ
<VAR>α : Type u<VAR>β : Set α<VAR>γ : Set ↑β<GOAL>↑γ ⊆ β
<VAR>α : Type u<VAR>β : Set α<VAR>γ : Set ↑β<VAR>a : α<VAR>ha : a ∈ ↑γ<GOAL>⟨a, ⋯⟩ ∈ γ
<VAR>α : Type u<VAR>β : Set α<VAR>γ : Set ↑β<VAR>hγ : ↑γ = β<GOAL>γ = Set.univ
<VAR>α : Type u<VAR>β : Set α<VAR>γ : Set ↑β<VAR>δ : Type u_1<VAR>f : α → δ<GOAL>f '' ↑γ = β.restrict f '' γ
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>n : Fin 2<GOAL>(WeierstrassCurve.Affine.CoordinateRing.basis W) n = (AdjoinRoot.powerBasis' ⋯).gen ^ ↑n
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<GOAL>(WeierstrassCurve.Affine.CoordinateRing.basis W) 0 = 1
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<GOAL>(WeierstrassCurve.Affine.CoordinateRing.basis W) 1 = (WeierstrassCurve.Affine.CoordinateRing.mk W) Y
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<GOAL>⇑(WeierstrassCurve.Affine.CoordinateRing.basis W) = ![1, (WeierstrassCurve.Affine.CoordinateRing.mk W) Y]
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x : R[X]<VAR>y : W.CoordinateRing<GOAL>x • y = (WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C x) * y
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>p q : R[X]<VAR>hpq : p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W) Y = 0<GOAL>p = 0 ∧ q = 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x : W.CoordinateRing<GOAL>∃ p q, p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W) Y = x
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>y p q : R[X]<GOAL>(p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W) Y) * (WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C y) = (p * y) • 1 + (q * y) • (WeierstrassCurve.Affine.CoordinateRing.mk W) Y
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>p q : R[X]<GOAL>(p • 1 + q • (WeierstrassCurve.Affine.CoordinateRing.mk W) Y) * (WeierstrassCurve.Affine.CoordinateRing.mk W) Y = (q * (Polynomial.X ^ 3 + Polynomial.C W.a₂ * Polynomial.X ^ 2 + Polynomial.C W.a₄ * Polynomial.X + Polynomial.C W.a₆)) • 1 + (p - q * (Polynomial.C W.a₁ * Polynomial.X + Polynomial.C W.a₃)) • (WeierstrassCurve.Affine.CoordinateRing.mk W) Y
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve.Affine R<VAR>f : R →+* S<VAR>x : R[X][Y]<GOAL>(WeierstrassCurve.Affine.CoordinateRing.map W f) ((WeierstrassCurve.Affine.CoordinateRing.mk W) x) = (WeierstrassCurve.Affine.CoordinateRing.mk (WeierstrassCurve.map W f)) (Polynomial.map (Polynomial.mapRingHom f) x)
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve.Affine R<VAR>f : R →+* S<VAR>x : R[X]<VAR>y : W.CoordinateRing<GOAL>(WeierstrassCurve.Affine.CoordinateRing.map W f) (x • y) = Polynomial.map f x • (WeierstrassCurve.Affine.CoordinateRing.map W f) y
<VAR>R : Type u<VAR>S : Type v<VAR>CommRing R<VAR>CommRing S<VAR>W : WeierstrassCurve.Affine R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<GOAL>Function.Injective ⇑(WeierstrassCurve.Affine.CoordinateRing.map W f)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>Nontrivial R<VAR>x : R<GOAL>WeierstrassCurve.Affine.CoordinateRing.XClass W x ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>Nontrivial R<VAR>y : R[X]<GOAL>WeierstrassCurve.Affine.CoordinateRing.YClass W y ≠ 0
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y L : R<GOAL>(WeierstrassCurve.Affine.CoordinateRing.mk W) (Polynomial.C (W.addPolynomial x y L)) = (WeierstrassCurve.Affine.CoordinateRing.mk W) ((Y - Polynomial.C (WeierstrassCurve.Affine.linePolynomial x y L)) * (W.negPolynomial - Polynomial.C (WeierstrassCurve.Affine.linePolynomial x y L)))
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x y L : R<GOAL>WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x (Polynomial.C y) = WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x (WeierstrassCurve.Affine.linePolynomial x y L)
<VAR>R : Type u<VAR>CommRing R<VAR>W : WeierstrassCurve.Affine R<VAR>x₁ x₂ y₁ L : R<GOAL>WeierstrassCurve.Affine.CoordinateRing.XYIdeal W (W.addX x₁ x₂ L) (Polynomial.C (W.addY x₁ x₂ y₁ L)) = Ideal.span {(WeierstrassCurve.Affine.CoordinateRing.mk W) (W.negPolynomial - Polynomial.C (WeierstrassCurve.Affine.linePolynomial x₁ y₁ L))} ⊔ WeierstrassCurve.Affine.CoordinateRing.XIdeal W (W.addX x₁ x₂ L)
<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.mk W) (Polynomial.C (W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂))) = -(WeierstrassCurve.Affine.CoordinateRing.XClass W x₁ * WeierstrassCurve.Affine.CoordinateRing.XClass W x₂ * WeierstrassCurve.Affine.CoordinateRing.XClass W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)))
<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.XYIdeal W x₂ (Polynomial.C y₂) = WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x₂ (WeierstrassCurve.Affine.linePolynomial 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 W x (Polynomial.C (W.negY x y)) * WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x (Polynomial.C y) = WeierstrassCurve.Affine.CoordinateRing.XIdeal W x