awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
i : Fin (rank K)
x : { w : InfinitePlace K // w ≠ w₀ }
a :
  Eq (α := ℝ) ((basisOfIsMaxRank ⋯ : (a : Fin (rank K)) → logSpace K) i x)
    ((↑((basisUnitLattice K : (a : Fin (rank K)) → ↥(unitLattice K)) i) : logSpace K) x)
a₁ :
  Eq (α := ℝ)
    ((logEmbedding K : (a : Additive (𝓞 K)ˣ) → logSpace K)
      ((Additive.ofMul : (a : (𝓞 K)ˣ) → Additive (𝓞 K)ˣ) (fundSystem K i) : Additive (𝓞 K)ˣ) x)
    ((↑((basisUnitLattice K : (a : Fin (rank K)) → ↥(unitLattice K)) i) : logSpace K) x)
a₂ a₃ :
  Eq (α := ℝ) ((↑((basisUnitLattice K : (a : Fin (rank K)) → ↥(unitLattice K)) i) : logSpace K) x)
    ((↑((basisUnitLattice K : (a : Fin (rank K)) → ↥(unitLattice K)) i) : logSpace K) x)
⊢ Eq (α := ℝ) ((basisOfIsMaxRank ⋯ : (a : Fin (rank K)) → logSpace K) i x : ℝ)
    (((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K) : Basis (Fin (rank K)) ℝ (logSpace K)) :
          (a : Fin (rank K)) → logSpace K)
        i x :
      ℝ)

Tactic:
rw [Basis.ofZLatticeBasis_apply, basisOfIsMaxRank_apply, logEmbedding_fundSystem]

Premises used: NumberField.Units.logEmbedding_fundSystem, Module.Basis.ofZLatticeBasis_apply, NumberField.Units.basisOfIsMaxRank_apply
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  regulator K =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank ⋯) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
rw₁ :
  ZLattice.covolume.{u_1} (E := logSpace K) (unitLattice K) (volume : Measure (logSpace K)) =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank ⋯) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
