Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: 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
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ ↑|asiegel K a kr lu| ≤ c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1 * (newBasis K) lu.2))

pp: 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
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ 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))

pp: 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
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ 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))

pp: 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
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * A * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) ≤ c K * A * supOfBasis K

pp: 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
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * A * supOfBasis K ≤ c₂ K * A

Tactic:
· have remark := basis_repr_norm_le_const_mul_house K
      simp only [Basis.repr_reindex, Finsupp.mapDomain_equiv_apply,
        integralBasis_repr_apply, eq_intCast, Rat.cast_intCast,
          Complex.norm_intCast] at remark
      exact mod_cast remark ((a kr.1 lu.1 * ((newBasis K) lu.2))) kr.2

Goal state after:
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
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ 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))

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
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ 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))

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
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * A * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) ≤ c K * A * 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
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * A * supOfBasis K ≤ c₂ K * A