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
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
ε_le :
  (↑(normBound abv bS) : ℝ) *
      HPow.hPow (β := ℝ) (HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε) (↑(Fintype.card ι) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑((abv : (a : R) → ℤ) b) : ℝ) (↑(Fintype.card ι) : ℝ)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := (bS.repr : (a : S) → ι →₀ R) a
s_eq :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := R) ((s : (a : ι) → R) i : R) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R)
qs : Fin (cardM bS adm).succ → ι → R :=
  fun (j : Fin (cardM bS adm).succ) (i : ι) ↦
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) / b
rs : Fin (cardM bS adm).succ → ι → R :=
  fun (j : Fin (cardM bS adm).succ) (i : ι) ↦
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) % b
r_eq :
  ∀ (j : Fin (cardM bS adm).succ) (i : ι),
    rs j i = HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) % b
μ_eq :
  ∀ (i : ι) (j : Fin (cardM bS adm).succ),
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) =
      b * qs j i + rs j i
j : Fin (cardM bS adm).succ
⊢ Eq.{u_2 + 1} (α := S)
    (∑ x : ι,
      HSMul.hSMul (α := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R)
        (HSMul.hSMul.{u_1, u_2, u_2} (α := R) (β := S) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) x : R)
          ((bS : (a : ι) → S) x : S)))
    (∑ x : ι,
      (b •
          HSMul.hSMul (β := S)
            (HMul.hMul (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R)
                ((s : (a : ι) → R) x : R) /
              b)
            ((bS : (a : ι) → S) x : S) +
        HSMul.hSMul (β := S)
          (HMul.hMul (α := R) (β := R) ((distinctElems bS adm : (a : Fin (cardM bS adm).succ) → R) j : R)
              ((s : (a : ι) → R) x : R) %
            b)
          ((bS : (a : ι) → S) x : S)))

Tactic:
Finset.sum_congr rfl fun i _ => ?_

Premises used: Finset.sum_congr, 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
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
ε_le :
  (↑(normBound abv bS) : ℝ) *
      HPow.hPow (β := ℝ) (HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε) (↑(Fintype.card ι) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑((abv : (a : R) → ℤ) b) : ℝ) (↑(Fintype.card ι) : ℝ)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := (bS.repr : (a : S) → ι →₀ R) a
s_eq :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := R) ((s : (a : ι) → R) i : R) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R)
qs : Fin (cardM bS adm).succ → ι → R :=
  fun (j : Fin (cardM bS adm).succ) (i : ι) ↦
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) / b
rs : Fin (cardM bS adm).succ → ι → R :=
  fun (j : Fin (cardM bS adm).succ) (i : ι) ↦
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) % b
r_eq :
  ∀ (j : Fin (cardM bS adm).succ) (i : ι),
    rs j i = HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) % b
μ_eq :
  ∀ (i : ι) (j : Fin (cardM bS adm).succ),
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) =
      b * qs j i + rs j i
⊢ ∀ (j : Fin (cardM bS adm).succ),
    HSMul.hSMul (α := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) a =
      HSMul.hSMul (β := S) b (∑ i : ι, HSMul.hSMul (β := S) (qs j i) ((bS : (a : ι) → S) i : S)) +
        ∑ i : ι, HSMul.hSMul (β := S) (rs j i) ((bS : (a : ι) → S) i : S)

Tactic:
have μ_mul_a_eq : ∀ j, μ j • a = b • ∑ i, qs j i • bS i + ∑ i, rs j i • bS i := by
    intro j
    rw [← bS.sum_repr a]
    simp only [μ, qs, rs, Finset.smul_sum, ← Finset.sum_add_distrib]
    refine Finset.sum_congr rfl fun i _ => ?_
    rw [← s_eq, ← mul_smul, μ_eq, add_smul, mul_smul, ← μ_eq]
