awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
i j k : ι
hijk :
  Ne.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
⊢ 0 <
    ((↑(Fintype.card ι) : ℤ) *
        Finset.max'
          (Finset.image
            (fun (ijk : ι × ι × ι) ↦
              (abv : (a : R) → ℤ)
                ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
            Finset.univ)
          ⋯) ^
      Fintype.card ι

Tactic:
pow_pos (mul_pos (Int.natCast_pos.mpr (Fintype.card_pos_iff.mpr ⟨i⟩)) ?_) _

Premises used: Iff.mpr, pow_pos, Nonempty.intro, mul_pos, Int.natCast_pos, Fintype.card_pos_iff
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
i j k : ι
hijk :
  Ne.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
refine :
  0 <
    Finset.max'
      (Finset.image
        (fun (ijk : ι × ι × ι) ↦
          (abv : (a : R) → ℤ)
            ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
        Finset.univ)
      ⋯
⊢ 0 <
    ((↑(Fintype.card ι) : ℤ) *
        Finset.max'
          (Finset.image
            (fun (ijk : ι × ι × ι) ↦
              (abv : (a : R) → ℤ)
                ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
            Finset.univ)
          ⋯) ^
      Fintype.card ι

Tactic:
refine pow_pos (mul_pos (Int.natCast_pos.mpr (Fintype.card_pos_iff.mpr ⟨i⟩)) ?_) _

Premises used: Iff.mpr, pow_pos, Nonempty.intro, mul_pos, Int.natCast_pos, Fintype.card_pos_iff
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
i j k : ι
hijk :
  Ne.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
⊢ 0 <
    Finset.max'
      (Finset.image
        (fun (ijk : ι × ι × ι) ↦
          (abv : (a : R) → ℤ)
            ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
        Finset.univ)
      ⋯

Tactic:
lt_of_lt_of_le (abv.pos hijk) (Finset.le_max' _ _ ?_)

Premises used: AbsoluteValue.pos, Finset.le_max', lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
i j k : ι
hijk :
  Ne.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
refine :
  Membership.mem (α := ℤ) (γ := Finset ℤ)
    (Finset.image
      (fun (ijk : ι × ι × ι) ↦
        (abv : (a : R) → ℤ)
          ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
      Finset.univ)
    ((abv : (a : R) → ℤ) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) : ℤ)
⊢ 0 <
    Finset.max'
      (Finset.image
        (fun (ijk : ι × ι × ι) ↦
          (abv : (a : R) → ℤ)
            ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
        Finset.univ)
      ⋯

Tactic:
refine lt_of_lt_of_le (abv.pos hijk) (Finset.le_max' _ _ ?_)

Premises used: AbsoluteValue.pos, Finset.le_max', lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
i j k : ι
hijk :
  Ne.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
⊢ Membership.mem (α := ℤ) (γ := Finset ℤ)
    (Finset.image
      (fun (ijk : ι × ι × ι) ↦
        (abv : (a : R) → ℤ)
          ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
      Finset.univ)
    ((abv : (a : R) → ℤ) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) : ℤ)

Tactic:
Finset.mem_image.mpr ⟨⟨i, j, k⟩, Finset.mem_univ _, rfl⟩

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_image, Prod.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
i j k : ι
hijk :
  Ne.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
⊢ Membership.mem (α := ℤ) (γ := Finset ℤ)
    (Finset.image
      (fun (ijk : ι × ι × ι) ↦
        (abv : (a : R) → ℤ)
          ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
      Finset.univ)
    ((abv : (a : R) → ℤ) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) : ℤ)

Tactic:
exact Finset.mem_image.mpr ⟨⟨i, j, k⟩, Finset.mem_univ _, rfl⟩

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_image, And.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
a : S
y : ℤ
hy : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y
rw :
  ((abv : (a : R) → ℤ)
      ((Algebra.norm R : (a : S) → R)
          (∑ i : ι,
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
              ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R) ((bS : (a : ι) → S) i : S)) :
        R) :
    ℤ)
| ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) a : R) : ℤ)

Tactic:
rw [← bS.sum_repr a]

Premises used: Module.Basis.sum_repr
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
a : S
y : ℤ
hy : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y
conv_lhs :
  (abv : (a : R) → ℤ)
      ((Algebra.norm R : (a : S) → R)
          (∑ i : ι,
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
              ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R) ((bS : (a : ι) → S) i : S)) :
        R) ≤
    normBound abv bS * y ^ Fintype.card ι
⊢ (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) a : R) ≤ normBound abv bS * y ^ Fintype.card ι

Tactic:
conv_lhs => rw [← bS.sum_repr a]

Premises used: Module.Basis.sum_repr
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
a : S
y : ℤ
hy : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y
rw :
  (abv : (a : R) → ℤ)
      (Matrix.det.{u_1, u_5} (n := ι)
        ((LinearMap.toMatrix bS bS : (a : S →ₗ[R] S) → Matrix ι ι R)
          ((Algebra.lmul R S : (a : S) → End R S)
            (∑ i : ι,
              HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
                ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R) ((bS : (a : ι) → S) i : S))))) ≤
    normBound abv bS * y ^ Fintype.card ι
