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
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'
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))
      ⋯ <
    y
⊢ (↑y' : T) < y

Tactic:
rw [y'_def,
      ← Finset.max'_image (show Monotone (_ : ℤ → T) from fun x y h => Int.cast_le.mpr h)
          _ (him.image _)]

Premises used: Iff.mpr, Int.cast_le, Finset.Nonempty.image, Finset.max'_image
-- 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
hy' : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y'
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
⊢ 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

Tactic:
apply (Finset.max'_lt_iff _ (him.image _)).mpr

Premises used: Iff.mpr, Finset.Nonempty.image, Finset.max'_lt_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
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'
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
⊢ ∀ (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:
simp only [Finset.mem_image]

Premises used: Finset.mem_image
-- 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
hy' : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y'
k : ι
⊢ (↑((abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R)) : T) < y

Tactic:
hy k
-- 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
hy' : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y'
k : ι
⊢ (↑((abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R)) : T) < y

Tactic:
exact hy k
-- 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
hy' : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y'
⊢ (↑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
-- 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
hy' : ∀ (k : ι), (abv : (a : R) → ℤ) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) k : R) ≤ y'
this : (↑y' : T) < y
⊢ 0 ≤ y'

Tactic:
have y'_nonneg : 0 ≤ y' := le_trans (abv.nonneg _) (hy' i)
-- 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
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'
apply : (↑(normBound abv bS * y' ^ Fintype.card ι) : 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:
apply (Int.cast_le.mpr (norm_le abv bS a hy')).trans_lt

Premises used: Iff.mpr, Int.cast_le, ClassGroup.norm_le, LE.le.trans_lt
-- 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
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'
simp :
  (↑(normBound abv bS) : T) * HPow.hPow (α := T) (↑y' : T) (Fintype.card ι) <
    (↑(normBound abv bS) : T) * y ^ Fintype.card ι
⊢ (↑(normBound abv bS * y' ^ Fintype.card ι) : T) < (↑(normBound abv bS) : T) * y ^ Fintype.card ι

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

Premises used: Int.cast_pow, Int.cast_mul
-- 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
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'
h₂ : HPow.hPow (α := T) (↑y' : T) (Fintype.card ι) < y ^ Fintype.card ι
c0 : 0 ≤ HPow.hPow (α := T) (↑y' : T) (Fintype.card ι)
b0 : LT.lt.{u_6} (α := T) 0 (↑(normBound abv bS) : T)
⊢ (↑(normBound abv bS) : T) * HPow.hPow (α := T) (↑y' : T) (Fintype.card ι) <
    (↑(normBound abv bS) : T) * y ^ Fintype.card ι

Tactic:
apply mul_lt_mul' le_rfl

Premises used: le_rfl, mul_lt_mul'
-- 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
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'
⊢ LE.le.{u_6} (α := T) 0 (↑y' : T)

Tactic:
positivity
-- 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
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'
⊢ HPow.hPow (α := T) (↑y' : T) (Fintype.card ι) < y ^ Fintype.card ι

Tactic:
exact pow_lt_pow_left₀ this (by positivity) (@Fintype.card_ne_zero _ _ ⟨i⟩)

Premises used: Fintype.card_ne_zero, pow_lt_pow_left₀
-- 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
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'
⊢ 0 ≤ HPow.hPow (α := T) (↑y' : T) (Fintype.card ι)

Tactic:
positivity
-- 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
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'
⊢ LT.lt.{u_6} (α := T) 0 (↑(normBound abv bS) : T)

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

Premises used: Iff.mpr, ClassGroup.normBound_pos, Int.cast_pos
-- 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
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'
⊢ LT.lt.{u_6} (α := T) 0 (↑(normBound abv bS) : T)

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

Premises used: Iff.mpr, ClassGroup.normBound_pos, Int.cast_pos
-- 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 ℤ
I : ↥(Ideal S)⁰
h :
  ∀ (z : ℤ),
    (fun (a : ℤ) ↦ ∃ b ∈ (↑I : Ideal S), b ≠ 0 ∧ (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) = a) z →
      0 ≤ z
⊢ ∃ (b : ℤ),
    ∀ (z : ℤ),
      (fun (a : ℤ) ↦ ∃ b ∈ (↑I : Ideal S), b ≠ 0 ∧ (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) = a) z →
        b ≤ z

Tactic:
use 0
-- 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 ℤ
I : ↥(Ideal S)⁰
b : S
left : b ∈ (↑I : Ideal S)
left_1 : b ≠ 0
⊢ LE.le (α := ℤ) (0 : ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)

Tactic:
apply abv.nonneg

Premises used: AbsoluteValue.nonneg
-- 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 ℤ
I : ↥(Ideal S)⁰
obtain :
  ∀ (b : S) (b_mem : b ∈ (↑I : Ideal S)) (b_ne_zero : b ≠ 0),
    ∃ (z : ℤ),
      (fun (a : ℤ) ↦ ∃ b ∈ (↑I : Ideal S), b ≠ 0 ∧ (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) = a) z
⊢ ∃ (z : ℤ),
    (fun (a : ℤ) ↦ ∃ b ∈ (↑I : Ideal S), b ≠ 0 ∧ (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) = a) z

Tactic:
obtain ⟨b, b_mem, b_ne_zero⟩ := (I : Ideal S).ne_bot_iff.mp (nonZeroDivisors.coe_ne_zero I)

Premises used: nonZeroDivisors.coe_ne_zero, Submodule.ne_bot_iff, Iff.mp, Subtype.val
-- 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 ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
⊢ ∃ (z : ℤ),
    (fun (a : ℤ) ↦ ∃ b ∈ (↑I : Ideal S), b ≠ 0 ∧ (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) = a) z

Tactic:
⟨_, ⟨b, b_mem, b_ne_zero, rfl⟩⟩

Premises used: 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 ℤ
I : ↥(Ideal S)⁰
b : S
b_mem : b ∈ (↑I : Ideal S)
b_ne_zero : b ≠ 0
⊢ ∃ (z : ℤ),
    (fun (a : ℤ) ↦ ∃ b ∈ (↑I : Ideal S), b ≠ 0 ∧ (abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) = a) z

Tactic:
exact ⟨_, ⟨b, b_mem, b_ne_zero, rfl⟩⟩