-- 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
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
ε_le :
  (↑(normBound abv bS) : ℝ) *
      HPow.hPow (β := ℝ) (HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε) (↑(Fintype.card ι) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑((abv : (a : R) → ℤ) b) : ℝ) (↑(Fintype.card ι) : ℝ)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := (bS.repr : (a : S) → ι →₀ R) a
s_eq :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := R) ((s : (a : ι) → R) i : R) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R)
qs : Fin (cardM bS adm).succ → ι → R :=
  fun (j : Fin (cardM bS adm).succ) (i : ι) ↦
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) / b
rs : Fin (cardM bS adm).succ → ι → R :=
  fun (j : Fin (cardM bS adm).succ) (i : ι) ↦
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) % b
r_eq :
  ∀ (j : Fin (cardM bS adm).succ) (i : ι),
    rs j i = HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) % b
μ_eq :
  ∀ (i : ι) (j : Fin (cardM bS adm).succ),
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) =
      b * qs j i + rs j i
μ_mul_a_eq :
  ∀ (j : Fin (cardM bS adm).succ),
    HSMul.hSMul (α := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) a =
      HSMul.hSMul (β := S) b (∑ i : ι, HSMul.hSMul (β := S) (qs j i) ((bS : (a : ι) → S) i : S)) +
        ∑ i : ι, HSMul.hSMul (β := S) (rs j i) ((bS : (a : ι) → S) i : S)
j k : Fin (adm.card ε ^ Fintype.card ι).succ
j_ne_k : j ≠ k
hjk :
  ∀ (k_1 : ι),
    (↑((abv : (a : R) → ℤ)
            (HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) k : R) ((s : (a : ι) → R) k_1 : R) %
                b -
              HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) k_1 : R) %
                b)) :
        ℝ) <
      HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
⊢ ∀ (i : ι), (↑((abv : (a : R) → ℤ) (rs k i - rs j i)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε

Tactic:
simpa only [r_eq] using hjk
-- 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
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
ε_le :
  (↑(normBound abv bS) : ℝ) *
      HPow.hPow (β := ℝ) (HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε) (↑(Fintype.card ι) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑((abv : (a : R) → ℤ) b) : ℝ) (↑(Fintype.card ι) : ℝ)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := (bS.repr : (a : S) → ι →₀ R) a
s_eq :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := R) ((s : (a : ι) → R) i : R) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R)
qs : Fin (cardM bS adm).succ → ι → R :=
  fun (j : Fin (cardM bS adm).succ) (i : ι) ↦
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) / b
rs : Fin (cardM bS adm).succ → ι → R :=
  fun (j : Fin (cardM bS adm).succ) (i : ι) ↦
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) % b
r_eq :
  ∀ (j : Fin (cardM bS adm).succ) (i : ι),
    rs j i = HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) % b
μ_eq :
  ∀ (i : ι) (j : Fin (cardM bS adm).succ),
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) =
      b * qs j i + rs j i
μ_mul_a_eq :
  ∀ (j : Fin (cardM bS adm).succ),
    HSMul.hSMul (α := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) a =
      HSMul.hSMul (β := S) b (∑ i : ι, HSMul.hSMul (β := S) (qs j i) ((bS : (a : ι) → S) i : S)) +
        ∑ i : ι, HSMul.hSMul (β := S) (rs j i) ((bS : (a : ι) → S) i : S)
j k : Fin (adm.card ε ^ Fintype.card ι).succ
j_ne_k : j ≠ k
hjk :
  ∀ (k_1 : ι),
    (↑((abv : (a : R) → ℤ)
            (HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) k : R) ((s : (a : ι) → R) k_1 : R) %
                b -
              HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) k_1 : R) %
                b)) :
        ℝ) <
      HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
