-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
α : Type u_2
β : Type u_3
a : Matrix.{u_2, u_3, u_1} α β (𝓞 K)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst_2 : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (a k l) : K) ≤ A
inst_3 : DecidableEq (K →+* ℂ)
inst_4 : Fintype α
cardα : Fintype.card α = p
let let₁ let₂ :
  ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
let₃ :
  let h := finrank ℚ K;
  ∀ (hphqh : p * h < q * h),
    ∃ (ξ : β → 𝓞 K),
      ξ ≠ 0 ∧
        a *ᵥ ξ = 0 ∧
          ∀ (l : β),
            house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
let₄ :
  let h := finrank ℚ K;
  ∀ (hphqh : p * h < q * h) (h0ph : 0 < p * h),
    ∃ (ξ : β → 𝓞 K),
      ξ ≠ 0 ∧
        a *ᵥ ξ = 0 ∧
          ∀ (l : β),
            house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
let₅ :
  let h := finrank ℚ K;
  ∀ (hphqh : p * h < q * h) (h0ph : 0 < p * h) (hfinp : Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) = p * h),
    ∃ (ξ : β → 𝓞 K),
      ξ ≠ 0 ∧
        a *ᵥ ξ = 0 ∧
          ∀ (l : β),
            house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
let₆ :
  let h := finrank ℚ K;
  ∀ (hphqh : p * h < q * h) (h0ph : 0 < p * h) (hfinp : Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) = p * h)
    (hfinq : Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ)) = q * h),
    ∃ (ξ : β → 𝓞 K),
      ξ ≠ 0 ∧
        a *ᵥ ξ = 0 ∧
          ∀ (l : β),
            house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
let₇ :
  let h := finrank ℚ K;
  ∀ (hphqh : p * h < q * h) (h0ph : 0 < p * h) (hfinp : Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) = p * h)
    (hfinq : Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ)) = q * h) (x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ) (hxl : x ≠ 0)
    (hmulvec0 : asiegel K a *ᵥ x = 0)
    (hxbound :
      ‖x‖ ≤
        ((↑(Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ))) : ℝ) * ‖asiegel K a‖) ^
          ((↑(Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ))) : ℝ) /
            HSub.hSub (α := ℝ) (↑(Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ))) : ℝ)
              (↑(Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ))) : ℝ))),
    ∃ (ξ : β → 𝓞 K),
      ξ ≠ 0 ∧
        a *ᵥ ξ = 0 ∧
          ∀ (l : β),
            house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
let₈ :
  let h := finrank ℚ K;
  ∀ (hphqh : p * h < q * h) (h0ph : 0 < p * h) (hfinp : Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) = p * h)
    (hfinq : Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ)) = q * h) (x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ) (hxl : x ≠ 0)
    (hmulvec0 : asiegel K a *ᵥ x = 0)
    (hxbound :
      ‖x‖ ≤
        (HMul.hMul (α := ℝ) (↑q : ℝ) (↑h : ℝ) * ‖asiegel K a‖) ^
          (HMul.hMul (α := ℝ) (↑p : ℝ) (↑h : ℝ) /
            (HMul.hMul (α := ℝ) (↑q : ℝ) (↑h : ℝ) - HMul.hMul (α := ℝ) (↑p : ℝ) (↑h : ℝ)))),
    ∃ (ξ : β → 𝓞 K),
      ξ ≠ 0 ∧
        a *ᵥ ξ = 0 ∧
          ∀ (l : β),
            house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
let₉ :
  let h := finrank ℚ K;
  ∀ (hphqh : p * h < q * h) (h0ph : 0 < p * h) (hfinp : Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) = p * h)
    (hfinq : Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ)) = q * h) (x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ) (hxl : x ≠ 0)
    (hmulvec0 : asiegel K a *ᵥ x = 0)
    (hxbound :
      ‖x‖ ≤ (HMul.hMul (α := ℝ) (↑q : ℝ) (↑h : ℝ) * ‖asiegel K a‖) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))),
    ∃ (ξ : β → 𝓞 K),
      ξ ≠ 0 ∧
        a *ᵥ ξ = 0 ∧
          ∀ (l : β),
            house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
let₁₀ :
  let h := finrank ℚ K;
  ∀ (hphqh : p * h < q * h) (h0ph : 0 < p * h) (hfinp : Fintype.card (Prod.{u_2, u_1} α (K →+* ℂ)) = p * h)
    (hfinq : Fintype.card (Prod.{u_3, u_1} β (K →+* ℂ)) = q * h) (x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ) (hxl : x ≠ 0)
    (hmulvec0 : asiegel K a *ᵥ x = 0)
    (hxbound :
      ‖x‖ ≤ (HMul.hMul (α := ℝ) (↑q : ℝ) (↑h : ℝ) * ‖asiegel K a‖) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)))
    (Apos : 0 ≤ A),
    ∃ (ξ : β → 𝓞 K),
      ξ ≠ 0 ∧
        a *ᵥ ξ = 0 ∧
          ∀ (l : β),
            house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
⊢ ∃ (ξ : β → 𝓞 K),
    ξ ≠ 0 ∧
      a *ᵥ ξ = 0 ∧
        ∀ (l : β), house (↑(ξ l) : K) ≤ c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))

Tactic:
classical
  let h := finrank ℚ K
  have hphqh : p * h < q * h := by gcongr; exact finrank_pos
  have h0ph : 0 < p * h := by rw [mul_pos_iff]; constructor; exact ⟨h0p, finrank_pos⟩
  have hfinp : Fintype.card (α × (K →+* ℂ)) = p * h := by
    rw [Fintype.card_prod, cardα, Embeddings.card]
  have hfinq : Fintype.card (β × (K →+* ℂ)) = q * h := by
    rw [Fintype.card_prod, cardβ, Embeddings.card]
  have ⟨x, hxl, hmulvec0, hxbound⟩ :=
    Int.Matrix.exists_ne_zero_int_vec_norm_le' (asiegel K a)
      (by rwa [hfinp, hfinq]) (by rwa [hfinp]) (asiegel_ne_0 K a ha)
  simp only [hfinp, hfinq, Nat.cast_mul] at hmulvec0 hxbound
  rw [← sub_mul, mul_div_mul_right _ _ (mod_cast finrank_pos.ne')] at hxbound
  have Apos : 0 ≤ A := by
    have ⟨k⟩ := Fintype.card_pos_iff.1 (cardα ▸ h0p)
    have ⟨l⟩ := Fintype.card_pos_iff.1 (cardβ ▸ h0p.trans hpq)
    exact le_trans (house_nonneg _) (habs k l)
  use ξ K x, ξ_ne_0 K x hxl, ξ_mulVec_eq_0 K a x hxl hmulvec0,
    house_le_bound K a hpq x habs Apos hxbound

Premises used: mul_div_mul_right, sub_mul, Nat.cast_mul