rw₂ :
  ZLattice.covolume.{u_1} (E := logSpace K)
      (span ℤ
        (Set.range (ι := Fin (rank K))
          (⇑(Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K)) =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank ⋯) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
rw₃ rw₄ :
  ZLattice.covolume.{u_1} (E := logSpace K)
      (span ℤ
        (Set.range (ι := Fin (rank K))
          (⇑(Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K)) =
    ZLattice.covolume.{u_1} (E := logSpace K)
      (span ℤ
        (Set.range (ι := Fin (rank K))
          (⇑(Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K) : Basis (Fin (rank K)) ℝ (logSpace K)) :
            (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
⊢ regulator K = regOfFamily (fundSystem K)

Tactic:
rw [regOfFamily_of_isMaxRank (isMaxRank_fundSystem K), regulator,
    ← (basisUnitLattice K).ofZLatticeBasis_span ℝ, basisOfIsMaxRank_fundSystem]

Premises used: NumberField.Units.basisUnitLattice, Real, NumberField.Units.isMaxRank_fundSystem, Module.Basis.ofZLatticeBasis_span, NumberField.Units.regOfFamily_of_isMaxRank, NumberField.Units.regulator, NumberField.Units.basisOfIsMaxRank_fundSystem
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
rw :
  regulator K =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank ⋯) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
rw₁ :
  ZLattice.covolume.{u_1} (E := logSpace K) (unitLattice K) (volume : Measure (logSpace K)) =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank ⋯) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
rw₂ :
  ZLattice.covolume.{u_1} (E := logSpace K)
      (span ℤ
        (Set.range (ι := Fin (rank K))
          (⇑(Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K)) =
    ZLattice.covolume (E := logSpace K)
      (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank ⋯) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
rw₃ rw₄ :
  ZLattice.covolume.{u_1} (E := logSpace K)
      (span ℤ
        (Set.range (ι := Fin (rank K))
          (⇑(Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) : (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K)) =
    ZLattice.covolume.{u_1} (E := logSpace K)
      (span ℤ
        (Set.range (ι := Fin (rank K))
          (⇑(Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K) : Basis (Fin (rank K)) ℝ (logSpace K)) :
            (a : Fin (rank K)) → logSpace K)))
      (volume : Measure (logSpace K))
⊢ regulator K = regOfFamily (fundSystem K)

Tactic:
classical
  rw [regOfFamily_of_isMaxRank (isMaxRank_fundSystem K), regulator,
    ← (basisUnitLattice K).ofZLatticeBasis_span ℝ, basisOfIsMaxRank_fundSystem]

Premises used: Real, NumberField.Units.isMaxRank_fundSystem, Module.Basis.ofZLatticeBasis_span, NumberField.Units.regOfFamily_of_isMaxRank, NumberField.Units.regulator, NumberField.Units.basisOfIsMaxRank_fundSystem
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ 0 < regulator K

Tactic:
regulator_eq_regOfFamily_fundSystem K ▸ regOfFamily_pos (isMaxRank_fundSystem K)

Premises used: NumberField.Units.isMaxRank_fundSystem, Eq.rec, NumberField.Units.regulator_eq_regOfFamily_fundSystem, Eq.symm, NumberField.Units.regOfFamily_pos
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
⊢ regulator K ≠ 0

Tactic:
(regulator_pos K).ne'

Premises used: LT.lt.ne', NumberField.Units.regulator_pos
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
pos :
  ∀ (hu : IsMaxRank u),
    regOfFamily u / regOfFamily v =
      (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
neg :
  ∀ (hu : ¬IsMaxRank u),
    regOfFamily u / regOfFamily v =
      (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
⊢ regOfFamily u / regOfFamily v =
    (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)

Tactic:
by_cases hu : IsMaxRank u

Premises used: NumberField.Units.IsMaxRank
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
rw :
  LE.le (α := AddSubgroup (logSpace K))
    (AddSubgroup.map (logEmbedding K)
      ((Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ))
        (Subgroup.closure (Set.range u) ⊔ torsion K)))
    (AddSubgroup.map (logEmbedding K)
      ((Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ))
        (Subgroup.closure (Set.range v) ⊔ torsion K)))
⊢ LE.le (α := Submodule ℤ (logSpace K))
    (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
    (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hv) : (a : Fin (rank K)) → logSpace K)))

Tactic:
rw [← toAddSubgroup_le, span_basisOfIsMaxRank hu, span_basisOfIsMaxRank hv,
        ← map_logEmbedding_sup_torsion (Subgroup.closure (Set.range u)).toAddSubgroup,
        ← map_logEmbedding_sup_torsion (Subgroup.closure (Set.range v)).toAddSubgroup,
        ← SupHomClass.map_sup, ← SupHomClass.map_sup]

Premises used: Subgroup.closure, Subgroup.toAddSubgroup, NumberField.Units.span_basisOfIsMaxRank, NumberField.Units.dirichletUnitTheorem.map_logEmbedding_sup_torsion, SupHomClass.map_sup, Set.range, DFunLike.coe, Submodule.toAddSubgroup_le
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
⊢ LE.le (α := AddSubgroup (logSpace K))
    (AddSubgroup.map (logEmbedding K)
      ((Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ))
        (Subgroup.closure (Set.range u) ⊔ torsion K)))
    (AddSubgroup.map (logEmbedding K)
      ((Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ))
        (Subgroup.closure (Set.range v) ⊔ torsion K)))

Tactic:
AddSubgroup.map_mono <| (OrderIso.le_iff_le Subgroup.toAddSubgroup).mpr h

Premises used: Iff.mpr, Subgroup.toAddSubgroup, Set.Mem, OrderIso.le_iff_le, AddSubgroup.map_mono
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
⊢ LE.le (α := AddSubgroup (logSpace K))
    (AddSubgroup.map (logEmbedding K)
      ((Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ))
        (Subgroup.closure (Set.range u) ⊔ torsion K)))
    (AddSubgroup.map (logEmbedding K)
      ((Subgroup.toAddSubgroup : (a : Subgroup (𝓞 K)ˣ) → AddSubgroup (Additive (𝓞 K)ˣ))
        (Subgroup.closure (Set.range v) ⊔ torsion K)))

Tactic:
exact AddSubgroup.map_mono <| (OrderIso.le_iff_le Subgroup.toAddSubgroup).mpr h

Premises used: Iff.mpr, Subgroup.toAddSubgroup, OrderIso.le_iff_le, AddSubgroup.map_mono
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
⊢ LE.le (α := Submodule ℤ (logSpace K))
    (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hu) : (a : Fin (rank K)) → logSpace K)))
    (span ℤ (Set.range (ι := Fin (rank K)) (⇑(basisOfIsMaxRank hv) : (a : Fin (rank K)) → logSpace K)))