⊢ ∀ (i : ι), (↑((abv : (a : R) → ℤ) (rs k i - rs j i)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε

Tactic:
have hjk' : ∀ i, (abv (rs k i - rs j i) : ℝ) < abv b • ε := by simpa only [r_eq] using hjk
-- 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
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
a : S
b : R
hb : b ≠ 0
dim_pos : 0 < Fintype.card ι
ε : ℝ := HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
ε_eq : ε = HPow.hPow (α := ℝ) (↑(normBound abv bS) : ℝ) (HDiv.hDiv (α := ℝ) (-1) (↑(Fintype.card ι) : ℝ))
hε : 0 < ε
ε_le :
  (↑(normBound abv bS) : ℝ) *
      HPow.hPow (β := ℝ) (HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε) (↑(Fintype.card ι) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (↑((abv : (a : R) → ℤ) b) : ℝ) (↑(Fintype.card ι) : ℝ)
μ : Fin (cardM bS adm).succ ↪ R := distinctElems bS adm
s : ι →₀ R := (bS.repr : (a : S) → ι →₀ R) a
s_eq :
  ∀ (i : ι),
    Eq.{u_1 + 1} (α := R) ((s : (a : ι) → R) i : R) ((((bS.repr : (a : S) → ι →₀ R) a : ι →₀ R) : (a : ι) → R) i : R)
qs : Fin (cardM bS adm).succ → ι → R :=
  fun (j : Fin (cardM bS adm).succ) (i : ι) ↦
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) / b
rs : Fin (cardM bS adm).succ → ι → R :=
  fun (j : Fin (cardM bS adm).succ) (i : ι) ↦
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) % b
r_eq :
  ∀ (j : Fin (cardM bS adm).succ) (i : ι),
    rs j i = HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) % b
μ_eq :
  ∀ (i : ι) (j : Fin (cardM bS adm).succ),
    HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) i : R) =
      b * qs j i + rs j i
μ_mul_a_eq :
  ∀ (j : Fin (cardM bS adm).succ),
    HSMul.hSMul (α := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) a =
      HSMul.hSMul (β := S) b (∑ i : ι, HSMul.hSMul (β := S) (qs j i) ((bS : (a : ι) → S) i : S)) +
        ∑ i : ι, HSMul.hSMul (β := S) (rs j i) ((bS : (a : ι) → S) i : S)
j k : Fin (adm.card ε ^ Fintype.card ι).succ
j_ne_k : j ≠ k
hjk :
  ∀ (k_1 : ι),
    (↑((abv : (a : R) → ℤ)
            (HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) k : R) ((s : (a : ι) → R) k_1 : R) %
                b -
              HMul.hMul (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) j : R) ((s : (a : ι) → R) k_1 : R) %
                b)) :
        ℝ) <
      HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
hjk' : ∀ (i : ι), (↑((abv : (a : R) → ℤ) (rs k i - rs j i)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
q : S := ∑ i : ι, HSMul.hSMul (β := S) (qs k i - qs j i) ((bS : (a : ι) → S) i : S)
⊢ let r :=
    HSub.hSub (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) k : R)
      ((μ : (a : Fin (cardM bS adm).succ) → R) j : R);
  r =
    HSub.hSub (α := R) (β := R) ((μ : (a : Fin (cardM bS adm).succ) → R) k : R)
      ((μ : (a : Fin (cardM bS adm).succ) → R) j : R)

Tactic:
set r := μ k - μ j with r_eq

Premises used: DFunLike.coe
-- 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
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
obtain :
  ∀ (a' : S) (b' : R) (hb' : b' ≠ 0) (h : b' • a = b * a'),
    ∃ (q : S),
      ∃ r ∈ finsetApprox bS adm,
        LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ)
          ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
⊢ ∃ (q : S),
    ∃ r ∈ finsetApprox bS adm,
      LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)

Tactic:
obtain ⟨a', b', hb', h⟩ := Algebra.IsAlgebraic.exists_smul_eq_mul R a hb

Premises used: Algebra.IsAlgebraic.exists_smul_eq_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
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
obtain :
  ∀ (q : S) (r : R) (hr : r ∈ finsetApprox bS adm)
    (hqr :
      LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)),
    ∃ (q : S),
      ∃ r ∈ finsetApprox bS adm,
        LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ)
          ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
