refactor(NumberTheory): Golf 100 files

Mathlib/NumberTheory/ArithmeticFunction/Defs.lean

@@ -262,15 +262,11 @@ theorem mul_smul' (f g : ArithmeticFunction R) (h : ArithmeticFunction M) :
 
 theorem one_smul' (b : ArithmeticFunction M) : (1 : ArithmeticFunction R) • b = b := by
   ext x
-  rw [smul_apply]
-  by_cases x0 : x = 0
-  · simp [x0]
-  have h : {(1, x)} ⊆ divisorsAntidiagonal x := by simp [x0]
-  rw [← sum_subset h]
+  rw [smul_apply, ← Nat.map_div_right_divisors, sum_map, sum_eq_single 1]
   · simp
-  intro y ymem ynotMem
-  have y1ne : y.fst ≠ 1 := fun con => by simp_all [Prod.ext_iff]
-  simp [y1ne]
+  · intro d hd hd1
+    simp [one_apply_ne hd1]
+  · simpa using fun hx : x = 0 => by simp [hx]
 
 end Module
 
@@ -282,17 +278,11 @@ instance instMonoid : Monoid (ArithmeticFunction R) where
   one_mul := one_smul'
   mul_one f := by
     ext x
-    rw [mul_apply]
-    by_cases x0 : x = 0
-    · simp [x0]
-    have h : {(x, 1)} ⊆ divisorsAntidiagonal x := by simp [x0]
-    rw [← sum_subset h]
+    rw [mul_apply, ← Nat.map_div_left_divisors, sum_map, sum_eq_single 1]
     · simp
-    intro ⟨y₁, y₂⟩ ymem ynotMem
-    have y2ne : y₂ ≠ 1 := by
-      intro con
-      simp_all
-    simp [y2ne]
+    · intro d hd hd1
+      simp [one_apply_ne hd1]
+    · simpa using fun hx : x = 0 => by simp [hx]
   mul_assoc := mul_smul'
 
 instance instSemiring : Semiring (ArithmeticFunction R) where

Mathlib/NumberTheory/BernoulliPolynomials.lean

@@ -80,12 +80,8 @@ theorem bernoulli_one : bernoulli 1 = X - C 2⁻¹ := by
 
 @[simp]
 theorem bernoulli_eval_zero (n : ℕ) : (bernoulli n).eval 0 = _root_.bernoulli n := by
-  rw [bernoulli, eval_finset_sum, sum_range_succ]
-  have : ∑ x ∈ range n, _root_.bernoulli x * n.choose x * 0 ^ (n - x) = 0 := by
-    apply sum_eq_zero fun x hx => _
-    intro x hx
-    simp [tsub_eq_zero_iff_le, mem_range.1 hx]
-  simp [this]
+  rw [← coeff_zero_eq_eval_zero, coeff_bernoulli, if_pos (Nat.zero_le n), Nat.sub_zero,
+    Nat.choose_zero_right, Nat.cast_one, mul_one]
 
 @[simp]
 theorem bernoulli_eval_one (n : ℕ) : (bernoulli n).eval 1 = bernoulli' n := by
@@ -147,15 +143,10 @@ nonrec theorem sum_bernoulli (n : ℕ) :
   simp only [add_eq_left, mul_one, cast_one, cast_add, add_tsub_cancel_left,
     choose_succ_self_right, one_smul, _root_.bernoulli_zero, sum_singleton, zero_add,
     map_add, range_one, mul_one]
-  apply sum_eq_zero fun x hx => _
-  have f : ∀ x ∈ range n, ¬n + 1 - x = 1 := by grind
+  refine sum_eq_zero ?_
   intro x hx
-  rw [sum_bernoulli]
-  have g : ite (n + 1 - x = 1) (1 : ℚ) 0 = 0 := by
-    simp only [ite_eq_right_iff, one_ne_zero]
-    intro h₁
-    exact (f x hx) h₁
-  rw [g, zero_smul]
+  have hx1 : n + 1 - x ≠ 1 := by grind
+  simp [_root_.sum_bernoulli, hx1]
 
 /-- Another version of `Polynomial.sum_bernoulli`. -/
 theorem bernoulli_eq_sub_sum (n : ℕ) :

