nicer way to do `refine ⟨?x1, let h := ?x1; ?_⟩`

Stream: Is there code for X?

[David Renshaw]

Often when I'm proving a conjunction A ∧ B, I find that I need A in the proof of B. One way to handle this is to first do have h : A := ... and then do refine ⟨h, ?_⟩. However, that can be annoying if A is long to write out. Another thing that works is to write refine ⟨?x1, let h := ?x1; ?_⟩, but that's annoying because x1 is then a global metavariable name, so copy-paste compositionality is broken. Is there a nicer way to proceed?

import Mathlib.Tactic

example (x y n t : ℤ)
    (ht : x + y = 3 * t)
    (htn : t = n * (n + 1))
    (h : 2 * x - 3 * n * n - 3 * n = (n * n + n - 2) * (2 * n + 1)) :
     x = n ^ 3 + 3 * n ^ 2 - 1 ∧ y = -n ^ 3 + 3 * n + 1 := by

  -- We're proving A ∧ B and we want to use A in the proof of B.
  -- Is there a nicer way to do this?
  refine ⟨?x1, let hx := ?x1; ?_⟩
  · rw [←Int.mul_eq_mul_left_iff (by positivity : ((2 : ℤ) ≠ 0))]
    linear_combination 1 * h
  · rw [hx, htn] at ht; linear_combination 1 * ht

[Edward van de Meent]

funnily enough, this is also my problem in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/using.20a.20proven.20goal.20in.20another.20goal

[Adam Topaz]

How about this?

import Mathlib

example (P Q : Prop) (p : P) (q : P → Q) : P ∧ Q := by
  suffices _ from ⟨this, ?_⟩
  · exact q p
  · exact p

[Adam Topaz]

Alternatively we could write a "telescoping_constructor" tactic.

[David Renshaw]

yeah this works (and reorders the subgoals):

import Mathlib.Tactic

example (x y n t : ℤ)
    (ht : x + y = 3 * t)
    (htn : t = n * (n + 1))
    (h : 2 * x - 3 * n * n - 3 * n = (n * n + n - 2) * (2 * n + 1)) :
     x = n ^ 3 + 3 * n ^ 2 - 1 ∧ y = -n ^ 3 + 3 * n + 1 := by
  suffices hx : _ from ⟨hx, ?_⟩
  · rw [hx, htn] at ht; linear_combination 1 * ht
  · rw [←Int.mul_eq_mul_left_iff (by positivity : ((2 : ℤ) ≠ 0))]
    linear_combination 1 * h

It avoids the need to manually name a metavariable. But I wouldn't say that suffices line is very readable.

[Yaël Dillies]

Is this related to peel?

[Yury G. Kudryashov]

And-specific: rw [← and_congr_right imp_iff_right]; constructor

[Jireh Loreaux]

How about docs#exists_prop ?