awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : Prod.{u_2, u_1} α (K →+* ℂ)
lu : Prod.{u_3, u_1} β (K →+* ℂ)
⊢ ‖HMul.hMul (α := (K →+* ℂ) → ℂ) (β := (K →+* ℂ) → ℂ)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (a kr.1 lu.1) : K) :
          (K →+* ℂ) → ℂ)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K) :
          (K →+* ℂ) → ℂ)‖ ≤
    norm (E := (K →+* ℂ) → ℂ)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (a kr.1 lu.1) : K) :
          (K →+* ℂ) → ℂ) *
      norm (E := (K →+* ℂ) → ℂ)
        ((canonicalEmbedding K : (a : K) → (K →+* ℂ) → ℂ)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K) :
          (K →+* ℂ) → ℂ)

Tactic:
apply norm_mul_le

Premises used: norm_mul_le
-- 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)
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : Prod.{u_2, u_1} α (K →+* ℂ)
lu : Prod.{u_3, u_1} β (K →+* ℂ)
calc_4 :
  c K *
      (house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (a kr.1 lu.1) : K) *
        house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K)) ≤
    c K *
      (A * house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K))
⊢ c K * house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (a kr.1 lu.1) : K) *
      house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K) ≤
    c K * A * house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K)

Tactic:
rw [mul_assoc, mul_assoc]

Premises used: mul_assoc
-- 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)
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : Prod.{u_2, u_1} α (K →+* ℂ)
lu : Prod.{u_3, u_1} β (K →+* ℂ)
calc_4 : 0 ≤ house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K)
calc_4₁ : house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (a kr.1 lu.1) : K) ≤ A
⊢ c K *
      (house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (a kr.1 lu.1) : K) *
        house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K)) ≤
    c K *
      (A * house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K))

Tactic:
gcongr _ * (?_ * _)

Premises used: HMul.hMul
-- 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)
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : Prod.{u_2, u_1} α (K →+* ℂ)
lu : Prod.{u_3, u_1} β (K →+* ℂ)
⊢ 0 ≤ house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K)

Tactic:
apply house_nonneg

Premises used: NumberField.house_nonneg
-- 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)
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : Prod.{u_2, u_1} α (K →+* ℂ)
lu : Prod.{u_3, u_1} β (K →+* ℂ)
⊢ house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (a kr.1 lu.1) : K) ≤ A

Tactic:
habs kr.1 lu.1

Premises used: Prod.fst
-- 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)
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : Prod.{u_2, u_1} α (K →+* ℂ)
lu : Prod.{u_3, u_1} β (K →+* ℂ)
⊢ house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (a kr.1 lu.1) : K) ≤ A

Tactic:
exact habs kr.1 lu.1

Premises used: Prod.fst
-- 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)
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : Prod.{u_2, u_1} α (K →+* ℂ)
lu : Prod.{u_3, u_1} β (K →+* ℂ)
calc_5 :
  house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K) ≤
    supOfBasis K
⊢ c K * A * house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K) ≤
    c K * A * supOfBasis K

Tactic:
gcongr
-- 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)
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : Prod.{u_2, u_1} α (K →+* ℂ)
lu : Prod.{u_3, u_1} β (K →+* ℂ)
calc_5 :
  ∃ (b : K →+* ℂ),
    True ∧
      house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K) ≤
        house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) b : 𝓞 K) : K)
⊢ house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K) ≤
    supOfBasis K

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

Premises used: Finset.mem_univ, Finset.le_sup'_iff, _private.0.NumberField.house.supOfBasis
-- 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)
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : Prod.{u_2, u_1} α (K →+* ℂ)
lu : Prod.{u_3, u_1} β (K →+* ℂ)
w : K →+* ℂ
h :
  True ∧
    house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K) ≤
      house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K)
⊢ ∃ (b : K →+* ℂ),
    True ∧
      house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K) ≤
        house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) b : 𝓞 K) : K)

Tactic:
use lu.2

Premises used: Prod.snd
-- 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)
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : Prod.{u_2, u_1} α (K →+* ℂ)
lu : Prod.{u_3, u_1} β (K →+* ℂ)
calc_6 : c K * supOfBasis K * A ≤ max 1 (c K) * supOfBasis K * A
⊢ c K * A * supOfBasis K ≤ c₂ K * A

Tactic:
rw [mul_right_comm, c₂]

Premises used: mul_right_comm, _private.0.NumberField.house.c₂
-- 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)
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : Prod.{u_2, u_1} α (K →+* ℂ)
lu : Prod.{u_3, u_1} β (K →+* ℂ)
calc_6 : 0 ≤ supOfBasis K
calc_6₁ : c K ≤ max 1 (c K)
⊢ c K * supOfBasis K * A ≤ max 1 (c K) * supOfBasis K * A

