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)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this_1 :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ u : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : β,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (↑(x (y, x_1)) : 𝓞 K)
          (∑ u : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k y x_1 u) : 𝓞 K) : 𝓞 K)
              ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
l : β
h :
  ∀ (l_1 : K →+* ℂ),
    HMul.hMul (α := 𝓞 K) (↑(x (l, l_1)) : 𝓞 K)
        (∑ u : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l l_1 u) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)) =
      (fun (j : β) ↦ a k j) l *
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, l_1)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l_1 : 𝓞 K)
⊢ Eq.{u_1 + 1} (α := (K →+* ℂ) → 𝓞 K)
    (fun (x_1 : K →+* ℂ) ↦
      HMul.hMul (α := 𝓞 K) (↑(x (l, x_1)) : 𝓞 K)
        (∑ u : K →+* ℂ,
          HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l x_1 u) : 𝓞 K) : 𝓞 K)
            ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
    fun (i : K →+* ℂ) ↦
    (fun (j : β) ↦ a k j) l *
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l, i)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) i : 𝓞 K)

Tactic:
ext1 l
-- 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)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this_1 :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ u : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : β,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (↑(x (y, x_1)) : 𝓞 K)
          (∑ u : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k y x_1 u) : 𝓞 K) : 𝓞 K)
              ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
l_1 : β
l : K →+* ℂ
h :
  (↑(x (l_1, l)) : 𝓞 K) * HMul.hMul (β := 𝓞 K) (a k l_1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l : 𝓞 K) =
    (fun (j : β) ↦ a k j) l_1 *
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l_1, l)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l : 𝓞 K)
⊢ HMul.hMul (α := 𝓞 K) (↑(x (l_1, l)) : 𝓞 K)
      (∑ u : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k l_1 l u) : 𝓞 K) : 𝓞 K)
          ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)) =
    (fun (j : β) ↦ a k j) l_1 *
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l_1, l)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l : 𝓞 K)

Tactic:
rw [← lin_1]

Premises used: _private.0.NumberField.house.lin_1
-- 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)
x : Prod.{u_3, u_1} β (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst_2 : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 :
  ∀ (u : K →+* ℂ),
    Eq.{u_1 + 1} (α := 𝓞 K) (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K))
      0
