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

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

Tactic:
simp only [house, _root_.map_mul, mul_assoc]

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

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

Tactic:
rw [mul_nonneg_iff]

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

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:
rw [mul_assoc, mul_assoc]

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

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:
simp only [Int.cast_abs, ← Real.norm_eq_abs (asiegel K a kr lu)]

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

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 →+* ℂ)
⊢ 0 ≤ house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) lu.2))

Tactic:
exact norm_nonneg ((canonicalEmbedding K) ((algebraMap (𝓞 K) K)
  ((newBasis K) 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 * A * NumberField.house.supOfBasis K ≤ NumberField.house.c₂ K * A

Tactic:
rw [mul_right_comm]

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

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

Tactic:
simp only [supOfBasis, le_sup'_iff, mem_univ]

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 →+* ℂ)
⊢ ∃ b,
    True ∧
      house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) lu.2)) ≤
        house ((algebraMap (𝓞 K) K) ((NumberField.house.newBasis K) b))

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

Tactic:
intro kr lu

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