Tactic:
have : span ℤ (Set.range (basisOfIsMaxRank hu)) ≤ span ℤ (Set.range (basisOfIsMaxRank hv)) := by
      rw [← toAddSubgroup_le, span_basisOfIsMaxRank hu, span_basisOfIsMaxRank hv,
        ← map_logEmbedding_sup_torsion (Subgroup.closure (Set.range u)).toAddSubgroup,
        ← map_logEmbedding_sup_torsion (Subgroup.closure (Set.range v)).toAddSubgroup,
        ← SupHomClass.map_sup, ← SupHomClass.map_sup]
      exact AddSubgroup.map_mono <| (OrderIso.le_iff_le Subgroup.toAddSubgroup).mpr h
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : ¬IsMaxRank u
neg : (Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K) = 0
⊢ regOfFamily u / regOfFamily v =
    (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)

Tactic:
rw [regOfFamily_eq_zero hu, zero_div, eq_comm, Nat.cast_eq_zero]

Premises used: zero_div, eq_comm, Nat.cast_eq_zero, NumberField.Units.regOfFamily_eq_zero
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : ¬IsMaxRank u
rw : Subgroup.FiniteIndex (Subgroup.closure (Set.range v))
⊢ (Subgroup.closure (Set.range v) ⊔ torsion K).index ≠ 0

Tactic:
rw [← Subgroup.finiteIndex_iff, ← finiteIndex_iff_sup_torsion_finiteIndex]

Premises used: NumberField.Units.finiteIndex_iff_sup_torsion_finiteIndex, Subgroup.finiteIndex_iff
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : ¬IsMaxRank u
⊢ Subgroup.FiniteIndex (Subgroup.closure (Set.range v))

Tactic:
isMaxRank_iff_closure_finiteIndex.mp hv

Premises used: Iff.mp, NumberField.Units.isMaxRank_iff_closure_finiteIndex
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : ¬IsMaxRank u
⊢ Subgroup.FiniteIndex (Subgroup.closure (Set.range v))

Tactic:
exact isMaxRank_iff_closure_finiteIndex.mp hv

Premises used: Iff.mp, NumberField.Units.isMaxRank_iff_closure_finiteIndex
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : ¬IsMaxRank u
⊢ (Subgroup.closure (Set.range v) ⊔ torsion K).index ≠ 0

Tactic:
have : (Subgroup.closure (Set.range v) ⊔ torsion K).index ≠ 0 := by
      rw [← Subgroup.finiteIndex_iff, ← finiteIndex_iff_sup_torsion_finiteIndex]
      exact isMaxRank_iff_closure_finiteIndex.mp hv
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : ¬IsMaxRank u
this : (Subgroup.closure (Set.range v) ⊔ torsion K).index ≠ 0
neg :
  (Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K) *
      (Subgroup.closure (Set.range v) ⊔ torsion K).index =
    0