Tactic:
gcongr
-- 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)
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : Prod.{u_2, u_1} α (K →+* ℂ)
lu : Prod.{u_3, u_1} β (K →+* ℂ)
⊢ 0 ≤ supOfBasis K

Tactic:
supOfBasis_nonneg _

Premises used: _private.0.NumberField.house.supOfBasis_nonneg
-- 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)
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : Prod.{u_2, u_1} α (K →+* ℂ)
lu : Prod.{u_3, u_1} β (K →+* ℂ)
⊢ c K ≤ max 1 (c K)

Tactic:
le_max_right ..

Premises used: le_max_right
-- 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)
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : Prod.{u_2, u_1} α (K →+* ℂ)
lu : Prod.{u_3, u_1} β (K →+* ℂ)
⊢ 0 ≤ supOfBasis K

Tactic:
exacts [supOfBasis_nonneg _, le_max_right ..]

Premises used: le_max_right, _private.0.NumberField.house.supOfBasis_nonneg
-- 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)
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
this : 0 ≤ c K
⊢ 0 ≤ c₂ K * A

Tactic:
mul_nonneg (c₂_nonneg _) Apos

Premises used: mul_nonneg, _private.0.NumberField.house.c₂_nonneg
-- 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)
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
this : 0 ≤ c K
⊢ 0 ≤ c₂ K * A

Tactic:
exact mul_nonneg (c₂_nonneg _) Apos

Premises used: mul_nonneg, _private.0.NumberField.house.c₂_nonneg
-- 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)
p q : ℕ
hpq : p < q
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
hxbound :
  ‖x‖ ≤
    (HMul.hMul (α := ℝ) (↑q : ℝ) (↑(finrank ℚ K) : ℝ) * ‖asiegel K a‖) ^
      ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
h : ℕ := finrank ℚ K
l : β
⊢ 0 ≤ supOfBasis K

Tactic:
have H₀ : 0 ≤ NumberField.house.supOfBasis K := supOfBasis_nonneg _
-- 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)
p q : ℕ
hpq : p < q
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
hxbound :
  ‖x‖ ≤
    (HMul.hMul (α := ℝ) (↑q : ℝ) (↑(finrank ℚ K) : ℝ) * ‖asiegel K a‖) ^
      ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
⊢ 0 < HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)

Tactic:
have H₁ : 0 < (q - p : ℝ) := sub_pos.mpr <| mod_cast hpq
-- 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)
p q : ℕ
hpq : p < q
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
hxbound :
  ‖x‖ ≤
    (HMul.hMul (α := ℝ) (↑q : ℝ) (↑(finrank ℚ K) : ℝ) * ‖asiegel K a‖) ^
      ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)
⊢ house (K := K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (∑ r : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, r)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K)) :
        K) =
    house (K := K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (∑ r : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, r)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K)) :
        K)

Tactic:
rfl

Premises used: rfl
-- 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)
p q : ℕ
hpq : p < q
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
hxbound :
  ‖x‖ ≤
    (HMul.hMul (α := ℝ) (↑q : ℝ) (↑(finrank ℚ K) : ℝ) * ‖asiegel K a‖) ^
      ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)
⊢ house (K := K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (∑ r : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, r)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K)) :
        K) ≤
    ∑ r : K →+* ℂ,
      house
        (HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x (l, r)) : 𝓞 K) : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K))

Tactic:
?_
-- 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)
p q : ℕ
hpq : p < q
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
hxbound :
  ‖x‖ ≤
    (HMul.hMul (α := ℝ) (↑q : ℝ) (↑(finrank ℚ K) : ℝ) * ‖asiegel K a‖) ^
      ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)
⊢ LE.le (α := ℝ)
    (∑ r : K →+* ℂ,
      house
        (HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x (l, r)) : 𝓞 K) : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K)))
    (∑ r : K →+* ℂ,
      ‖x (l, r)‖ *
        house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K))

Tactic:
?_
-- 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)
p q : ℕ
hpq : p < q
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
hxbound :
  ‖x‖ ≤
    (HMul.hMul (α := ℝ) (↑q : ℝ) (↑(finrank ℚ K) : ℝ) * ‖asiegel K a‖) ^
      ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)
⊢ LE.le (α := ℝ)
    (∑ r : K →+* ℂ,
      ‖x (l, r)‖ *
        house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K))
    (∑ r : K →+* ℂ, ‖x (l, r)‖ * supOfBasis K)

