-- Mathlib/NumberTheory/ClassNumber/Finite.lean
theorem norm_lt {T : Type*} [LinearOrderedRing T] (a : S) {y : T}
    (hy : ∀ k, (abv (bS.repr a k) : T) < y) :
    (abv (Algebra.norm R a) : T) < normBound abv bS * y ^ Fintype.card ι

Proof state:
case intro.h₂
R : Type u_1
S : Type u_2
inst✝⁶ : EuclideanDomain R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝ : LinearOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him
y'_def : y' = (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
this : ↑y' < y
y'_nonneg : 0 ≤ y'
⊢ ↑y' ^ Fintype.card ι < y ^ Fintype.card ι

Tactic:
exact pow_lt_pow_left₀ this (Int.cast_nonneg.mpr y'_nonneg) (@Fintype.card_ne_zero _ _ ⟨i⟩)

Result:
no goals

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝⁶ : EuclideanDomain R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝ : LinearOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him
y'_def : y' = (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
this : ↑y' < y
y'_nonneg : 0 ≤ y'
⊢ ↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι

Tactic:
apply (Int.cast_le.mpr (norm_le abv bS a hy')).trans_lt

Result:
case intro
R : Type u_1
S : Type u_2
inst✝⁶ : EuclideanDomain R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝ : LinearOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him
y'_def : y' = (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
this : ↑y' < y
y'_nonneg : 0 ≤ y'
⊢ ↑(normBound abv bS * y' ^ Fintype.card ι) < ↑(normBound abv bS) * y ^ Fintype.card ι

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : EuclideanDomain R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝ : LinearOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him
y'_def : y' = (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
⊢ ∀ y_1 ∈ Finset.image (fun x => ↑x) (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ), y_1 < y

Tactic:
simp only [Finset.mem_image, exists_prop]

Result:
R : Type u_1
S : Type u_2
inst✝⁶ : EuclideanDomain R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝ : LinearOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him
y'_def : y' = (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
⊢ ∀ (y_1 : T), (∃ a_1, (∃ a_2 ∈ Finset.univ, abv ((bS.repr a) a_2) = a_1) ∧ ↑a_1 = y_1) → y_1 < y

Proof state:
case intro
R : Type u_1
S : Type u_2
inst✝⁶ : EuclideanDomain R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝ : LinearOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him
y'_def : y' = (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
this : ↑y' < y
y'_nonneg : 0 ≤ y'
⊢ ↑(normBound abv bS * y' ^ Fintype.card ι) < ↑(normBound abv bS) * y ^ Fintype.card ι

Tactic:
simp only [Int.cast_mul, Int.cast_pow]

Result:
case intro
R : Type u_1
S : Type u_2
inst✝⁶ : EuclideanDomain R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝ : LinearOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him
y'_def : y' = (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him
hy' : ∀ (k : ι), abv ((bS.repr a) k) ≤ y'
this : ↑y' < y
y'_nonneg : 0 ≤ y'
⊢ ↑(normBound abv bS) * ↑y' ^ Fintype.card ι < ↑(normBound abv bS) * y ^ Fintype.card ι

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : EuclideanDomain R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝ : LinearOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him
y'_def : y' = (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him
⊢ ∀ (k : ι), abv ((bS.repr a) k) ≤ y'

Tactic:
intro k

Result:
R : Type u_1
S : Type u_2
inst✝⁶ : EuclideanDomain R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝ : LinearOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
him : (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).Nonempty
y' : ℤ := (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him
y'_def : y' = (Finset.image (fun k => abv ((bS.repr a) k)) Finset.univ).max' him
k : ι
⊢ abv ((bS.repr a) k) ≤ y'

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : EuclideanDomain R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝ : LinearOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
⊢ ↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι

Tactic:
obtain ⟨i⟩ := bS.index_nonempty

Result:
case intro
R : Type u_1
S : Type u_2
inst✝⁶ : EuclideanDomain R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain S
inst✝³ : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
bS : Basis ι R S
T : Type u_6
inst✝ : LinearOrderedRing T
a : S
y : T
hy : ∀ (k : ι), ↑(abv ((bS.repr a) k)) < y
i : ι
⊢ ↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι