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

Proof state:
case calc_5
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 * A * house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) lu.2)) ≤
    NumberField.house.c K * A * NumberField.house.supOfBasis K

Tactic:
apply mul_le_mul_of_nonneg_left ?_ (mul_nonneg (c_nonneg K) Apos)

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) ((NumberField.house.newBasis K) lu.2)) ≤ NumberField.house.supOfBasis K

Proof state:
case hr
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 ∨ NumberField.house.c₂ K ≤ 0 ∧ A ≤ 0

Tactic:
left

Result:
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

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 →+* ℂ)
⊢ ‖NumberField.house.asiegel K a kr lu‖ ≤ NumberField.house.c₂ K * A

Tactic:
calc
  ‖asiegel K a kr lu‖ = |asiegel K a kr lu| := ?_
  _ ≤ (c K) *
    house ((algebraMap (𝓞 K) K) (a kr.1 lu.1 * ((newBasis K) lu.2))) := ?_
  _ ≤ (c K) * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) *
    house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) := ?_
  _ ≤ (c K) * A * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) := ?_
  _ ≤ (c K) * A * (supOfBasis K) := ?_
  _ ≤ (c₂ K) * A := ?_

Result:
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|

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))

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 * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1 * (NumberField.house.newBasis K) lu.2)) ≤
    NumberField.house.c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) *
      house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) lu.2))

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))

case calc_5
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 * A * house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) lu.2)) ≤
    NumberField.house.c K * A * NumberField.house.supOfBasis K

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 * A * NumberField.house.supOfBasis K ≤ NumberField.house.c₂ K * A

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
⊢ ‖NumberField.house.asiegel K a‖ ≤ NumberField.house.c₂ K * A

Tactic:
rw [Matrix.norm_le_iff]

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
⊢ ∀ (i : α × (K →+* ℂ)) (j : β × (K →+* ℂ)), ‖NumberField.house.asiegel K a i j‖ ≤ NumberField.house.c₂ K * A

case hr
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 * A

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 →+* ℂ),
    |↑(((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))

Tactic:
exact mod_cast remark ((a kr.1 lu.1 * ((newBasis K) lu.2))) kr.2

Result:
no goals