⊢ (abv : (a : R) → ℤ)
      ((Algebra.norm R : (a : S) → R)
          (∑ i : ι,
            HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
              ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R) ((bS : (a : ι) → S) i : S)) :
        R) ≤
    normBound abv bS * y ^ Fintype.card ι

Tactic:
rw [Algebra.norm_apply, ← LinearMap.det_toMatrix bS]

Premises used: Algebra.norm_apply, LinearMap.det_toMatrix
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
a : S
y : ℤ
hy : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y
simp :
  (abv : (a : R) → ℤ)
      (Matrix.det.{u_1, u_5} (n := ι)
        (∑ x : ι,
          HSMul.hSMul (α := R) (β := Matrix ι ι R) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) x : R)
            ((LinearMap.toMatrix bS bS : (a : S →ₗ[R] S) → Matrix ι ι R)
                ((Algebra.lmul R S : (a : S) → End R S) ((bS : (a : ι) → S) x : S)) :
              Matrix ι ι R))) ≤
    (Fintype.card ι).factorial •
      (Fintype.card ι •
          (Finset.max'
              (Finset.image
                (fun (ijk : ι × ι × ι) ↦
                  (abv : (a : R) → ℤ)
                    ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 :
                      R))
                Finset.univ)
              ⋯ *
            y)) ^
        Fintype.card ι
⊢ (abv : (a : R) → ℤ)
      (Matrix.det.{u_1, u_5} (n := ι)
        ((LinearMap.toMatrix bS bS : (a : S →ₗ[R] S) → Matrix ι ι R)
          ((Algebra.lmul R S : (a : S) → End R S)
            (∑ i : ι,
              HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S)
                ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R) ((bS : (a : ι) → S) i : S))))) ≤
    normBound abv bS * y ^ Fintype.card ι

Tactic:
simp only [map_sum, map_smul, map_sum, map_smul,
    normBound, smul_mul_assoc, ← mul_pow]

