From 1379e40b2fb5636183043881c58ef1e03b7c411a Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Tue, 31 Mar 2026 14:49:37 -0400 Subject: [PATCH] Fix misleading comment in tactics2, add and_map exercise The and_swap comment said "Combine constructor and apply" but apply wasn't needed. Reword that comment and add and_map, which genuinely requires both tactics. Closes #1 --- .solutions/10_tactics/tactics2.lean | 6 ++++++ exercises/10_tactics/tactics2.lean | 6 +++++- 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/.solutions/10_tactics/tactics2.lean b/.solutions/10_tactics/tactics2.lean index 75cdc1b..2525534 100644 --- a/.solutions/10_tactics/tactics2.lean +++ b/.solutions/10_tactics/tactics2.lean @@ -11,3 +11,9 @@ theorem and_swap (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by constructor · exact h.right · exact h.left + +theorem and_map (P Q R : Prop) (h : P ∧ Q) (f : Q → R) : P ∧ R := by + constructor + · exact h.left + · apply f + exact h.right diff --git a/exercises/10_tactics/tactics2.lean b/exercises/10_tactics/tactics2.lean index c01f423..240dac6 100644 --- a/exercises/10_tactics/tactics2.lean +++ b/exercises/10_tactics/tactics2.lean @@ -20,6 +20,10 @@ theorem and_intro (P Q : Prop) (hp : P) (hq : Q) : P ∧ Q := by -- For the next theorem, you can access parts of `h : P ∧ Q` -- using `h.left` (or `h.1`) and `h.right` (or `h.2`). --- Combine constructor and apply +-- Use constructor and the .left/.right accessors together theorem and_swap (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by sorry + +-- Combine constructor and apply +theorem and_map (P Q R : Prop) (h : P ∧ Q) (f : Q → R) : P ∧ R := by + sorry