internlm/Lean-Github huggingface dataset:
Theorem: lh_pow_free'
Proof state before:
case pos.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 : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
b : ℤ
hb : a₁ = ↑↑p * b
⊢ ∑ i : Fin (r + 1), Function.extend Fin.castSucc ι₁ 0 i • η i = (b * ↑↑p) • Additive.ofMul ζ
Tactic:
rw [← hb.trans (mul_comm _ _), ← e₁]
Proof state after:
case pos.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 : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
b : ℤ
hb : a₁ = ↑↑p * b
⊢ ∑ i : Fin (r + 1), Function.extend Fin.castSucc ι₁ 0 i • η i = ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i
Theorem: lh_pow_free'
Proof state before:
case pos.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 : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
b : ℤ
hb : a₁ = ↑↑p * b
⊢ ∑ i : Fin (r + 1), Function.extend Fin.castSucc ι₁ 0 i • η i = ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i
Tactic:
simp [Fin.sum_univ_castSucc, (Fin.castSucc_injective r).extend_apply,
  (Fin.castSucc_lt_last _).ne]
Proof state after:
no goals
Theorem: lh_pow_free'
Proof 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 : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
b : ℤ
hb : a₁ = ↑↑p * b
⊢ ¬↑↑p ∣ Function.extend Fin.castSucc ι₁ 0 i₁.castSucc
Tactic:
rwa [(Fin.castSucc_injective r).extend_apply]
Proof state after:
no goals
Theorem: lh_pow_free'
Proof state before:
case pos
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 : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
ha₂ : ↑↑p ∣ a₂
⊢ ∃ a ι i, ∑ i : Fin (r + 1), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i ∧ (ζ = 1 → ↑i ≠ r + 1 - 1)
Tactic:
obtain ⟨b, hb⟩ := ha₂
Proof state after:
case pos.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 : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
b : ℤ
hb : a₂ = ↑↑p * b
⊢ ∃ a ι i, ∑ i : Fin (r + 1), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i ∧ (ζ = 1 → ↑i ≠ r + 1 - 1)
Theorem: lh_pow_free'
Proof state before:
case pos.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 : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
b : ℤ
hb : a₂ = ↑↑p * b
⊢ ∃ a ι i, ∑ i : Fin (r + 1), ι i • η i = (a * ↑↑p) • Additive.ofMul ζ ∧ ¬↑↑p ∣ ι i ∧ (ζ = 1 → ↑i ≠ r + 1 - 1)
Tactic:
refine ⟨b, Function.extend (Fin.succAbove i₁.castSucc) ι₂ 0, Fin.succAbove i₁.castSucc i₂, ?_,
  by rwa [Fin.succAbove_right_injective.extend_apply], fun H ↦ (hζ' H).elim⟩
Proof state after:
case pos.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 : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
b : ℤ
hb : a₂ = ↑↑p * b
⊢ ∑ i : Fin (r + 1), Function.extend i₁.castSucc.succAbove ι₂ 0 i • η i = (b * ↑↑p) • Additive.ofMul ζ
Theorem: lh_pow_free'
Proof state before:
case pos.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 : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
b : ℤ
hb : a₂ = ↑↑p * b
⊢ ∑ i : Fin (r + 1), Function.extend i₁.castSucc.succAbove ι₂ 0 i • η i = (b * ↑↑p) • Additive.ofMul ζ
Tactic:
rw [← hb.trans (mul_comm _ _), ← e₂]
Proof state after:
case pos.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 : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
b : ℤ
hb : a₂ = ↑↑p * b
⊢ ∑ i : Fin (r + 1), Function.extend i₁.castSucc.succAbove ι₂ 0 i • η i =
    ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i
Theorem: lh_pow_free'
Proof state before:
case pos.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 : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
b : ℤ
hb : a₂ = ↑↑p * b
⊢ ∑ i : Fin (r + 1), Function.extend i₁.castSucc.succAbove ι₂ 0 i • η i =
    ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i
Tactic:
simp [Fin.sum_univ_succAbove _ i₁.castSucc, Fin.succAbove_right_injective.extend_apply]
Proof state after:
no goals
Theorem: lh_pow_free'
Proof 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 : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
b : ℤ
hb : a₂ = ↑↑p * b
⊢ ¬↑↑p ∣ Function.extend i₁.castSucc.succAbove ι₂ 0 (i₁.castSucc.succAbove i₂)
Tactic:
rwa [Fin.succAbove_right_injective.extend_apply]
Proof state after:
no goals
Theorem: lh_pow_free'
Proof state before:
case neg.intro.intro.intro.intro.refine_1
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 : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
ha₂ : ¬↑↑p ∣ a₂
α₁ β₁ : ℤ
h₁ : α₁ * ↑↑p + β₁ * a₁ = 1
α₂ β₂ : ℤ
h₂ : α₂ * ↑↑p + β₂ * a₂ = 1
⊢ ∑ i : Fin (r + 1),
      (β₁ • Function.extend Fin.castSucc ι₁ 0 - β₂ • Function.extend i₁.castSucc.succAbove ι₂ 0) i • η i =
    ((α₂ - α₁) * ↑↑p) • Additive.ofMul ζ
Tactic:
rw [sub_mul, eq_sub_iff_add_eq.mpr h₁, eq_sub_iff_add_eq.mpr h₂]
Proof state after:
case neg.intro.intro.intro.intro.refine_1
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 : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
ha₂ : ¬↑↑p ∣ a₂
α₁ β₁ : ℤ
h₁ : α₁ * ↑↑p + β₁ * a₁ = 1
α₂ β₂ : ℤ
h₂ : α₂ * ↑↑p + β₂ * a₂ = 1
⊢ ∑ i : Fin (r + 1),
      (β₁ • Function.extend Fin.castSucc ι₁ 0 - β₂ • Function.extend i₁.castSucc.succAbove ι₂ 0) i • η i =
    (1 - β₂ * a₂ - (1 - β₁ * a₁)) • Additive.ofMul ζ
Theorem: lh_pow_free'
Proof state before:
case neg.intro.intro.intro.intro.refine_1
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 : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
ha₂ : ¬↑↑p ∣ a₂
α₁ β₁ : ℤ
h₁ : α₁ * ↑↑p + β₁ * a₁ = 1
α₂ β₂ : ℤ
h₂ : α₂ * ↑↑p + β₂ * a₂ = 1
⊢ ∑ i : Fin (r + 1),
      (β₁ • Function.extend Fin.castSucc ι₁ 0 - β₂ • Function.extend i₁.castSucc.succAbove ι₂ 0) i • η i =
    (1 - β₂ * a₂ - (1 - β₁ * a₁)) • Additive.ofMul ζ
Tactic:
simp only [zsmul_eq_mul, Pi.intCast_def, Int.cast_id, Pi.sub_apply, Pi.mul_apply,
  Fin.succAbove_of_le_castSucc, ne_eq, not_not, not_exists, sub_sub_sub_cancel_left]
Proof state after:
case neg.intro.intro.intro.intro.refine_1
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 : ℕ
η : Fin (r + 1) → Additive M
hr : finrank ℤ (Additive M) < r
a₁ : ℤ
ι₁ : Fin r → ℤ
i₁ : Fin r
e₁ : ∑ i : Fin r, ι₁ i • (η ∘ Fin.castSucc) i = a₁ • Additive.ofMul ζ
hi₁ : ¬↑↑p ∣ ι₁ i₁
a₂ : ℤ
ι₂ : Fin r → ℤ
i₂ : Fin r
e₂ : ∑ i : Fin r, ι₂ i • (η ∘ i₁.castSucc.succAbove) i = a₂ • Additive.ofMul ζ
hi₂ : ¬↑↑p ∣ ι₂ i₂
hζ' : ¬ζ = 1
ha₁ : ¬↑↑p ∣ a₁
ha₂ : ¬↑↑p ∣ a₂
α₁ β₁ : ℤ
h₁ : α₁ * ↑↑p + β₁ * a₁ = 1
α₂ β₂ : ℤ
h₂ : α₂ * ↑↑p + β₂ * a₂ = 1
⊢ ∑ x : Fin (r + 1),
      (β₁ * Function.extend Fin.castSucc ι₁ 0 x - β₂ * Function.extend i₁.castSucc.succAbove ι₂ 0 x) • η x =
    (β₁ * a₁ - β₂ * a₂) • Additive.ofMul ζ