Premises used: smul_mul_assoc, map_sum, ClassGroup.normBound, mul_pow, map_smul
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
a : S
y : ℤ
hy : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y
⊢ (abv : (a : R) → ℤ)
      (Matrix.det.{u_1, u_5} (n := ι)
        (∑ k : ι,
          HSMul.hSMul (α := R) (β := Matrix ι ι R) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R)
            ((LinearMap.toMatrix bS bS : (a : S →ₗ[R] S) → Matrix ι ι R)
                ((Algebra.lmul R S : (a : S) → End R S) ((bS : (a : ι) → S) k : S)) :
              Matrix ι ι R))) ≤
    (Fintype.card ι).factorial •
      (Finset.card.{u_5} (α := ι) Finset.univ • y *
          Finset.max'
            (Finset.image
              (fun (ijk : ι × ι × ι) ↦
                (abv : (a : R) → ℤ)
                  ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
              Finset.univ)
            ⋯) ^
        Fintype.card ι

Tactic:
Matrix.det_sum_smul_le Finset.univ _ hy

Premises used: Finset.univ, Matrix.det_sum_smul_le
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
a : S
y : ℤ
hy : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y
h :
  Fintype.card ι •
      (Finset.max'
          (Finset.image
            (fun (ijk : ι × ι × ι) ↦
              (abv : (a : R) → ℤ)
                ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
            Finset.univ)
          ⋯ *
        y) =
    Finset.card.{u_5} (α := ι) Finset.univ • y *
      Finset.max'
        (Finset.image
          (fun (ijk : ι × ι × ι) ↦
            (abv : (a : R) → ℤ)
              ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
          Finset.univ)
        ⋯
convert_5 : ℤ
convert_6 :
  ∀ (k i j : ι),
    (abv : (a : R) → ℤ)
        ((LinearMap.toMatrix bS bS : (a : S →ₗ[R] S) → Matrix ι ι R)
            ((Algebra.lmul R S : (a : S) → End R S) ((bS : (a : ι) → S) k : S)) i j :
          R) ≤
      Finset.max'
        (Finset.image
          (fun (ijk : ι × ι × ι) ↦
            (abv : (a : R) → ℤ)
              ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
          Finset.univ)
        ⋯
⊢ (abv : (a : R) → ℤ)
      (Matrix.det.{u_1, u_5} (n := ι)
        (∑ x : ι,
          HSMul.hSMul (α := R) (β := Matrix ι ι R) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) x : R)
            ((LinearMap.toMatrix bS bS : (a : S →ₗ[R] S) → Matrix ι ι R)
                ((Algebra.lmul R S : (a : S) → End R S) ((bS : (a : ι) → S) x : S)) :
              Matrix ι ι R))) ≤
    (Fintype.card ι).factorial •
      (Fintype.card ι •
          (Finset.max'
              (Finset.image
                (fun (ijk : ι × ι × ι) ↦
                  (abv : (a : R) → ℤ)
                    ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 :
                      R))
                Finset.univ)
              ⋯ *
            y)) ^
        Fintype.card ι

Tactic:
convert! Matrix.det_sum_smul_le Finset.univ _ hy using 3

Premises used: Finset.univ, Matrix.det_sum_smul_le
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
a : S
y : ℤ
hy : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y
i j k : ι
convert_6 :
  Membership.mem (α := ℤ) (γ := Finset ℤ)
    (Finset.image
      (fun (ijk : ι × ι × ι) ↦
        (abv : (a : R) → ℤ)
          ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
      Finset.univ)
    ((abv : (a : R) → ℤ)
        ((LinearMap.toMatrix bS bS : (a : S →ₗ[R] S) → Matrix ι ι R)
            ((Algebra.lmul R S : (a : S) → End R S) ((bS : (a : ι) → S) i : S)) j k :
          R) :
      ℤ)
⊢ (abv : (a : R) → ℤ)
      ((LinearMap.toMatrix bS bS : (a : S →ₗ[R] S) → Matrix ι ι R)
          ((Algebra.lmul R S : (a : S) → End R S) ((bS : (a : ι) → S) i : S)) j k :
        R) ≤
    Finset.max'
      (Finset.image
        (fun (ijk : ι × ι × ι) ↦
          (abv : (a : R) → ℤ)
            ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
        Finset.univ)
      ⋯

Tactic:
apply Finset.le_max'

Premises used: Finset.le_max'
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
a : S
y : ℤ
hy : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y
i j k : ι
⊢ Membership.mem (α := ℤ) (γ := Finset ℤ)
    (Finset.image
      (fun (ijk : ι × ι × ι) ↦
        (abv : (a : R) → ℤ)
          ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
      Finset.univ)
    ((abv : (a : R) → ℤ)
        ((LinearMap.toMatrix bS bS : (a : S →ₗ[R] S) → Matrix ι ι R)
            ((Algebra.lmul R S : (a : S) → End R S) ((bS : (a : ι) → S) i : S)) j k :
          R) :
      ℤ)

Tactic:
Finset.mem_image.mpr ⟨⟨i, j, k⟩, Finset.mem_univ _, rfl⟩

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_image, Prod.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
a : S
y : ℤ
hy : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y
i j k : ι
⊢ Membership.mem (α := ℤ) (γ := Finset ℤ)
    (Finset.image
      (fun (ijk : ι × ι × ι) ↦
        (abv : (a : R) → ℤ)
          ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
      Finset.univ)
    ((abv : (a : R) → ℤ)
        ((LinearMap.toMatrix bS bS : (a : S →ₗ[R] S) → Matrix ι ι R)
            ((Algebra.lmul R S : (a : S) → End R S) ((bS : (a : ι) → S) i : S)) j k :
          R) :
      ℤ)

Tactic:
exact Finset.mem_image.mpr ⟨⟨i, j, k⟩, Finset.mem_univ _, rfl⟩

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_image, And.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
T : Type u_6
inst_6 : Ring T
inst_7 : LinearOrder T
inst_8 : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), (↑((abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R)) : T) < y
obtain :
  ∀ (i : ι),
    (↑((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) a : R)) : T) < (↑(normBound abv bS) : T) * y ^ Fintype.card ι
⊢ (↑((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) a : R)) : T) < (↑(normBound abv bS) : T) * y ^ Fintype.card ι

Tactic:
obtain ⟨i⟩ := bS.index_nonempty

Premises used: Module.Basis.index_nonempty
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
T : Type u_6
inst_6 : Ring T
inst_7 : LinearOrder T
inst_8 : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), (↑((abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R)) : T) < y
i : ι
⊢ Finset.Nonempty (α := ℤ)
    (Finset.image (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
      Finset.univ)

Tactic:
have him : (Finset.univ.image fun k => abv (bS.repr a k)).Nonempty :=
    ⟨_, Finset.mem_image.mpr ⟨i, Finset.mem_univ _, rfl⟩⟩
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
T : Type u_6
inst_6 : Ring T
inst_7 : LinearOrder T
inst_8 : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), (↑((abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R)) : T) < y
i : ι
him :
  Finset.Nonempty (α := ℤ)
    (Finset.image (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
      Finset.univ)
⊢ let y' :=
    Finset.max'
      (Finset.image
        (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
        Finset.univ)
      him;
  y' =
    Finset.max'
      (Finset.image
        (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
        Finset.univ)
      him

Tactic:
set y' : ℤ := Finset.max' _ him with y'_def

Premises used: Finset.max'
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
T : Type u_6
inst_6 : Ring T
inst_7 : LinearOrder T
inst_8 : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), (↑((abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R)) : T) < y
i : ι
him :
  Finset.Nonempty (α := ℤ)
    (Finset.image (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
      Finset.univ)
y' : ℤ :=
  Finset.max'
    (Finset.image (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
      Finset.univ)
    him
y'_def :
  y' =
    Finset.max'
      (Finset.image
        (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
        Finset.univ)
      him
k : ι
⊢ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y'

Tactic:
@Finset.le_max' ℤ _ _ _ (Finset.mem_image.mpr ⟨k, Finset.mem_univ _, rfl⟩)

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_image, Finset.le_max', And.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
T : Type u_6
inst_6 : Ring T
inst_7 : LinearOrder T
inst_8 : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), (↑((abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R)) : T) < y
i : ι
him :
  Finset.Nonempty (α := ℤ)
    (Finset.image (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
      Finset.univ)
y' : ℤ :=
  Finset.max'
    (Finset.image (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
      Finset.univ)
    him
y'_def :
  y' =
    Finset.max'
      (Finset.image
        (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
        Finset.univ)
      him
k : ι
⊢ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y'

Tactic:
exact @Finset.le_max' ℤ _ _ _ (Finset.mem_image.mpr ⟨k, Finset.mem_univ _, rfl⟩)

Premises used: Iff.mpr, Finset.mem_univ, Finset.mem_image, Finset.le_max', And.intro, Exists.intro, rfl
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
T : Type u_6
inst_6 : Ring T
inst_7 : LinearOrder T
inst_8 : IsStrictOrderedRing T
a : S
y : T
hy : ∀ (k : ι), (↑((abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R)) : T) < y
i : ι
him :
  Finset.Nonempty (α := ℤ)
    (Finset.image (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
      Finset.univ)
y' : ℤ :=
  Finset.max'
    (Finset.image (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
      Finset.univ)
    him
y'_def :
  y' =
    Finset.max'
      (Finset.image
        (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
        Finset.univ)
      him
⊢ ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y'

Tactic:
have hy' : ∀ k, abv (bS.repr a k) ≤ y' := by
    intro k
    exact @Finset.le_max' ℤ _ _ _ (Finset.mem_image.mpr ⟨k, Finset.mem_univ _, rfl⟩)