this_1 :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ u : K →+* ℂ,
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K)
        (∑ r : K →+* ℂ, ∑ l : β, HMul.hMul (α := 𝓞 K) (↑(a' K a k l r u) : 𝓞 K) (↑(x (l, r)) : 𝓞 K) : 𝓞 K)
        ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K))
this :
  Eq.{u_1 + 1} (α := 𝓞 K) 0
    (∑ y : β,
      ∑ x_1 : K →+* ℂ,
        HMul.hMul (α := 𝓞 K) (↑(x (y, x_1)) : 𝓞 K)
          (∑ u : K →+* ℂ,
            HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(a' K a k y x_1 u) : 𝓞 K) : 𝓞 K)
              ((newBasis K : (a : K →+* ℂ) → 𝓞 K) u : 𝓞 K)))
l_1 : β
l : K →+* ℂ
⊢ (↑(x (l_1, l)) : 𝓞 K) * HMul.hMul (β := 𝓞 K) (a k l_1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l : 𝓞 K) =
    (fun (j : β) ↦ a k j) l_1 *
      HMul.hMul (α := 𝓞 K) (β := 𝓞 K) ((↑(x (l_1, l)) : 𝓞 K) : 𝓞 K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) l : 𝓞 K)

Tactic:
ring
-- Module: Mathlib.NumberTheory.NumberField.House
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
inst_2 : DecidableEq (K →+* ℂ)
⊢ 0 ≤ c₂ K

Tactic:
mul_nonneg (le_trans zero_le_one (le_max_left ..)) (supOfBasis_nonneg _)

Premises used: mul_nonneg, zero_le_one, _private.0.NumberField.house.supOfBasis_nonneg, le_max_left, le_trans
-- 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
⊢ 0 ≤ c K

Tactic:
have := c_nonneg K
-- 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
rw : ∀ (i : Prod.{u_2, u_1} α (K →+* ℂ)) (j : Prod.{u_3, u_1} β (K →+* ℂ)), ‖asiegel K a i j‖ ≤ c₂ K * A
hr : 0 ≤ c₂ K * A
⊢ ‖asiegel K a‖ ≤ c₂ K * A

Tactic:
rw [Matrix.norm_le_iff]

Premises used: Matrix.norm_le_iff
-- 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 →+* ℂ)
⊢ ‖asiegel K a kr lu‖ = (↑|asiegel K a kr lu| : ℝ)

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)
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 →+* ℂ)
⊢ (↑|asiegel K a kr lu| : ℝ) ≤
    c K *
      house (K := K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (HMul.hMul (β := 𝓞 K) (a kr.1 lu.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 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)
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 *
      house (K := K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (HMul.hMul (β := 𝓞 K) (a kr.1 lu.1) ((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)

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)
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 * 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:
?_
-- 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 * 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:
?_
-- 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 * A * supOfBasis K ≤ c₂ K * A

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)
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_1 : ‖asiegel K a kr lu‖ = (↑|asiegel K a kr lu| : ℝ)
calc_2 :
  (↑|asiegel K a kr lu| : ℝ) ≤
    c K *
      house (K := K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (HMul.hMul (β := 𝓞 K) (a kr.1 lu.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K)) :
          K)
calc_3 :
  c K *
      house (K := K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (HMul.hMul (β := 𝓞 K) (a kr.1 lu.1) ((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)
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)
calc_5 :
  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
calc_6 : c K * A * supOfBasis K ≤ c₂ K * A
⊢ ‖asiegel K a kr lu‖ ≤ 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 := ?_

Premises used: HMul.hMul, _private.0.NumberField.house.newBasis, _private.0.NumberField.house.asiegel, Algebra.algebraMap, _private.0.NumberField.house.c, _private.0.NumberField.house.supOfBasis, Prod.fst, NumberField.house, _private.0.NumberField.house.c₂, NumberField.RingOfIntegers, Prod.snd, DFunLike.coe
-- 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_1 : ‖asiegel K a kr lu‖ = norm (E := ℝ) (↑(asiegel K a kr lu) : ℝ)
⊢ ‖asiegel K a kr lu‖ = (↑|asiegel K a kr lu| : ℝ)

Tactic:
simp only [Int.cast_abs, ← Real.norm_eq_abs (asiegel K a kr lu)]

Premises used: Int.cast, Int.cast_abs, _private.0.NumberField.house.asiegel, Real.norm_eq_abs
-- 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 →+* ℂ)
⊢ ‖asiegel K a kr lu‖ = norm (E := ℝ) (↑(asiegel K a kr lu) : ℝ)

Tactic:
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)
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 →+* ℂ)
⊢ ∀ (α : 𝓞 K) (i : K →+* ℂ),
    norm (E := ℂ)
        (↑(((((Basis.repr
                          (Basis.reindex (ι := ChooseBasisIndex ℤ (𝓞 K))
                            (integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K)
                            (Equiv.symm (equivReindex K) : ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ))) :
                        K ≃ₗ[ℚ] (K →+* ℂ) →₀ ℚ) :
                      (a : K) → (K →+* ℂ) →₀ ℚ)
                    (↑α : K) :
                  (K →+* ℂ) →₀ ℚ) :
                (a : K →+* ℂ) → ℚ)
              i) :
          ℂ) ≤
      c K * house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K)

Tactic:
have remark := basis_repr_norm_le_const_mul_house K
-- 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 →+* ℂ)
remark :
  ∀ (α : 𝓞 K) (i : K →+* ℂ),
    norm (E := ℂ)
        (↑(((((Basis.repr
                          (Basis.reindex (ι := ChooseBasisIndex ℤ (𝓞 K))
                            (integralBasis K : Basis (ChooseBasisIndex ℤ (𝓞 K)) ℚ K)
                            (Equiv.symm (equivReindex K) : ChooseBasisIndex ℤ (𝓞 K) ≃ (K →+* ℂ))) :
                        K ≃ₗ[ℚ] (K →+* ℂ) →₀ ℚ) :
                      (a : K) → (K →+* ℂ) →₀ ℚ)
                    (↑α : K) :
                  (K →+* ℂ) →₀ ℚ) :
                (a : K →+* ℂ) → ℚ)
              i) :
          ℂ) ≤
      c K * house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K)