neg₁ : (Subgroup.closure (Set.range u) ⊔ torsion K).index = 0
neg₂ : ¬(Subgroup.closure (Set.range u) ⊔ torsion K).FiniteIndex
neg₃ : ¬Subgroup.FiniteIndex (Subgroup.closure (Set.range u))
neg₄ neg₅ neg₆ neg₇ : ¬IsMaxRank u
⊢ (Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K) = 0

Tactic:
rwa [← mul_eq_zero_iff_right this, Subgroup.relIndex_mul_index h,
      ← Subgroup.not_finiteIndex_iff, ← finiteIndex_iff_sup_torsion_finiteIndex,
      ← isMaxRank_iff_closure_finiteIndex.not]

Premises used: Subgroup.not_finiteIndex_iff, Subgroup.relIndex_mul_index, Iff.not, mul_eq_zero_iff_right, NumberField.Units.isMaxRank_iff_closure_finiteIndex, NumberField.Units.finiteIndex_iff_sup_torsion_finiteIndex
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
pos :
  ∀ (hu : IsMaxRank u),
    regOfFamily u / regOfFamily v =
      (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
neg neg₁ :
  ∀ (hu : ¬IsMaxRank u),
    regOfFamily u / regOfFamily v =
      (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)
⊢ regOfFamily u / regOfFamily v =
    (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K)) : ℝ)

Tactic:
classical
  by_cases hu : IsMaxRank u
  · have : span ℤ (Set.range (basisOfIsMaxRank hu)) ≤ span ℤ (Set.range (basisOfIsMaxRank hv)) := by
      rw [← toAddSubgroup_le, span_basisOfIsMaxRank hu, span_basisOfIsMaxRank hv,
        ← map_logEmbedding_sup_torsion (Subgroup.closure (Set.range u)).toAddSubgroup,
        ← map_logEmbedding_sup_torsion (Subgroup.closure (Set.range v)).toAddSubgroup,
        ← SupHomClass.map_sup, ← SupHomClass.map_sup]
      exact AddSubgroup.map_mono <| (OrderIso.le_iff_le Subgroup.toAddSubgroup).mpr h
    rw [regOfFamily_of_isMaxRank hu, regOfFamily_of_isMaxRank hv,
      covolume_div_covolume_eq_relIndex _ _ this, span_basisOfIsMaxRank hu,
      span_basisOfIsMaxRank hv, AddSubgroup.relIndex_map_map, logEmbedding_ker,
      ← OrderIso.map_sup, ← OrderIso.map_sup, ← Subgroup.relIndex_toAddSubgroup]
  · rw [regOfFamily_eq_zero hu, zero_div, eq_comm, Nat.cast_eq_zero]
    have : (Subgroup.closure (Set.range v) ⊔ torsion K).index ≠ 0 := by
      rw [← Subgroup.finiteIndex_iff, ← finiteIndex_iff_sup_torsion_finiteIndex]
      exact isMaxRank_iff_closure_finiteIndex.mp hv
    rwa [← mul_eq_zero_iff_right this, Subgroup.relIndex_mul_index h,
      ← Subgroup.not_finiteIndex_iff, ← finiteIndex_iff_sup_torsion_finiteIndex,
      ← isMaxRank_iff_closure_finiteIndex.not]

Premises used: Subgroup.not_finiteIndex_iff, Subgroup.relIndex_mul_index, AddSubgroup.relIndex_map_map, NumberField.Units.span_basisOfIsMaxRank, zero_div, Iff.not, NumberField.Units.regOfFamily_of_isMaxRank, eq_comm, Nat.cast_eq_zero, OrderIso.map_sup, NumberField.Units.isMaxRank_iff_closure_finiteIndex, NumberField.Units.IsMaxRank, NumberField.Units.finiteIndex_iff_sup_torsion_finiteIndex, NumberField.Units.dirichletUnitTheorem.logEmbedding_ker, Subgroup.relIndex_toAddSubgroup
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
⊢ Subgroup.closure (Set.range u) ⊔ torsion K ≤
    Subgroup.closure (Set.range (ι := Fin (rank K)) (fundSystem K)) ⊔ torsion K