Mathlib/NumberTheory/Cyclotomic/Gal.lean

@@ -56,24 +56,10 @@ variable [CommRing L] [IsDomain L] (hμ : IsPrimitiveRoot μ n) [Algebra K L]
 field extension. -/
 theorem autToPow_injective : Function.Injective <| hμ.autToPow K := by
   intro f g hfg
-  apply_fun Units.val at hfg
-  simp only [IsPrimitiveRoot.coe_autToPow_apply] at hfg
-  generalize_proofs hf' hg' at hfg
-  have hf := hf'.choose_spec
-  have hg := hg'.choose_spec
-  generalize_proofs hζ at hf hg
-  suffices f (hμ.toRootsOfUnity : Lˣ) = g (hμ.toRootsOfUnity : Lˣ) by
-    apply AlgEquiv.coe_algHom_injective
-    apply (hμ.powerBasis K).algHom_ext
-    exact this
-  rw [ZMod.natCast_eq_natCast_iff] at hfg
-  refine (hf.trans ?_).trans hg.symm
-  rw [← rootsOfUnity.coe_pow _ hf'.choose, ← rootsOfUnity.coe_pow _ hg'.choose]
-  congr 2
-  rw [pow_eq_pow_iff_modEq]
-  convert hfg
-  conv => enter [2]; rw [hμ.eq_orderOf, ← hμ.val_toRootsOfUnity_coe]
-  rw [orderOf_units, Subgroup.orderOf_coe]
+  apply AlgEquiv.coe_algHom_injective
+  apply (hμ.powerBasis K).algHom_ext
+  simpa only [IsPrimitiveRoot.autToPow_spec] using
+    congrArg (fun t : (ZMod n)ˣ ↦ μ ^ (t : ZMod n).val) hfg
 
 end IsPrimitiveRoot
 

Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean

@@ -507,15 +507,9 @@ theorem norm_pow_sub_one_eq_prime_pow_of_ne_zero {k s : ℕ} (hζ : IsPrimitiveR
     (hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)) (hs : s ≤ k) (hk : k ≠ 0) :
     norm K (ζ ^ p ^ s - 1) = (p : K) ^ p ^ s := by
   by_cases htwo : p ^ (k - s + 1) = 2
