Theorem: exists_int_sModEq (FltRegular/ReadyForMathlib/PowerBasis.lean)

State before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
⊢ ∃ n, x ≡ ↑n [SMOD span {pb.gen}]
Tactic:
refine' ⟨(pb.basis.repr x) ⟨0, pb.dim_pos⟩, _⟩
State after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]

State before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Tactic:
have H := Basis.sum_repr pb.basis x
State after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H : ∑ i : Fin pb.dim, (pb.basis.repr x) i • pb.basis i = x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]

State before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H : ∑ i : Fin pb.dim, (pb.basis.repr x) i • pb.basis i = x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Tactic:
rw [PowerBasis.coe_basis, ← insert_erase (mem_univ (⟨0, pb.dim_pos⟩ : Fin pb.dim)), sum_insert] at H
State after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]

K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H : ∑ i ∈ insert ⟨0, ⋯⟩ (univ.erase ⟨0, ⋯⟩), (pb.basis.repr x) i • (fun i => pb.gen ^ ↑i) i = x
⊢ ⟨0, ⋯⟩ ∉ univ.erase ⟨0, ⋯⟩

State before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Tactic:
have :
  ∀ i : (univ : Finset (Fin pb.dim)).erase ⟨0, pb.dim_pos⟩,
    ↑((pb.basis.repr x) i) * pb.gen ^ ((i : Fin pb.dim) : ℕ) =
      ↑((pb.basis.repr x) i) * pb.gen ^ (i : ℕ).pred.succ := by
  rintro ⟨i, hi⟩
  congr 1
  rw [succ_pred_eq_of_pos]
  rw [Subtype.coe_mk]
  refine' Nat.pos_of_ne_zero fun h => _
  cases' i with i₁ hi₁
  simp only [Subtype.coe_mk] at h
  simp only [mem_univ, not_true, mem_erase, ne_eq, Fin.mk.injEq, and_true] at hi
  exact hi h
State after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]

State before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Tactic:
simp only [Fin.val_mk, _root_.pow_zero, zsmul_eq_mul] at H
State after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H : ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 + ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, ↑((pb.basis.repr x) x_1) * pb.gen ^ ↑x_1 = x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]

State before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H : ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 + ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, ↑((pb.basis.repr x) x_1) * pb.gen ^ ↑x_1 = x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Tactic:
rw [← Finset.sum_finset_coe] at H
State after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H : ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 + ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]

State before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H : ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 + ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Tactic:
conv_lhs at H =>
  congr
  rfl
  congr
  rfl
  ext i
  rw [this i, _root_.pow_succ, ← mul_assoc, mul_comm _ pb.gen]
State after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H :
  ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), pb.gen * (↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred) =
    x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]

State before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H :
  ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), pb.gen * (↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred) =
    x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Tactic:
rw [← mul_sum] at H
State after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H :
  ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      pb.gen * ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred =
    x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]

State before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H :
  ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      pb.gen * ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred =
    x
⊢ x ≡ ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Tactic:
nth_rw 1 [← H]
State after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H :
  ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      pb.gen * ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred =
    x
⊢ ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      pb.gen * ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred ≡
    ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]

State before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H :
  ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      pb.gen * ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred =
    x
⊢ ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      pb.gen * ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred ≡
    ↑((pb.basis.repr x) ⟨0, ⋯⟩) [SMOD span {pb.gen}]
