Theorem: BallsCoverBalls.pow (Carleson/CoverByBalls.lean)

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
k : ℕ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
⊢ BallsCoverBalls X (a ^ k) 1 (n ^ k)
Tactic:
convert BallsCoverBalls.pow_mul h using 1
State after:
case h.e'_3
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
k : ℕ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
⊢ a ^ k = a ^ k * 1

State before:
case h.e'_3
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
k : ℕ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
⊢ a ^ k = a ^ k * 1
Tactic:
simp
State after:
no goals