⊢ ∀ (α : 𝓞 K) (i : K →+* ℂ),
    |(↑(((((Basis.repr (RingOfIntegers.basis K) : 𝓞 K ≃ₗ[ℤ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℤ) :
                      (a : 𝓞 K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℤ)
                    α :
                  ChooseBasisIndex ℤ (𝓞 K) →₀ ℤ) :
                (a : ChooseBasisIndex ℤ (𝓞 K)) → ℤ)
              (((Equiv.symm (Equiv.symm (equivReindex K)) : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) :
                    (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K))
                  i :
                ChooseBasisIndex ℤ (𝓞 K))) :
          ℝ)| ≤
      c K * house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K)

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

Premises used: Rat.cast_intCast, Module.Basis.repr_reindex, eq_intCast, NumberField.integralBasis_repr_apply, Finsupp.mapDomain_equiv_apply, Complex.norm_intCast
-- 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 →+* ℂ)
remark :
  ∀ (α : 𝓞 K) (i : K →+* ℂ),
    |(↑(((((Basis.repr (RingOfIntegers.basis K) : 𝓞 K ≃ₗ[ℤ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℤ) :
                      (a : 𝓞 K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℤ)
                    α :
                  ChooseBasisIndex ℤ (𝓞 K) →₀ ℤ) :
                (a : ChooseBasisIndex ℤ (𝓞 K)) → ℤ)
              (((Equiv.symm (Equiv.symm (equivReindex K)) : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) :
                    (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K))
                  i :
                ChooseBasisIndex ℤ (𝓞 K))) :
          ℝ)| ≤
      c K * house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K)
⊢ (↑|asiegel K a kr lu| : ℝ) ≤
    c K *
      house (K := K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (HMul.hMul (β := 𝓞 K) (a kr.1 lu.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K)) :
          K)

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

Premises used: HMul.hMul, _private.0.NumberField.house.newBasis, _private.0.NumberField.house.asiegel, Algebra.algebraMap, congrArg, _private.0.NumberField.house.c, cast, LE.le, Prod.fst, NumberField.house, Int.cast_abs._simp_1, congrFun', NumberField.RingOfIntegers, _private.0.NumberField.house.a', Prod.snd, DFunLike.coe
-- 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 →+* ℂ)
remark :
  ∀ (α : 𝓞 K) (i : K →+* ℂ),
    |(↑(((((Basis.repr (RingOfIntegers.basis K) : 𝓞 K ≃ₗ[ℤ] ChooseBasisIndex ℤ (𝓞 K) →₀ ℤ) :
                      (a : 𝓞 K) → ChooseBasisIndex ℤ (𝓞 K) →₀ ℤ)
                    α :
                  ChooseBasisIndex ℤ (𝓞 K) →₀ ℤ) :
                (a : ChooseBasisIndex ℤ (𝓞 K)) → ℤ)
              (((Equiv.symm (Equiv.symm (equivReindex K)) : (K →+* ℂ) ≃ ChooseBasisIndex ℤ (𝓞 K)) :
                    (a : K →+* ℂ) → ChooseBasisIndex ℤ (𝓞 K))
                  i :
                ChooseBasisIndex ℤ (𝓞 K))) :
          ℝ)| ≤
      c K * house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) α : K)
⊢ (↑|asiegel K a kr lu| : ℝ) ≤
    c K *
      house (K := K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (HMul.hMul (β := 𝓞 K) (a kr.1 lu.1) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K)) :
          K)

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

Premises used: HMul.hMul, _private.0.NumberField.house.newBasis, Prod.fst, Prod.snd, DFunLike.coe
-- 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_3 :
  c 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 →+* ℂ) → ℂ)‖ ≤
    c 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 →+* ℂ) → ℂ))
⊢ c K *
      house (K := K)
        ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K)
            (HMul.hMul (β := 𝓞 K) (a kr.1 lu.1) ((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)

Tactic:
simp only [house, map_mul, mul_assoc]

Premises used: mul_assoc, map_mul, NumberField.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)
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_3 :
  ‖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 →+* ℂ) → ℂ)
⊢ c 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 →+* ℂ) → ℂ)‖ ≤
    c 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:
gcongr