Tactic:
rw [SModEq.sub_mem, mul_one, add_sub_cancel_left, mul_comm, mem_span_singleton']
State after:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H :
  ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      pb.gen * ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred =
    x
⊢ ∃ a, a * pb.gen = (∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred) * pb.gen

State before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
this :
  ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
H :
  ↑((pb.basis.repr x) ⟨0, ⋯⟩) * 1 +
      pb.gen * ∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred =
    x
⊢ ∃ a, a * pb.gen = (∑ i : ↑↑(univ.erase ⟨0, ⋯⟩), ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred) * pb.gen
Tactic:
exact ⟨_, rfl⟩
State after:
no goals

State before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
⊢ ∀ (i : { x // x ∈ univ.erase ⟨0, ⋯⟩ }),
    ↑((pb.basis.repr x) ↑i) * pb.gen ^ ↑↑i = ↑((pb.basis.repr x) ↑i) * pb.gen ^ (↑↑i).pred.succ
Tactic:
rintro ⟨i, hi⟩
State after:
case mk
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ ↑((pb.basis.repr x) ↑⟨i, hi⟩) * pb.gen ^ ↑↑⟨i, hi⟩ = ↑((pb.basis.repr x) ↑⟨i, hi⟩) * pb.gen ^ (↑↑⟨i, hi⟩).pred.succ

State before:
case mk
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ ↑((pb.basis.repr x) ↑⟨i, hi⟩) * pb.gen ^ ↑↑⟨i, hi⟩ = ↑((pb.basis.repr x) ↑⟨i, hi⟩) * pb.gen ^ (↑↑⟨i, hi⟩).pred.succ
Tactic:
congr 1
State after:
case mk.e_a
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ pb.gen ^ ↑↑⟨i, hi⟩ = pb.gen ^ (↑↑⟨i, hi⟩).pred.succ

State before:
case mk.e_a
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ pb.gen ^ ↑↑⟨i, hi⟩ = pb.gen ^ (↑↑⟨i, hi⟩).pred.succ
Tactic:
rw [succ_pred_eq_of_pos]
State after:
case mk.e_a
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ 0 < ↑↑⟨i, hi⟩

State before:
case mk.e_a
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ 0 < ↑↑⟨i, hi⟩
Tactic:
rw [Subtype.coe_mk]
State after:
case mk.e_a
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ 0 < ↑i

State before:
case mk.e_a
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
⊢ 0 < ↑i
Tactic:
refine' Nat.pos_of_ne_zero fun h => _
State after:
case mk.e_a
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
h : ↑i = 0
⊢ False

State before:
case mk.e_a
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i : Fin pb.dim
hi : i ∈ univ.erase ⟨0, ⋯⟩
h : ↑i = 0
⊢ False
Tactic:
cases' i with i₁ hi₁
State after:
case mk.e_a.mk
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i₁ : ℕ
hi₁ : i₁ < pb.dim
hi : ⟨i₁, hi₁⟩ ∈ univ.erase ⟨0, ⋯⟩
h : ↑⟨i₁, hi₁⟩ = 0
⊢ False

State before:
case mk.e_a.mk
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i₁ : ℕ
hi₁ : i₁ < pb.dim
hi : ⟨i₁, hi₁⟩ ∈ univ.erase ⟨0, ⋯⟩
h : ↑⟨i₁, hi₁⟩ = 0
⊢ False
Tactic:
simp only [Subtype.coe_mk] at h
State after:
case mk.e_a.mk
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i₁ : ℕ
hi₁ : i₁ < pb.dim
hi : ⟨i₁, hi₁⟩ ∈ univ.erase ⟨0, ⋯⟩
h : i₁ = 0
⊢ False

State before:
case mk.e_a.mk
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i₁ : ℕ
hi₁ : i₁ < pb.dim
hi : ⟨i₁, hi₁⟩ ∈ univ.erase ⟨0, ⋯⟩
h : i₁ = 0
⊢ False
Tactic:
simp only [mem_univ, not_true, mem_erase, ne_eq, Fin.mk.injEq, and_true] at hi
State after:
case mk.e_a.mk
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i₁ : ℕ
hi₁ : i₁ < pb.dim
h : i₁ = 0
hi : ¬i₁ = 0
⊢ False

State before:
case mk.e_a.mk
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H :
  (pb.basis.repr x) ⟨0, ⋯⟩ • (fun i => pb.gen ^ ↑i) ⟨0, ⋯⟩ +
      ∑ x_1 ∈ univ.erase ⟨0, ⋯⟩, (pb.basis.repr x) x_1 • (fun i => pb.gen ^ ↑i) x_1 =
    x
i₁ : ℕ
hi₁ : i₁ < pb.dim
h : i₁ = 0
hi : ¬i₁ = 0
⊢ False
Tactic:
exact hi h
State after:
no goals

State before:
K : Type u_1
inst✝ : Field K
pb : PowerBasis ℤ (𝓞 K)
x : 𝓞 K
H : ∑ i ∈ insert ⟨0, ⋯⟩ (univ.erase ⟨0, ⋯⟩), (pb.basis.repr x) i • (fun i => pb.gen ^ ↑i) i = x
⊢ ⟨0, ⋯⟩ ∉ univ.erase ⟨0, ⋯⟩
Tactic:
exact not_mem_erase (⟨0, pb.dim_pos⟩ : Fin pb.dim) univ
State after:
no goals