awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
⊢ Eq (α := logSpace K) (sorry : logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ) :
      logSpace K)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ sorry

Tactic:
Module.Free.of_equiv (logEmbeddingEquiv K).symm

Premises used: Module.Free.of_equiv
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ sorry

Tactic:
Module.Finite.equiv (logEmbeddingEquiv K).symm

Premises used: Module.Finite.equiv
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : Submodule.FG.{0, u_1} (R := ℤ) (M := Additive (𝓞 K)ˣ) ⊤
⊢ Module.Finite.{0, u_1} ℤ (Additive (𝓞 K)ˣ)

Tactic:
rw [Module.finite_def]

Premises used: Module.finite_def
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Submodule.FG.{0, u_1} (R := ℤ) (M := Additive (𝓞 K)ˣ) ⊤

Tactic:
Submodule.fg_of_fg_map_of_fg_inf_ker
    (MonoidHom.toAdditive (QuotientGroup.mk' (torsion K))).toIntLinearMap ?_ ?_

Premises used: AddMonoidHom.toIntLinearMap, Submodule.fg_of_fg_map_of_fg_inf_ker
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw : Module.Finite.{0, u_1} ℤ (Additive (𝓞 K)ˣ)
⊢ Monoid.FG.{u_1} (𝓞 K)ˣ

Tactic:
rw [Monoid.fg_iff_add_fg, ← AddGroup.fg_iff_addMonoid_fg, ← Module.Finite.iff_addGroup_fg]

Premises used: AddGroup.fg_iff_addMonoid_fg, Monoid.fg_iff_add_fg, Module.Finite.iff_addGroup_fg
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ Module.Finite.{0, u_1} ℤ (Additive (𝓞 K)ˣ)

Tactic:
infer_instance
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x ζ : (𝓞 K)ˣ
f : Fin (rank K) → ℤ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
h : x = ζ * ∏ i : Fin (rank K), fundSystem K i ^ f i
suffices :
  Eq (α := Additive (𝓞 K)ˣ) ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ)
    (∑ i : Fin (rank K), HSMul.hSMul (β := Additive (𝓞 K)ˣ) (f i) sorry : Additive (𝓞 K)ˣ)
⊢ f = sorry

Tactic:
suffices Additive.ofMul ↑x = ∑ i, (f i) • (basisModTorsion K i) by
    rw [← (basisModTorsion K).repr_sum_self f, ← this]
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x ζ : (𝓞 K)ˣ
f : Fin (rank K) → ℤ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
h : x = ζ * ∏ i : Fin (rank K), fundSystem K i ^ f i
rw :
  Eq (α := Additive (𝓞 K)ˣ)
    ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (ζ * ∏ i : Fin (rank K), fundSystem K i ^ f i) : Additive (𝓞 K)ˣ)
    (∑ i : Fin (rank K),
        HSMul.hSMul (β := Additive (𝓞 K)ˣ) (f i)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (fundSystem K i) : Additive (𝓞 K)ˣ) :
      Additive (𝓞 K)ˣ)
⊢ Eq (α := Additive (𝓞 K)ˣ) ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ)
    (∑ i : Fin (rank K),
        HSMul.hSMul (β := Additive (𝓞 K)ˣ) (f i)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (fundSystem K i) : Additive (𝓞 K)ˣ) :
      Additive (𝓞 K)ˣ)

Tactic:
rw [h, QuotientGroup.mk_mul, (QuotientGroup.eq_one_iff _).mpr hζ, one_mul,
            QuotientGroup.mk_prod, ofMul_prod]

Premises used: Iff.mpr, ofMul_prod, QuotientGroup.mk_mul, QuotientGroup.mk_prod, QuotientGroup.eq_one_iff, one_mul
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x ζ : (𝓞 K)ˣ
f : Fin (rank K) → ℤ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
h : x = ζ * ∏ i : Fin (rank K), fundSystem K i ^ f i
simp_rw :
  Eq.{u_1 + 1} (α := Additive (𝓞 K)ˣ)
    (∑ x : Fin (rank K),
      HSMul.hSMul (β := Additive (𝓞 K)ˣ) (f x) ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (sorry K x)))
    (∑ i : Fin (rank K), HSMul.hSMul (β := Additive (𝓞 K)ˣ) (f i) sorry)