-  · have hp : p = 2 := by
-      rw [← pow_one 2] at htwo
-      exact eq_of_prime_pow_eq (prime_iff.1 hpri.out) (prime_iff.1 Nat.prime_two) (succ_pos _) htwo
-    replace hs : s = k := by
-      rw [hp] at htwo
-      nth_rw 2 [← pow_one 2] at htwo
-      replace htwo := Nat.pow_right_injective rfl.le htwo
-      rw [add_eq_right, Nat.sub_eq_zero_iff_le] at htwo
-      exact le_antisymm hs htwo
+  · obtain ⟨hp, hks⟩ := (Nat.prime_two.pow_eq_iff).1 htwo
+    simp only [add_eq_right] at hks
+    replace hs : s = k := le_antisymm hs (Nat.sub_eq_zero_iff_le.mp hks)
     simp only [hp, hs] at hζ hirr hcycl ⊢
     obtain ⟨k₁, hk₁⟩ := Nat.exists_eq_succ_of_ne_zero hk
     rw [hζ.norm_pow_sub_one_two hirr, hk₁, _root_.pow_succ', pow_mul, neg_eq_neg_one_mul,

Mathlib/NumberTheory/Dioph.lean

@@ -567,12 +567,8 @@ theorem sub_dioph : DiophFn fun v => f v - g v :=
     (diophFn_vec _).2 <|
       ext (D&1 D= D&0 D+ D&2 D∨ D&1 D≤ D&2 D∧ D&0 D= D.0) <|
         (vectorAll_iff_forall _).1 fun x y z =>
-          show y = x + z ∨ y ≤ z ∧ x = 0 ↔ y - z = x from
-            ⟨fun o => by
-              rcases o with (ae | ⟨yz, x0⟩)
-              · rw [ae, add_tsub_cancel_right]
-              · rw [x0, tsub_eq_zero_iff_le.mpr yz], by
-              lia⟩
+          show y = x + z ∨ y ≤ z ∧ x = 0 ↔ y - z = x by
+            grind
 
 @[inherit_doc]
 scoped infixl:80 " D- " => Dioph.sub_dioph
@@ -623,16 +619,10 @@ theorem div_dioph : DiophFn fun v => f v / g v :=
       ext this <|
         (vectorAll_iff_forall _).1 fun z x y =>
           show y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < (z + 1) * y ↔ x / y = z by
-            refine Iff.trans ?_ eq_comm
-            exact y.eq_zero_or_pos.elim
-              (fun y0 => by
-                rw [y0, Nat.div_zero]
-                exact ⟨fun o => (o.resolve_right fun ⟨_, h2⟩ => Nat.not_lt_zero _ h2).right,
-                  fun z0 => Or.inl ⟨rfl, z0⟩⟩)
-              fun ypos =>
-                Iff.trans ⟨fun o => o.resolve_left fun ⟨h1, _⟩ => Nat.ne_of_gt ypos h1, Or.inr⟩
-                  (le_antisymm_iff.trans <| and_congr (Nat.le_div_iff_mul_le ypos) <|
-                    Iff.trans ⟨lt_succ_of_le, le_of_lt_succ⟩ (div_lt_iff_lt_mul ypos)).symm
+            rcases y.eq_zero_or_pos with rfl | hy
+            · simp [eq_comm]
+            · rw [Nat.div_eq_iff hy, Nat.succ_mul]
+              grind
 
 end
 

Mathlib/NumberTheory/DiophantineApproximation/Basic.lean

@@ -338,18 +338,12 @@ theorem convergent_succ (ξ : ℝ) (n : ℕ) :
 /-- All convergents of `0` are zero. -/
 @[simp]
 theorem convergent_of_zero (n : ℕ) : convergent 0 n = 0 := by
-  induction n with
-  | zero => simp only [convergent_zero, floor_zero, cast_zero]
-  | succ n ih =>
-    simp only [ih, convergent_succ, floor_zero, cast_zero, fract_zero, add_zero, inv_zero]
+  induction n <;> simp [convergent, *]
 
 /-- If `ξ` is an integer, all its convergents equal `ξ`. -/
 @[simp]
 theorem convergent_of_int {ξ : ℤ} (n : ℕ) : convergent ξ n = ξ := by
-  cases n
-  · simp only [convergent_zero, floor_intCast]
-  · simp only [convergent_succ, floor_intCast, fract_intCast, convergent_of_zero, add_zero,
-      inv_zero]
+  cases n <;> simp [convergent, convergent_of_zero]
 
 end Real
 

Mathlib/NumberTheory/Divisors.lean

@@ -476,20 +476,13 @@ theorem Prime.prod_divisors {α : Type*} [CommMonoid α] {p : ℕ} {f : ℕ →
   rw [← cons_self_properDivisors h.ne_zero, prod_cons, h.prod_properDivisors]
 
 theorem properDivisors_eq_singleton_one_iff_prime : n.properDivisors = {1} ↔ n.Prime := by
-  refine ⟨?_, ?_⟩
-  · intro h
-    refine Nat.prime_def.mpr ⟨?_, fun m hdvd => ?_⟩
-    · match n with
-      | 0 => contradiction
-      | 1 => contradiction
-      | Nat.succ (Nat.succ n) => simp
-    · rw [← mem_singleton, ← h, mem_properDivisors]
-      have := Nat.le_of_dvd ?_ hdvd
-      · simpa [hdvd, this] using (le_iff_eq_or_lt.mp this).symm
-      · by_contra!
-        simp only [nonpos_iff_eq_zero.mp this] at h
-        contradiction
-  · exact fun h => Prime.properDivisors h
+  refine ⟨?_, Prime.properDivisors⟩
+  intro h
+  rw [Nat.prime_def_lt]
+  refine ⟨Nat.succ_le_iff.mpr <| one_mem_properDivisors_iff_one_lt.mp (by simp [h]), ?_⟩
+  intro m hm hdvd
+  have hm' : m ∈ n.properDivisors := mem_properDivisors.2 ⟨hdvd, hm⟩
+  simpa [h] using hm'
 
 theorem sum_properDivisors_eq_one_iff_prime : ∑ x ∈ n.properDivisors, x = 1 ↔ n.Prime := by
   rcases n with - | n
@@ -507,25 +500,18 @@ theorem sum_properDivisors_eq_one_iff_prime : ∑ x ∈ n.properDivisors, x = 1
 
 theorem mem_properDivisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) {x : ℕ} :
     x ∈ properDivisors (p ^ k) ↔ ∃ (j : ℕ) (_ : j < k), x = p ^ j := by
-  rw [mem_properDivisors, Nat.dvd_prime_pow pp, ← exists_and_right]
-  simp only [exists_prop, and_assoc]
-  apply exists_congr
-  intro a
-  constructor <;> intro h
-  · rcases h with ⟨_h_left, rfl, h_right⟩
-    rw [Nat.pow_lt_pow_iff_right pp.one_lt] at h_right
-    exact ⟨h_right, rfl⟩
-  · rcases h with ⟨h_left, rfl⟩
-    rw [Nat.pow_lt_pow_iff_right pp.one_lt]
-    simp [h_left, le_of_lt]
+  rw [mem_properDivisors, Nat.dvd_prime_pow pp]
+  constructor
+  · rintro ⟨⟨j, hjk, rfl⟩, hlt⟩
+    exact ⟨j, (Nat.pow_lt_pow_iff_right pp.one_lt).1 hlt, rfl⟩
+  · rintro ⟨j, hjk, rfl⟩
+    exact ⟨⟨j, le_of_lt hjk, rfl⟩, (Nat.pow_lt_pow_iff_right pp.one_lt).2 hjk⟩
 
 theorem properDivisors_prime_pow {p : ℕ} (pp : p.Prime) (k : ℕ) :
     properDivisors (p ^ k) = (Finset.range k).map ⟨(p ^ ·), Nat.pow_right_injective pp.two_le⟩ := by
   ext a
-  simp only [mem_properDivisors, mem_map, mem_range, Function.Embedding.coeFn_mk]
-  have := mem_properDivisors_prime_pow pp k (x := a)
-  rw [mem_properDivisors] at this
-  grind
+  rw [mem_properDivisors_prime_pow pp]
+  simp [eq_comm]
 
 @[to_additive (attr := simp)]
 theorem prod_properDivisors_prime_pow {α : Type*} [CommMonoid α] {k p : ℕ} {f : ℕ → α}
@@ -562,19 +548,13 @@ lemma primeFactors_filter_dvd_of_dvd {m n : ℕ} (hn : n ≠ 0) (hmn : m ∣ n)
 @[simp]
 theorem image_div_divisors_eq_divisors (n : ℕ) :
     image (fun x : ℕ => n / x) n.divisors = n.divisors := by
-  by_cases hn : n = 0
-  · simp [hn]
-  ext a
-  constructor
-  · rw [mem_image]
-    rintro ⟨x, hx1, hx2⟩
-    rw [mem_divisors] at *
-    refine ⟨?_, hn⟩
-    rw [← hx2]
-    exact div_dvd_of_dvd hx1.1
-  · rw [mem_divisors, mem_image]
-    rintro ⟨h1, -⟩
-    exact ⟨n / a, mem_divisors.mpr ⟨div_dvd_of_dvd h1, hn⟩, Nat.div_div_self h1 hn⟩
+  calc
+    image (fun x : ℕ => n / x) n.divisors =
+        (n.divisors.map ⟨fun d => (n / d, d), fun _ _ => congr_arg Prod.snd⟩).image Prod.fst := by
+      rw [map_eq_image, image_image]
+      rfl
+    _ = n.divisorsAntidiagonal.image Prod.fst := by rw [map_div_left_divisors]
+    _ = n.divisors := image_fst_divisorsAntidiagonal
 
 @[to_additive (attr := simp) sum_div_divisors]
 theorem prod_div_divisors {α : Type*} [CommMonoid α] (n : ℕ) (f : ℕ → α) :

Mathlib/NumberTheory/EllipticDivisibilitySequence.lean

@@ -329,14 +329,9 @@ lemma normEDS_dvd_normEDS_two_mul (k : ℤ) : normEDS b c d k ∣ normEDS b c d
 lemma complEDS₂_mul_b (k : ℤ) : complEDS₂ b c d k * b =
     normEDS b c d (k - 1) ^ 2 * normEDS b c d (k + 2) -
       normEDS b c d (k - 2) * normEDS b c d (k + 1) ^ 2 := by
-  induction k using Int.negInduction with
-  | nat k =>
-    simp_rw [complEDS₂, normEDS, Int.even_add, Int.even_sub, even_two, iff_true, Int.not_even_one,
-      iff_false]
-    split_ifs <;> ring1
-  | neg ih =>
-    simp_rw [complEDS₂_neg, ← sub_neg_eq_add, ← neg_sub', ← neg_add', normEDS_neg, ih]
-    ring1
+  simp_rw [complEDS₂, normEDS, Int.even_add, Int.even_sub, even_two, iff_true, Int.not_even_one,
+    iff_false]
+  split_ifs <;> ring1
 
 lemma normEDS_even (m : ℤ) : normEDS b c d (2 * m) * b =
     normEDS b c d (m - 1) ^ 2 * normEDS b c d m * normEDS b c d (m + 2) -

Mathlib/NumberTheory/EulerProduct/Basic.lean

@@ -366,15 +366,11 @@ This version is stated in the form of convergence of finite partial products. -/
 theorem eulerProduct_completely_multiplicative {f : ℕ →*₀ F} (hsum : Summable (‖f ·‖)) :
     Tendsto (fun n : ℕ ↦ ∏ p ∈ primesBelow n, (1 - f p)⁻¹) atTop (𝓝 (∑' n, f n)) := by
   have hmul {m n} (_ : Nat.Coprime m n) := f.map_mul m n
-  have := (eulerProduct_hasProd_mulIndicator f.map_one hmul hsum f.map_zero).tendsto_prod_nat
-  have H (n : ℕ) : ∏ p ∈ range n, {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) p =
-                     ∏ p ∈ primesBelow n, (1 - f p)⁻¹ :=
-    prod_mulIndicator_eq_prod_filter
-      (range n) (fun _ ↦ fun p ↦ (1 - f p)⁻¹) (fun _ ↦ {p | Nat.Prime p}) id
-  have H' : {p | Nat.Prime p}.mulIndicator (fun p ↦ (1 - f p)⁻¹) =
-              {p | Nat.Prime p}.mulIndicator (fun p ↦ ∑' e : ℕ, f (p ^ e)) :=
-    Set.mulIndicator_congr fun p hp ↦ one_sub_inv_eq_geometric_of_summable_norm hp hsum
-  simpa only [← H, H'] using this
+  have H (n : ℕ) :
+      ∏ p ∈ primesBelow n, (1 - f p)⁻¹ = ∏ p ∈ primesBelow n, ∑' e, f (p ^ e) := by
+    refine prod_congr rfl fun p hp ↦ ?_
+    exact one_sub_inv_eq_geometric_of_summable_norm (Nat.prime_of_mem_primesBelow hp) hsum
+  simpa [H] using (eulerProduct f.map_one hmul hsum f.map_zero)
 
 end EulerProduct
 

Mathlib/NumberTheory/FLT/Four.lean

@@ -112,16 +112,11 @@ theorem neg_of_minimal {a b c : ℤ} : Minimal a b c → Minimal a b (-c) := by
 theorem exists_odd_minimal {a b c : ℤ} (h : Fermat42 a b c) :
     ∃ a0 b0 c0, Minimal a0 b0 c0 ∧ a0 % 2 = 1 := by
   obtain ⟨a0, b0, c0, hf⟩ := exists_minimal h
-  rcases Int.emod_two_eq_zero_or_one a0 with hap | hap
-  · rcases Int.emod_two_eq_zero_or_one b0 with hbp | hbp
-    · exfalso
-      have h1 : 2 ∣ (Int.gcd a0 b0 : ℤ) :=
-        Int.dvd_coe_gcd (Int.dvd_of_emod_eq_zero hap) (Int.dvd_of_emod_eq_zero hbp)
-      rw [Int.isCoprime_iff_gcd_eq_one.mp (coprime_of_minimal hf)] at h1
-      revert h1
-      decide
-    · exact ⟨b0, ⟨a0, ⟨c0, minimal_comm hf, hbp⟩⟩⟩
-  exact ⟨a0, ⟨b0, ⟨c0, hf, hap⟩⟩⟩
+  rcases Int.emod_two_eq_zero_or_one a0 with ha0 | ha0
+  · refine ⟨b0, a0, c0, minimal_comm hf, ?_⟩
+    exact Int.odd_iff.mp <| Int.isCoprime_two_left.mp <|
+      IsCoprime.of_isCoprime_of_dvd_left (coprime_of_minimal hf) (Int.dvd_of_emod_eq_zero ha0)
+  · exact ⟨a0, b0, c0, hf, ha0⟩
 
 /-- We can assume that a minimal solution to `a ^ 4 + b ^ 4 = c ^ 2` has
 `a` odd and `c` positive. -/
@@ -188,10 +183,9 @@ theorem not_minimal {a b c : ℤ} (h : Minimal a b c) (ha2 : a % 2 = 1) (hc : 0
   -- Now use the fact that (b / 2) ^ 2 = m * r * s, and m, r and s are pairwise coprime to obtain
   -- i, j and k such that m = i ^ 2, r = j ^ 2 and s = k ^ 2.
   -- m and r * s are coprime because m = r ^ 2 + s ^ 2 and r and s are coprime.
-  have hcp : Int.gcd m (r * s) = 1 := by
+  have hcp : IsCoprime m (r * s) := by
     rw [htt3]
-    exact Int.isCoprime_iff_gcd_eq_one.mp
-      (Int.isCoprime_of_sq_sum' (Int.isCoprime_iff_gcd_eq_one.mpr htt4))
+    exact Int.isCoprime_of_sq_sum' (Int.isCoprime_iff_gcd_eq_one.mpr htt4)
   -- b is even because b ^ 2 = 2 * m * n.
   have hb2 : 2 ∣ b := by
     apply @Int.Prime.dvd_pow' _ 2 _ Nat.prime_two
@@ -203,27 +197,20 @@ theorem not_minimal {a b c : ℤ} (h : Minimal a b c) (ha2 : a % 2 = 1) (hc : 0
     linear_combination (-b - 2 * b') * hb2' + ht2 + 2 * m * htt2
   have hrsz : r * s ≠ 0 := by grind
   have h2b0 : b' ≠ 0 := by grind
-  obtain ⟨i, hi⟩ := Int.sq_of_gcd_eq_one hcp hs.symm
+  obtain ⟨i, hi⟩ := Int.sq_of_isCoprime hcp hs.symm
   -- use m is positive to exclude m = - i ^ 2
   have hi' : ¬m = -i ^ 2 := by
-    by_contra h1
-    have hit : -i ^ 2 ≤ 0 := neg_nonpos.mpr (sq_nonneg i)
-    rw [← h1] at hit
-    apply absurd h4 (not_lt.mpr hit)
+    intro h1
+    nlinarith [sq_nonneg i, h4, h1]
   replace hi : m = i ^ 2 := Or.resolve_right hi hi'
   rw [mul_comm] at hs
-  rw [Int.gcd_comm] at hcp
   -- obtain d such that r * s = d ^ 2
-  obtain ⟨d, hd⟩ := Int.sq_of_gcd_eq_one hcp hs.symm
+  obtain ⟨d, hd⟩ := Int.sq_of_isCoprime hcp.symm hs.symm
   -- (b / 2) ^ 2 and m are positive so r * s is positive
   have hd' : ¬r * s = -d ^ 2 := by
-    by_contra h1
+    intro h1
     rw [h1] at hs
-    have h2 : b' ^ 2 ≤ 0 := by
-      rw [hs, (by ring : -d ^ 2 * m = -(d ^ 2 * m))]
-      exact neg_nonpos.mpr ((mul_nonneg_iff_of_pos_right h4).mpr (sq_nonneg d))
-    have h2' : 0 ≤ b' ^ 2 := by apply sq_nonneg b'
-    exact absurd (lt_of_le_of_ne h2' (Ne.symm (pow_ne_zero _ h2b0))) (not_lt.mpr h2)
+    nlinarith [sq_nonneg d, h4, hs, sq_pos_of_ne_zero h2b0]
   replace hd : r * s = d ^ 2 := Or.resolve_right hd hd'
   -- r = +/- j ^ 2
   obtain ⟨j, hj⟩ := Int.sq_of_gcd_eq_one htt4 hd