-- 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:
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

Tactic:
rintro _ ⟨x, ⟨k, -, rfl⟩, rfl⟩

Result:
case intro.intro.intro.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'
k : ι
⊢ ↑(abv ((bS.repr a) k)) < 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
⊢ ↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι

Tactic:
have y'_nonneg : 0 ≤ y' := le_trans (abv.nonneg _) (hy' i)

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'
⊢ ↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι

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 : ι
⊢ ↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι

Tactic:
have him : (Finset.univ.image fun k => abv (bS.repr a k)).Nonempty :=
  ⟨_, Finset.mem_image.mpr ⟨i, Finset.mem_univ _, rfl⟩⟩

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
⊢ ↑(abv ((Algebra.norm R) a)) < ↑(normBound abv bS) * y ^ Fintype.card ι

Proof state:
case intro.b0
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'
⊢ 0 < ↑(normBound abv bS)

Tactic:
exact Int.cast_pos.mpr (normBound_pos abv bS)

Result:
no goals