-- Mathlib/Algebra/Module/ZLattice/Basic.lean
theorem floor_eq_self_of_mem (m : E) (h : m ∈ span ℤ (Set.range b)) : (floor b m : E) = m

Proof state:
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)
⊢ ↑(floor b m) = m

Tactic:
apply b.ext_elem

Result:
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 ↑(floor b m)) i = (b.repr m) i

Proof state:
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

Tactic:
obtain ⟨z, hz⟩ := (b.mem_span_iff_repr_mem ℤ _).mp h i

Result:
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

Proof state:
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

Tactic:
intro i

Result:
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

Proof state:
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

Tactic:
rw [← hz]

Result:
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

Proof state:
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

Tactic:
exact congr_arg (Int.cast : ℤ → K) (Int.floor_intCast z)

Result:
no goals

Proof state:
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 ↑(floor b m)) i = (b.repr m) i

Tactic:
simp_rw [repr_floor_apply b]

Result:
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