awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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 * A
have calc_1 : ‖asiegel K a kr lu‖ = (↑|asiegel K a kr lu| : ℝ)
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 := ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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| : ℝ)
⊢ ‖asiegel K a kr lu‖ ≤ c₂ K * A
have 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)
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 := ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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)
⊢ ‖asiegel K a kr lu‖ ≤ c₂ K * A
have 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)
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 := ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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)
⊢ ‖asiegel K a kr lu‖ ≤ c₂ K * A
have 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)
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 := ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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)
⊢ ‖asiegel K a kr lu‖ ≤ c₂ K * A
have 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
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 := ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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
⊢ ‖asiegel K a kr lu‖ ≤ c₂ K * A
have calc_6 : c K * A * supOfBasis K ≤ 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 := ?_
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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| : ℝ)
have calc_1 : ‖asiegel K a kr lu‖ = norm (E := ℝ) (↑(asiegel K a kr lu) : ℝ)
Tactic: simp only [Int.cast_abs, ← Real.norm_eq_abs (asiegel K a kr lu)]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (hypothesis)
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)
have 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)
Tactic: have remark := basis_repr_norm_le_const_mul_house K
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (hypothesis)
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)
⊢ (↑|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)
have 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)
Tactic: simp only [Basis.repr_reindex, Finsupp.mapDomain_equiv_apply,
        integralBasis_repr_apply, eq_intCast, Rat.cast_intCast,
          Complex.norm_intCast] at remark
Cleared hypotheses: remark
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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)
have 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 →+* ℂ) → ℂ))
Tactic: simp only [house, map_mul, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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 *
      ‖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 →+* ℂ) → ℂ))
have 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 →+* ℂ) → ℂ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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)
have 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))
Tactic: rw [mul_assoc, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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))
have calc_4 : 0 ≤ house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K)
Tactic: gcongr _ * (?_ * _)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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)
⊢ 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))
have calc_4₁ : house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) (a kr.1 lu.1) : K) ≤ A
Tactic: gcongr _ * (?_ * _)
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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
have calc_5 : house (K := K) ((algebraMap (𝓞 K) K : (a : 𝓞 K) → K) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K) ≤ supOfBasis K
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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) ((newBasis K : (a : K →+* ℂ) → 𝓞 K) lu.2 : 𝓞 K) : K) ≤
    supOfBasis K
have 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)
Tactic: simp only [supOfBasis, le_sup'_iff, mem_univ]
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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 →+* ℂ)
⊢ ∃ (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)
have w : K →+* ℂ
Tactic: use lu.2
-- Lean 4 proof step from Mathlib.NumberTheory.NumberField.House (goal)
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 →+* ℂ
⊢ ∃ (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)
have 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)
Tactic: use lu.2