Tactic:
simp only [closure_fundSystem_sup_torsion_eq_top, le_top]

Premises used: NumberField.Units.closure_fundSystem_sup_torsion_eq_top, le_top
-- Module: Mathlib.NumberTheory.NumberField.Units.Regulator
Goal:
K : Type u_1
inst : Field K
inst_1 : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
rw : regOfFamily u / regOfFamily (fundSystem K) = (↑(Subgroup.closure (Set.range u) ⊔ torsion K).index : ℝ)
rw₁ :
  Eq (α := ℝ)
    (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex
          (Subgroup.closure (Set.range (ι := Fin (rank K)) (fundSystem K)) ⊔ torsion K)) :
      ℝ)
    (↑(Subgroup.closure (Set.range u) ⊔ torsion K).index : ℝ)
rw₂ :
  Eq (α := ℝ) (↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex ⊤) : ℝ)
    (↑(Subgroup.closure (Set.range u) ⊔ torsion K).index : ℝ)
rw₃ rw₄ :
  Eq (α := ℝ) (↑(Subgroup.closure (Set.range u) ⊔ torsion K).index : ℝ)
    (↑(Subgroup.closure (Set.range u) ⊔ torsion K).index : ℝ)
⊢ regOfFamily u / regulator K = (↑(Subgroup.closure (Set.range u) ⊔ torsion K).index : ℝ)

Tactic:
rw [regulator_eq_regOfFamily_fundSystem, regOfFamily_div_regOfFamily (isMaxRank_fundSystem K)
    (by simp only [closure_fundSystem_sup_torsion_eq_top, le_top]),
    closure_fundSystem_sup_torsion_eq_top, Subgroup.relIndex_top_right]

Premises used: NumberField.Units.isMaxRank_fundSystem, NumberField.Units.closure_fundSystem_sup_torsion_eq_top, NumberField.Units.regOfFamily_div_regOfFamily, NumberField.Units.regulator_eq_regOfFamily_fundSystem, Subgroup.relIndex_top_right
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
κ : AddChar ℤ_[p] R
hκ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R)
⊢ Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ HSub.hSub (α := R) (β := R) ((κ : (a : ℤ_[p]) → R) 1 : R) (1 : R) ^ n) atTop
    (𝓝 0)

Tactic:
(PadicInt.fwdDiff_tendsto_zero ⟨κ, hκ⟩).congr fun n ↦ ?_

Premises used: ContinuousMap.mk, PadicInt.fwdDiff_tendsto_zero, Filter.Tendsto.congr, DFunLike.coe
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
κ : AddChar ℤ_[p] R
hκ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R)
refine :
  ∀ (n : ℕ),
    Δ_[1]^[n] (⇑{ toFun := (⇑κ : (a : ℤ_[p]) → R), continuous_toFun := hκ : C(ℤ_[p], R) } : (a : ℤ_[p]) → R) 0 =
      HSub.hSub (α := R) (β := R) ((κ : (a : ℤ_[p]) → R) 1 : R) (1 : R) ^ n
⊢ Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ HSub.hSub (α := R) (β := R) ((κ : (a : ℤ_[p]) → R) 1 : R) (1 : R) ^ n) atTop
    (𝓝 0)

Tactic:
refine (PadicInt.fwdDiff_tendsto_zero ⟨κ, hκ⟩).congr fun n ↦ ?_

Premises used: ContinuousMap.mk, PadicInt.fwdDiff_tendsto_zero, Filter.Tendsto.congr, DFunLike.coe
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
κ : AddChar ℤ_[p] R
hκ : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (⇑κ : (a : ℤ_[p]) → R)
n : ℕ
⊢ Δ_[1]^[n] (⇑{ toFun := (⇑κ : (a : ℤ_[p]) → R), continuous_toFun := hκ : C(ℤ_[p], R) } : (a : ℤ_[p]) → R) 0 =
    HSub.hSub (α := R) (β := R) ((κ : (a : ℤ_[p]) → R) 1 : R) (1 : R) ^ n