⊢ Eq.{u_1 + 1} (α := Additive (𝓞 K)ˣ)
    (∑ i : Fin (rank K),
      HSMul.hSMul (β := Additive (𝓞 K)ˣ) (f i)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (fundSystem K i) : Additive (𝓞 K)ˣ))
    (∑ i : Fin (rank K), HSMul.hSMul (β := Additive (𝓞 K)ˣ) (f i) sorry)

Tactic:
simp_rw [fundSystem, QuotientGroup.out_eq', ofMul_toMul]

Premises used: QuotientGroup.out_eq', NumberField.Units.fundSystem, ofMul_toMul
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x ζ : (𝓞 K)ˣ
f : Fin (rank K) → ℤ
hζ : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
h : x = ζ * ∏ i : Fin (rank K), fundSystem K i ^ f i
_ :
  Eq (α := Additive (𝓞 K)ˣ) ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ)
    (∑ i : Fin (rank K),
        HSMul.hSMul (β := Additive (𝓞 K)ˣ) (f i)
          ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (fundSystem K i) : Additive (𝓞 K)ˣ) :
      Additive (𝓞 K)ˣ)
_₁ :
  Eq.{u_1 + 1} (α := Additive (𝓞 K)ˣ)
    (∑ i : Fin (rank K),
      HSMul.hSMul (β := Additive (𝓞 K)ˣ) (f i)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (fundSystem K i) : Additive (𝓞 K)ˣ))
    (∑ i : Fin (rank K), HSMul.hSMul (β := Additive (𝓞 K)ˣ) (f i) sorry)
⊢ Eq (α := Additive (𝓞 K)ˣ) ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) x : Additive (𝓞 K)ˣ)
    (∑ i : Fin (rank K), HSMul.hSMul (β := Additive (𝓞 K)ˣ) (f i) sorry : Additive (𝓞 K)ˣ)

Tactic:
calc
    Additive.ofMul ↑x
    _ = ∑ i, (f i) • Additive.ofMul ↑(fundSystem K i) := by
          rw [h, QuotientGroup.mk_mul, (QuotientGroup.eq_one_iff _).mpr hζ, one_mul,
            QuotientGroup.mk_prod, ofMul_prod]; rfl
    _ = ∑ i, (f i) • (basisModTorsion K i) := by
          simp_rw [fundSystem, QuotientGroup.out_eq', ofMul_toMul]

Premises used: Additive.ofMul, DFunLike.coe
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i : Fin (rank K), HPow.hPow (β := ℕ) (fundSystem K i) sorry)⁻¹
rw :
  HAdd.hAdd (α := Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))) (β :=
      Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)))
      ((Additive.ofMul : (a : (𝓞 K)ˣ ⧸ torsion K) → Additive ((𝓞 K)ˣ ⧸ torsion K)) (↑x : (𝓞 K)ˣ ⧸ torsion K) :
        Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K)))
      (-∑ i : Fin (rank K),
            (Additive.ofMul : (a : (𝓞 K)ˣ ⧸ torsion K) → Additive ((𝓞 K)ˣ ⧸ torsion K))
              (↑(HPow.hPow (β := ℕ) (fundSystem K i) sorry) : (𝓞 K)ˣ ⧸ torsion K) :
        Additive (HasQuotient.Quotient (𝓞 K)ˣ (B := Subgroup (𝓞 K)ˣ) (torsion K))) =
    0
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ

Tactic:
rw [← QuotientGroup.eq_one_iff, QuotientGroup.mk_mul, QuotientGroup.mk_inv, ← ofMul_eq_zero,
      ofMul_mul, ofMul_inv, QuotientGroup.mk_prod, ofMul_prod]

Premises used: ofMul_inv, QuotientGroup.mk_inv, ofMul_mul, ofMul_prod, QuotientGroup.mk_mul, QuotientGroup.mk_prod, QuotientGroup.eq_one_iff, ofMul_eq_zero
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i : Fin (rank K), HPow.hPow (β := ℕ) (fundSystem K i) sorry)⁻¹
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ

Tactic:
have h_tors : ζ ∈ torsion K := by
    rw [← QuotientGroup.eq_one_iff, QuotientGroup.mk_mul, QuotientGroup.mk_inv, ← ofMul_eq_zero,
      ofMul_mul, ofMul_inv, QuotientGroup.mk_prod, ofMul_prod]
    simp_rw [QuotientGroup.mk_zpow, ofMul_zpow, fundSystem, QuotientGroup.out_eq']
    rw [add_eq_zero_iff_eq_neg, neg_neg]
    exact ((basisModTorsion K).sum_repr (Additive.ofMul ↑x)).symm
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i : Fin (rank K), HPow.hPow (β := ℕ) (fundSystem K i) sorry)⁻¹
h_tors : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
⊢ ∃! ζe : ↥(torsion K) × (Fin (rank K) → ℤ), x = (↑ζe.1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ ζe.2 i

Tactic:
⟨⟨⟨ζ, h_tors⟩, ((basisModTorsion K).repr (Additive.ofMul ↑x) : Fin (rank K) → ℤ)⟩, ?_, ?_⟩

Premises used: Prod.mk, Subtype.mk, ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i : Fin (rank K), HPow.hPow (β := ℕ) (fundSystem K i) sorry)⁻¹
h_tors : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
refine_1 :
  (fun (ζe : ↥(torsion K) × (Fin (rank K) → ℤ)) ↦ x = (↑ζe.1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ ζe.2 i)
    (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) ζ h_tors, sorry)
refine_2 :
  ∀ (y : ↥(torsion K) × (Fin (rank K) → ℤ)),
    (fun (ζe : ↥(torsion K) × (Fin (rank K) → ℤ)) ↦ x = (↑ζe.1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ ζe.2 i)
        y →
      y = (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) ζ h_tors, sorry)
⊢ ∃! ζe : ↥(torsion K) × (Fin (rank K) → ℤ), x = (↑ζe.1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ ζe.2 i

Tactic:
refine ⟨⟨⟨ζ, h_tors⟩, ((basisModTorsion K).repr (Additive.ofMul ↑x) : Fin (rank K) → ℤ)⟩, ?_, ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i : Fin (rank K), HPow.hPow (β := ℕ) (fundSystem K i) sorry)⁻¹
h_tors : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
refine_1 :
  x =
    x * (∏ i : Fin (rank K), HPow.hPow (β := ℕ) (fundSystem K i) sorry)⁻¹ *
      ∏ x : Fin (rank K), HPow.hPow (β := ℤ) (fundSystem K x) (sorry x)
⊢ (fun (ζe : ↥(torsion K) × (Fin (rank K) → ℤ)) ↦ x = (↑ζe.1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ ζe.2 i)
    (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) ζ h_tors, sorry)

Tactic:
simp only [ζ, _root_.inv_mul_cancel_right]

Premises used: inv_mul_cancel_right
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i : Fin (rank K), HPow.hPow (β := ℕ) (fundSystem K i) sorry)⁻¹
h_tors : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
η : Fin (rank K) → ℤ
ζ' : (𝓞 K)ˣ
h_tors' : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ'
hf :
  x =
    (↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) ζ' h_tors', η).1 :
        (𝓞 K)ˣ) *
      ∏ i : Fin (rank K),
        fundSystem K i ^
          (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) ζ' h_tors', η).2 i
refine_2 : ζ' = x * (∏ i : Fin (rank K), HPow.hPow (β := ℕ) (fundSystem K i) sorry)⁻¹
⊢ (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) ζ' h_tors', η) =
    (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) ζ h_tors, sorry)

Tactic:
simp only [ζ, ← fun_eq_repr K h_tors' hf, Prod.mk.injEq, Subtype.mk.injEq, and_true]

Premises used: NumberField.Units.fun_eq_repr, and_true, Prod.mk.injEq, Subtype.mk.injEq
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
ζ : (𝓞 K)ˣ := x * (∏ i : Fin (rank K), HPow.hPow (β := ℕ) (fundSystem K i) sorry)⁻¹
h_tors : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ
η : Fin (rank K) → ℤ
ζ' : (𝓞 K)ˣ
h_tors' : Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) ζ'
hf :
  x =
    (↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) ζ' h_tors', η).1 :
        (𝓞 K)ˣ) *
      ∏ i : Fin (rank K),
        fundSystem K i ^
          (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) ζ' h_tors', η).2 i
