E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
⊢ ∀ (i : ι), ↑(↑b.repr ↑(ceil b m)) i = ↑(↑b.repr m) i
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
⊢ ↑(ceil b m) = m
apply b.ext_elem
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
⊢ ∀ (i : ι), ↑⌈↑(↑b.repr m) i⌉ = ↑(↑b.repr m) i
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
⊢ ∀ (i : ι), ↑(↑b.repr ↑(ceil b m)) i = ↑(↑b.repr m) i
simp_rw [repr_ceil_apply b]
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
i : ι
⊢ ↑⌈↑(↑b.repr m) i⌉ = ↑(↑b.repr m) i
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
⊢ ∀ (i : ι), ↑⌈↑(↑b.repr m) i⌉ = ↑(↑b.repr m) i
intro i
case intro
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
i : ι
z : ℤ
hz : ↑(algebraMap ℤ K) z = ↑(↑b.repr m) i
⊢ ↑⌈↑(↑b.repr m) i⌉ = ↑(↑b.repr m) i
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
i : ι
⊢ ↑⌈↑(↑b.repr m) i⌉ = ↑(↑b.repr m) i
obtain ⟨z, hz⟩ := (b.mem_span_iff_repr_mem ℤ _).mp h i
case intro
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
i : ι
z : ℤ
hz : ↑(algebraMap ℤ K) z = ↑(↑b.repr m) i
⊢ ↑⌈↑(algebraMap ℤ K) z⌉ = ↑(algebraMap ℤ K) z
case intro
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
i : ι
z : ℤ
hz : ↑(algebraMap ℤ K) z = ↑(↑b.repr m) i
⊢ ↑⌈↑(↑b.repr m) i⌉ = ↑(↑b.repr m) i
rw [← hz]
no goals
case intro
E : Type u_1
ι : Type u_2
K : Type u_3
inst✝⁴ : NormedLinearOrderedField K
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace K E
b : Basis ι K E
inst✝¹ : FloorRing K
inst✝ : Fintype ι
m : E
h : m ∈ span ℤ (Set.range ↑b)
i : ι
z : ℤ
hz : ↑(algebraMap ℤ K) z = ↑(↑b.repr m) i
⊢ ↑⌈↑(algebraMap ℤ K) z⌉ = ↑(algebraMap ℤ K) z
exact congr_arg (Int.cast : ℤ → K) (Int.ceil_intCast z)