-- Mathlib/NumberTheory/NumberField/House.lean
theorem asiegel_remark : ‖asiegel K a‖ ≤ c₂ K * A

Proof state:
case calc_4
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ NumberField.house.c K *
      (house ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) *
        house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) lu.2))) ≤
    NumberField.house.c K * (A * house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) lu.2)))

Tactic:
apply mul_le_mul_of_nonneg_left ?_ (c_nonneg K)

Result:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ house ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) * house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) lu.2)) ≤
    A * house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) lu.2))

Proof state:
case calc_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ ↑|NumberField.house.asiegel K a kr lu| ≤
    NumberField.house.c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1 * (NumberField.house.newBasis K) lu.2))

Tactic:
have remark := basis_repr_norm_le_const_mul_house K

Result:
case calc_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
remark :
  ∀ (α : 𝓞 K) (i : K →+* ℂ),
    ‖↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)‖ ≤
      NumberField.house.c K * house ((algebraMap (𝓞 K) K) α)
⊢ ↑|NumberField.house.asiegel K a kr lu| ≤
    NumberField.house.c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1 * (NumberField.house.newBasis K) lu.2))

Proof state:
case calc_1
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ ‖NumberField.house.asiegel K a kr lu‖ = ‖↑(NumberField.house.asiegel K a kr lu)‖

Tactic:
rfl

Result:
no goals

Proof state:
case calc_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
remark :
  ∀ (α : 𝓞 K) (i : K →+* ℂ),
    ‖↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)‖ ≤
      NumberField.house.c K * house ((algebraMap (𝓞 K) K) α)
⊢ ↑|NumberField.house.asiegel K a kr lu| ≤
    NumberField.house.c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1 * (NumberField.house.newBasis K) lu.2))

Tactic:
simp only [Basis.repr_reindex, Finsupp.mapDomain_equiv_apply,
  integralBasis_repr_apply, eq_intCast, Rat.cast_intCast,
    Complex.norm_intCast] at remark

Result:
case calc_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
remark :
  ∀ (α : 𝓞 K) (i : K →+* ℂ),
    |↑(((RingOfIntegers.basis K).repr α) ((equivReindex K).symm.symm i))| ≤
      NumberField.house.c K * house ((algebraMap (𝓞 K) K) α)
⊢ ↑|NumberField.house.asiegel K a kr lu| ≤
    NumberField.house.c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1 * (NumberField.house.newBasis K) lu.2))

Proof state:
case calc_3
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ NumberField.house.c K *
      ‖(canonicalEmbedding K) ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) *
          (canonicalEmbedding K) ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) lu.2))‖ ≤
    NumberField.house.c K *
      (‖(canonicalEmbedding K) ((algebraMap (𝓞 K) K) (a kr.1 lu.1))‖ *
        ‖(canonicalEmbedding K) ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) lu.2))‖)

Tactic:
exact mul_le_mul_of_nonneg_left (norm_mul_le _ _) (c_nonneg K)

Result:
no goals

Proof state:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ house ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) * house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) lu.2)) ≤
    A * house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) lu.2))

Tactic:
apply mul_le_mul_of_nonneg_right (habs kr.1 lu.1) ?_

Result:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ 0 ≤ house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) lu.2))

Proof state:
case hr.h
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
⊢ 0 ≤ NumberField.house.c₂ K ∧ 0 ≤ A

Tactic:
exact ⟨c₂_nonneg K, Apos⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ ∃ b,
    True ∧
      house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) lu.2)) ≤
        house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) b))

Tactic:
use lu.2

Result:
no goals

Proof state:
case calc_6
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ NumberField.house.c K * NumberField.house.supOfBasis K * A ≤ NumberField.house.c₂ K * A

Tactic:
exact mul_le_mul_of_nonneg_right
  (mul_le_mul_of_nonneg_right (le_max_right ..) (supOfBasis_nonneg K)) Apos

Result:
no goals