refine_2 :
  ζ' =
    ((↑(Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) ζ' h_tors', η).1 :
          (𝓞 K)ˣ) *
        ∏ i : Fin (rank K),
          fundSystem K i ^
            (Subtype.mk (p := fun (x : (𝓞 K)ˣ) ↦ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K) x) ζ' h_tors', η).2
              i) *
      (∏ i : Fin (rank K), HPow.hPow (β := ℕ) (fundSystem K i) sorry)⁻¹
⊢ ζ' = x * (∏ i : Fin (rank K), HPow.hPow (β := ℕ) (fundSystem K i) sorry)⁻¹

Tactic:
nth_rewrite 1 [hf]
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  ∀ (x : (𝓞 K)ˣ),
    Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K ⊔ Subgroup.closure (Set.range (ι := Fin (rank K)) (fundSystem K)))
      x
⊢ Eq (α := Subgroup (𝓞 K)ˣ) (Subgroup.closure (Set.range (ι := Fin (rank K)) (fundSystem K)) ⊔ torsion K) ⊤

Tactic:
rw [Subgroup.eq_top_iff', sup_comm]

Premises used: Subgroup.eq_top_iff', sup_comm
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
x : (𝓞 K)ˣ
obtain :
  ∀ (c : ↥(torsion K) × (Fin (rank K) → ℤ)),
    (∀ (y : ↥(torsion K) × (Fin (rank K) → ℤ)),
        (fun (ζe : ↥(torsion K) × (Fin (rank K) → ℤ)) ↦
              (↑c.1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ c.2 i =
                (↑ζe.1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ ζe.2 i)
            y →
          y = c) →
      Membership.mem (γ := Subgroup (𝓞 K)ˣ)
        (torsion K ⊔ Subgroup.closure (Set.range (ι := Fin (rank K)) (fundSystem K)))
        ((↑c.1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ c.2 i)
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K ⊔ Subgroup.closure (Set.range (ι := Fin (rank K)) (fundSystem K))) x

Tactic:
obtain ⟨c, rfl, _⟩ := exist_unique_eq_mul_prod K x

Premises used: NumberField.Units.exist_unique_eq_mul_prod, rfl
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ↥(torsion K) × (Fin (rank K) → ℤ)
right :
  ∀ (y : ↥(torsion K) × (Fin (rank K) → ℤ)),
    (fun (ζe : ↥(torsion K) × (Fin (rank K) → ℤ)) ↦
          (↑c.1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ c.2 i =
            (↑ζe.1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ ζe.2 i)
        y →
      y = c
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K ⊔ Subgroup.closure (Set.range (ι := Fin (rank K)) (fundSystem K)))
    ((↑c.1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ c.2 i)

Tactic:
Subgroup.mul_mem_sup (SetLike.coe_mem c.1) <| Subgroup.prod_mem _
    fun i _ ↦ Subgroup.zpow_mem _ (Subgroup.subset_closure (Set.mem_range_self i)) _

Premises used: Set.mem_range_self, Subgroup.closure, NumberField.Units.fundSystem, SetLike.coe_mem, Set.Mem, Subgroup.prod_mem, Prod.fst, Subgroup.subset_closure, Subgroup.mul_mem_sup, Set.range, Prod.snd, Subgroup.zpow_mem
-- Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
c : ↥(torsion K) × (Fin (rank K) → ℤ)
right :
  ∀ (y : ↥(torsion K) × (Fin (rank K) → ℤ)),
    (fun (ζe : ↥(torsion K) × (Fin (rank K) → ℤ)) ↦
          (↑c.1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ c.2 i =
            (↑ζe.1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ ζe.2 i)
        y →
      y = c
⊢ Membership.mem (γ := Subgroup (𝓞 K)ˣ) (torsion K ⊔ Subgroup.closure (Set.range (ι := Fin (rank K)) (fundSystem K)))
    ((↑c.1 : (𝓞 K)ˣ) * ∏ i : Fin (rank K), fundSystem K i ^ c.2 i)

Tactic:
exact Subgroup.mul_mem_sup (SetLike.coe_mem c.1) <| Subgroup.prod_mem _
    fun i _ ↦ Subgroup.zpow_mem _ (Subgroup.subset_closure (Set.mem_range_self i)) _

Premises used: Set.mem_range_self, Subgroup.closure, SetLike.coe_mem, Subgroup.prod_mem, Prod.fst, Subgroup.subset_closure, Subgroup.mul_mem_sup, Set.range, Subgroup.zpow_mem
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  Fintype.card (Fin (rank K)) =
    Fintype.card.{u_1} (InfinitePlace K) - Fintype.card.{u_1} { x : InfinitePlace K // x = w₀ }
rw₁ : Fintype.card (Fin (rank K)) = Fintype.card.{u_1} (InfinitePlace K) - 1
rw₂ : rank K = Fintype.card.{u_1} (InfinitePlace K) - 1
rw₃ rw₄ : Fintype.card.{u_1} (InfinitePlace K) - 1 = Fintype.card.{u_1} (InfinitePlace K) - 1
⊢ Fintype.card (Fin (rank K)) = Fintype.card.{u_1} { w : InfinitePlace K // w ≠ w₀ }

Tactic:
rw [Fintype.card_subtype_compl, Fintype.card_ofSubsingleton, Fintype.card_fin, rank]

Premises used: Fintype.card_fin, NumberField.Units.rank, Fintype.card_ofSubsingleton, Fintype.card_subtype_compl
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
i : Fin (rank K)
⊢ Eq (α := logSpace K) ((basisOfIsMaxRank hu : (a : Fin (rank K)) → logSpace K) i : logSpace K)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (u i) : Additive (𝓞 K)ˣ) :
      logSpace K)

Tactic:
simp [basisOfIsMaxRank, Basis.coe_reindex, Equiv.symm_symm, Function.comp_apply,
    coe_basisOfPiSpaceOfLinearIndependent]

Premises used: coe_basisOfPiSpaceOfLinearIndependent, Equiv.symm_symm, Module.Basis.coe_reindex, NumberField.Units.basisOfIsMaxRank, Function.comp_apply
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
rw :
  Eq (α := AddSubgroup (logSpace K))
    (toAddSubgroup (module_M := AddCommGroup.toIntModule (logSpace K))
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K))))
    (toAddSubgroup (module_M := AddCommGroup.toIntModule (logSpace K))
      (span ℤ
        (Set.image (α := Additive (𝓞 K)ˣ) (⇑(logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((⇑Additive.toMul : (a : Additive (𝓞 K)ˣ) → (𝓞 K)ˣ) ⁻¹' Set.range u))))
⊢ Eq (α := AddSubgroup (logSpace K))
    (toAddSubgroup (module_M := AddCommGroup.toIntModule (logSpace K))
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K))))
    (AddSubgroup.map (logEmbedding K)
      ((Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ))
        (Subgroup.closure (Set.range u))))

Tactic:
rw [Subgroup.toAddSubgroup_closure, AddMonoidHom.map_closure, ← span_int_eq_addSubgroupClosure]

Premises used: AddMonoidHom.map_closure, Submodule.span_int_eq_addSubgroupClosure, Subgroup.toAddSubgroup_closure
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
e_p :
  Eq (α := Set (logSpace K)) (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K))
    (Set.image (α := Additive (𝓞 K)ˣ) (⇑(logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((⇑Additive.toMul : (a : Additive (𝓞 K)ˣ) → (𝓞 K)ˣ) ⁻¹' Set.range u))
⊢ Eq (α := AddSubgroup (logSpace K))
    (toAddSubgroup (module_M := AddCommGroup.toIntModule (logSpace K))
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K))))
    (toAddSubgroup (module_M := AddCommGroup.toIntModule (logSpace K))
      (span ℤ
        (Set.image (α := Additive (𝓞 K)ˣ) (⇑(logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((⇑Additive.toMul : (a : Additive (𝓞 K)ˣ) → (𝓞 K)ˣ) ⁻¹' Set.range u))))

Tactic:
congr
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
e_p :
  ∀ (x : logSpace K),
    Membership.mem (γ := Set (logSpace K))
        (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)) x ↔
      Membership.mem (γ := Set (logSpace K))
        (Set.image (α := Additive (𝓞 K)ˣ) (⇑(logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K)
          ((⇑Additive.toMul : (a : Additive (𝓞 K)ˣ) → (𝓞 K)ˣ) ⁻¹' Set.range u))
        x
⊢ Eq (α := Set (logSpace K)) (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K))
    (Set.image (α := Additive (𝓞 K)ˣ) (⇑(logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((⇑Additive.toMul : (a : Additive (𝓞 K)ˣ) → (𝓞 K)ˣ) ⁻¹' Set.range u))

Tactic:
ext
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
x : logSpace K
⊢ Membership.mem (γ := Set (logSpace K))
      (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)) x ↔
    Membership.mem (γ := Set (logSpace K))
      (Set.image (α := Additive (𝓞 K)ˣ) (⇑(logEmbedding K) : (a : Additive (𝓞 K)ˣ) → logSpace K)
        ((⇑Additive.toMul : (a : Additive (𝓞 K)ˣ) → (𝓞 K)ˣ) ⁻¹' Set.range u))
      x

Tactic:
simp
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Subgroup (𝓞 K)ˣ
⊢ s.FiniteIndex ↔ (s ⊔ torsion K).FiniteIndex

Tactic:
⟨fun h ↦ Subgroup.finiteIndex_of_le le_sup_left, fun h ↦ ?_⟩

Premises used: le_sup_left, Subgroup.finiteIndex_of_le, Iff.intro
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Subgroup (𝓞 K)ˣ
refine : ∀ (h : (s ⊔ torsion K).FiniteIndex), s.FiniteIndex
⊢ s.FiniteIndex ↔ (s ⊔ torsion K).FiniteIndex

Tactic:
refine ⟨fun h ↦ Subgroup.finiteIndex_of_le le_sup_left, fun h ↦ ?_⟩
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Subgroup (𝓞 K)ˣ
h : (s ⊔ torsion K).FiniteIndex
rw : s.relIndex (s ⊔ torsion K) * (s ⊔ torsion K).index ≠ 0
⊢ s.FiniteIndex

Tactic:
rw [Subgroup.finiteIndex_iff, ← Subgroup.relIndex_mul_index (le_sup_left : s ≤ s ⊔ torsion K)]

Premises used: Subgroup.relIndex_mul_index, le_sup_left, Subgroup.finiteIndex_iff
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Subgroup (𝓞 K)ˣ
h : (s ⊔ torsion K).FiniteIndex
⊢ s.relIndex (s ⊔ torsion K) * (s ⊔ torsion K).index ≠ 0

Tactic:
Nat.mul_ne_zero ?_ (Subgroup.finiteIndex_iff.mp h)

Premises used: Nat.mul_ne_zero, Iff.mp, Subgroup.finiteIndex_iff
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Subgroup (𝓞 K)ˣ
h : (s ⊔ torsion K).FiniteIndex
refine : s.relIndex (s ⊔ torsion K) ≠ 0
⊢ s.relIndex (s ⊔ torsion K) * (s ⊔ torsion K).index ≠ 0

Tactic:
refine Nat.mul_ne_zero ?_ (Subgroup.finiteIndex_iff.mp h)

Premises used: Nat.mul_ne_zero, Iff.mp, Subgroup.finiteIndex_iff
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Subgroup (𝓞 K)ˣ
h : (s ⊔ torsion K).FiniteIndex
rw : s.relIndex (torsion K) ≠ 0
⊢ s.relIndex (s ⊔ torsion K) ≠ 0

Tactic:
rw [Subgroup.relIndex_sup_left]

Premises used: Subgroup.relIndex_sup_left
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Subgroup (𝓞 K)ˣ
h : (s ⊔ torsion K).FiniteIndex
⊢ s.relIndex (torsion K) ≠ 0

Tactic:
Subgroup.FiniteIndex.index_ne_zero

Premises used: Subgroup.FiniteIndex.index_ne_zero, Subgroup.relIndex
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
s : Subgroup (𝓞 K)ˣ
h : (s ⊔ torsion K).FiniteIndex
⊢ s.relIndex (torsion K) ≠ 0

Tactic:
exact Subgroup.FiniteIndex.index_ne_zero

Premises used: Subgroup.FiniteIndex.index_ne_zero