Golfing to remove a boilerplate hypothesis

Stream: new members

[Ryan Smith]

Sort of a golf question, but if I have an expression like

import Mathlib
variable {G: Type*} [Group G] [Finite G]

lemma foo (r n : ℕ) [Fact r.Prime] (h : Nat.card G = r ^ n) : IsSolvable G := by
  have tmp : ∃ n, Nat.card G = r ^ n := by use n
  have hpg : IsPGroup r G := IsPGroup.iff_card.mpr tmp
  sorry

Is there a way to avoid creating a temp hypothesis here? I already basically have a hypothesis which says what I need for IsPGroup.iff_card.mpr but I couldn't find a way to wrangle it without a temporary variable.

[Ruben Van de Velde]

You can write \<n, h\>

[Aaron Liu]

import Mathlib
variable {G: Type*} [Group G] [Finite G]

lemma foo (r n : ℕ) [Fact r.Prime] (h : Nat.card G = r ^ n) : IsSolvable G := by
  have hpg : IsPGroup r G := IsPGroup.iff_card.mpr (by use n)
  sorry

[Ryan Smith]

Thanks those are both good ways