From a22346e411f20a63dda427a5e8867b5bcde24ef6 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sun, 3 Jan 2016 21:40:56 -0500 Subject: [PATCH] fix(lean/tests/lean/run/new_obtain{3,4}): adapt tests to new notation for image --- tests/lean/run/new_obtain3.lean | 12 ++++++------ tests/lean/run/new_obtain4.lean | 2 +- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/tests/lean/run/new_obtain3.lean b/tests/lean/run/new_obtain3.lean index 0bcae0cd7..e44a084af 100644 --- a/tests/lean/run/new_obtain3.lean +++ b/tests/lean/run/new_obtain3.lean @@ -3,13 +3,13 @@ open set function eq.ops variables {X Y Z : Type} -lemma image_compose (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) '[a] = f '[g '[a]] := +lemma image_compose (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) ' a = f ' (g ' a) := ext (take z, iff.intro - (assume Hz : z ∈ (f ∘ g) '[a], + (assume Hz : z ∈ (f ∘ g) ' a, obtain x (Hx₁ : x ∈ a) (Hx₂ : f (g x) = z), from Hz, - have Hgx : g x ∈ g '[a], from mem_image Hx₁ rfl, - show z ∈ f '[g '[a]], from mem_image Hgx Hx₂) - (assume Hz : z ∈ f '[g '[a]], + have Hgx : g x ∈ g ' a, from mem_image Hx₁ rfl, + show z ∈ f ' (g ' a), from mem_image Hgx Hx₂) + (assume Hz : z ∈ f ' (g ' a), obtain y [x (Hz₁ : x ∈ a) (Hz₂ : g x = y)] (Hy₂ : f y = z), from Hz, - show z ∈ (f ∘ g) '[a], from mem_image Hz₁ (Hz₂⁻¹ ▸ Hy₂))) + show z ∈ (f ∘ g) ' a, from mem_image Hz₁ (Hz₂⁻¹ ▸ Hy₂))) diff --git a/tests/lean/run/new_obtain4.lean b/tests/lean/run/new_obtain4.lean index f6a8c92a3..0af8bac43 100644 --- a/tests/lean/run/new_obtain4.lean +++ b/tests/lean/run/new_obtain4.lean @@ -3,7 +3,7 @@ open set function eq.ops variables {X Y Z : Type} -lemma image_compose (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) '[a] = f '[g '[a]] := +lemma image_compose (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) ' a = f ' (g ' a) := ext (take z, iff.intro (assume Hz,