Tactic:
simpa only [AddChar.map_zero_eq_one, mul_one] using fwdDiff_addChar_eq κ 0 1 n

Premises used: AddChar.map_zero_eq_one, fwdDiff_addChar_eq, mul_one, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
r : R
hr : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)
rw : Eq.{u_1 + 1} (α := R) ((mahlerSeries fun (x : ℕ) ↦ r ^ x : (a : ℤ_[p]) → R) (↑0 : ℤ_[p]) : R) (1 : R)
rw₁ : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range (HAdd.hAdd (α := ℕ) 0 1), Nat.choose 0 i • r ^ i) 1
rw₂ : Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range 1, Nat.choose 0 i • r ^ i) 1
rw₃ : Nat.choose 0 0 • HPow.hPow (β := ℕ) r 0 = 1
rw₄ : HSMul.hSMul (α := ℕ) 1 (HPow.hPow (β := ℕ) r 0) = 1
rw₅ : HSMul.hSMul (α := ℕ) (β := R) 1 1 = 1
rw₆ rw₇ : Eq.{u_1 + 1} (α := R) 1 1
⊢ Eq.{u_1 + 1} (α := R) ((mahlerSeries fun (x : ℕ) ↦ r ^ x : (a : ℤ_[p]) → R) 0 : R) (1 : R)

Tactic:
rw [← Nat.cast_zero, mahlerSeries_apply_nat hr le_rfl, zero_add, Finset.sum_range_one,
      Nat.choose_self, pow_zero, one_smul]

Premises used: le_rfl, PadicInt.mahlerSeries_apply_nat, Finset.sum_range_one, zero_add, pow_zero, one_smul, Nat.cast_zero, Nat.choose_self
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
r : R
hr : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)
a b : ℤ_[p]
F : C(ℤ_[p], R) := mahlerSeries fun (x : ℕ) ↦ r ^ x
change :
  (F : (a : ℤ_[p]) → R) (a + b) =
    HMul.hMul (α := R) (β := R) ((F : (a : ℤ_[p]) → R) a : R) ((F : (a : ℤ_[p]) → R) b : R)
⊢ (mahlerSeries fun (x : ℕ) ↦ r ^ x : (a : ℤ_[p]) → R) (a + b) =
    HMul.hMul (α := R) (β := R) ((mahlerSeries fun (x : ℕ) ↦ r ^ x : (a : ℤ_[p]) → R) a : R)
      ((mahlerSeries fun (x : ℕ) ↦ r ^ x : (a : ℤ_[p]) → R) b : R)

Tactic:
change F (a + b) = F a * F b

Premises used: HAdd.hAdd, DFunLike.coe
-- Module: Mathlib.NumberTheory.Padics.AddChar
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : NormedRing R
inst_2 : Algebra ℤ_[p] R
inst_3 : IsBoundedSMul ℤ_[p] R
inst_4 : IsUltrametricDist R
inst_5 : CompleteSpace R
r : R
hr : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ r ^ x) atTop (𝓝 0)
a b : ℤ_[p]
F : C(ℤ_[p], R) := mahlerSeries fun (x : ℕ) ↦ r ^ x
n : ℕ
rw :
  Eq.{u_1 + 1} (α := R) (∑ i ∈ Finset.range (n + 1), n.choose i • r ^ i)
    (∑ m ∈ Finset.range (n + 1), r ^ m * HPow.hPow (α := R) 1 (n - m) * (↑(n.choose m) : R))
⊢ (F : (a : ℤ_[p]) → R) (↑n : ℤ_[p]) = (r + 1) ^ n

Tactic:
rw [mahlerSeries_apply_nat hr le_rfl, (Commute.one_right _).add_pow]

Premises used: le_rfl, PadicInt.mahlerSeries_apply_nat, Commute.add_pow