Theorem: lh_pow_free_aux (FltRegular/NumberTheory/Hilbert92.lean)

State before:
p : ℕ+
K : Type u_1
inst✝¹⁵ : Field K
inst✝¹⁴ : NumberField K
k : Type u_2
inst✝¹³ : Field k
inst✝¹² : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : CommGroup H
inst✝⁹ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r✝ : ℕ
inst✝⁸ : DistribMulAction H G
inst✝⁷ : Module.Free ℤ G
inst✝⁶ : Module.Finite ℤ G
hf : finrank ℤ G = r✝ * (↑p - 1)
inst✝⁵ : Algebra k K
inst✝⁴ : IsGalois k K
inst✝³ : FiniteDimensional k K
inst✝² : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
hr : finrank ℤ (Additive M) < r
η : Fin r → Additive M
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i
Tactic:
obtain ⟨f, hf, hf'⟩ := Fintype.not_linearIndependent_iff.mp
  (mt (LinearIndependent.fintype_card_le_finrank (R := ℤ) (b := η))
    ((hr.trans_eq (Fintype.card_fin r).symm).not_le))
State after:
case intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁵ : Field K
inst✝¹⁴ : NumberField K
k : Type u_2
inst✝¹³ : Field k
inst✝¹² : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : CommGroup H
inst✝⁹ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r✝ : ℕ
inst✝⁸ : DistribMulAction H G
inst✝⁷ : Module.Free ℤ G
inst✝⁶ : Module.Finite ℤ G
hf✝ : finrank ℤ G = r✝ * (↑p - 1)
inst✝⁵ : Algebra k K
inst✝⁴ : IsGalois k K
inst✝³ : FiniteDimensional k K
inst✝² : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
hr : finrank ℤ (Additive M) < r
η : Fin r → Additive M
f : Fin r → ℤ
hf : ∑ i : Fin r, f i • η i = 0
hf' : ∃ i, f i ≠ 0
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i