⊢ ∃ (q : S),
    ∃ r ∈ finsetApprox bS adm,
      LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)

Tactic:
obtain ⟨q, r, hr, hqr⟩ := exists_mem_finsetApprox bS adm a' hb'

Premises used: ClassGroup.exists_mem_finsetApprox
-- 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
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr :
  LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
⊢ ∃ (q : S),
    ∃ r ∈ finsetApprox bS adm,
      LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)

Tactic:
⟨q, r, hr, ?_⟩

Premises used: And.intro, Exists.intro
-- 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
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr :
  LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
refine :
  LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
⊢ ∃ (q : S),
    ∃ r ∈ finsetApprox bS adm,
      LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ)
        ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)

Tactic:
refine ⟨q, r, hr, ?_⟩
-- 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
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr :
  LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
⊢ LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)

Tactic:
lt_of_mul_lt_mul_left ?_ (show 0 ≤ abv (Algebra.norm R (algebraMap R S b')) from abv.nonneg _)

Premises used: lt_of_mul_lt_mul_left, Algebra.algebraMap, AbsoluteValue.nonneg, Algebra.norm, DFunLike.coe
-- 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
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr :
  LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
lt_of_mul_lt_mul_left :
  HMul.hMul (α := ℤ) (β := ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ) <
    HMul.hMul (α := ℤ) (β := ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
⊢ LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)

Tactic:
refine
    lt_of_mul_lt_mul_left ?_ (show 0 ≤ abv (Algebra.norm R (algebraMap R S b')) from abv.nonneg _)

Premises used: lt_of_mul_lt_mul_left, Algebra.algebraMap, AbsoluteValue.nonneg, Algebra.norm, DFunLike.coe
-- 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
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr :
  LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
⊢ HMul.hMul (α := ℤ) (β := ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ) <
    HMul.hMul (α := ℤ) (β := ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)

Tactic:
lt_of_le_of_lt (le_of_eq ?_)
      (mul_lt_mul hqr le_rfl (abv.pos ((Algebra.norm_ne_zero_iff_of_basis bS).mpr hb))
        (abv.nonneg _))

Premises used: Iff.mpr, lt_of_le_of_lt, le_rfl, mul_lt_mul, AbsoluteValue.pos, AbsoluteValue.nonneg, Algebra.norm_ne_zero_iff_of_basis, le_of_eq
-- 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
adm : abv.IsAdmissible
inst_6 : Infinite R
inst_7 : DecidableEq R
inst_8 : Algebra.IsAlgebraic R S
a b : S
hb : b ≠ 0
a' : S
b' : R
hb' : b' ≠ 0
h : b' • a = b * a'
q : S
r : R
hr : r ∈ finsetApprox bS adm
hqr :
  LT.lt (α := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
    ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
lt_of_le_of_lt :
  HMul.hMul (α := ℤ) (β := ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ) =
    HMul.hMul (α := ℤ) (β := ℤ) ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a' - b' • q) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)
⊢ HMul.hMul (α := ℤ) (β := ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) (r • a - q * b) : R) : ℤ) <
    HMul.hMul (α := ℤ) (β := ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) ((algebraMap R S : (a : R) → S) b' : S) : R) : ℤ)
      ((abv : (a : R) → ℤ) ((Algebra.norm R : (a : S) → R) b : R) : ℤ)

Tactic:
refine
    lt_of_le_of_lt (le_of_eq ?_)
      (mul_lt_mul hqr le_rfl (abv.pos ((Algebra.norm_ne_zero_iff_of_basis bS).mpr hb))
        (abv.nonneg _))

Premises used: Iff.mpr, lt_of_le_of_lt, le_rfl, mul_lt_mul, AbsoluteValue.pos, AbsoluteValue.nonneg, Algebra.norm_ne_zero_iff_of_basis, le_of_eq