Theorem: BallsCoverBalls.pow_mul (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 * r) r (n ^ k)
Tactic:
induction k
State after:
case zero
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
⊢ BallsCoverBalls X (a ^ 0 * r) r (n ^ 0)

case succ
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
n✝ : ℕ
a✝ : BallsCoverBalls X (a ^ n✝ * r) r (n ^ n✝)
⊢ BallsCoverBalls X (a ^ (n✝ + 1) * r) r (n ^ (n✝ + 1))

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
⊢ BallsCoverBalls X (a ^ 0 * r) r (n ^ 0)
Tactic:
case zero =>
  simp
  intro x
  exact BallCoversSelf x r
State after:
no goals

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
⊢ BallsCoverBalls X (a ^ (m + 1) * r) r (n ^ (m + 1))
Tactic:
case succ m h2 =>
  specialize h (r * a^m)
  rw[<- mul_assoc, mul_comm, <- mul_assoc] at h
  norm_cast
  ring_nf
  rw[mul_comm a]
  rw[mul_comm] at h2
  norm_cast at h2
  exact BallsCoverBalls.trans h h2
State after:
no goals

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
⊢ BallsCoverBalls X (a ^ 0 * r) r (n ^ 0)
Tactic:
simp
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
⊢ BallsCoverBalls X r r 1

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
⊢ BallsCoverBalls X r r 1
Tactic:
intro x
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
x : X
⊢ CoveredByBalls (ball x r) 1 r

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
x : X
⊢ CoveredByBalls (ball x r) 1 r
Tactic:
exact BallCoversSelf x r
State after:
no goals

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
h : ∀ (r : ℝ), BallsCoverBalls X (a * r) r n
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
⊢ BallsCoverBalls X (a ^ (m + 1) * r) r (n ^ (m + 1))
Tactic:
specialize h (r * a^m)
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
h : BallsCoverBalls X (a * (r * a ^ m)) (r * a ^ m) n
⊢ BallsCoverBalls X (a ^ (m + 1) * r) r (n ^ (m + 1))

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
h : BallsCoverBalls X (a * (r * a ^ m)) (r * a ^ m) n
⊢ BallsCoverBalls X (a ^ (m + 1) * r) r (n ^ (m + 1))
Tactic:
rw[<- mul_assoc, mul_comm, <- mul_assoc] at h
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
h : BallsCoverBalls X (a ^ m * a * r) (r * a ^ m) n
⊢ BallsCoverBalls X (a ^ (m + 1) * r) r (n ^ (m + 1))

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
h : BallsCoverBalls X (a ^ m * a * r) (r * a ^ m) n
⊢ BallsCoverBalls X (a ^ (m + 1) * r) r (n ^ (m + 1))
Tactic:
ring_nf
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
h : BallsCoverBalls X (a ^ m * a * r) (r * a ^ m) n
⊢ BallsCoverBalls X (a * a ^ m * r) r (n * n ^ m)

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
h : BallsCoverBalls X (a ^ m * a * r) (r * a ^ m) n
⊢ BallsCoverBalls X (a * a ^ m * r) r (n * n ^ m)
Tactic:
rw[mul_comm a]
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
h : BallsCoverBalls X (a ^ m * a * r) (r * a ^ m) n
⊢ BallsCoverBalls X (a ^ m * a * r) r (n * n ^ m)

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (a ^ m * r) r (n ^ m)
h : BallsCoverBalls X (a ^ m * a * r) (r * a ^ m) n
⊢ BallsCoverBalls X (a ^ m * a * r) r (n * n ^ m)
Tactic:
rw[mul_comm] at h2
State after:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (r * a ^ m) r (n ^ m)
h : BallsCoverBalls X (a ^ m * a * r) (r * a ^ m) n
⊢ BallsCoverBalls X (a ^ m * a * r) r (n * n ^ m)

State before:
X : Type u_1
inst✝ : PseudoMetricSpace X
s t : Set X
n m✝ : ℕ
r r' r₁ r₂ r₃ a : ℝ
m : ℕ
h2 : BallsCoverBalls X (r * a ^ m) r (n ^ m)
h : BallsCoverBalls X (a ^ m * a * r) (r * a ^ m) n
⊢ BallsCoverBalls X (a ^ m * a * r) r (n * n ^ m)
Tactic:
exact BallsCoverBalls.trans h h2
State after:
no goals