awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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
⊢ 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)
        ⋯
have 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)
        sorry *
      y) =
  Fintype.card ι • 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)
      sorry
Tactic: rw [Finset.card_univ, smul_mul_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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) =
    Fintype.card ι • 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 ι •
      (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)
        ⋯
have 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)
        sorry *
      y) =
  Fintype.card ι •
    (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)
        sorry)
Tactic: rw [Finset.card_univ, smul_mul_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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) =
    Fintype.card ι • 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)
        ⋯
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) =
    Fintype.card ι •
      (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)
          ⋯)
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)
        ⋯
have h₃ : Fintype.card ι •
    (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)
        sorry) =
  Fintype.card ι •
    (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)
        sorry)
Tactic: rw [Finset.card_univ, smul_mul_assoc, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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 : ι
⊢ (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)
      ⋯
have 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) :
    ℤ)
Tactic: apply Finset.le_max'
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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
⊢ (↑((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) a : R)) : T) < (↑(normBound abv bS) : T) * y ^ Fintype.card ι
have obtain : ∀ (i : ι),
  (↑((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
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (hypothesis)
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 : ι
⊢ (↑((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) a : R)) : T) < (↑(normBound abv bS) : T) * y ^ Fintype.card ι
have him : 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⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (hypothesis)
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)
⊢ (↑((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) a : R)) : T) < (↑(normBound abv bS) : T) * y ^ Fintype.card ι
have y'_def : 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
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (hypothesis)
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
⊢ (↑((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) a : R)) : T) < (↑(normBound abv bS) : T) * y ^ Fintype.card ι
have hy' : ∀ (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⟩)
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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
hy' : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y'
⊢ (↑y' : T) < y
have rw : Finset.max'
    (Finset.image (fun (x : ℤ) ↦ (↑x : T))
      (Finset.image
        (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
        Finset.univ))
    sorry <
  y
Tactic: rw [y'_def,
      ← Finset.max'_image (show Monotone (_ : ℤ → T) from fun x y h => Int.cast_le.mpr h)
          _ (him.image _)]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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
hy' : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y'
⊢ Finset.max'
      (Finset.image (fun (x : ℤ) ↦ (↑x : T))
        (Finset.image
          (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
          Finset.univ))
      ⋯ <
    y
have apply : ∀ (y_1 : T),
  Membership.mem (γ := Finset T)
      (Finset.image (fun (x : ℤ) ↦ (↑x : T))
        (Finset.image
          (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
          Finset.univ))
      y_1 →
    y_1 < y
Tactic: apply (Finset.max'_lt_iff _ (him.image _)).mpr
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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
hy' : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y'
⊢ ∀ (y_1 : T),
    Membership.mem (γ := Finset T)
        (Finset.image (fun (x : ℤ) ↦ (↑x : T))
          (Finset.image
            (fun (k : ι) ↦ (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R))
            Finset.univ))
        y_1 →
      y_1 < y
have simp : ∀ (y_1 : T),
  (∃ (a_1 : ℤ),
      (∃ (a_2 : ι),
          Membership.mem (γ := Finset ι) Finset.univ a_2 ∧
            (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) a_2 : R) = a_1) ∧
        (↑a_1 : T) = y_1) →
    y_1 < y
Tactic: simp only [Finset.mem_image]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (hypothesis)
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
hy' : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y'
⊢ (↑((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) a : R)) : T) < (↑(normBound abv bS) : T) * y ^ Fintype.card ι
have this : (↑y' : T) < y
Tactic: have : (y' : T) < y := by
    rw [y'_def,
      ← Finset.max'_image (show Monotone (_ : ℤ → T) from fun x y h => Int.cast_le.mpr h)
          _ (him.image _)]
    apply (Finset.max'_lt_iff _ (him.image _)).mpr
    simp only [Finset.mem_image]
    rintro _ ⟨x, ⟨k, -, rfl⟩, rfl⟩
    exact hy k
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (hypothesis)
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
hy' : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y'
this : (↑y' : T) < y
⊢ (↑((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) a : R)) : T) < (↑(normBound abv bS) : T) * y ^ Fintype.card ι
have y'_nonneg : 0 ≤ y'
Tactic: have y'_nonneg : 0 ≤ y' := le_trans (abv.nonneg _) (hy' i)
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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
hy' : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y'
this : (↑y' : T) < y
y'_nonneg : 0 ≤ y'
⊢ (↑((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) a : R)) : T) < (↑(normBound abv bS) : T) * y ^ Fintype.card ι
have apply : (↑(normBound abv bS * y' ^ Fintype.card ι) : T) < (↑(normBound abv bS) : T) * y ^ Fintype.card ι
Tactic: apply (Int.cast_le.mpr (norm_le abv bS a hy')).trans_lt
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.Finite (goal)
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
hy' : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y'
this : (↑y' : T) < y
y'_nonneg : 0 ≤ y'
⊢ (↑(normBound abv bS * y' ^ Fintype.card ι) : T) < (↑(normBound abv bS) : T) * y ^ Fintype.card ι
have simp : (↑(normBound abv bS) : T) * HPow.hPow (α := T) (↑y' : T) (Fintype.card ι) <
  (↑(normBound abv bS) : T) * y ^ Fintype.card ι
Tactic: simp only [Int.cast_mul, Int.cast_pow]