Tactic:
?_
-- 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)
p q : ℕ
hpq : p < q
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
hxbound :
  ‖x‖ ≤
    (HMul.hMul (α := ℝ) (↑q : ℝ) (↑(finrank ℚ K) : ℝ) * ‖asiegel K a‖) ^
      ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)
⊢ LE.le (α := ℝ) (∑ r : K →+* ℂ, ‖x (l, r)‖ * supOfBasis K)
    (∑ _r : K →+* ℂ,
      (HMul.hMul (α := ℝ) (↑q : ℝ) (↑h : ℝ) * ‖asiegel K a‖) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)) *
        supOfBasis K)

Tactic:
?_
-- 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)
p q : ℕ
hpq : p < q
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
hxbound :
  ‖x‖ ≤
    (HMul.hMul (α := ℝ) (↑q : ℝ) (↑(finrank ℚ K) : ℝ) * ‖asiegel K a‖) ^
      ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)
⊢ ∑ _r : K →+* ℂ,
      (HMul.hMul (α := ℝ) (↑q : ℝ) (↑h : ℝ) * ‖asiegel K a‖) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)) *
        supOfBasis K ≤
    (↑h : ℝ) * c₂ K * ((↑q : ℝ) * c₁ K * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))

Tactic:
?_
-- 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)
p q : ℕ
hpq : p < q
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
hxbound :
  ‖x‖ ≤
    (HMul.hMul (α := ℝ) (↑q : ℝ) (↑(finrank ℚ K) : ℝ) * ‖asiegel K a‖) ^
      ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)
⊢ (↑h : ℝ) * c₂ K * ((↑q : ℝ) * c₁ K * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)) ≤
    c₁ K * (c₁ K * (↑q : ℝ) * A) ^ ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))

Tactic:
?_
-- 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)
p q : ℕ
hpq : p < q
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
hxbound :
  ‖x‖ ≤
    (HMul.hMul (α := ℝ) (↑q : ℝ) (↑(finrank ℚ K) : ℝ) * ‖asiegel K a‖) ^
      ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)
calc_1 :
  house.{u_1} (K := K)
      (∑ x_1 : K →+* ℂ,
        (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, x_1)) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))) ≤
    ∑ x_1 : K →+* ℂ,
      house (K := K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, x_1)) : 𝓞 K) : 𝓞 K)
              ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K)) :
          K)
⊢ house (K := K)
      ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (∑ r : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, r)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K)) :
        K) ≤
    ∑ r : K →+* ℂ,
      house
        (HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x (l, r)) : 𝓞 K) : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K))

Tactic:
simp_rw [← map_mul, map_sum]

Premises used: map_sum, map_mul
-- 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)
p q : ℕ
hpq : p < q
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
hxbound :
  ‖x‖ ≤
    (HMul.hMul (α := ℝ) (↑q : ℝ) (↑(finrank ℚ K) : ℝ) * ‖asiegel K a‖) ^
      ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)
⊢ house.{u_1} (K := K)
      (∑ x_1 : K →+* ℂ,
        (algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
          (HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, x_1)) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K))) ≤
    ∑ x_1 : K →+* ℂ,
      house (K := K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, x_1)) : 𝓞 K) : 𝓞 K)
              ((newBasis K : (a : K →+* ℂ) → 𝓞 K) x_1 : 𝓞 K)) :
          K)

Tactic:
apply house_sum_le_sum_house

Premises used: NumberField.house_sum_le_sum_house
-- 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)
p q : ℕ
hpq : p < q
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
inst_2 : Fintype β
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 α
Apos : 0 ≤ A
hxbound :
  ‖x‖ ≤
    (HMul.hMul (α := ℝ) (↑q : ℝ) (↑(finrank ℚ K) : ℝ) * ‖asiegel K a‖) ^
      ((↑p : ℝ) / HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < HSub.hSub (α := ℝ) (↑q : ℝ) (↑p : ℝ)
calc_2 :
  ∀ (r : K →+* ℂ),
    Membership.mem (γ := Finset (K →+* ℂ)) univ r →
      house
          (HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x (l, r)) : 𝓞 K) : K)
            ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K)) ≤
        ‖x (l, r)‖ *
          house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K)
⊢ LE.le (α := ℝ)
    (∑ r : K →+* ℂ,
      house
        (HMul.hMul (α := K) (β := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (↑(x (l, r)) : 𝓞 K) : K)
          ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K)))
    (∑ r : K →+* ℂ,
      ‖x (l, r)‖ *
        house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) r : 𝓞 K) : K))

Tactic:
gcongr with r _