State before:
case intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁵ : Field K
inst✝¹⁴ : NumberField K
k : Type u_2
inst✝¹³ : Field k
inst✝¹² : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : CommGroup H
inst✝⁹ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r✝ : ℕ
inst✝⁸ : DistribMulAction H G
inst✝⁷ : Module.Free ℤ G
inst✝⁶ : Module.Finite ℤ G
hf✝ : finrank ℤ G = r✝ * (↑p - 1)
inst✝⁵ : Algebra k K
inst✝⁴ : IsGalois k K
inst✝³ : FiniteDimensional k K
inst✝² : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
hr : finrank ℤ (Additive M) < r
η : Fin r → Additive M
f : Fin r → ℤ
hf : ∑ i : Fin r, f i • η i = 0
hf' : ∃ i, f i ≠ 0
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i
Tactic:
obtain ⟨n, f', hf', i, hi⟩ := exists_pow_smul_eq_and_not_dvd f
  (Function.ne_iff.mpr hf') p hp.ne_one
State after:
case intro.intro.intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁵ : Field K
inst✝¹⁴ : NumberField K
k : Type u_2
inst✝¹³ : Field k
inst✝¹² : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : CommGroup H
inst✝⁹ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r✝ : ℕ
inst✝⁸ : DistribMulAction H G
inst✝⁷ : Module.Free ℤ G
inst✝⁶ : Module.Finite ℤ G
hf✝ : finrank ℤ G = r✝ * (↑p - 1)
inst✝⁵ : Algebra k K
inst✝⁴ : IsGalois k K
inst✝³ : FiniteDimensional k K
inst✝² : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
hr : finrank ℤ (Additive M) < r
η : Fin r → Additive M
f : Fin r → ℤ
hf : ∑ i : Fin r, f i • η i = 0
hf'✝ : ∃ i, f i ≠ 0
n : ℕ
f' : Fin r → ℤ
hf' : f = ↑p ^ n • f'
i : Fin r
hi : ¬↑↑p ∣ f' i
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i

State before:
case intro.intro.intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁵ : Field K
inst✝¹⁴ : NumberField K
k : Type u_2
inst✝¹³ : Field k
inst✝¹² : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : CommGroup H
inst✝⁹ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r✝ : ℕ
inst✝⁸ : DistribMulAction H G
inst✝⁷ : Module.Free ℤ G
inst✝⁶ : Module.Finite ℤ G
hf✝ : finrank ℤ G = r✝ * (↑p - 1)
inst✝⁵ : Algebra k K
inst✝⁴ : IsGalois k K
inst✝³ : FiniteDimensional k K
inst✝² : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
hr : finrank ℤ (Additive M) < r
η : Fin r → Additive M
f : Fin r → ℤ
hf : ∑ i : Fin r, f i • η i = 0
hf'✝ : ∃ i, f i ≠ 0
n : ℕ
f' : Fin r → ℤ
hf' : f = ↑p ^ n • f'
i : Fin r
hi : ¬↑↑p ∣ f' i
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i
Tactic:
simp_rw [hf', Pi.smul_apply, smul_assoc, ← smul_sum] at hf
State after:
case intro.intro.intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁵ : Field K
inst✝¹⁴ : NumberField K
k : Type u_2
inst✝¹³ : Field k
inst✝¹² : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : CommGroup H
inst✝⁹ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r✝ : ℕ
inst✝⁸ : DistribMulAction H G
inst✝⁷ : Module.Free ℤ G
inst✝⁶ : Module.Finite ℤ G
hf✝ : finrank ℤ G = r✝ * (↑p - 1)
inst✝⁵ : Algebra k K
inst✝⁴ : IsGalois k K
inst✝³ : FiniteDimensional k K
inst✝² : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
hr : finrank ℤ (Additive M) < r
η : Fin r → Additive M
f : Fin r → ℤ
hf'✝ : ∃ i, f i ≠ 0
n : ℕ
f' : Fin r → ℤ
hf' : f = ↑p ^ n • f'
i : Fin r
hi : ¬↑↑p ∣ f' i
hf : ↑p ^ n • ∑ x : Fin r, f' x • η x = 0
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i

State before:
case intro.intro.intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁵ : Field K
inst✝¹⁴ : NumberField K
k : Type u_2
inst✝¹³ : Field k
inst✝¹² : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : CommGroup H
inst✝⁹ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r✝ : ℕ
inst✝⁸ : DistribMulAction H G
inst✝⁷ : Module.Free ℤ G
inst✝⁶ : Module.Finite ℤ G
hf✝ : finrank ℤ G = r✝ * (↑p - 1)
inst✝⁵ : Algebra k K
inst✝⁴ : IsGalois k K
inst✝³ : FiniteDimensional k K
inst✝² : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
hr : finrank ℤ (Additive M) < r
η : Fin r → Additive M
f : Fin r → ℤ
hf'✝ : ∃ i, f i ≠ 0
n : ℕ
f' : Fin r → ℤ
hf' : f = ↑p ^ n • f'
i : Fin r
hi : ¬↑↑p ∣ f' i
hf : ↑p ^ n • ∑ x : Fin r, f' x • η x = 0
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i
Tactic:
obtain ⟨a, ha⟩ := hk _ _ hf
State after:
case intro.intro.intro.intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁵ : Field K
inst✝¹⁴ : NumberField K
k : Type u_2
inst✝¹³ : Field k
inst✝¹² : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : CommGroup H
inst✝⁹ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r✝ : ℕ
inst✝⁸ : DistribMulAction H G
inst✝⁷ : Module.Free ℤ G
inst✝⁶ : Module.Finite ℤ G
hf✝ : finrank ℤ G = r✝ * (↑p - 1)
inst✝⁵ : Algebra k K
inst✝⁴ : IsGalois k K
inst✝³ : FiniteDimensional k K
inst✝² : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
hr : finrank ℤ (Additive M) < r
η : Fin r → Additive M
f : Fin r → ℤ
hf'✝ : ∃ i, f i ≠ 0
n : ℕ
f' : Fin r → ℤ
hf' : f = ↑p ^ n • f'
i : Fin r
hi : ¬↑↑p ∣ f' i
hf : ↑p ^ n • ∑ x : Fin r, f' x • η x = 0
a : ℕ
ha : ζ ^ a = ∑ x : Fin r, f' x • η x
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i

State before:
case intro.intro.intro.intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁵ : Field K
inst✝¹⁴ : NumberField K
k : Type u_2
inst✝¹³ : Field k
inst✝¹² : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : CommGroup H
inst✝⁹ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r✝ : ℕ
inst✝⁸ : DistribMulAction H G
inst✝⁷ : Module.Free ℤ G
inst✝⁶ : Module.Finite ℤ G
hf✝ : finrank ℤ G = r✝ * (↑p - 1)
inst✝⁵ : Algebra k K
inst✝⁴ : IsGalois k K
inst✝³ : FiniteDimensional k K
inst✝² : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
hr : finrank ℤ (Additive M) < r
η : Fin r → Additive M
f : Fin r → ℤ
hf'✝ : ∃ i, f i ≠ 0
n : ℕ
f' : Fin r → ℤ
hf' : f = ↑p ^ n • f'
i : Fin r
hi : ¬↑↑p ∣ f' i
hf : ↑p ^ n • ∑ x : Fin r, f' x • η x = 0
a : ℕ
ha : ζ ^ a = ∑ x : Fin r, f' x • η x
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i
Tactic:
rw [← zpow_natCast] at ha
State after:
case intro.intro.intro.intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁵ : Field K
inst✝¹⁴ : NumberField K
k : Type u_2
inst✝¹³ : Field k
inst✝¹² : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : CommGroup H
inst✝⁹ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r✝ : ℕ
inst✝⁸ : DistribMulAction H G
inst✝⁷ : Module.Free ℤ G
inst✝⁶ : Module.Finite ℤ G
hf✝ : finrank ℤ G = r✝ * (↑p - 1)
inst✝⁵ : Algebra k K
inst✝⁴ : IsGalois k K
inst✝³ : FiniteDimensional k K
inst✝² : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
hr : finrank ℤ (Additive M) < r
η : Fin r → Additive M
f : Fin r → ℤ
hf'✝ : ∃ i, f i ≠ 0
n : ℕ
f' : Fin r → ℤ
hf' : f = ↑p ^ n • f'
i : Fin r
hi : ¬↑↑p ∣ f' i
hf : ↑p ^ n • ∑ x : Fin r, f' x • η x = 0
a : ℕ
ha : ζ ^ ↑a = ∑ x : Fin r, f' x • η x
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i

State before:
case intro.intro.intro.intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁵ : Field K
inst✝¹⁴ : NumberField K
k : Type u_2
inst✝¹³ : Field k
inst✝¹² : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝¹¹ : AddCommGroup G
inst✝¹⁰ : CommGroup H
inst✝⁹ : Fintype H
hCard : Fintype.card H = ↑p
σ✝ : H
hσ✝ : Subgroup.zpowers σ✝ = ⊤
r✝ : ℕ
inst✝⁸ : DistribMulAction H G
inst✝⁷ : Module.Free ℤ G
inst✝⁶ : Module.Finite ℤ G
hf✝ : finrank ℤ G = r✝ * (↑p - 1)
inst✝⁵ : Algebra k K
inst✝⁴ : IsGalois k K
inst✝³ : FiniteDimensional k K
inst✝² : IsUnramifiedAtInfinitePlaces k K
hKL : finrank k K = ↑p
σ : K ≃ₐ[k] K
hσ : ∀ (x : K ≃ₐ[k] K), x ∈ Subgroup.zpowers σ
M : Type u_5
inst✝¹ : CommGroup M
inst✝ : Module.Finite ℤ (Additive M)
ζ : M
hk : ∀ (ε : M) (n : ℕ), ε ^ ↑p ^ n = 1 → ∃ i, ζ ^ i = ε
r : ℕ
hr : finrank ℤ (Additive M) < r
η : Fin r → Additive M
f : Fin r → ℤ
hf'✝ : ∃ i, f i ≠ 0
n : ℕ
f' : Fin r → ℤ
hf' : f = ↑p ^ n • f'
i : Fin r
hi : ¬↑↑p ∣ f' i
hf : ↑p ^ n • ∑ x : Fin r, f' x • η x = 0
a : ℕ
ha : ζ ^ ↑a = ∑ x : Fin r, f' x • η x
⊢ ∃ a ι i, ∑ i : Fin r, ι i • η i = a • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i
Tactic:
exact ⟨a, f', i, ha.symm, hi⟩
State after:
no goals